Skip to Main content Skip to Navigation
Conference papers

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

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 lasso-shaped 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üchi automata. This paper introduces a new SMT-based BMC approach that can find a counter-example to any non-holding Büchi 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.
Complete list of metadata

Cited literature [20 references]  Display  Hide  Download
Contributor : Hal Ifip <>
Submitted on : Monday, May 29, 2017 - 3:54:03 PM
Last modification on : Thursday, November 26, 2020 - 2:56:03 PM
Long-term archiving on: : Wednesday, September 6, 2017 - 11:22:45 AM


Files produced by the author(s)


Distributed under a Creative Commons Attribution 4.0 International License



Roland Kindermann, Tommi Junttila, Ilkka Niemelä. Beyond Lassos: Complete SMT-Based Bounded Model Checking for Timed Automata. 14th International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS) / 32nd International Conference on Formal Techniques for Networked and Distributed Systems (FORTE), Jun 2012, Stockholm, Sweden. pp.84-100, ⟨10.1007/978-3-642-30793-5_6⟩. ⟨hal-01528739⟩



Record views


Files downloads