The open family of temporal logics: annotating temporal operators with input constraints

Banerjee, Ansuman ; Dasgupta, Pallab (2005) The open family of temporal logics: annotating temporal operators with input constraints ACM Transactions on Design Automation of Electronic Systems, 10 (3). pp. 492-522. ISSN 1084-4309

Full text not available from this repository.

Official URL:

Related URL:


Assume-guarantee style verification of modules relies on the appropriate modeling of the interaction of the module with its environment. Popular temporal logics such as Computation Tree Logic (CTL) and Linear Temporal Logic (LTL) that were originally defined for closed systems (Kripke structures) do not make any syntactic discrimination between input and output variables. As a result, these logics and their recent derivatives (such as System Verilog, Sugar, Forspec, etc) permit the specification of properties that have some semantic problems when interpreted over open systems or modules. These semantic problems are quite common in practice, but are computationally hard to detect within a given specification. In this article, we propose a new style for writing temporal specifications of open systems that helps the designer to avoid most of these problems. In the proposed style, the basic temporal operators (such as next and until) are annotated with assume constraints over the input variables. We formalize this style through an extension of LTL, namely Open-LTL and an extension of CTL with fairness, called Open-CTL. We show that this simple syntactic separation between the assume and the guarantee achieves the desired results. We show that the proposed style can be integrated with traditional symbolic model-checking techniques and present a complete tool for the verification of Verilog RTL modules in isolation.

Item Type:Article
Source:Copyright of this article belongs to Association for Computing Machinery.
ID Code:101441
Deposited On:12 Dec 2016 11:32
Last Modified:12 Dec 2016 11:32

Repository Staff Only: item control page