Modal algebra and Petri nets

Abstract

We use the by now well established setting of modal semirings to derive a modal algebra for Petri nets. It is based on a relation-algebraic calculus for separation logic that enables calculations of properties in a pointfree fashion and at an abstract level. Basically, we start from an earlier logical approach to Petri nets that in particular uses modal box and diamond operators for stating properties about the state space of such a net. We provide relational translations of the logical formulas which further allow the characterisation of general behaviour of transitions in an algebraic fashion. From the relational structure an algebra for frequently used properties of Petri nets is derived. In particular, we give connections to typical used assertion classes of separation logic. Moreover, we demonstrate applicability of the algebraic approach by calculations concerning a standard example of a mutex net.

1 Introduction

The formalism of Petri nets has been a major research topic for many decades and has a large variety of applications. As a particular case of such nets there are so-called Signal Transition Graphs to which Walter Vogler has contributed a multitude of papers (e.g. [24, 42]). In earlier papers he has been involved with questions of equivalence and refinement of Petri nets (e.g. [18, 41]). The present paper constructs an algebraic framework for some of the basic aspects of Petri nets, such as transitions, markings, reachability and fairness. It is based on the by now well established theory of modal semirings [12, 13] as well as on earlier logical approaches to Petri nets [15, 35, 36], where, in particular, connections to separation logic [38] have been introduced. Separation logic was originally introduced to facilitate reasoning about data structures involving pointers in a Hoare logic style. In [35, 36] the logical approach to Petri nets developed in [15] is reconsidered and extended with modal operators used to state properties about reachable markings within such nets.

The goal of the present work is to develop from that approach a general modal algebraic structure that allows abstract reasoning about reachability within Petri nets. As a starting point, we use a general relational approach to separation logic developed in [9, 10].

The paper is structured as follows. In Sect. 2 we define Petri nets. In Sect. 3 we present a logic for them that allows reasoning with modal formulas about reachability of markings. In Sect. 4 we introduce the basics of separation algebras and a relational semantics for commands over them. In Sect. 5 we specialise that semantics to Petri nets viewed as a separation algebra and extend it to the logic of Sect. 2. In Sect. 6 this is abstracted to give a Petri net algebra based on well-known algebraic concepts. In Sect. 7 we enrich that algebra by the notions of tests and modal operators. Moreover, we provide useful consequences of the algebraic laws that, in particular, allow pointfree proofs of frequently used inference rules in Petri net logic. In Sect. 8 we state properties of nets in an algebraic fashion. In Sect. 9 and Sect. 10 we show how to express safety, fairness and liveness algebraically and illustrate this with concrete calculations for a mutex net. Finally, we discuss some related work in Sect. 11 and conclude with a summary and an outlook on future work in Sect. 12.

2 Petri nets

We repeat the basic notions of Petri nets as given in [15].

Definition 2.1

• A Petri net  is a structure $\mathcal {N} = (P,T, {\textit{pre}}(\_),{\textit{post}}(\_))$. The set $P$ consists of places  and is disjoint from the set $T$ of transitions .

• A marking  is a function $M: P \rightarrow \mathbb {N}$, i.e., a mapping from places to natural numbers, assigning a number of tokens  to each place. The set of all markings is denoted by $\mathcal {M}$.

• pre(_) and post(_) are functions of type $T \rightarrow \mathcal {M}$. For a transition $t$, the marking ${\textit{pre}}(t)$ represents the number of tokens on each place required to enable firing  $t$, while ${\textit{post}}(t)$ denotes the number of tokens that $t$ emits to each place once it fires.

• The addition of markings $M,N$ is given by $(M + N)(p) \,=_{ df}\,M(p) + N(p)$ for any place $p$, and $[]$ denotes the empty marking, i.e., $[](p) = 0$ for any $p \in P$. Moreover, for a place $p \in P$ we define the singleton marking  $M_{p}$ with $M_{p}(p) = 1$ and $M_{p}(q) = 0$ for all other places $q \ne p$.

• The order $\preceq$ on $\mathcal {M}$ is the pointwise extension of $\le$ on $\mathbb {N}$, i.e., $M \preceq N \,\Leftrightarrow _{ df}\,\forall \, p \in P : M(p) \le N(p)$.

Definition 2.2

