SAT-Based Reachability Checking for Timed Automata with Discrete Data

Issue title: Special Issue on Concurrency Specification and Programming (CS&P)

Article type: Research Article

Authors: Zbrzezny, Andrzej | Półrola, Agata

Affiliations: Institute of Mathematics and Computer Science, Jan Długosz University, Armii Krajowej 13/15, 42-200 Czestochowa, Poland. E-mail: a.zbrzezny@ajd.czest.pl | Faculty of Mathematics and Computer Science, University of Lodz Banacha 22, 90-238 Lodz, Poland. E-mail: polrola@math.uni.lodz.pl

Abstract: Reachability analysis for timed automata using SAT-based methods was considered in many papers, occurring to be a very efficient model checking technique. In this paper we show how to apply this method of verification to timed automata with discrete data, i.e., to standard timed automata augmented with integer variables. The theoretical description is supported by some preliminary experimental results.

Journal: Fundamenta Informaticae, vol. 79, no. 3-4, pp. 579-593, 2007