SAT-based Reachability Checking for Timed Automata with Diagonal Constraints

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

Article type: Research Article

Authors: Zbrzezny, Andrzej

Affiliations: Institute of Mathematics and Computer Science, Pedagogical University of Cz�stochowa, Al. Armii Krajowej 13 15, 42-200 Cz�stochowa, Poland. E-mail: [email protected]

Abstract: This paper deals with the problemof checking reachability for timed automata with diagonal constraints. Such automata are needed in many applications e.g. to model scheduling problems. We introduce a new discretization for timed automata which enables SAT based reachability analysis for timed automata for which comparisons between two clocks are allowed. In our earlier papers SAT based reachability analysis was restricted to the so called diagonal-free timed automata, where only comparisons between clocks and constants are allowed.

Journal: Fundamenta Informaticae, vol. 67, no. 1-3, pp. 303-322, 2005