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

Article type: Research Article

Authors: Woźna, Bożena | Zbrzezny, Andrzej

Affiliations: Institute of Mathematics and Computer Science, Jan Długosz University Al. Armii Krajowej 13/15, 42-200 Cz�stochowa, Poland. E-mail: {b.wozna,a.zbrzezny}@ajd.czest.pl

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.

Journal: Fundamenta Informaticae, vol. 79, no. 1-2, pp. 229-256, 2007