Checking Reachability Properties for Timed Automata via SAT

Issue title: Concurrency Specification and Programming (CS&P'2002), Part 2

Article type: Research Article

Authors: Woźna, Bożena | Zbrzezny, Andrzej | Penczek, Wojciech^;

Affiliations: Institute of Mathematics and Computer Science, PU, Armii Krajowej 13/15, 42-200 Czestochowa, Poland | Institute of Computer Science, PAS, Ordona 21, 01-237 Warsaw, Poland | Institute of Informatics, Podlasie Academy, 3 maja 54, 08-110 Siedlce, Poland

Abstract: The paper deals with the problem of checking reachability for timed automata. The main idea consists in combining the well-know forward reachability algorithm and the Bounded Model Checking (BMC) method. In order to check reachability of a~state satisfying some desired property, first the transition relation of a timed automaton is unfolded iteratively to some depth and encoded as a propositional formula. Next, the desired property is translated to a propositional formula and the satisfiability of the conjunction of the two defined above formulas is checked. The unfolding of the transition relation can be terminated when either a state satisfying the property has been found or all the states of the timed automaton have been searched. The efficiency of the method is strongly supported by the experimental results.

Keywords: , ,

Journal: Fundamenta Informaticae, vol. 55, no. 2, pp. 223-241, 2003