Abstractions for model checking of event timings

Deka, J. K. ; Chaki, S. ; Dasgupta, P. ; Chakrabarti, P. P. (2001) Abstractions for model checking of event timings In: The 2001 IEEE International Symposium on Circuits and Systems, ISCAS 2001, 6-9 May 2001, Sydney, NSW, Australia.

Full text not available from this repository.

Official URL: http://ieeexplore.ieee.org/document/922001/

Related URL: http://dx.doi.org/10.1109/ISCAS.2001.922001


Verification of timed temporal properties of a circuit is a computationally complex problem both in terms of space and time. In this paper we study different abstractions of timed systems and the temporal logics which are preserved under these abstractions. In particular we show that while known timed logics such as RTCTL and TCTL are preserved by bisimulation equivalence, the timings of events (signal changes) are preserved in a more compact abstraction. Experimental results show that this abstraction requires significantly less space and is competitive in terms of time required for verification.

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

Repository Staff Only: item control page