On Deciding Behavioral Properties for Petri Nets : Timed-Arc Petri Nets and their Extensions
Authors
Óskarsdóttir, Ragnhildur Þórunn ; Stefánsson, Sigmar ; Jónasson, Tómas
Term
10. Term
Education
Publication year
2005
Abstract
Petri-net-modellen er et udbredt matematisk værktøj i model checking, hvor man automatisk verificerer, at systemer opfører sig som forventet. For den klassiske Petri-net-model er centrale adfærdsspørgsmål – som reachability (nåbarhed: kan en bestemt situation opstå?), coverability (dækbarhed: kan vi nå noget, der mindst opfylder et mål?), deadlock (fastlåsning: kan systemet gå i stå?), og liveness (livlighed/fremdrift: vil der altid ske noget før eller siden?) – kendt for at være afgørbare, dvs. der findes en metode, der altid giver et klart ja/nej-svar. Klassiske Petri-net mangler dog tidsaspekter, som er afgørende for realtidssystemer med deadlines og forsinkelser. Derfor blev timed-arc Petri net-modellen indført som en udvidelse, der knytter tidsinformation til modellens forbindelser. Dette arbejde undersøger, hvor langt afgørbarhedsresultaterne rækker for timed-arc Petri net. Vi giver resultater for, om reachability, coverability, deadlock og liveness er afgørbare for timed-arc Petri net-modellen samt for flere beslægtede udvidelser af modellen, som vi enten definerer selv eller bygger på andres forslag.
Petri nets are a widely used mathematical model in model checking, where systems are automatically verified to behave as intended. For the classic Petri net model, core behavioral questions—reachability (can a specific situation occur?), coverability (can we reach a situation that meets at least a given goal?), deadlock (can the system get stuck?), and liveness (will progress continue?)—are known to be decidable, meaning there is a method that always yields a clear yes/no answer. Classic Petri nets, however, do not capture timing, which is essential for real-time systems with deadlines and delays. To address this, the timed-arc Petri net model extends Petri nets by attaching timing information to connections. This thesis examines how far these decidability results extend to timed-arc Petri nets. We provide results on whether reachability, coverability, deadlock, and liveness are decidable for the timed-arc Petri net model, as well as for several related extensions of the model, either defined by us or inspired by prior work.
[This abstract was generated with the help of AI]
Documents