題名: AN INCREMENTAL VERIFICATION ALGORITHM FOR REAL-TIME SYSTEMS 作者: A SAHAY;JJP TSAI;AP SISTLA
貢獻者: Department of Bioinformatics
關鍵詞: Model-checking;timed mu-calculus;timed automata;requirements specification;labeled transition systems
日期: 1999
上傳時間: 2009-11-17T11:17:43Z 出版者: Asia University
摘要: We present an incremental algorithm for model checking the real-time systems against the requirements specified in the real-time extension of modal mu-calculus.
Using this algorithm, we avoid the repeated construction and analysis of the whole state-space during the course of evolution of the system from time to time. We use a finite representation of the system, like most other algorithms on real-time systems. We construct and update a graph (called TSG) that is derived from the region graph and the formula. This allows us to halt the construction of this graph when enough nodes have been explored to determine the truth of the formula. TSG is minimal in the sense of partitioning the infinite state space into regions and it expresses a relation on the set of regions of the partition. We use the structure of the formula to derive this partition. When a change is applied to the timed
automaton of the system, we find a new partition from the current partition and the TSG with minimum cost.
