Back to Search
Start Over
Efficient timed model checking for discrete-time systems
- Source :
-
Theoretical Computer Science . Mar2006, Vol. 353 Issue 1-3, p249-271. 23p. - Publication Year :
- 2006
-
Abstract
- Abstract: We consider model checking of timed temporal formulae in durational transition graphs (DTGs), i.e., Kripke structures where transitions have integer durations. Two semantics for DTGs are presented and motivated. We consider timed versions of where subscripts put quantitative constraints on the time it takes before a property is satisfied. We exhibit an important gap between logics where subscripts of the form “” (exact duration) are allowed, and simpler logics that only allow subscripts of the form “” or “” (bounded duration). Without exact durations, model checking can be done in polynomial time, but with exact durations, it becomes -complete or -complete depending on the considered semantics. [Copyright &y& Elsevier]
- Subjects :
- *DISCRETE-time systems
*SEMANTICS
*LOGIC
*POLYNOMIALS
Subjects
Details
- Language :
- English
- ISSN :
- 03043975
- Volume :
- 353
- Issue :
- 1-3
- Database :
- Academic Search Index
- Journal :
- Theoretical Computer Science
- Publication Type :
- Academic Journal
- Accession number :
- 19848813
- Full Text :
- https://doi.org/10.1016/j.tcs.2005.11.020