The behaviour of transitions $t$ described above can be formalised by the following firing  relation $[t\rangle$ between markings:

$$\begin{aligned} M [t\rangle N \,\Leftrightarrow _{ df}\,\exists \, M' \in \mathcal {M}: \ M = {\textit{pre}}(t) + M' \,\wedge \,N = {\textit{post}}(t) + M'. \end{aligned}$$

(1)

This induces the one-step reachability  relation given by

$$\begin{aligned} M \leadsto N \,\Leftrightarrow _{ df}\,\exists \, t \in T: \ M [t\rangle N. \end{aligned}$$

Finally, we call $N$ reachable  from $M$ if $M \leadsto ^* N$, where $\leadsto ^*$ is the reflexive and transitive closure of $\leadsto$.

As a standard example, consider the net depicted in Fig. 1. It illustrates two processes ${ Pro}\,_1$ and ${ Pro}\,_2$ that are synchronised by a semaphore represented by the place $s$ (cf. [25]). Both processes are separated graphically from each other by the semaphore, i.e., ${ Pro}\,_1$ denotes the left subnet and ${ Pro}\,_2$ the right one. The components of the whole net are given by $P = \{p_1,p_2,c_1,c_2,i_1,i_2,s\}$ and $T = \{t_i \,|\,i \in \{1, \dots ,6\} \}$ where

• $p_i$ denotes a state where ${ Pro}\,_i$ is pending, i.e., ${ Pro}\,_i$ is waiting for the semaphore to be available for entering its critical section;

• $i_i$ corresponds to an idle state where ${ Pro}\,_i$ does nothing;

• $c_i$ represents the critical section of each process.

The semaphore $s$ works in the following way: The transitions $t_2$ or $t_5$ can only fire if a token is available on $s$ and process $i$ is in its pending state, i.e., $p_i$ is marked. By firing $t_2$ or $t_5$ a token of $s$ and $p_i$ is consumed by the respective transition and a further token is produced in $c_i$ which means that ${ Pro}\,_i$ is in its critical section. Hence, for the case of $t_2$ we have ${\textit{pre}}(t_2) = M_{p_1} + M_s$ and ${\textit{post}}(t_2) = M_{c_1}$. Analogous markings can be given for the transition $t_5$.

Fig. 1

An example of a mutex net

Then we have $({\textit{pre}}(t_2) + M_{p_1})(p_1) = 2$, $({\textit{pre}}(t_2) + M_{p_1})(s) = 1$ and $({\textit{pre}}(t_2) + M_{p_1})(p) = 0$ on the remaining places $p$. It is not difficult to see that transition $t_2$ satisfies $({\textit{pre}}(t_2) + M_{p_1}) \ [t_2\rangle \ ({\textit{post}}(t_2) + M_{p_1})$ by choosing $M' = M_{p_1}$ in Definition 2.2. In particular, by setting $M' = []$ we also have ${\textit{pre}}(t_2) \ [t_2\rangle \ {\textit{post}}(t_2)$ since $[]$ is neutral w.r.t. $+$ on markings and $({\textit{pre}}(t_2) + M_p) \ [t_2\rangle \ ({\textit{post}}(t_2) + M_p)$ for any other marking $M_p \in \mathcal {M}$. For this behaviour of transitions in Petri nets we will later provide an algebraic formalisation that reflects the described observation in a simple and abstract fashion.

3 A logic for petri nets

We continue by giving the syntax and semantics of a logic, presented in [35, 36], for characterising states, i.e., markings, and reachability conditions in Petri nets using modal operators. The purpose of the logic is to define formulas that characterise sets of markings in a given fixed Petri net. The syntax is as follows:

$$\begin{aligned} \begin{array}{rcl} A &{} {::=} &{} \pi \ \,|\ {\mathsf{false}} \ \,|\ {\mathsf{true}} \ \,|\ \lnot \, A \ \,|\ A \,\vee \,A \ \,|\ A \,\wedge \,A \ \,|\ \\ &{} &{} A * A \ \,|\ A \mathop {{-}*}A \ \,|\ I \ \,|\ \\ &{} &{} \Box _+ A \ \,|\ \Box _- A \ \,|\ \Diamond _+ A \ \,|\ \Diamond _- A. \end{array} \end{aligned}$$

The base case assertions $\pi$ are taken from a set of atomic formulas. Frequently used examples are ${\textit{pre}}(t)$ or ${\textit{post}}(t)$ that simply characterise the corresponding markings w.r.t. a transition $t$ or any $p \in P$ which logically denotes the singleton marking $M_p$.

The remaining syntactic constructs in the first row are the same as in classical logic. In the second row the assertions are built from operators that are well-known in separation logic, i.e., separating conjunction  $*$ and separating implication  $\mathop {{-}*}$.

Intuitively, the former corresponds to the sum of markings in the following sense: e.g., $p * q$ means a singleton marking of each of the places $p$ and $q$ if they are different, while by $p*p$ one would characterise that $p$ carries two tokens (separating conjunction is not idempotent). By contrast, the standard conjunction $p \,\wedge \,q$ expresses that both $p$ and $q$ are marked, regardless of whether they are the same or not. Note that $p \,\wedge \,q$ might be unsatisfiable if $p,q$ make assumptions about different places. As an example consider $p = c_1$ which asserts a marking where exactly one token on the place $c_1$ is available and nothing anywhere else. Similarly, $q = c_2$ asserts exactly one token in $c_2$ and nothing elsewhere. Hence $c_1$ and $c_2$ can not hold at the same time and therefore $c_1 \,\wedge \,c_2$ is unsatisfiable. Finally, $p * \mathsf{true}$ requires at least $p$ to be marked.

Separating implication is the upper adjoint of separating conjunction, satisfying for any assertions $P,Q,R$ the relationship

$$\begin{aligned} (P * Q) \rightarrow R \ \,\Leftrightarrow \,\ Q \rightarrow (P \mathop {{-}*}R). \end{aligned}$$

Basically, the formula $P \mathop {{-}*}R$ characterises all markings $M$ such that whenever a marking $N$ satisfying $P$ is added to $M$ then $N + M$ will satisfy $R$.

The special assertion $I$ denotes the empty marking and is the unit of $*$.

Finally, we deal with the modal operators in the third row above. As an example we again consider the net of Fig. 1. The formula $\Box _+ (s * i_1 * i_2)$ characterises all markings $M$ where every marking reachable from $M$ is always only singly-marked in the semaphore $s$ and the idle states. Symmetrically, $\Box _- (s * i_1 * i_2)$ denotes the markings $M$ where every marking leading to $M$ has to satisfy $s * i_1 * i_2$. The diamond operators are the De Morgan duals of the box ones, i.e., $\Diamond \varphi$ is equivalent to $\lnot \Box \lnot \varphi$, and hence are existential quantifiers about markings, whereas the boxes act as universal quantifiers.

In the formal semantics of the modal operators we follow the approach of [35, 36] which overcomes the drawbacks of the restrictive intuitionistic logic in [15] and yields a more flexible and expressive logic for reasoning about reachability conditions within a Petri net. Formally, a Kripke semantics for the logic is given as follows. We assume a valuation function $i$ that assigns to each atomic formula $\pi$ the set of markings for which this formula is true.

All remaining well-known connectives of classical and modal logic can be defined as follows:

$$\begin{aligned} \begin{array}{rcl@{}rcl} \lnot A &{} \,\Leftrightarrow _{ df}\,&{}A \rightarrow {\mathsf{false}}, &{} \mathsf{true} &{} \,\Leftrightarrow _{ df}\,&{} \lnot {\mathsf{false}}, \\ A \,\vee \,B &{} \,\Leftrightarrow _{ df}\,&{} \lnot A \rightarrow B, &{} A \,\wedge \,B &{} \,\Leftrightarrow _{ df}\,&{} \lnot (\lnot A \,\vee \,\lnot B), \\ \Diamond _+ A &{} \,\Leftrightarrow _{ df}\,&{} \lnot \Box _+ \lnot A, &{} \Diamond _- A &{} \,\Leftrightarrow _{ df}\,&{} \lnot \Box _- \lnot A. \end{array} \end{aligned}$$

4 Separation algebras and commands

In Definition 2.2 we have seen that every transition $t$ induces a relation $[t\rangle$ between markings which then was lifted to the relation $\leadsto$. This is the motivation for tying in Petri nets and their logic with the well established area of relational program semantics. We use the general relational approach of [7, 10] which also comprises the above-mentioned $*$ operator of separation logic (SL). It is built using the concept of separation algebras [4] that provides a general way to characterise the structure and properties of abstract resources.

In Petri nets the resources are the markings. The firing rule involves splitting (or separating ) the token supply on a place, which is why separation logic is relevant to the area of Petri nets. The converse combination  operator is the sum of markings. An algebraic abstraction of this is the following notion.

Definition 4.1

• 1. A partial monoid  is a structure $(\varSigma , \mathop {{\bullet }}, u)$ with a set $\varSigma$ of states  (e.g., markings of Petri net places), a partial combination operator $\mathop {{\bullet }}: \varSigma \times \varSigma \,\rightarrow \,\varSigma$ and an element $e \in \varSigma$ such that the following properties hold:

  • $e$ is the neutral element w.r.t. $\mathop {{\bullet }}$, i.e., for all $\sigma \in \varSigma$ we have $e \mathop {{\bullet }}\sigma = \sigma =\sigma \mathop {{\bullet }}e$.

  • $\mathop {{\bullet }}$ is associative, i.e., for all $\rho ,\sigma ,\tau \in \varSigma$ we have $(\rho \mathop {{\bullet }}\sigma ) \mathop {{\bullet }}\tau =\rho \mathop {{\bullet }}(\sigma \mathop {{\bullet }}\tau )$.

  Here an equation $t_1 = t_2$ between terms $t_1,t_2$ means that both terms are defined and equal or both terms are undefined.

• 2. A partial monoid is cancellative  if $\sigma _1 \mathop {{\bullet }}\tau = \sigma _2 \mathop {{\bullet }}\tau \,\Rightarrow \,\sigma _1 = \sigma _2$ for all $\sigma _1, \sigma _2, \tau \in \varSigma$.

• 3. A separation algebra  is a partial monoid in which $\mathop {{\bullet }}$ is commutative and cancellative. It induces a combinability  relation $\#$ defined by

  $$\begin{aligned} \sigma _0 \,\#\, \sigma _1 \, \,\Leftrightarrow _{ df}\,\, \sigma _0 \mathop {{\bullet }}\sigma _1 \hbox { is defined}. \end{aligned}$$

  In the following, when writing $\sigma \mathop {{\bullet }}\tau$ for states $\sigma ,\tau$ we will implicitly assume $\sigma \, \#\, \tau$.

For a given Petri net the structure $(\mathcal {M},+,[])$ forms a separation algebra in which the combination operator $\mathop {{\bullet }}$ is total, i.e, $M \#M'$ holds for all states $M,M' \in \mathcal {M}$. Splitting and combining markings was already part of the semantic definition of the separating conjunction operator $*$ in Sect. 3. The absence of a proper combinability relation means that there exist no bounds on the capacity of the places, i.e., we are considering unbounded Petri nets.

The operator $\mathop {{\bullet }}$ is the basis for defining the central connective separating conjunction  of SL, see below. It allows splitting a resource, e.g., a program state, into disjoint parts about which one can assert separate properties conjunctively. In the case where states are markings, $\mathop {{\bullet }}$ is just pointwise sum, which is even a total operator.

Definition 4.2

Assume a separation algebra $(\varSigma , \mathop {{\bullet }}, u)$. A command  is a relation $R \subseteq \varSigma \times \varSigma$. Relational composition of commands is denoted by $\mathbin {;}$. Its unit ${\mathsf{skip}}\,=_{ df}\,\{(\sigma ,\sigma ) \,|\,\sigma \in \varSigma \}$ is the identity relation, while the universal relation is denoted by $\top$. A test  is a command $p$ with $p \subseteq {\mathsf{skip}}$, i.e., $p = \{(\sigma ,\sigma ) \,|\,\sigma \in S\}$ for some $S \subseteq \varSigma$. Hence tests are in one-to-one correspondence with subsets of $\varSigma$ and will be used as an algebraic representation of such subsets. We denote tests by $p,q,r,\ldots$ in the sequel. The relative complement of a test $p$ w.r.t. ${\mathsf{skip}}$ is denoted by $\lnot p$. As particular tests we define ${\mathsf{emp}}\,=_{ df}\,\{(u,u)\}$ that characterises the empty state $u$, that represents the domain of a command $R$ and dually that denotes the codomain of $R$, defined analogously. The former is characterised by the universal property

(2)

for all tests $q$. In particular, and hence . Moreover, we have and for relations $R,S$ we have . A characterisation for codomain can be given symmetrically.

Note that tests form a Boolean algebra with ${\mathsf{skip}}$ as its greatest and $\emptyset$ as its least element w.r.t. $\,\subseteq \,$. Moreover, on tests $\,\cup \,$ coincides with join and $;$ with meet. In particular, tests are idempotent and commute under composition, i.e., $p \mathbin {;}p \,=\,p$ and $p \mathbin {;}q \,=\,q \mathbin {;}p$.

Using domain and codomain we can define forward and backward modal diamond and box operators. They are given for a command $R$ and test $q$ as follows:

(3)

Hence $| R\rangle q$ characterises those states for which there exists an execution of $R$ that ends in a state in (the subset represented by) $q$ while $|R]q$ characterises those states for which all executions of $R$ will end in a state in $q$. The dual statements hold for the backward modal operators.

Next we introduce a relational operator $*$ on commands that corresponds to the separating conjunction of SL. It connects the actions of two commands by “running” them on separate portions of the overall program state; this is indeed expressed by a logical conjunction. Formally,

$$\begin{aligned} \begin{array}{rll} \sigma \ (R * S) \ \tau \,\Leftrightarrow _{ df}\,&{} \exists \, \sigma _1, \sigma _2, \tau _1, \tau _2 : \, &{} \sigma = \sigma _1 \mathop {{\bullet }}\sigma _2 \,\wedge \,\tau = \tau _1 \mathop {{\bullet }}\tau _2 \,\wedge \,\sigma _1 \#\sigma _2 \,\wedge \,\tau _1 \#\tau _2 \,\wedge \,\,\\ &{} &{} \sigma _1 \ R \ \tau _1 \,\wedge \,\sigma _2 \ S \ \tau _2. \end{array} \end{aligned}$$

Hence, separated composition of commands can be interpreted as their parallel execution on combinable portions of states [9, 10], i.e., $\sigma \,(R*S)\,\tau$ iff $\sigma$ can be split into states $\sigma _1, \sigma _2$ on which $R$ and $S$ can act and produce results $\tau _1,\tau _2$ that are again combinable to $\tau = \tau _1 \mathop {{\bullet }}\tau _2$. Another interpretation of $R * S$ is that it provides a possibility to characterise the structure of commands, i.e., their behaviour on parts of a state. We will later give a characterisation of a general behaviour of transitions in Petri nets.

Note that for tests $p,q$ the command $p * q$ is also a test and, in particular,

$$\begin{aligned} {\mathsf{skip}}* {\mathsf{skip}}= {\mathsf{skip}}. \end{aligned}$$

(4)

Additionally, $*$ is associative and commutative and has ${\mathsf{emp}}$ as its unit. Moreover, it distributes through arbitrary unions from both sides.

5 A command semantics for petri nets

Using the definitions for Petri nets of the previous sections we can now give a denotational model for such nets based on the relational structure from Sect. 5. Later on we will abstract from the concrete relational setting to a modal Kleene algebraic approach.

Definition 5.1

Given a fixed Petri net, a net command  is a relation $R\subseteq \mathcal {M} \times \mathcal {M}$, considering markings as states. The set of all net commands is denoted by $\mathcal {C}$. We assign to each formula $A$ the test command

$$\begin{aligned}{}[\![A]\!] \,=_{ df}\,\{ (M,M) \,|\,M \,\models \,A \}, \end{aligned}$$

where validity $\,\models \,$ is as in the Kripke semantics of Sect. 3.

As is well known, by this the logical operators $\,\vee \,$ and $\,\wedge \,$ correspond to $\,\cup \,$ and $\,\cap \,$, respectively. Moreover, since $M_1 \#M_2 \,\Leftrightarrow \,\mathsf{true}$, we have

$$\begin{aligned} \begin{array}{rcl} [\![A * B]\!] &{} = &{} \{ (M_1 + M_2, M_1 + M_2) \,|\,M_1 \,\models \,A, M_2 \,\models \,B \} \\ &{} = &{} \{ (M_1 + M_2, M_1 + M_2) \,|\,M_1 \in [\![A]\!], M_2 \in [\![B]\!] \} \\ &{} = &{} \{ (M_1 + M_2, M_1 + M_2) \,|\,M_1 \in [\![A]\!], M_2 \in [\![B]\!], M_1 \#M_2 \} \\ &{} = &{} [\![A]\!] * [\![B]\!]. \end{array} \end{aligned}$$

A direct consequence of the definition of $*$ is that the reverse exchange law [10], which provides an interplay of relation composition $\mathbin {;}$ and separating conjunction $*$, holds unconditionally in the relational setting of this section. The law reads for any net commands $R_1,R_2,S_1,S_2$ over a separation algebra with a total combination operator as follows:

$$\begin{aligned} (R_1 \mathbin {;}R_2) * (S_1 \mathbin {;}S_2) \,\subseteq \,(R_1 * S_1) \mathbin {;}(R_2 * S_2). \end{aligned}$$

(5)

By interpreting the operator $\mathbin {;}$ as sequential composition and $*$ as interference-free concurrent composition of transitions in Petri nets, one sees that the parallel execution of the sequentially composed transitions $R_1 \mathbin {;}R_2$ and $S_1 \mathbin {;}S_2$ can be reordered to the sequential execution of the parallely composed transitions $R_1 * S_1$ and $R_2 * S_2$. Moreover, in the case of an underlying total separation algebra, the domain and codomain operators distribute over $*$, i.e, we have for relations $R,S$

(6)

Proofs of (5) and (6) can be found in [10]. We mention that in general only the $\,\subseteq \,$- directions hold for arbitrary separation algebras. An example of a partial separation algebra that does not satisfy the above (in)equations for any relations is given by safe  Petri nets $\mathcal {N}$ which satisfy for all $M \in \mathcal {M}$ and $p \in P$ the inequation $M(p) \le 1$ (cf. [4]). In that separation algebra we have $M \#M' \,\Leftrightarrow \,\forall \, p \in P:\, (M+ M')(p) \le 1$. In this work we mainly consider unbounded Petri nets; bounded ones can be handled by imposing a corresponding safety condition. This will be shown in an example later.

Finally, we immediately infer that the modal $\Box _+$ operator can be interpreted as a forward box operator $|\_]$ (cf. Eq. (3)) in the relational structure using the defined abstractions:

where $|\leadsto ^*]$ is the forward box operator associated with the transition relation $\leadsto ^*$.

Clearly, by analogous calculations we immediately get

$$\begin{aligned}{}[\![\Box _- A]\!] = [\leadsto ^*\!\!|{[\![A]\!]}, [\![\Diamond _+ A]\!] = | \!\leadsto ^*\rangle {[\![A]\!]}, \hbox {and} [\![\Diamond _- A]\!] = \langle \leadsto ^*\!\! |{[\![A]\!]}. \end{aligned}$$

Now we turn to a pointfree treatment of transitions.

Definition 5.2

For a transition $t$ we define the semantics $[\![\,t\,]\!]$ to be the one-step reachability relation $[t\rangle$ considered as a net command, i.e.,

$$\begin{aligned}{}[\![\,t\,]\!] \,=_{ df}\,\{ (M,N) \,|\,M [t\rangle N \} = [t\rangle . \end{aligned}$$

As mentioned in Sect. 2 after Fig. 1, the transitions come with a special behaviour.

Definition 5.3

A net command $R$ is local  [10] if it satisfies $R * {\mathsf{skip}}= R$.

Intuitively, this characterises the ability of $R$ to perform its task with a possibly smaller substate of the overall state.

Theorem 5.4

For every transition $t$ the relational abstraction $[\![\,t\,]\!]$ is local.

Applying the above intuitive explanation of local commands, we obtain that if $t$ can fire on some marking $M$ then it will also be able to fire on any larger marking $N \succeq M$. Conversely, any execution of an enabled transition $t$ starting from a marking $N$ can be tracked back to a possibly smaller marking $M \preceq N$.

Proof

First, we show the $(\,\supseteq \,)$ part of the locality equation. By neutrality of ${\mathsf{emp}}$ and isotony,

$$\begin{aligned}{}[\![\,t\,]\!] = [\![\,t\,]\!] * {\mathsf{emp}}\,\subseteq \,[\![\,t\,]\!] * {\mathsf{skip}}. \end{aligned}$$

For the converse $(\,\subseteq \,)$ we calculate

$\square$

We will show later in a more abstract setting that locality of a net command lifts to its reflexive and transitive closure.

6 Applying algebra to petri nets

In this section we abstract the net command semantics algebraically to elements of special algebraic structures known as a quantales; these, in turn are special cases of idempotent semirings.

Definition 6.1

 

• 1. An idempotent semiring  is a structure $(A,+,0,\cdot ,1)$ such that $(A,+,0)$ is a commutative monoid with idempotent addition, that is, $a+a = a$ for all $a \in A$, $(A,\cdot ,1)$ is a monoid, multiplication distributes over addition, that is, for all $a,b,c\in A$,

  $$\begin{aligned} a \cdot (b+c) = a \cdot b + a \cdot c \quad \text {and} \quad (a+b) \cdot c = a \cdot c + b \cdot c , \end{aligned}$$

  and $0$ is a left and right annihilator for multiplication, that is, for all $a\in A$,

  $$\begin{aligned} a \cdot 0 = 0 = 0 \cdot a. \end{aligned}$$

• 2. Every idempotent semiring is partially ordered by

  $$\begin{aligned} a \le b \,\Leftrightarrow _{ df}\,a+b = b. \end{aligned}$$

  Then $+$ and $\cdot$ are isotone w.r.t. $\le$ and $0$ is the least element. Moreover, $a+b$ is the supremum of $a,b \in A$.

• 3. A semiring is Boolean  if it has a complement operator and satisfies Huntington’s axiom:

  

  In this case one defines the meet operator as

  

• 4. A Kleene algebra  is a structure $(A,+,\cdot ,{}^*,0,1)$ such that $(A,+,\cdot ,0,1)$ is an idempotent semiring and the star operator ${}^*$ satisfies the unfold and induction laws

  $$\begin{aligned} 1 + a \cdot a^*&\le a^*,&\quad \quad \quad \quad \quad 1+a^*\cdot a&\le a^*,\end{aligned}$$

  (7)
  $$\begin{aligned} c + a \cdot b \le b&\,\Rightarrow \,a^* \cdot c \le b,&\quad \quad \quad c + b \cdot a \le b&\,\Rightarrow \,c \cdot a^* \le b. \end{aligned}$$

  (8)

  The star here should not be confused with the separation operator $*$ above.

• 5. An idempotent semiring $(A,+,0,\cdot ,1)$ is called a quantale  [34, 39] or standard Kleene algebra  [5] if $\le$ induces a complete lattice on $A$ and multiplication distributes over arbitrary suprema. The infimum and the supremum of a subset $B \subseteq A$ are denoted by $\sqcap B$ and $\bigsqcup B$, respectively. Their binary variants are and (the latter coinciding with $a+b$). Every quantale can be made into a Kleene algebra by defining $a^* \,=_{ df}\,\mu x.\, 1 + a \cdot x$, where $\mu$ is the least fixed point operator.

• 6. A bi-semiring  is a structure $(A,+,0,\cdot ,1,*,u)$ such that both $(A,+,0,\cdot ,1)$ and $(A,+,0,*,u)$ are idempotent semirings with commutative $*$. Note that $u$ here is the abstraction of the command ${\mathsf{emp}}$ and not the neutral element of a separation algebra as in Definition 4.1.

• 7. A concurrent net semiring  is a bi-semiring in which the operators are connected by the following additional axioms:

  $$\begin{aligned} 1*1&\le 1, \end{aligned}$$

  (9)
  $$\begin{aligned} (a \cdot b) * (c \cdot d)&\le (a * c) \cdot (b * d). \end{aligned}$$

  (r-exchange)

  The second of these is the generalised form of the reverse exchange law (cf. Eq. 5). The first one was stated in equational form in (4); in fact the direction $\ge$ follows from the reverse exchange axiom.

• 8. A concurrent net quantale  is a concurrent net semiring in which both component semirings are quantales.

In a concurrent net quantale one could also define an iteration operator w.r.t. to the $*$ composition operator, but we will not need that here.

Our concurrent net semirings/quantales are quite similar to the concurrent semirings/Kleene algebras of [19, 20]. The main difference is that our exchange axiom is order-reverse to the one in those structures, which reflects a bias towards relation-like models.

Commands provide a model in the following way.

Theorem 6.2

The structure forms a Boolean concurrent net quantale.

Proof

The quantale property of is well known (e.g. [40]). The semiring property of has been shown in [10]. Since there $*$ is defined in terms of $\mathbin {;}$ as

$$\begin{aligned} R*S = \mathbin {{\large \lhd }}\mathbin {;}(R \times S) \mathbin {;}\mathbin {{\large \rhd }}, \end{aligned}$$

$\mathbin {{\large \lhd }}$ and $\mathbin {{\large \rhd }}$ are constant relations and $\mathbin {;}$ and $\times$ distribute over arbitrary unions, the quantale property of also holds. The remaining axioms of concurrent net semirings were again shown in [10], as mentioned in Sect. 2. $\square$

Lemma 6.3

In every concurrent net semiring the following inequations hold.

• 1. $u \le 1$.

• 2. $a \le a * 1$.

Proof

 

• 1. By neutrality of $u$ w.r.t. $*$, neutrality of $1$ w.r.t. $\cdot$, reverse exchange and neutrality of $u$ w.r.t. $*$ again,

  $$\begin{aligned} u = u*u = (u \cdot 1) * (1 \cdot u) \le (u*1) \cdot (1*u) = 1 \cdot 1 = 1. \end{aligned}$$

• 2. By neutrality of $u$ w.r.t. $*$, Part 1 and isotony,

  $$\begin{aligned} a = a * u \le a * 1. \end{aligned}$$

$\square$

We distinguish some special properties.

Definition 6.4

An element $a$ of a concurrent net semiring is called

$$\begin{aligned} \begin{array}{ll} {\textit{reflexive}}&\quad \quad \qquad \qquad \qquad \hbox {if } 1 \le a, \end{array} \end{aligned}$$

(reflexivity)

$$\begin{aligned} \begin{array}{ll} {\textit{transitive}}&\qquad \qquad \qquad \qquad \hbox {if } a \cdot a \le a, \end{array} \end{aligned}$$

(transitivity)

$$\begin{aligned} \begin{array}{ll} {\textit{local}}&\quad \qquad \qquad \qquad \qquad \qquad \hbox {if } a * 1 \le a. \end{array} \end{aligned}$$

(locality)

Since the semiring elements are abstractions of relations, we call a reflexive and transitive element a preorder.  A preorder with locality is called a transition element .

By our axioms, $1$ is a transition element.

Lemma 6.5

For a local element $a$ and arbitrary elements $b,c$ the reverse small exchange laws hold:

• 1. $b * (c \cdot a) \le (b * c) \cdot a$,

• 2. $b * (a \cdot c) \le a \cdot (b * c)$.

Proof

We only give a proof of the first result since the second can be proved analogously. Using neutrality of $1$, the reverse exchange law and locality of $a$, we calculate:

$$\begin{aligned} b * (c \cdot a) = (b \cdot 1) * (c \cdot a) \le (b * c) \cdot (1 * a) = (b * c) \cdot a. \end{aligned}$$

$\square$

As a first application of our algebraic structures we deal with the behaviour of local elements under iteration.

Lemma 6.6

If an element $a$ of a concurrent net quantale is local then so is $a^*$.

Proof

We use the principle of least-fixed-point sub-fusion (e.g. [1]): Let $f,g,h : L \,\rightarrow \,L$ be isotone functions on a complete lattice $(L,\le )$ with least element $0$. Suppose that $g$ is continuous, i.e., preserves suprema of non-empty chains, and assume $g(0) \le \mu h$. Then

$$\begin{aligned} g \circ h \le f \circ g \,\Rightarrow \,g(\mu h) \le \mu f. \end{aligned}$$

(10)

This allows fusing the application of $g$ into the recursion described by $h$.

To prove our claim we need to show $a^* * 1 \le a^*$. We set $f(x) = h(x) = 1 + a \cdot x$ and $g(x) = x * 1$. Then $\mu f = \mu h = a^*$ and our claim is shown if the premises of least-fixed-point sub-fusion are satisfied. By the global assumption $g$ is continuous. Moreover, $g(0) = 0 \le \mu h$. So it remains to check $g \circ h \le f \circ g$. We calculate:

$\square$

Apart from this, the iteration operator of Kleene algebra is used in calculating the transition elements corresponding to concrete nets. However, we will have no need to refer to it in our further proofs, since they all just deploy reflexivity, transitivity and sometimes locality.

7 Tests and modal semirings

Next we introduce some further algebraic concepts that abstract tests and the domain/codomain operators and as presented in Definition 4.2 and give some useful consequences.

Definition 7.1

A test  [26, 28] in an idempotent semiring $A$ is an element $p \le 1$ that has a complement relative to $1$, i.e., an element $\lnot p$ that satisfies $p + \lnot p = 1$ and $p \cdot \lnot p = 0 = \lnot p \cdot p$. The set of tests of $A$ is denoted by . Test implication is defined by $p \rightarrow q \,=_{ df}\,\lnot p + q$.

It is not hard to show that forms a Boolean subalgebra in which $+$ coincides with the binary supremum and $\cdot$ with the binary infimum . We always have , with $0$ corresponding to the predicate and $1$ to $\mathsf{true}$. In a Boolean semiring, every element $p \le 1$ is a test with relative complement (e.g. [13]).

Definition 7.2

• A modal semiring  is a structure where $(A,+,0,\cdot ,1)$ is an idempotent semiring and the operators satisfy the following axioms for arbitrary element $a$ and test $p$:

  

• A modal concurrent net semiring  is a structure in which is a modal semiring such that the $*$-distributivity laws for domain and codomain (cf. Eq. 6) hold:

  

  (11)

  Since, by the above axioms, (r-exchange) and the above axioms again,

  

  and symmetrically for , these inequations strengthen to equalities by antisymmetry of $\le$.

• A modal concurrent net quantale  is a modal concurrent net semiring  that forms a concurrent net quantale.

• In any of the above modal structures forward and backward diamond and box operators can be defined as in Eq. (3):

  

Forward diamond $| a\rangle$ and backward diamond $| a\rangle$ respectively correspond to the preimage and image operators as discussed after (3) for binary relations. The notation is a combination of standard modal notation and transition relation notation: if one writes $\mathop {\mapsto }\limits ^{a} q$ for the set of all predecessors of $q$-states under transition relation $a$ and omits the horizontal line so that $a$ “drops to the bottom” one obtains $| a\rangle q$. Symmetrically $p \mathop {\mapsto }\limits ^{a}$ denotes the set of all successors of $p$-states under $a$; to make the modal operators compose more easily we flip sides and write $\langle a |q$. The result $|a]p$ of applying the forward box $|a]$ to a test $p$ is another test that represents the set of all states from which every transition under $a$ leads inevitably into the subset represented by the test $p$. An analogous interpretation can be given for the backward box. When the direction of the operators does not matter we will write and for them.

By Theorem 6.2 and the results mentioned in Sect. 2 we have the following result.

Theorem 7.3

The structure forms a modal Boolean concurrent net quantale.

The modal operators satisfy a rich set of laws; for proofs see [13, 30, 32, 33].

First, De Morgan duality gives the swapping rules 

$$\begin{aligned} | a\rangle p \le |b]q \,\Leftrightarrow \,| b\rangle \lnot q \le |a]\lnot p, \langle a |p \le [b|q \,\Leftrightarrow \,\langle b |\lnot q \le [a|\lnot p. \end{aligned}$$

(12)

They correspond to the Schröder rules of relation algebra.

Strictness of $\cdot$ w.r.t. $0$ and De Morgan yield what is known as axiom (M) of modal logic:

By distributivity, the modalities are homomorphic w.r.t. $+$ :

(13)

Hence box is antitone and diamond is isotone in the first argument:

(14)

Moreover, both box and diamond are isotone in their second arguments:

(15)

Isotony entails interactions of the operators with subtraction and implication, since every additive endofunction $f$ and every multiplicative endofunction $g$ on a Boolean algebra satisfy, for all elements $p$ and $q$,

$$\begin{aligned} f(p)-f(q) \le f(p-q), \qquad g(p \rightarrow q) \le g(p) \rightarrow g(q). \end{aligned}$$

(16)

Instantiating $g$ with the box operators we obtain the normality  laws, also known as axiom (K) of modal logic:

For tests $p$ the forward and backward modalities behave as follows:

(17)

Hence, is the identity function on tests. Moreover, and .

Moreover, the modal operators are homomorphic w.r.t. $\cdot$ as well:

(18)

We have the exchange laws

$$\begin{aligned} p \le |a]q \,\Leftrightarrow \,\langle a |p \le q, p \le [a|q \,\Leftrightarrow \,| a\rangle p \le q, \end{aligned}$$

(19)

which establish Galois connections between diamonds and boxes.

The Galois connections have interesting consequences. In particular, diamonds (boxes) commute with all existing suprema (infima) of the test algebra.

The modal structures allow abstract and pointfree proofs of a large set of inference rules of the logical approach to Petri nets given in [35, 36]. Moreover, they avoid tedious inductions over transition sequences, which is a gain for manual proving as well as for partially automated proof support.

We start with a proof rule stating an interplay between the diamond operator and separating conjunction, i.e.,

Note that this law holds for both past and future diamond operators $\Diamond _{-}$ and $\Diamond _{+}$. Intuitively, in the case of $\Diamond _+$ this rule states that if there is a reachable marking $M$ for which one part satisfies $A$ and a further distinct part that ensures that $B$ is reachable, then one can also reach from $M$ a marking for which $A$ and $B$ hold on distinct parts. The entailment operator $\vdash$ can be interpreted as the partial order $\le$ of a quantale or, in the case of the concrete relational structure, by the subset inclusion order.

In the abstract setting of a modal concurrent net quantale the above rule can be translated, for a transitive and local element $a$ and tests $p,q$, into

(20)

We only give a proof for the backward diamond, since the forward case is analogous.

As evidence of adequacy of our algebraic semantics we provide some further validity proofs of the inference rules given in [35, 36]. Since they do not mention the $*$ operator, they do not need a concurrent net semiring; a modal semiring is sufficient. Therefore these rules and their proofs apply to a much wider class of structures and temporal logics such as $\mathsf{LTL}$, $\mathsf{CTL}/\mathsf{CTL}^*$ (cf. [14]) or $\mathsf{STL}$ [27]. It has been shown in [31] how to give quantale semantics for some of these logics.

Lemma 7.4

The following proof rules are valid, where $\vdash A$ is short for $\mathsf{true} \vdash A$:

Proof

For the proof it is sufficient to assume that the underlying element $a$ is a preorder, i.e., reflexive and transitive; locality is not needed.

$\mathrm{(R1)}$ translates for test $p$ to $1 \le \lnot \lnot p \,\Rightarrow \,1 \le p$ which is clear, since tests form a Boolean algebra.

For $\mathrm{(R2)}-\mathrm{(R6)}$ we give all calculations in terms of $|\_]$ and $| \_\rangle$, since the proofs for $[\_|$ and $\langle \_ |$ are analogous.

For $\mathrm{(R2)}$ we calculate by reflexivity of $a$, anti-disjunctivity of $|\_]$ in its first argument and isotony $|a]p = |1 + a]p = |1]p \cdot |a]p = p \cdot |a]p \le p$.

Rule $\mathrm{(R3)}$ translates into $1 \le p \,\Rightarrow \,1 \le |a]p$. For this we have $1 = |a]1 \le |a]p$ by (M), isotony and the assumption.

