direkt zum Inhalt springen

direkt zum Hauptnavigationsmenü

Sie sind hier

TU Berlin

Page Content

Publications of KBS

Non-reachability in Petri Nets with Delaying Places
Citation key WeMu:2006:PNDPs
Author Matthias Werner and Gero Mühl
Title of Book The 14th IEEE/ACM International Symposium on Modeling, Analysis and Simulation of Computer and Telecommunication Systems (MASCOTS 2006)
Pages 401-412
Year 2006
ISBN 0-7695-2573-3
Address Monterey, California
Month sep
Publisher IEEE
Abstract The correctness of systems is frequently proved by demonstrating the non-reachability of certain (incorrect) states with the help of formal frameworks, e.g., Petri nets. Especially for real-time systems, the timely behavior has to be considered. Thus, there exist several extensions that allow the modeling of time in Petri nets. Non-reachability proofs in time-dependent Petri nets are usually done by proving the non-reachability within the time-less skeleton. However, in many cases this approach fails to prove non-reachability, since the skeleton can reach more markings than the timedependent Petri net. In this paper, we introduce a state equation for a class of time-augmented Petri nets and demonstrate in an example application how this state equation can be used to prove non-reachability within the actual timedependent net.
Link to publication Download Bibtex entry

Zusatzinformationen / Extras

Quick Access:

Schnellnavigation zur Seite über Nummerneingabe

Auxiliary Functions