Path Compression in Timed Automata

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

Article type: Research Article

Authors: Janowska, Agata | Penczek, Wojciech

Affiliations: Institute of Informatics, Warsaw University Banacha 2, 02-097 Warsaw, Poland. E-mail: janowska@mimuw.edu.pl | Institute of Computer Science, PAS Ordona 21, 01-237 Warsaw, Poland. E-mail: penczek@ipipan.waw.pl

Abstract: The paper presents a method of abstraction for timed systems. To extract an abstract model of a timed system we propose to use static analysis, namely a technique called path compression. The idea behind the path compression consists in identifying a path (or a set of paths) on which a process executes a sequence of transitions that do not influence a property being verified, and replacing this path with a single transition. The method is property driven since it depends on a formula in question. The abstraction is exact with respect to all the properties expressible in the temporal logic CTL^*_{-X}.

Journal: Fundamenta Informaticae, vol. 79, no. 3-4, pp. 379-399, 2007