$\mathrm{(R4)}$ means $|a]p \le |a \cdot a]p$, which holds by transitivity of $a$ and antitony of $|\_]$ in its first argument, while $\mathrm{(R5)}$ and $\mathrm{(R6)}$ follow from the exchange laws in (19). $\square$

We conclude with an exchange property between diamond and separating conjunction.

Lemma 7.5

For all elements $a,b$ and tests $p,q$ we have .

Proof

We show the property for the forward diamond; for the backward one it is symmetric.

$\square$

8 Further properties and characterisations

As further ingredients for the algebraic setting we continue with some pointfree characterisations that describe special classes of assertions in separation logic. Since they have been given in abstract algebraic terms in [7], they can easily be interpreted also in the particular application of the present paper. We start with so-called intuitionistic  assertions which are closely related to assertions used in the early paper [15]. These authors additionally assumed a downward closure condition w.r.t. reachability on markings, i.e., for assertions $A$ and markings $M,N$:

$$\begin{aligned} (N \vdash A \,\wedge \,M \leadsto ^* N) \,\Rightarrow \,M \vdash A. \end{aligned}$$

This restriction was replaced in [35, 36] by the use of modal operators, which makes formulas more expressive than using just standard intuitionistic logic. In the algebraic setting such a closure condition could be stated as $| a\rangle p \le p$.

