Back to Search
Start Over
Sound and complete timed CTL model checking of timed Kripke structures and real-time rewrite theories.
- Source :
-
Science of Computer Programming . Mar2015, Vol. 99, p128-192. 65p. - Publication Year :
- 2015
-
Abstract
- In this paper we show that the satisfaction of timed CTL (TCTL) formulas under the natural continuous semantics for both discrete-time and dense-time timed Kripke structures can be reduced to a model-checking problem in the pointwise semantics for a large class of timed Kripke structures, which includes many discrete-event systems. We then present a TCTL model checking algorithm for the pointwise case. An important consequence of our results is that they together describe a sound and complete TCTL model checking procedure for time-robust real-time rewrite theories also for dense time domains. We have implemented such a TCTL model checker for Real-Time Maude. Our model checker provides for free a sound and complete TCTL model checker for subsets of modeling languages, such as Ptolemy II and (Synchronous) AADL, which have Real-Time Maude analysis integrated into their tool environments. [ABSTRACT FROM AUTHOR]
Details
- Language :
- English
- ISSN :
- 01676423
- Volume :
- 99
- Database :
- Academic Search Index
- Journal :
- Science of Computer Programming
- Publication Type :
- Academic Journal
- Accession number :
- 100134060
- Full Text :
- https://doi.org/10.1016/j.scico.2014.06.006