## Paper: On model checking for real-time properties with durations (at LICS 1993)

**Ahmed Bouajjani Rachid Echahed Joseph Sifakis**

### Abstract

The verification problem for real-time properties involving duration constraints (predicates) is addressed. The duration of a state property, along an interval of a computation sequence of a real-time system, is the time the property is true. In particular, the global time spent in such an interval is the duration of the formula `true'. The real-time logic TCTL is extended to a duration logic called SDTL in which duration constraints can be expressed. The problem of the verification of SDTL formulas with respect to a class of timed models of reactive systems is investigated. New model checking procedures are proposed for the most significant properties expressible in SDTL, including eventuality and invariance properties. Such results are provided for the two cases of discrete and dense time

### BibTeX

@InProceedings{BouajjaniEchahedSif-Onmodelcheckingforr, author = {Ahmed Bouajjani and Rachid Echahed and Joseph Sifakis}, title = {On model checking for real-time properties with durations}, booktitle = {Proceedings of the Eighth Annual IEEE Symposium on Logic in Computer Science (LICS 1993)}, year = {1993}, month = {June}, pages = {147--159}, location = {Montreal, Canada}, publisher = {IEEE Computer Society Press} }