In separation logic, local tests play an important role; for historical reasons they are called intuitionistic assertions  there. Such a test $p$ shows the behaviour that if $p$ holds for some state $\sigma$ then it is also valid for any larger state $\tau \succeq \sigma$.

A concrete example w.r.t. the running mutex example in Fig. 1 can be given by the test $s * 1$ which describes markings where at least the place $s$ is marked. In the concrete case of relations the test $s * 1$ coincides with $\{ (M,M) \,|\,M(s) \ge 1, p \ne s \,\Rightarrow \,M(p) \ge 0 \}$. Hence, local tests allow an imprecise description of states in the sense that parts of the states may be arbitrary.

Next we consider another class of tests that, contrary to local tests, describe a set of marked places in a precise fashion, i.e., states in which no part can be arbitrary. An algebraic characterisation can be given as follows [4].

Definition 8.1

A test $p$ is called precise  iff for all

We formulate the property using rather than $\cdot$, since then a generalisation to infinite sets of tests is possible, see (21) below.

Obviously, the above inequation can be strengthened to an equation by isotony of and $*$. Moreover, it was shown in [7] that precise tests are closed under $*$. In the above form the property is also called determinacy , as known from relation algebras (e.g., [11]). An example of such a test is $c_1*s*c_2$ which characterises a state where exactly one token is available in the places $c_1,c_2$ and $s$, whereas the test $c_1 + s + c_2$ is not precise, since it describes states where a token is available in $c_1,c_2$ or $s$.

