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.


Abstract
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
@article{timed_btp_tr,
    AUTHOR = {Maria Sorea},
    TITLE = {Bounded Model Checking for Timed Automata},
    NUMBER = {{SRI-CSL-02-03}},
    URL = {http://www.csl.sri.com/papers/timedbtptr/}
}
Files
 













 

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