Improved Bounded Model Checking of Timed Automata

TL;DR

This paper enhances the bounded model checking of Timed Automata by directly encoding networks into SMT solvers, improving efficiency while supporting rich temporal logic properties.

Contribution

It introduces a novel direct encoding method into SMT solvers for Timed Automata, maintaining MITL support and optimizing performance over previous CLTLoc-based approaches.

Findings

Significant performance improvements in practical scenarios.

Effective encoding of MITL properties into SMT logic.

Enhanced scalability of Timed Automata verification.

Abstract

Timed Automata (TA) are a very popular modeling formalism for systems with time-sensitive properties. A common task is to verify if a network of TA satisfies a given property, usually expressed in Linear Temporal Logic (LTL), or in a subset of Timed Computation Tree Logic (TCTL). In this paper, we build upon the TACK bounded model checker for TA, which supports a signal-based semantics of TA and the richer Metric Interval Temporal Logic (MITL). TACK encodes both the TA network and property into a variant of LTL, Constraint LTL over clocks (CLTLoc). The produced CLTLoc formula can then be solved by tools such as Zot, which transforms CLTLoc properties into the input logics of Satisfiability Modulo Theories (SMT) solvers. We present a novel method that preserves TACK's encoding of MITL properties while encoding the TA network directly into the SMT solver language, making use of both the BitVector logic and the logic of real arithmetics. We also introduce several optimizations that allow us to significantly outperform the CLTLoc encoding in many practical scenarios.