TEMPO: A Model Checker for Event-Recording Automata

We present a symbolic on-the-fly model checking algorithm for event-recording automata, a subclass of timed automata. This algorithm is based on a forward reachability analysis and uses a symbolic representation of clock constraints. It forms the core of the verification tool Tempo. We also develop a real-time logic for specifying properties of event-recording automata in a suitable way and demonstrate that the model checking problem for this logic is decidable.

Workshop on Real-Time Tools, Aalborg, Denmark 2001.

postscript

BibTeX Entry

@InProceedings{Sor01,
  author =    "Maria Sorea",
  title =     "Tempo: {A} Model-Checker for Event-Recording Automata",
  booktitle = "Proceedings of RT-TOOLS'01",
  year =      2001,
  address =   "Aalborg, Denmark",
  month =     "August",
  note =      "Also available as Technical Report SRI-CSL-01-04, 
               Computer Science Laboratory, SRI International, Menlo Park, CA, 2001,
               http://www.csl.sri.com/papers/csl-01-04/"
}