SMT-Based Induction Methods for Timed Systems


Roland Kindermann, Tommi Junttila, and Ilkka Niemelä. SMT-based induction methods for timed systems. In Marcin Jurdzinski and Dejan Nickovic, editors, Formal Modeling and Analysis of Timed Systems, volume 7595 of Lecture Notes in Computer Science, pages 171–187. Springer, 2012.


Modeling time-related aspects is important in many applications of verification methods. For precise results, it is necessary to interpret time as a dense domain, e.g. using timed automata as a formalism, even though the system’s resulting infinite state space is challenging for verification methods. Furthermore, fully symbolic treatment of both timing related and non-timing related elements of the state space seems to offer an attractive approach to model checking timed systems with a large amount of non-determinism. This paper presents an SMT-based timed system extension to the IC3 algorithm, a SAT-based novel, highly efficient, complete verification method for untimed systems. Handling of the infinite state spaces of timed system in the extended IC3 algorithm is based on suitably adapting the well-known region abstraction for timed systems. Additionally, k-induction, another symbolic verification method for discrete time systems, is extended in a similar fashion to support timed systems. Both methods are evaluated and experimentally compared to a booleanization-based verification approach that uses the original discrete time IC3 algorithm.


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

Suggested BibTeX entry:

    author = {Roland Kindermann and Tommi Junttila and Ilkka Niemel{\"a}},
    booktitle = {Formal Modeling and Analysis of Timed Systems},
    editor = {Marcin Jurdzinski and Dejan Nickovic},
    language = {eng},
    pages = {171--187},
    publisher = {Springer},
    series = {Lecture Notes in Computer Science},
    title = {{SMT}-Based Induction Methods for Timed Systems},
    volume = {7595},
    year = {2012},

See ...