Min-max event-triggered computation tree logic

Dasgupta, Pallab ; Chakrabarti, P. P. ; Deka, Jatindra Kumar (2002) Min-max event-triggered computation tree logic Sadhana, 27 (2). pp. 163-180. ISSN 0256-2499

[img] PDF - Other

Official URL: http://www.ias.ac.in/describe/article/sadh/027/02/...

Related URL: http://dx.doi.org/10.1007/BF02717182


Very often timing verification involves the analysis of the timings of discrete events such as signal changes, sending and receiving of signals, and sensitization of edge-triggered circuit components. The main bottleneck in verifying timing properties of timed finite state machines (FSM) has been the inherent complexity of verifying timed properties (PSPACE-complete for timed extensions of computational tree logic (CTL)). Often however, we are interested in the best case or worst case timings between events. In this paper we introduce a temporal query language called Min-max Event-Triggered Computational Tree Logic for expressing such extremal queries on the timings of events and show that such queries can be evaluated in time polynomial in the size of the system times the length of the formula.

Item Type:Article
Source:Copyright of this article belongs to Indian Academy of Sciences.
Keywords:Computational Tree Logic; Timing Verification; Temporal Query Language
ID Code:101443
Deposited On:09 Mar 2018 10:13
Last Modified:09 Mar 2018 10:13

Repository Staff Only: item control page