Logic in Computer Science (LICS 1993)

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

Authors: 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 Symp. on Logic in Computer Science, {LICS} 1993},
    year =	 1993,
    editor =	 {Moshe Vardi},
    month =	 {June}, 
    pages =      {147--159},
    location =   {Montreal, Canada}, 
    publisher =	 {IEEE Computer Society Press}
  }