SRI Logo
About Us|R and D Divisions|Careers|Newsroom|Contact Us|SRI Home
  SRI Logo

Bounded Model Checking for Timed Automata
 by Maria Sorea.

Number SRI-CSL-02-03.

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 systems of timed automata in a compositional way.
BibTEX Entry
    AUTHOR = {Maria Sorea},
    TITLE = {Bounded Model Checking for Timed Automata},
    NUMBER = {{SRI-CSL-02-03}},
    URL = {}


About Us  |  R&D Divisions  |  Careers  |  Newsroom  |  Contact Us
© 2024 SRI International 333 Ravenswood Avenue, Menlo Park, CA 94025-3493
SRI International is an independent, nonprofit corporation. Privacy policy