State Space Methods for Timed Petri Nets

Søren Christensen; Kurt Jensen; Thomas Mailund; Herbert Weber; Harmut Ehrig; Wolfgang Reisig

State Space Methods for Timed Petri Nets

Søren Christensen, Kurt Jensen, Thomas Mailund, Herbert Weber (Editor), Harmut Ehrig (Editor), Wolfgang Reisig (Editor)

Research output: Contribution to book/anthology/report/proceeding › Article in proceedings › Research

Abstract

We present two recently developed state space methods for timed Petri nets. The two methods reconciles state space methods and time concepts based on the introduction of a global clock and associating time stamps to tokens. The first method is based on an equivalence relation on states which makes it possible to condense the usually infinite state space of a timed Petri net into a finite condensed state space without loosing analysis power. The second method supports on-the-fly verification of certain safety properties of timed systems. We discuss the application of the two methods in a number of different areas.

Original language	English
Title of host publication	Proc. of 2nd Int. Coll. on Petri Net Technologies for Modelling Communication Based Systems : DFG Research Group "Petri Net Technology"
Number of pages	10
Publisher	DFG-Forschergruppe Petri Net Technologie
Publication date	2001
Pages	33-42
Publication status	Published - 2001
Event	Colloquium on Petri Net Technologies for Modeling Communication Based Systems - Berlin, Germany Duration: 14 Sept 2001 → 15 Sept 2001 Conference number: 2

Conference

Conference	Colloquium on Petri Net Technologies for Modeling Communication Based Systems
Number	2
Country/Territory	Germany
City	Berlin
Period	14/09/2001 → 15/09/2001

Cite this

@inproceedings{b58a67d0983b11dabee902004c4f4f50,

title = "State Space Methods for Timed Petri Nets",

abstract = "We present two recently developed state space methods for timed Petri nets. The two methods reconciles state space methods and time concepts based on the introduction of a global clock and associating time stamps to tokens. The first method is based on an equivalence relation on states which makes it possible to condense the usually infinite state space of a timed Petri net into a finite condensed state space without loosing analysis power. The second method supports on-the-fly verification of certain safety properties of timed systems. We discuss the application of the two methods in a number of different areas. ",

author = "S{\o}ren Christensen and Kurt Jensen and Thomas Mailund and Herbert Weber and Harmut Ehrig and Wolfgang Reisig",

year = "2001",

language = "English",

pages = "33--42",

booktitle = "Proc. of 2nd Int. Coll. on Petri Net Technologies for Modelling Communication Based Systems",

publisher = "DFG-Forschergruppe Petri Net Technologie",

note = "Colloquium on Petri Net Technologies for Modeling Communication Based Systems ; Conference date: 14-09-2001 Through 15-09-2001",

}

Christensen, S , Jensen, K, Mailund, T, Weber, H (ed.), Ehrig, H (ed.) & Reisig, W (ed.) 2001, State Space Methods for Timed Petri Nets. in Proc. of 2nd Int. Coll. on Petri Net Technologies for Modelling Communication Based Systems: DFG Research Group "Petri Net Technology". DFG-Forschergruppe Petri Net Technologie, pp. 33-42, Colloquium on Petri Net Technologies for Modeling Communication Based Systems, Berlin, Germany, 14/09/2001.

State Space Methods for Timed Petri Nets. / Christensen, Søren ; Jensen, Kurt; Mailund, Thomas et al.
Proc. of 2nd Int. Coll. on Petri Net Technologies for Modelling Communication Based Systems: DFG Research Group "Petri Net Technology". DFG-Forschergruppe Petri Net Technologie, 2001. p. 33-42.

Research output: Contribution to book/anthology/report/proceeding › Article in proceedings › Research

TY - GEN

T1 - State Space Methods for Timed Petri Nets

AU - Christensen, Søren

AU - Jensen, Kurt

AU - Mailund, Thomas

A2 - Weber, Herbert

A2 - Ehrig, Harmut

A2 - Reisig, Wolfgang

N1 - Conference code: 2

PY - 2001

Y1 - 2001

N2 - We present two recently developed state space methods for timed Petri nets. The two methods reconciles state space methods and time concepts based on the introduction of a global clock and associating time stamps to tokens. The first method is based on an equivalence relation on states which makes it possible to condense the usually infinite state space of a timed Petri net into a finite condensed state space without loosing analysis power. The second method supports on-the-fly verification of certain safety properties of timed systems. We discuss the application of the two methods in a number of different areas.

AB - We present two recently developed state space methods for timed Petri nets. The two methods reconciles state space methods and time concepts based on the introduction of a global clock and associating time stamps to tokens. The first method is based on an equivalence relation on states which makes it possible to condense the usually infinite state space of a timed Petri net into a finite condensed state space without loosing analysis power. The second method supports on-the-fly verification of certain safety properties of timed systems. We discuss the application of the two methods in a number of different areas.

M3 - Article in proceedings

SP - 33

EP - 42

BT - Proc. of 2nd Int. Coll. on Petri Net Technologies for Modelling Communication Based Systems

PB - DFG-Forschergruppe Petri Net Technologie

T2 - Colloquium on Petri Net Technologies for Modeling Communication Based Systems

Y2 - 14 September 2001 through 15 September 2001

ER -

State Space Methods for Timed Petri Nets

Abstract

Conference

Fingerprint

Cite this