Bounded Model Checking for Timed Automata

Given a timed automaton M, a linear temporal logic formula phi, and a bound k, bounded model checking for timed automata determines if there is a falsifying path of length k to the hypothesis that M satisfies the specification phi. This problem can be reduced to the satisfiability problem for Boolean constraint formulas over linear arithmetic constraints. We show that bounded model checking for timed automata is complete, and we give lower and upper bounds for the length k of counterexamples. Moreover, we define bounded model checking for networks of timed automata in a compositional way.

Electronic Notes in Theoretical Computer Science, Vol. 68, No. 5, 2002. Third Workshop on Models for Time-Critical Systems (MTCS) 2002.

gzipped postscript or postscript

BibTeX Entry

@Article{Sorea:mtcs02,
  author =       {Maria Sorea},
  title =        {Bounded Model Checking for Timed Automata},
  journal =      {Electronic Notes in Theoretical Computer Science},
  year =         {2002},
  volume =       {68},
  number =       {5},
  note =         {http://www.elsevier.com/locate/entcs/volume68.html}
}