Bounded Model Checking for Timed Automata |
| |
Authors: | Maria Sorea |
| |
Affiliation: | aSRI International, Computer Science Laboratory, 333 Ravenswood Avenue, Menlo Park, CA 94025, USA |
| |
Abstract: | Given a timed automaton M, a linear temporal logic formula φ, 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 φ. 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. |
| |
Keywords: | |
本文献已被 ScienceDirect 等数据库收录! |
|