Min-max event-triggered computation tree logic

Abstract

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.