Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Invariants and Home Spaces in Transition Systems and Petri Nets

Gerard Memmi

Abstract

This lecture note focuses on comparing the notions of invariance and home spaces in Transition Systems and more particularly, in Petri Nets. We also describe how linear algebra relates to these basic notions in Computer Science, how it can be used for extracting invariant properties from a parallel system described by a Labeled Transition System in general and a Petri Net in particular. We endeavor to regroup a number of algebraic results dispersed throughout the Petri Nets literature with the addition of new results around the notions of semiflows and generating sets. \newline Several extensive examples are given to illustrate how the notion of invariants and home spaces can be methodically utilized through basic arithmetic and algebra to prove behavioral properties of a Petri Net. Some additional thoughts on invariants and home spaces will conclude this note.

Invariants and Home Spaces in Transition Systems and Petri Nets

Abstract

This lecture note focuses on comparing the notions of invariance and home spaces in Transition Systems and more particularly, in Petri Nets. We also describe how linear algebra relates to these basic notions in Computer Science, how it can be used for extracting invariant properties from a parallel system described by a Labeled Transition System in general and a Petri Net in particular. We endeavor to regroup a number of algebraic results dispersed throughout the Petri Nets literature with the addition of new results around the notions of semiflows and generating sets. \newline Several extensive examples are given to illustrate how the notion of invariants and home spaces can be methodically utilized through basic arithmetic and algebra to prove behavioral properties of a Petri Net. Some additional thoughts on invariants and home spaces will conclude this note.
Paper Structure (78 sections, 19 theorems, 12 equations, 18 figures)

This paper contains 78 sections, 19 theorems, 12 equations, 18 figures.

Table of Contents

  1. Introduction
  2. Motivations
  3. Outline and contributions
  4. Notations and abbreviations
  5. Observer, systems under study, models, and conceptual models
  6. Observer
  7. Systems under study (SuS)
  8. Models (M)
  9. Conceptual models (CM)
  10. State Variables, States, and Transitions
  11. State variables, states, and trajectories
  12. State variables
  13. States and state spaces
  14. trajectories
  15. Transitions and traces
  16. ...and 63 more sections

Key Result

Theorem 1

A source is minimal if and only if it is an scc-s. Similarly, a sink is minimal if and only if it is an scc-sk. If $S$ is an scc and $A \subseteq S$ is a sink (source respectively) then $S$ is a minimal sink (source respectively).

Figures (18)

  • Figure 1: $Q = \{q_1, q_2, q_3, q_4, q_5, q_6, q_7\}, T =\{t_0, t_1, t_2, t_3\}$. The sequence of transitions $t_1t_3$ can never be a possible trace whatever is $Init$. In (a), $\textit{Term} = \varnothing$ and the sequence of transitions $t_0t_2$ is a possible trace beginning at $q_1$; however, it is not a trace from $\textit{Init} = \{q_2,q_3\}$. In (b), $q_2 \overset{t_1}{\rightarrow} q_4\overset{t_2}{\rightarrow}q_6$ is the only computation given $Init$ and $Term$.
  • Figure 2: $Q=\{q_0,q_1,q_2,q_3,q_4,q_5,q_6,q_7\},\ HS_1 = \{q_1,q_3,q_4\},\ HS_2= \{q_1, q_5\}, \ HS_3=\{q_1,q_3,q_5\}$ are three $\{q_0\}$-home space. $HS_4=\{q_1, q_4,q_7\}$ is a $\{q_6\}$-home space as well as a $\{q_0\}$-home space.
  • Figure 3: Different definitions of boundedness according to the fact that every state variable is bounded or not for every possible state or not.
  • Figure 4: Program1 and Program2 are two instances of the process(i) and are concurrently running sharing a common resource guarded by a semaphore $\texttt{S}$. $\texttt{S}$ is initialized to $1$ to guarantee the mutual exclusion between the critical section of each program. We assume that there are no dependencies (i.e. shared resources) between an initial piece of code called action and the critical section, in particular that only the critical section handles the common resource protected by the semaphore.
  • Figure 5: Labeled Reachability Graph (LRG) of the LTS modeling the two concurrent programs in mutual exclusion of figure \ref{['fig: mutex-prog']}. Each vertex is labeled by a state of $RS$, each edge is labeled by a transition of $T$. We can observe that $q(\texttt{S}) < 2$ for all reachable state: the semaphore is accomplishing its mission in preventing the execution of semp twice in a row.
  • ...and 13 more figures

Theorems & Definitions (50)

  • Definition 1
  • Definition 2
  • Definition 3
  • Definition 4
  • Definition 5
  • Definition 6
  • Definition 7
  • Definition 8
  • Definition 9
  • Definition 10
  • ...and 40 more