Bounded Model Checking for the Existential Fragment of TCTL _{-G} and Diagonal Timed Automata

Abstract

Bounded Model Checking (BMC) is one of the well known SAT based symbolic model checking techniques. It consists in searching for a counterexample of a particular length, and generating a propositional formula that is satisfiable iff such a counterexample exists. The BMC method is feasible for the various classes of temporal logic; in particular it is feasible for TECTL (the existential fragment of Time Computation Tree Logic) and Diagonal-free Timed Automata. The main contribution of the paper is to show that the concept of Bounded Model Checking can be extended to deal with TECTL _{-G} properties of Diagonal Timed Automata. We have implemented our new BMC algorithm, and we present preliminary experimental results, which demonstrate the efficiency of the method.