Since in a Boolean quantale the test algebra is complete, it is also possible to extend Definition 8.1 to distributivity over arbitrary non-empty infima, like in [4], i.e.,

$$\begin{aligned} X \ne \emptyset \,\Rightarrow \,\sqcap \{ p * q \,|\,q \in X\} \le p \cdot \sqcap X. \end{aligned}$$

(21)

We state a useful property of precise tests.

Lemma 8.2

$p$ is precise iff $p * \lnot {q} \le \lnot {(p * q)}$ for all tests $q$.

A proof can be found in [11]. This lemma gives a characterisation of preciseness using test negation. For precise tests it is therefore possible to state an interaction of separating conjunction and Boolean test negation.

Corollary 8.3

For precise test $p$ and arbitrary test $q$ we have

Proof

First, which follows from Lemma 8.2, Boolean algebra and diamond/box duality. Second, holds by Lemma 8.2 and diamond/box duality. $\square$

9 Treating safety

In the following three sections we show how safety, liveness and fairness can be dealt with in our algebraic setting. For illustration we use again the mutex example (cf. [25]).

First, as a further ingredient of our algebraic approach we introduce a characteristic inequation for the particular test $\lnot u$ that represents all non-empty markings. The Petri net model of the modal algebra satisfies the inequation

$$\begin{aligned} \lnot {u} * \lnot {u} \le \lnot {u} \end{aligned}$$

