A proposal for relative time petri nets
Date
2005
Authors
Kuehn, J.
Lakos, C.
Esser, R.
Editors
Aichernig, B.
Beckert, B.
Beckert, B.
Advisors
Journal Title
Journal ISSN
Volume Title
Type:
Conference paper
Citation
Third IEEE International Conference on Software Engineering and Formal Methods (SEFM'05), 2005 : pp. 240-249
Statement of Responsibility
Joseph Kuehn, Charles Lakos, Robert Esser
Conference Name
IEEE International Conference on Software Engineering and Formal Methods (3rd : 2005 : Koblenz, Germany)
Abstract
Petri nets are a graph-based modelling formalism which has been widely used for the formal specification and analysis of concurrent systems. A common analysis technique is that of state space exploration (or reachability analysis). Here, every possible reachable state of the system is generated and desirable properties are evaluated for each state. This approach has the great advantage of conceptual simplicity, but the great disadvantage of being susceptible to state space explosion, where the number of states is simply too large for exhaustive exploration. Many reduction techniques have been suggested to ameliorate the problem of state space explosion. In the case of timed systems, the state space is infinite, unless analysis is restricted to a bounded time period. In this paper, we present a Petri net formalism based on the notion of relative time (as opposed to the traditional approach of dealing with absolute time). The goal is to derive a finite state space for timed systems which have repeating patterns of behaviour, even though time continues to advance indefinitely.
School/Discipline
Dissertation Note
Provenance
Description
Copyright © 2005, IEEE