Where academic tradition
meets the exciting future

You are here: TUCS > PUBLICATIONS > Publication Search > Efficient State Space Search f...

Efficient State Space Search for Time Petri Nets

Johan Lilius, Efficient State Space Search for Time Petri Nets. Electronic Notes in Theoretical Computer Science 18, 113–133, 1998.

Abstract:

Partial-order reduction methods provide a number of well studied methods that have been succesfully applied to the state-space explosion problem that arises when analysing state based models of concurrent and reactive systems.

The techniques have mainly been studied within the context of untimed systems, in the context of real-time systems little progress has been made. The main problem seems to be the global nature of time, that makes all clocks in the system dependent on each other. Typically this is manifested in the semantics of real-time models in which the ordering of events is implicitely stored in the state of the system.

In this work we propose a new semantics for time Petri nets that, does not store the firing order into the timing constraints. This allows us to lift the notion of independence from untimed Petri nets, and it becomes possible to directly apply the theory of partial-order reductions to time Petri nets. We show that our semantics is finite and that it preserves reachable markings.

As a second contribution we propose to exploit the branching prefix originally introduced by McMillan in the state-space search of time Petri nets. To make sure that the state-space search algorithm terminates, one needs a list of states that have already been seen during the search. This list is searched each time a new state is generated. We propose to only store states after cutoff events. The cutoff events in a branching prefix describe events after which the system will return to a state in which it has previously been. Finally we also show how to extract persistent sets from the branching prefix.

Files:

Full publication in PDF-format

BibTeX entry:

@ARTICLE{jLilius98a,
  title = {Efficient State Space Search for Time Petri Nets},
  author = {Lilius, Johan},
  journal = {Electronic Notes in Theoretical Computer Science},
  volume = {18},
  pages = {113–133},
  year = {1998},
}

Belongs to TUCS Research Unit(s): Embedded Systems Laboratory (ESLAB)

Publication Forum rating of this publication: level 1

Edit publication