(non-emp)

which means that any composition $M + N$ of non-empty markings $M$ and $N$ is non-empty again. An immediate consequence of this is the following.

Lemma 9.1

$\lnot {u} * 1 = \lnot {u}$ and $u \le \lnot {(\lnot {u}*\lnot {u})}$.

Proof

First, by Boolean algebra, distributivity, neutrality and (non-emp) with the definition of $\le$,

$$\begin{aligned} \lnot {u} * 1 = \lnot {u} * (u + \lnot {u}) = \lnot {u} * u + \lnot {u} * \lnot {u} = \lnot {u} + \lnot u * \lnot {u} = \lnot {u}. \end{aligned}$$

The second inequation follows from (non-emp) by contraposition. $\square$

Hence, assuming (non-emp), the test $\lnot {u}$ becomes local. In particular, the empty marking $[]$ is contained in the test $\lnot {(\lnot {u}*\lnot {u})}$.

In the literature, the test $\lnot {(\lnot {e} \circ \lnot {e})}$, where $\circ$ denotes a multiplicative operator and $e$ its neutral element, has also been used for the multiplicative operator $\cdot$ in the concrete context of temporal logics [21, 31, 43], where it is called step. While it is interpreted there by progress in time, it provides a spatial resource interpretation for the application of Petri nets by choosing $*$ and $u$ for $\circ$ and $e$. Intuitively, the element $\lnot {(\lnot {u} * \lnot {u})}$ represents the set of all singleton markings $M_s$ for places $s$ together with the empty marking $[]$. The former are the atoms in the set of markings w.r.t. the submarking order $\preceq$.

Therefore we define and abstractly characterise sets of such states by tests $p$ with

$$\begin{aligned} p \le \mathsf{single\_mark}. \end{aligned}$$

If we further assume $p$ to be a precise test, it represents in an abstract fashion a state where only a single token is available in one place, which we denote again by $p$. We write $\mathcal {M}_{sp}$ for the set of such tests and further assume, for arbitrary tests $p \in \mathcal {M}_{sp}$,

$$\begin{aligned} \lnot (p * 1) * \lnot (p * 1) \le \lnot (p * 1), \end{aligned}$$

(22)

$$\begin{aligned} \mathsf{single\_mark}\le p + \lnot (p*1). \end{aligned}$$

(23)

