TU Berlin

Fachgebiet Kommunikations- und BetriebssystemePublikationen

Logo Fachgebiet KBS

Inhalt des Dokuments

zur Navigation

KBS Publikationen

Non-reachability in Petri Nets with Delaying Places
Zitatschlüssel WeMu:2006:PNDPs
Autor Matthias Werner and Gero Mühl
Buchtitel The 14th IEEE/ACM International Symposium on Modeling, Analysis and Simulation of Computer and Telecommunication Systems (MASCOTS 2006)
Seiten 401-412
Jahr 2006
ISBN 0-7695-2573-3
Adresse Monterey, California
Monat sep
Verlag IEEE
Zusammenfassung 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 zur Publikation Download Bibtex Eintrag

Navigation

Direktzugang

Schnellnavigation zur Seite über Nummerneingabe