Slicing of Timed Automata with Discrete Data

Issue title: SPECIAL ISSUE ON CONCURRENCY SPECIFICATION AND PROGRAMMING (CS&P 2005) Ruciane-Nide, Poland, 28–30 September 2005

Article type: Research Article

Authors: Janowska, Agata | Janowski, Paweł

Affiliations: Institute of Informatics Warsaw University Banacha 2, 02-097 Warsaw, Poland. E-mail: {janowska,janowski}@mimuw.edu.pl

Abstract: 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 CTL_{-X}*.

Keywords: timed systems, Timed Automata, static analysis, program slicing

Journal: Fundamenta Informaticae, vol. 72, no. 1-3, pp. 181-195, 2006