Inequation (22) states that if the place $p$ is not marked in disjoint parts of a state then it is not marked in the whole state. Inequation (23) expresses that in any $\mathsf{single\_mark}$ state every place $p$ is either marked with a single token or unmarked.

As an application of this we can formulate a condition when a net $\mathcal {N}$ is safe , i.e., every place $p$ of the net contains at most one token. For this we assume an initial marking of a net $\mathcal {N}$ that we denote by $p_0$ and a preorder $a$ that abstracts the reflexive transitive closure of the firing relation of the net and define

By $\langle a |p_0$ we only consider markings reachable from the initial marking $p_0$. For every particular test $q \in \mathcal {M}_{sp}$, the composed test $\lnot (q *q * 1)$ in the right-hand side excludes any occurrences of two or more markings in the place $q$. Taking the infimum over all tests $q \in \mathcal {M}_{sp}$ corresponds to a universal quantification.

For an example we consider again the mutex net of Fig. 1. We use the initial marking $p_0 \,=_{ df}\,i_1*s*i_2$ shown in that figure. Now, the test representing all reachable markings is given by

$$\begin{aligned} \begin{array}{rcl} \langle a |p_0 &{} = &{} i_1*s*i_2 \,+\, p_1*s*i_2 \,+\, c_1*i_2 \,+ \, i_1*s*p_2 \\ &{} &{}+\, i_1*c_2 \,+\, p_1*s*p_2 \,+\, c_1*p_2 \,+\, p_1*c_2. \end{array} \end{aligned}$$

(24)

The states in that sum and the possible transitions between them are depicted in the reachability graph [25] of Fig. 2.

Fig. 2

The reachability graph of the mutex example

For the mutex net we have $\mathcal {M}_{sp} = \{s,i_1,p_1,c_1,i_2,p_2,c_2\}$. This yields

To show safety of the mutex net we use the supremum property of $+$, viz., $p + q \le r \,\Leftrightarrow \,p \le r \,\wedge \,q \le r$ and the dual one for infima , viz., for arbitrary tests $p,q,r$. Using this we can individually show that each part of the sum in Eq. (24) needs to be included in all parts of the meet. We exemplify a part of the calculation showing $i_1*s*i_2 \le \lnot (s*s*1)$ :

Now, $i_1*i_2 \le \lnot (s*1)$, since from Eq. (23) with $p=s$, we can infer by distributivity, Boolean algebra and isotony that . Moreover, $i_1,i_2 \le \lnot s$ and $i_1,i_2 \le \mathsf{single\_mark}$ imply $i_1,i_2 \le \lnot (s *1)$. Hence, by Eq. (22) and isotony we have $i_1*i_2 \le \lnot (s*1) * \lnot (s*1) \le \lnot (s*1)$. Therefore, which is equivalent to $i_1*s*i_2 \le \lnot (s*s*1)$ by contraposition.

As a further frequently used property of Petri nets we can extend the formulation for safeness to an arbitrary bound $k$ on the places of a net:

Here $q^{k+1} = \underbrace{q * \dots * q}_{k+1}$, i.e., a $(k+1)$-fold iteration of separating conjunction, and hence $q^{k+1}*1$ is the set of all markings where $q$ carries at least $k+1$ tokens.

For a further proof of correct behaviour in the mutex net (cf. [25]) consider Fig. 3. The process ${ Pro}\,_1$ enters its critical section by firing transition $t_2$. Note that ${ Pro}\,_2$ cannot enter its critical section even when $p_2$ is marked, since there is no token available on $s$. When ${ Pro}\,_1$ leaves its critical section, transition $t_3$ fires and leaves tokens in the places $i_1$ and $s$. Note that the whole scenario can symmetrically be applied to ${ Pro}\,_2$. In any such state either $c_1$, $c_2$ or $s$ is marked, i.e., we cannot reach a state where more than two of these places are marked. This can also be seen in the reachability graph of Fig. 2. This behaviour represents an invariant of the net and is required to guarantee that both processes do not enter their critical sections at the same time. Formally, a test $p$ is an invariant  of an element $a$ if $p \le |a]p$.

Fig. 3

The process ${ Pro}\,_1$ is its pending state and the semaphore $s$ is available

In a logical fashion we can describe the invariant, that either $c_1$, $c_2$ or $s$ is marked, e.g., by the assertion $\Box _+ (c_1 \,\vee \,s \,\vee \,c_2)$ which means that for all states of net only one of the mentioned places is singly-marked. Algebraically this is stated by the inequation

$$\begin{aligned} \langle a |p_0 \le |a](c_1 + s + c_2) \end{aligned}$$

(25)

for a transition element $a$ and initial state $p_0$. By the explanation of the modal operators after Definition 7.1, this means that all states reachable from $p_0$ have $a$-transitions only to states where $c_1, c_2$ or $s$ are marked, and hence satisfy the invariant.

Next we give a proof showing that we cannot reach a state where both $c_1$ and $c_2$ are marked.

Lemma 9.2

$|a](c_1 + s + c_2) \le |a]\lnot (c_1*c_2*1)$. Informally, states which have $a$-transitions only to states where $c_1, c_2$ or $s$ are marked are guaranteed to have no $a$-transitions to states in which at least $c_1$ and $c_2$ are marked.

Proof

First, we know that $c_i \le \lnot u$ and $s, c_i \le \lnot (\lnot u * \lnot u)$. This implies by isotony of $*$ and Lemma 9.1 that $c_1 * c_2 * 1 \le \lnot u * \lnot u * 1 = \lnot u * \lnot u$. By contraposition this is equivalent to $\lnot (\lnot u * \lnot u) \le \lnot (c_1 * c_2* 1)$. Now, since by assumption $s,c_i \le \lnot (\lnot u * \lnot u)$, we have that $s,c_i \le \lnot (c_1 *c_2*1)$.

By this we can easily infer from isotony of box in its second argument and idempotence of $+$ that $|a](c_1 + s + c_2) \le |a]\lnot (c_1*c_2*1)$. $\square$

Again it is an easy task to infer from this lemma and Eq. (25) that

$$\begin{aligned} \langle a |p_0 \le |a]\lnot (c_1*c_2*1), \end{aligned}$$

meaning that in no reachable state both processes are in their critical sections.

10 Liveness and fairness

For describing progress and fairness of particular transitions in the mutex net we need a further temporal concept which is called the leadsto  operator (e.g. [27, 37]) and defined for formulas $A,B$ by $A \triangleright B = \Box _+ (A \rightarrow \Diamond _+ B)$. The corresponding algebraic formulation of the leadsto operator for tests $p,q$ and preorder $a$ is

$$\begin{aligned} p \triangleright q \,=_{ df}\,|a](p \rightarrow | a\rangle q). \end{aligned}$$

This operator again only needs a modal semiring to be well defined; the $*$ operator does not appear in it. Therefore our laws concerning it and their proofs carry over to $\mathsf{LTL}$, $\mathsf{CTL}/\mathsf{CTL}^*$ and $\mathsf{STL}$ etc.

We stipulate that $\triangleright$ binds weaker than $\cdot$ and $*$.

Before proving properties of $\triangleright$ we present two auxiliary results.

Lemma 10.1

The implication operator $\rightarrow$ on tests (Def. 7.1) is reflexive and transitive and satisfies an exchange law, i.e., for all tests $p,q,r,s$ we have

$$\begin{aligned} \begin{array}{c} 1 \le p \rightarrow p,\\ (p \rightarrow q) \cdot (q \rightarrow r) \le (p \rightarrow r), \\ (p \rightarrow q) \cdot (r \rightarrow s) \le (p + r) \rightarrow (q + s). \end{array} \end{aligned}$$

Proof

Reflexivity is obvious. For transitivity we calculate

$$\begin{aligned} \begin{array}{rcl} (p \rightarrow q) \cdot (q \rightarrow r) &{} = &{} (\lnot p + q) \cdot (\lnot q + r) = \lnot p \cdot q + \lnot p \cdot r + q \cdot \lnot q + \lnot q \cdot r \\ &{} \le &{} \lnot p + \lnot p + r = p \rightarrow r \end{array} \end{aligned}$$

