Open computation tree logic with fairness

Banerjee, A. ; Dasgupta, P. ; Chakrabarti, P. (2003) Open computation tree logic with fairness In: Proceedings of the 2003 International Symposium on Circuits and Systems, 2003. ISCAS '03, 25-28 May 2003, Bangkok, Thailand.

Full text not available from this repository.

Official URL:

Related URL:


One of the main concerns of the designer of a circuit module is to guarantee that the interface of the module conforms to specific protocols (such as PCI Bus, AMBA bus or Ethernet) by which it interacts with its environment. The computational complexity of verifying such open systems under all possible environments has been shown to be very hard (EXPTIME complete). On the other hand, designers are typically required to guarantee correct behavior only for specific valid behaviors of the environment (such as a valid PCI Bus environment). Open Computation Tree Logic (Open-CTL) provides the designer the ability to model the environment constraints and the correctness property in a unified way, and has been shown to be useful for checking protocol compliance of modules. In this paper, we introduce the notion of fairness constraints on the environment. We show that the use of fairness constraints allows us to model the designer's intent in a meaningful way that conforms with the protocol being checked. We present a symbolic model checking algorithm for verifying Open-CTL properties under given fairness constraints.

Item Type:Conference or Workshop Item (Paper)
Source:Copyright of this article belongs to Institute of Electrical and Electronics Engineers.
ID Code:101718
Deposited On:09 Mar 2018 10:15
Last Modified:09 Mar 2018 10:15

Repository Staff Only: item control page