An efficiently checkable subset of TCTL for formal verification of transition systems with delays

Deka, J. K. ; Dasgupta, P. ; Chakrabarti, P. P. (1999) An efficiently checkable subset of TCTL for formal verification of transition systems with delays In: Twelfth International Conference on VLSI Design 1999, 7-10 January 1999.

Full text not available from this repository.

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

Related URL: http://dx.doi.org/10.1109/ICVD.1999.745163

Abstract

Model checking transition systems with delays using timed logics such as TCTL is an attractive technique for proper verification of hardware descriptions. TCTL model checking requires the construction of time regions which depends not only on the timed graph, but also the TCTL formula. This limits the efficiency of a pure top-down approach for model checking. We propose a restricted version of TCTL, namely DCTL, which can be checked in a pure top-down manner without augmenting the region graph a priori.

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

Repository Staff Only: item control page