Reachability Analysis for Timed Automata Using Partitioning Algorithms

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

Article type: Research Article

Authors: Półrola, Agata | Penczek, Wojciech | Szreter, Maciej

Affiliations: Faculty of Mathematics, University of Lodz, Banacha 22, 90-238 Lodz, Poland | Institute of Computer Science, PAS, Ordona 21, 01-237 Warsaw, Poland

Abstract: The paper presents a new method for checking reachability properties of Timed Automata. The idea consists in on-the-fly verification of a property on a pseudo-bisimulating model generated by a modified partitioning algorithm. Pseudo-bisimulating models are often much smaller than forward-reachability graphs commonly used in reachability analysis. A theoretical description of the algorithm is supported by several experimental results.

Journal: Fundamenta Informaticae, vol. 55, no. 2, pp. 203-221, 2003