which follows from the definition of $\rightarrow$, distributivity, Boolean algebra and isotony. Using a similar argumentation we infer

$$\begin{aligned} \begin{array}{rcl} (p \rightarrow q) \cdot (r \rightarrow s) &{} = &{} (\lnot p + q) \cdot (\lnot r + s) = \lnot p \cdot \lnot r + q \cdot \lnot r + \lnot p \cdot s + q \cdot s \\ &{} \le &{} \lnot (p + r) + q + s + q = (p + r) \rightarrow (q + s). \end{array} \end{aligned}$$

$\square$

The following proof principle (see e.g. [27]) will be handy in the next lemma.

Lemma 10.2

Starting in a state $\sigma$ that is guaranteed to reach a state $p$ while maintaining $q$ guarantees that from $\sigma$ a state in $p \cdot q$ can be reached. Formally,

Proof

$\square$

Lemma 10.3

The operator $\triangleright$ is reflexive and transitive and satisfies an exchange law, i.e., for all tests $p,q,r,s$ we have

$$\begin{aligned} \begin{array}{c} 1 \le p \triangleright p,\\ (p \triangleright q)\cdot (q \triangleright r) \le (p \triangleright r), \\ (p \triangleright q)\cdot (r \triangleright s) \le (p+r) \triangleright (q+s). \end{array} \end{aligned}$$

Proof

Reflexivity follows from reflexivity of $a$, isotony of diamond and (M) via $| a\rangle (\lnot p + | a\rangle p) \ge |a](\lnot p + p) = |a]1 = 1$. The exchange law follows immediately from (13) and Lemma 10.1.

Transitivity can be shown as follows.

$\square$

Using $\triangleright$ we are now able to algebraically state the property that the net is fair in the sense that whenever ${ Pro}\,_i$ has requested the semaphore $s$, i.e., is pending, it will eventually enter its critical section. This is formalised by

$$\begin{aligned} \langle a |p_0\ \le \ (p_i*1) \triangleright (c_i*1). \end{aligned}$$

(26)

Note that we use local tests to ensure that some place is marked, while the remaining part of the state can be characterised imprecisely, since we do not need to impose any further restriction on it. For a proof of Eq. (26) we need some further assumptions (cf. [25]) about the behaviour of the mutex net. First, we need to state that whenever one of the places $c_i$ representing the critical sections is marked then also the semaphore will eventually become marked again. This means that neither ${ Pro}\,_1$ nor ${ Pro}\,_2$ will stay in its critical section forever. Using the $\triangleright$ operator we describe this behaviour algebraically as follows:

$$\begin{aligned} \langle a |p_0 \le (c_i*1) \triangleright (s*1). \end{aligned}$$

(27)

Next, we infer from the invariant in (25), isotony, definition of $\rightarrow$, reflexivity of $a$ and the definition of $\triangleright$,

$$\begin{aligned} \begin{array}{rcl} \langle a |p_0 &{} \le &{} |a](c_1 + s + c_2) \\ &{} \le &{} |a](\lnot (p_i*1) + c_1*1 + s*1 + c_2*1) \\ &{} = &{} |a]((p_i*1) \rightarrow (c_1*1 + s*1 + c_2*1)) \\ &{} \le &{} |a]((p_i*1) \rightarrow | a\rangle (c_1*1 + s*1 + c_2*1)) \\ &{} = &{} (p_i*1) \triangleright (c_1*1 + s*1 + c_2*1). \end{array} \end{aligned}$$

Moreover, by idempotence of test w.r.t. $\cdot$, disjunctivity, reflexivity of $\triangleright$ in Corollary 10.3 and the assumptions in (27) we have

$$\begin{aligned} \begin{array}{rcl} \langle a |p_0 &{} \le &{} (c_1*1 \triangleright s*1) \cdot (c_2*1 \triangleright s*1) \cdot (s*1 \triangleright s*1) \\ &{} = &{} (c_1*1 + c_2*1 + s*1) \triangleright (s*1). \end{array} \end{aligned}$$

In sum, we can further infer from transitivity of $\triangleright$ that

$$\begin{aligned} \langle a |p_0 \le (p_i*1) \triangleright (s*1), \end{aligned}$$

(28)

which means that any reachable state where at least $p_i$ is marked will lead to a state where $s$ is marked so that the corresponding process is able to enter its critical region.

As a final ingredient to prove (26) we need to additionally assume further behaviour for the mutex net. For this we state that whenever the semaphore $s$ becomes marked then the transition $t_2$, respectively $t_5$, will eventually fire and therefore produce a token on $c_i$. For transition $t_2$ this is formalized by

$$\begin{aligned} \langle a |p_0 \le |a](| a\rangle (s*1) \rightarrow | a\cdot t_2\rangle (c_1*1)). \end{aligned}$$

(29)

A similar formula can be given for $t_5$. Note that $a \cdot t_2$ states that finally $t_2$ will fire, yielding a state that contains at least a token on $c_1$. From (29) we obtain by antitony of $\rightarrow$ in its first argument, reflexivity of $a$, isotony and transitivity of $a$, that

$$\begin{aligned} \langle a |p_0 \le |a]((s*1) \rightarrow | a\rangle (c_1*1)) = (s*1) \triangleright (c_1*1). \end{aligned}$$

(30)

Finally, transitivity of $\triangleright$ and Eq. (28) show the goal $\langle a |p_0 \le (p_i*1) \triangleright (c_i*1)$.

11 Related work

The concept of locality for transitions in Petri nets has already been discussed in other papers (e.g. [17]). However, algebraic treatments yielding simple and pointfree characterisations have not been widely investigated. A similar abstract approach that builds a formal model for Petri nets based on predicate transformers, i.e., mappings between sets of states, that also introduces a notion of locality, can be found in [44].

A further work where also a Petri net algebra is developed can be found in [3]. That approach basically uses a process algebraic approach to such nets that is called the Petri Box  calculus. In particular, an abstract approach called the Box Algebra  is discussed of which the Petri Box calculus and other process algebras can be seen as instances. Compared to that work we rather focus on general algebraic structures involving especially modal operators for reasoning about the concrete application of Petri nets.

In [2, 16], a relation-algebraic approach to Petri nets is considered that introduces relational formulas for frequently used properties such as enabledness or liveness in such nets. This allows in particular mechanised reasoning and visualisations by the graphical system RelView. Compared to the present approach formulas become quite complex and difficult to read. Moreover, they are not as general as the formulas provided in the present paper. Mechanisation or automation can be obtained in parts for the first-order fragment of the algebra with theorem proving tools like Prover9/Mace4 [29]. Such tools have already been successfully instantiated for the algebras used here (e.g. [6, 22, 23]).

12 Conclusion and outlook

We have shown that algebraic structures like modal concurrent net quantales can be used for abstract reasoning about the behaviour of Petri nets. In particular, we have been able to avoid any inductive arguments about transition sequences in favour of just invoking transitivity, and presented several pointfree formulas that allowed algebraic correctness proofs of inference rules given in the logic of [35, 36]. Additionally, we demonstrated practicality of the approach within the example of a standard mutex net in calculating with safety, liveness and fairness properties.

As future work, it would be interesting to investigate concrete connections to the work on relational system support to the analysis of Petri nets in [2, 16]. This might yield wider applicability for the present algebraic approach and, in turn, might help to facilitate the relational approach there.

A further interesting topic concerns so-called Signal Transition Graphs (e.g. [42]) which are central to a large part of Walter Vogler’s papers. Since such graphs are basically Petri nets, we hope that our modal Petri net algebra can be also applied to such nets.

Finally, it is worth investigating whether the algebraic structures we have introduced can be used for automated proofs using Prover9/Mace4 or similar systems, along the lines of earlier case studies (e.g. [8, 22, 23]).