Analysis of RTCP-nets with Reachability Graphs

Article type: Research Article

Authors: Szpyrka, Marcin

Affiliations: Institute of Automatics, AGH University of Science and Technology, Al. Mickiewicza 30, 30-059 Kraków, Poland. E-mail: [email protected]

Abstract: RTCP-nets are a subclass of timed coloured Petri nets defined for modelling and analysis of embedded real-time systems. One of the main advantages of strongly bounded RTCP-nets is a possibility to present the set of reachable states of an RTCP-net using a finite reachability and/or coverability graph. These graphs can be used to verify most of the net's properties, including the timing ones. The paper discusses analysis methods based on these graphs. A formal definition of RTCP-nets and a survey of their properties are also presented in the paper.

Keywords: RTCP-nets, analysis, reachability graphs, coverability graphs

Journal: Fundamenta Informaticae, vol. 74, no. 2-3, pp. 375-390, 2006