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.

@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/}
}

• timed_btp_tr.pdf
• timed_btp_tr.ps