Bounded Model Checking of an MITL Fragment for Timed Automata

TL;DR

This paper extends the semantics of a fragment of MITL for timed automata to super-dense time traces and develops a bounded model checking method, with proofs of correctness and completeness, and experimental evaluation.

Contribution

It introduces a novel BMC encoding for MITL over super-dense time traces and proves its correctness and completeness.

Findings

The approach can find counter-examples with sufficiently large bounds.

Implementation demonstrates efficiency and scalability.

Extended MITL semantics for super-dense time traces.

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. MITL is a real-time extension of the linear time logic LTL. Originally, MITL was defined for traces of non-overlapping time intervals rather than the "super-dense" time traces allowing for intervals overlapping in single points that are employed by the nowadays common semantics of timed automata. In this paper we extend the semantics of a fragment of MITL to super-dense time traces and devise a bounded model checking encoding for the fragment. We prove correctness and completeness in the sense that using a sufficiently large bound a counter-example to any given non-holding property can be found. We have implemented the proposed bounded model checking approach and experimentally studied the efficiency and scalability of the implementation.