SMT-based induction methods for timed systems

DOI10.1007/978-3-642-33365-1_13MaRDI QIDQ4649395zbMATH OpenOpenAlexFDO

Authors Roland Kindermann, Tommi Junttila, Ilkka Niemelä

Publication date 21 November 2012

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1204.5639

Mathematics Subject Classification ID

Performance evaluation, queueing, and scheduling in the context of computer systems (68M20) Specification and verification (program logics, model checking, etc.) (68Q60)

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.

Recommendations

• scientific article; zbMATH DE number 1973987
• Simple SMT-based bounded model checking for timed interpreted systems
• The automatic verification using symbolic model-checking
• Improvements for the Symbolic Verification of Timed Automata
• Verification of timed automata via satisfiability checking

Cited in

(11)

• Zone-based verification of timed automata: extrapolations, simulations and what next?
• Abstraction-based incremental inductive coverability for Petri nets
• Configurable verification of timed automata with discrete variables
• Automatic discovery of fair paths in infinite-state transition systems
• SMT-based satisfiability of first-order LTL with event freezing functions and metric operators
• Proving the existence of fair paths in infinite-state systems
• Infinite-state invariant checking with IC3 and predicate abstraction
• Exact Incremental Analysis of Timed Automata with an SMT-Solver
• Lazy Reachability Checking for Timed Automata with Discrete Variables
• Verification Modulo theories
• Timed automata verification and synthesis via finite automata learning

This page was built for publication: SMT-based induction methods for timed systems

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4649395)