Min-max event-triggered computation tree logic

作     者：Dasgupta, P Chakrabarti, PP Deka, JK 

作者机构：Indian Inst Technol Dept Comp Sci & Engn Kharagpur 721302 W Bengal India 

出 版 物：《SADHANA-ACADEMY PROCEEDINGS IN ENGINEERING SCIENCES》 (Sadhana)

年 卷 期：2002年第27卷第2期

页      面：163-180页

核心收录：

学科分类：12[管理学] 1201[管理学-管理科学与工程(可授管理学、工学学位)] 08[工学] 

主　　题：computational tree logic timing verification temporal query language 

摘      要：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.