Path Compression in Timed Automata

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 in question. The abstraction is exact with respect to all the properties expressible in the temporal logic CTL∗ −X.

• Type: Journal
• Year: 2007
• Where: FUIN
• Authors: Agata Janowska, Wojciech Penczek
• Keywords: Abstract Model, FUIN 2007, Path Compression, Static Analysis