SMT-based Induction Methods for Timed Systems

TL;DR

This paper extends the IC3 and $k$-induction algorithms with SMT-based techniques to verify timed systems, effectively handling infinite state spaces through region abstraction and demonstrating improved performance over booleanization methods.

Contribution

It introduces SMT-based extensions of IC3 and $k$-induction algorithms tailored for timed systems, enabling efficient verification of infinite state spaces.

Findings

SMT-based IC3 effectively handles dense time domains.

Extended $k$-induction supports timed system verification.

Experimental results show improved efficiency over booleanization approaches.

Abstract

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 new methods are evaluated and experimentally compared to a booleanization-based verification approach that uses the original discrete time IC3 algorithm.