Beyond Lassos: Complete SMT-Based Bounded Model Checking for Timed Automata

Reference:

Roland Kindermann, Tommi Junttila, and Ilkka Niemelä. Beyond lassos: Complete SMT-based bounded model checking for timed automata. In Holger Giese and Grigore Rosu, editors, Formal Techniques for Distributed Systems, volume 7273 of Lecture Notes in Computer Science, pages 84–100. Springer, 2012.

Abstract:

Timed automata (TAs) are a common formalism for modeling timed systems. Bounded model checking (BMC) is a verification method that searches for runs violating a property using a SAT or SMT solver. Previous SMT-based BMC approaches for TAs search for finite counter-examples and infinite lassoshaped counter-examples. This paper shows that lasso-based BMC cannot detect counter-examples for some linear time specifications expressed, e.g., with LTL or B¨uchi automata. This paper introduces a new SMT-based BMC approach that can find a counter-example to any non-holding B¨uchi automaton or LTL specification and also, in theory, prove that a specification holds. Different BMC encodings tailored for the supported features of different SMT solvers are compared experimentally to lasso-based BMC and discretization-based SAT BMC.

Keywords:

bounded model checking, timed automata, satisfiability modulo theories, symbolic model checking

Suggested BibTeX entry:

@inproceedings{KindermannJunttilaNiemela:FORTE2012,
    author = {Roland Kindermann and Tommi Junttila and Ilkka Niemel{\"a}},
    booktitle = {Formal Techniques for Distributed Systems},
    editor = {Holger Giese and Grigore Rosu},
    language = {eng},
    pages = {84--100},
    publisher = {Springer},
    series = {Lecture Notes in Computer Science},
    title = {Beyond Lassos: Complete {SMT}-Based Bounded Model Checking for Timed Automata},
    volume = {7273},
    year = {2012},
}