Path Compression in Timed Automata

11 years 1 months ago
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.
Agata Janowska, Wojciech Penczek
Added 14 Dec 2010
Updated 14 Dec 2010
Type Journal
Year 2007
Where FUIN
Authors Agata Janowska, Wojciech Penczek
Comments (0)