Slicing of timed automata with discrete data. (English) Zbl 1097.68061

Janowska, Agata; Janowski, Paweł

Fundam. Inform. 72, No. 1-3, 181-195 (2006).

Summary: The paper proposes how to use static analysis to extract an abstract model of a system. The method uses techniques of program slicing to examine syntax of a system modeled as a set of timed automata with discrete data, a common input formalism of model checkers dealing with time. The method is property driven. The abstraction is exact with respect to all properties expressed in the temporal logic \(\text{CTL}_{-X^*}\).

MSC:

68Q45	Formal languages and automata
68Q60	Specification and verification (program logics, model checking, etc.)
68Q85	Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)

Keywords:

timed systems; timed automata; static analysis; program slicing

Software:

Uppaal2k; VerICS