# Logics for Petri Nets with Propagating Failures

Leandro Gomes, Alexandre Madeira, Mario Benevides

► To cite this version:

Leandro Gomes, Alexandre Madeira, Mario Benevides. Logics for Petri Nets with Propagating Failures. 8th International Conference on Fundamentals of Software Engineering (FSEN), May 2019, Tehran, Iran. pp.145-157, 10.1007/978-3-030-31517-7_10. hal-03769133

HAL Id: hal-03769133

https://inria.hal.science/hal-03769133v1

Submitted on 5 Sep 2022

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons CC BY 4.0 - Attribution - International License
<figure><img src="image_2.png" /></figure>

ifip

International Federation for Information Processing

This document is the original author manuscript of a paper submitted to an IFIP
conference proceedings or other IFIP publication by Springer Nature. As such, there
may be some differences in the official published version of the paper. Such
differences, if any, are usually due to reformatting during preparation for publication or
minor corrections made by the author(s) during final proofreading of the publication
manuscript.
# Logics for Petri nets with propagating failures

Leandro Gomes¹, and Alexandre Madeira² and Mario Benevides³

¹ HASLab INESC TEC - Univ. Minho, Portugal

² CIDMA - Univ. Aveiro, Portugal

³ COPPE/PESC - Instituto de Matemática/DCC
Universidade Federal do Rio de Janeiro, Brasil

**Abstract.** Petri nets play a central role in the formal modelling of a wide range of complex systems and scenarios. Their ability to handle with both concurrency and resource awareness justifies their spread in the current formal development practices. On the logic side, Dynamic Logics are widely accepted as the *de facto* formalisms to reason about computational systems. However, as usual, the application to new situations raises new challenges and issues.

The ubiquity of failures in the execution of current systems, interpreted in these models as triggered events that are not followed by the corresponding transition, entails not only the adjustment of these structures to deal with this reality, but also the introduction of new logics adequate to this emerging phenomenon.

This paper contributes to this challenge by exploring a combination of two previous works of the authors, namely the Propositional Dynamic Logic for Petri Nets [1] and a parametric construction of multi-valued dynamic logics presented in [13]. This exercise results in a new family of Dynamic Logics for Petri Nets suitable to deal with firing failures.

# 1 Introduction

Petri nets are semantic structures widely used in computer science. Their adequacy to model, specify and analyze complex systems dealing with concurrency and resource awareness is well known. At the core of this success is their rich and intuitive graphical syntax. Nevertheless, for property oriented specification and verification purposes, it is useful to consider logic systems having this structure as a semantics. The first attempt in such direction was done by the linear logic community (e.g. [6]). A number of other logics were then proposed in the literature for standard and timed versions of Petri nets eg. [3].

Propositional dynamic logic (PDL) [8], a very versatile logic for verification of computational systems, was also explored in this context. Particularly, Petri-PDL [12] was introduced as an extension of PDL to give logical semantics to Petri

<footnote>* This work is financed by the ERDF European Regional Development Fund through the Operational Programme for Competitiveness and Internationalisation - COMPETE 2020 Programme and by National Funds through the Portuguese funding agency, FCT - Fundação para a Ciência e a Tecnologia, within projects POCI-01-0145-FEDER-016826, POCI-01-0145-FEDER-029946 and UID/MAT/04106/2019. The second author is supported in the scope of the framework contract foreseen in the numbers 4, 5 and 6 of the article 23, of the Decree-Law 57/2016, of August 29, changed by Portuguese Law 57/2017, of July 19</footnote>
nets. In such variant, the programs are marked Petri nets expressed by a textual syntax (with a choice and a composition operators). Another approach was taken in [5], where the well established theory of modal semirings was used to develop a generic modal algebra for reasoning about reachability properties in Petri nets. The BI resource based semantics presented in [16] introduces another proposal to allow comparison of “amounts of information” modelled by the possible worlds of the model. In this work, Petri nets are presented as concrete instances of this semantics. Later, the work of [12] was extended [1] to include the iteration operator. This logic is expressive enough to describe properties of systems like the one shown in the example below:

**Example 1.** Let us present the following situation, based on the example presented in [1], which illustrates the behaviour of a chocolate vending machine. The system works as follows: we turn the machine on (l) and put one coin (m) and then it releases the chocolate (c).

Its behaviour can be specified by the Petri net of Figure 1. The upper left place ($\ell$) is the power button of a vending machine; the bottom left is the coin inserted (m) and the bottom right is the chocolate output (c); if the vending machine is powered on, always when a coin is inserted you will have a chocolate released. We can express that *once we turn the machine on and put one coin we can obtain a chocolate* by the formula $\langle(\ell, m), (\ellmt_2x \odot xt_3yc)\rangle \top$, meaning that, if we are in a state were states $\ell$ and $m$ are marked, after executing the Petri net program $\ellmt_2x \odot xt_3yc$, we reach a state were $\top$ is satisfied.

<figure><img src="image_3.png" /><figcaption>**Fig. 1.** Execution of the program $\ellmt_2x \odot xt_3yc$ in the chocolate machine</figcaption></figure>

The above formula can be proved using the proof system presented in [1].

The complexity of modern systems, namely the heterogeneity of the environments where they live, entails a more demanding approach in their design and building processes. The inevitability that human beings eventually make mistakes in such processes extols the advantage of adopting formalisms which deal with the possibility of failures at the outset.

Recalling again the previous example, we would bet that the reader already experienced undesirable situations like *after putting a coin in a vending machine, the desired chocolate gets stuck behind of the glass*. The analysis of such kinds of failures would require a formalism able to express statements like *once we turn the machine on and put one coin we have an assurance $\alpha$ that we will obtain a chocolate*. A possible model for handling these scenarios would be
a variation of the classical definition of Petri nets, where the triggering of a
transition happens with some reliability degree. The resulting assurance would
depend on two aspects: on one side, the reliability degree associated to the
execution of a program; on the other, an appropriate evaluation of a formula
in a many-valued truth space. Despite their adequacy in the reasoning about
several properties of Petri nets, none of the approaches presented in [11], [5] or
[16] aim to formalise the attribution of such degrees.

In order to achieve a Dynamic Logic analogous to [1], but suitable to this
scenario, we base this work on the construction of multi-valued dynamic logics
introduced in [14, 13]. First, we introduce a new variant of the Petri Nets, the
*Petri nets with A-failures*, which explicitly assumes that the modelled system
may eventually fail, supporting a claim of reliability to each firing of a transition.
In the case where a failure occurs, the firing event is consumed without the
occurrence of the expected transition. Depending on the system modelled, it
would make sense to measure these reliability degrees in a discrete scale, in a
continuous interval, or simply in an universe only with the values *true* and *false*.
Hence, instead of fixing the domain of the assurances degrees as the usual real
interval [0, 1], we will be more generic: the proposed models are parametric to the
nature of the reliability degrees that are most suitable for each concrete situation.
This flexibility is realised by assuming, as parameter, an (action) lattice **A**. Some
additional considerations on this parameter are in order.

As in standard PDL, the interpretation of programs in Petri-PDL [11] relies
on the Kleene algebra of relations (as we will see in the next section, firing
functions are interpreted as binary relations). However, firing functions in Petri
nets with **A**-failures are based on reliability degrees given by elements of an
action lattice, and not on the interpretation of classic binary relations.

To give meaning to Petri net programs in this new formalism, this paper
adopts a class of Kleene algebras, parameterised by an action lattice **A**. These
algebraic structures base the interpretation of (composed) programs in Petri nets
with **A**-failures, by reflecting how failures in transitions are propagated into the
whole execution of a program. This is also reflected in the kind of assertions we
can express in the logic, as well as in the outcome we expect for the validity of
a Dynamic Logic formula in a Petri net with **A**-failures. For that purpose, we
follow a strategy similar to that used in [14, 13], where an action lattice will follow
a similar role in our method, namely as a computational model (by representing
weighted fails) and as a truth universe (by giving a (possible) many-valued truth
space to the addressed logics). The proposed method for constructing graded
dynamic logics is parametric on whatever truth/computational domain is the
most suitable to the system under consideration.

*Outline.* The remaining of this paper is organized as follows. Section 2 presents all the background needed about the Petri-PDL* formalism and the concept of action lattice. Section 3 is devoted to Petri Net with **A**-failures, as well as, to suitable Kleene Algebras to interpret programs in these structures. In Section 4, we introduce a parametric construction of dynamic logics for Petri nets with **A**-
failures, and proper illustrations for such a method. Finally, Section 5 concludes the paper with some final remarks on future work.

## 2 Background

In this section, we present a brief overview of two topics on which the later development is based. First, we review the syntax and semantics of Petri-PDL* [1]. Second, we recall the main notions behind the method introduced in [13], for the generation of many-valued dynamic logics parametrized by an action lattice. This parameter supports both the (possible non-bivalent) truth spaces and the base computational model.

### 2.1 Propositional Dynamic Logic for Petri nets with Iteration

This subsection recalls the syntax and semantics of Petri-PDL*, as presented in [1]. The language of Petri-PDL* consists of

**Propositional symbols:** $Prop = \{p, q, \dots\}$

**Place names:** $a, b, c, d, \dots$

**Transition types:** $T_1 : xt_1y, T_2 : xyt_2z$ and $T_3 : xt_3yz$

**Petri net Composition symbol:** $\odot$

**PDL operator:** $\_*$ (iteration)

**Markings:** $S = \{\epsilon, s_1, s_2, \dots\}$, where $\epsilon$ is the empty sequence. The notation $a \in s$ is used to denote that the place name $a$ occurs in $s$. The expression $(s, a)$ is the number of occurrences of place name $a$ in $s$. It is said that a sequence $r$ is a subsequence of $s$, denoted $r \preceq s$, if for any place name $a$, if $a \in r$ implies $a \in s$.

**Definition 1.** *Petri-PDL*<sup>*</sup> *Programs for a set of places P*

**Basic programs:** $\mathit{set} \ \Pi_0(P)$ *defined by the grammar*

$$ \pi ::= at_1b \mid abt_2c \mid at_3bc $$

where $t_i$ is of type $T_i$, $i = 1, 2, 3$ and $a, b, c \in P$.

**Petri net Programs:** $\mathit{set} \ \Pi(P)$ *defined by the grammar*

$$ \eta ::= \pi \mid \pi \odot \eta \mid \eta^* $$

for $\pi \in \Pi_0(P)$

**Definition 2.** *Let Prop be a set of propositions. The set of Petri-PDL*<sup>*</sup> *formulas for Prop, denoted by $\mathit{Fm}^{\mathit{Petri-PDL}^*(A)}$, is defined by the grammar*

$$ \rho ::= p \mid \top \mid \neg \rho \mid \rho \wedge \rho \mid \langle s, \eta \rangle \rho $$

where $p \in \mathit{Prop}$.
We use the standard abbreviations $⊥ ≡ ¬⊤$, $ρ ∨ ρ ≡ ¬(¬ρ ∧ ¬ρ)$, $ρ → ρ ≡ ¬(ρ ∧ ¬ρ)$ and $[s, η]ρ ≡ ¬⟨s, η⟩¬ρ$.

The definition below introduces the firing function. It defines how the marking of a basic Petri net changes after a firing.

**Definition 3.** For a set of markings $S$, we define the firing function $f : S × Π_0 → S$ as follows

$$ 
\begin{aligned}
- f(s, at_1b) &= \left\{ \begin{array}{l} s_1bs_2, \text{ if } s = s_1as_2 \\ \qquad \epsilon, \text{ if } a \notin s \end{array} \right\} \\[1em]
- f(s, abt_2c) &= \left\{ \begin{array}{l} s_1cs_2s_3, \text{ if } s = s_1as_2bs_3 \\ \qquad \epsilon, \text{ if } a \notin s \text{ or } b \notin s \end{array} \right\} \\[1em]
- f(s, at_3bc) &= \left\{ \begin{array}{l} s_1s_2bc, \text{ if } s = s_1as_2 \\ \qquad \epsilon, \text{ if } a \notin s \end{array} \right\}
\end{aligned}
$$

The definitions of frame, model and satisfaction, that we recall below, are adapted from PDL to deal with the firing of basic Petri nets.

**Definition 4.** A frame for Petri-PDL\* is a triple $⟨W, R_π, M⟩$, where

- $W$ is a non-empty set of states;

- $M: W → S$;

- $R_π$ is a binary relation over $W$, for each basic program $π$, satisfying the following condition: let $s = M(w)$

• if $f(s, π) ≠ ϵ$, if $wR_πv$ then $f(s, π) ≤ M(v)$

• if $f(s, π) = ϵ$, $(w, v) ∉ R_π$

- we inductively define a binary relation $R_η$, for each Petri net program $η$, as follows:

• $R_{η*} = R_η^*$, where $R_η^*$ denotes the reflexive transitive closure of $R_η$.

• $η = η_1 ⊙ η_2 ⊙ ... ⊙ η_n$

$$ R_{\eta} = \{(w, v) | \text{ for some } \eta_i, \exists u \text{ such that } s_i \in M(u) \text{ and } wR_{\eta_i}u \text{ and } uR_{\eta_i}v\} $$

where $s = M(w)$, $η_i$ are Petri net programs and $s_i = f(s, η_i)$, for all $1 ≤ i ≤ n$.

**Definition 5.** A model for Petri-PDL\* is a pair $M = ⟨F, V⟩$, where $F$ is a Petri-PDL frame and $V$ is a valuation function from a set of propositions $Prop$, $V: Prop → 2^W$.

The semantical notion of satisfaction for Petri-PDL\* is defined below.

**Definition 6.** Let $M = (F, V)$ be a model. The notion of satisfaction of a formula $ρ$ in a model $M$ at a state $w$, notation $M, w |→ ρ$, can be inductively defined as follows:

- $M, w |→ p$ iff $w ∈ V(p)$;

- $M, w |→ ⊤$ always;

- $M, w |→ ¬ρ$ iff $M, w |≠ ρ$;

- $M, w |→ ρ ∧ ρ'$ iff $M, w |→ ρ$ and $M, w |→ ρ'$;

- $M, w |→ ⟨s, η⟩ρ$ if there exists $w' ∈ W, wR_η w', s ⊆ M(w)$ and $M, w' |→ ρ$.

If $M, v |→ A$ for every state $v$, we say that $A$ is valid in the model $M$, notation $M |→ A$. And if $A$ is valid in all $M$ we say that $A$ is valid, notation $|→ A$.
## 2.2 Kleene algebras and Action Lattice

We review in this section the notion of Action Lattice [10] as it was used in [13].

**Definition 7 (Kleene Algebra and Action lattice).** An action lattice is a tuple $A = (A, +, \cdot, 0, 1, \cdot, \rightarrow, \cdot)$, where A is a set, 0 and 1 are constants, $\cdot$ is an unary operation in A and $+; \cdot, \rightarrow$ and $\cdot$ are binary operations in A satisfying the axioms enumerated in Figure 2, where the relation $\le$ is induced by $+; a \le b$ iff $a + b = b$. An integral action lattice consists of an action lattice satisfying $a \le 1$, for all $a \in A$. A Kleene Algebra is a structure $(A, +, \cdot, 0, 1, \cdot)$ satisfying (1)-(13).

$$
\begin{align*}
& a + (b + c) = (a + b) + c \quad (1) & 1 + (a; a^*) = a^* \quad (10) \\
& a + b = b + a \quad (2) & 1 + (a^*; a) = a^* \quad (11) \\
& a + a = a \quad (3) & a; x \leq y \Rightarrow a^*; x \leq y \quad (12) \\
& a + 0 = 0 + a = a \quad (4) & x; a \leq y \Rightarrow a; x^* \leq y \quad (13) \\
& a; (b; c) = (a; b); c \quad (5) & a; x \leq y \Leftrightarrow x \leq a \rightarrow b \quad (14) \\
& a; 1 = 1; a = a \quad (6) & a \cdot (b \cdot c) = (a \cdot b) \cdot c \quad (15) \\
& a; (b + c) = (a; b) + (a; c) \quad (7) & a \cdot b = b \cdot a \quad (16) \\
& (a + b); c = (a; c) + (b; c) \quad (8) & a \cdot a = a \quad (17) \\
& a; 0 = 0; a = 0 \quad (9) & a + (a \cdot b) = a \quad (18) \\
& & a \cdot (a + b) = a \quad (19)
\end{align*}
$$

<caption>**Fig. 2.** Axiomatisation of action lattices (from [10])</caption>

As stated in the introduction, the structure of an action lattice is explored in this paper along a double dimension: as a computational model and as a truth space. The intuitions for some of its operations shall be taken from both of these perspectives. Such is the case of operation $+$, which plays the role of non-deterministic choice, in the interpretation of programs, and of logical disjunction, in the interpretation of sentences. However, there are operations whose intuition is borrowed from just in one of these domains. For instance, while operations $*$ and $;$ are taken as iterative execution and sequential composition of actions, operations $\rightarrow$ and $\cdot$ play the role of logical implication and conjunction, respectively.

The following structures are examples of action lattices:

*Example 2 (2 - linear two-values lattice).* As a first action lattice example, we consider the two valued boolean lattice $\mathbf{2} = (\{\top, \bot\}, \vee, \wedge, \bot, \top, \cdot, \rightarrow, \wedge)$ with the standard boolean connectives defined as follows:

$$ \begin{array}{c|c|c|c|c|c} \top & \bot & \top & \bot & \top & \bot \\ \bot & \bot & \top & \bot & \bot & \top \\ \top & \top & \top & \top & \bot & \top \end{array} \rightarrow \begin{array}{c|c} \top & \top \\ \bot & \top \\ \top & \bot \end{array} = \begin{array}{c} * \\ \bot \\ \top \end{array} $$
*Example 3* (*W*<sub>*k*</sub> finite Wajsberg hoops). We consider now an action lattice endowing the finite Wajsberg hoops [2] with a suitable star operation. Hence, for a fix natural *k* > 0 and a generator *a*, we define the structure *W*<sub>*k*</sub> = (*W*<sub>*k*</sub>, +, ;, 0, 1, *, →, ·), where *W*<sub>*k*</sub> = {*a*<sup>0</sup>, *a*<sup>1</sup>, ..., *a*<sup>*k*</sup>}, 1 = *a*<sup>0</sup> and 0 = *a*<sup>*k*</sup>, and for any *m*, *n* ≤ *k*: *a*<sup>*m*</sup> + *a*<sup>*n*</sup> = *a*<sup>min{*m*,*n*}</sup>, *a*<sup>*m*</sup>; *a*<sup>*n*</sup> = *a*<sup>min{*m*+*n*,*k*}</sup>, (*a*<sup>*m*</sup>)<sup>*</sup> = *a*<sup>0</sup>, *a*<sup>*m*</sup> → *a*<sup>*n*</sup> = *a*<sup>max{*n*−*m*,0}</sup> and *a*<sup>*m*</sup> · *a*<sup>*n*</sup> = *a*<sup>max{*m*,*n*}</sup>.

*Example 4* (*L* - the Łukasiewicz arithmetic lattice). The Łukasiewicz arithmetic lattice is the structure *L* = ([0, 1], max, ⊙, 0, 1, *, →, min), where *x* → *y* = min(1, 1 − *x* + *y*), *x* ⊙ *y* = max(0, *y* + *x* − 1) and *x*<sup>*</sup> = 1.

More examples and properties of action lattices can be found in [13].

### 3 Petri nets with failures

This section introduces the notion of Petri net with **A**-failures, as well as suitable Kleene algebras to interpret (composed) programs. As referred in the introduction, the use of an action lattice **A** as parameter is due to the necessity of supporting a double dimension: (i) attribute a reliability degree to the firing of a transition, referring to the interpretation of Petri net programs; (ii) state a degree for a specific property of a Petri net, on the logical side.

As stated, this work is concerned with Petri nets where transitions between markings may fail. This assumption entails adjusting the system dynamics of classical Petri nets: while, in such case, we argue that a system evolves to another markings if a transition is enabled, in our approach, a transition to a new marking occurs with a reliability degree $\alpha$, where $\alpha$ is an element of the lattice **A**. In cases where the Petri net does not transit to another marking, the transition is still consumed. Formally:

**Definition 8.** Given an action lattice **A** = (*A*, +, ;, 0, 1, *, →, ·), a set *S* of markings (over a set of place names *P*) and a basic Petri net program $\pi \in \Pi_0$, an $\alpha$-firing function, for $\alpha \in A$, is a function $f_{\pi}^{\alpha}: S \times S \rightarrow A$ defined as

$$
\begin{align*}
- \text{ for any } a t_1 b \in \Pi_1, f_{at_1b}^{\alpha}(s, s') &= \left\{ \begin{array}{l} \alpha, \text{ if } a \in s \text{ and } b \in s' \\ \alpha \to 0, \text{ if } a \in s \text{ and } a \in s' \\ 0 \text{ if } a \notin s \end{array} \right\} \\
- \text{ for any } ab t_2 c \in \Pi_2, f_{abt_2c}^{\alpha}(s, s') &= \left\{ \begin{array}{l} \alpha, \text{ if } a, b \in s \text{ and } c \in s' \\ \alpha \to 0, \text{ if } a, b \in s \text{ and } a, b \in s' \\ 0 \text{ if } a, b \notin s \end{array} \right\} \\
- \text{ for any } a t_3 bc \in \Pi_3, f_{at_3bc}^{\alpha}(s, s') &= \left\{ \begin{array}{l} \alpha, \text{ if } a \in s \text{ and } b, c \in s' \\ \alpha \to 0, \text{ if } a \in s \text{ and } a \in s' \\ 0 \text{ if } a \notin s \end{array} \right\}
\end{align*}
$$

where $\Pi_i(P)$ are the following partitions of the atomic programs: $\Pi(P)$, $\Pi_1(P) = \{xt_1y \mid x, y \in P\}$, $\Pi_2(P) = \{xyt_2z \mid x, y, z \in P\}$ and $\Pi_3(P) = \{xt_3yz \mid x, y, z \in P\}$.
Note that, in this work, we do not take into consideration the order of the tokens in the markings. Hence, those are represented as multisets, instead of sequences as done for Petri-PDL\* [1].

Now, we have conditions to introduce the intended model.

**Definition 9 (Petri net with A-failures).** Let $\mathbf{A} = (A, +, \;, 0, 1, *, \rightarrow, \cdot)$ be an action lattice. A Petri net with $\mathbf{A}$-failures consists of a tuple $\mathcal{P} = (P, S, \Pi_0, I, M_0)$ where $P$ is a set of places; $S \subseteq P^*$ is the set of (admissible) markings; $\Pi_0 \subseteq \Pi(P)$ is the set of atomic programs; $I: \Pi_0 \rightarrow A$ is the atomic programs reliability degree and $M_0 \in S$ is the initial marking. The interpretation of an atomic program $\pi \in \Pi_0$ is given by the firing function $f_{\pi}^{I(\pi)}$.

In this work, as in [13], the underlying Kleene algebra of $\mathbf{A}$ (c.f. Defn 7) provides a generic computational model for interpreting programs. However, differently form such work, we interpret computations as $\alpha$-firing functions of Definition 8, which carry the information about their effect when executed. Hence, we define the following algebra:

**Definition 10.** Let $\mathbf{A} = (A, +, \;, 0, 1, *, \rightarrow, \cdot)$ be an action lattice and $S$ be a finite set. The algebra of $\mathbf{A}$-firing functions is the structure $\mathbf{F} = (F, \cup, \circ, \emptyset, \chi, *)$ where:

$$ - F \text{ is the universe of all the } \alpha\text{-firing functions, for all } \alpha \in A $$

$$ - (f_{\pi_1}^{\alpha_1} \cup f_{\pi_2}^{\alpha_2})(s, s') = f_{\pi_1}^{\alpha_1}(s, s') + f_{\pi_2}^{\alpha_2}(s, s') $$

$$ - (f_{\pi_1}^{\alpha_1} \circ f_{\pi_2}^{\alpha_2})(s, s') = \sum_{s'' \in S} f_{\pi_1}^{\alpha_1}(s, s''); f_{\pi_2}^{\alpha_2}(s'', s') $$

$$ - \emptyset(s, s') = 0 $$

$$ - \chi(s, s') = \begin{cases} 1, & \text{if } s = s' \\ 0, & \text{otherwise} \end{cases} $$

$$ - (f_{\pi}^{\alpha})^{*}(s, s') = \bigvee_{i \ge 0} (f_{\pi}^{\alpha})^{i}(s, s') = (f_{\pi}^{\alpha})^{0}(s, s') + (f_{\pi}^{\alpha})^{1}(s, s') + (f_{\pi}^{\alpha})^{2}(s, s') + \dots $$

The next theorem states that $\mathbf{F}$ represents an adequate structure to interpret Petri net programs for Petri nets with $\mathbf{A}$-failures$^4$.

**Theorem 1.** $\mathbf{F}$ is a Kleene Algebra

*Proof.* This proof is analogous to the proof of the classical result [4], stating that the algebra of $n \times n$ matrices over a Kleene algebra is a Kleene algebra.

With this Kleene algebra, we are able to interpret regular programs in Petri nets with $\mathbf{A}$-failures, i.e. regular expressions of atomic transitions in $\mathbf{A}$:

**Definition 11 (A-interpretations of programs).**

Let $\mathbf{A} = (A, +, \;, 0, 1, *, \rightarrow, \cdot)$ be an action lattice and $(P, S, \Pi_0, I, M_0)$ a Petri net with $\mathbf{A}$-failures. The interpretation of a Petri net program $\eta$ is a firing function recursively defined as follows:

<footnote n="4">⁴ A more generic algebraic structure, suitable to deal with generic weighted computations was recently introduced by the authors in [7].</footnote>
- for any atomic program $\pi \in \Pi_0$, $\llbracket \pi \rrbracket(s, s') = f_\pi^{F(\pi)}(s, s')$

- $\llbracket \pi_1; \pi_2 \rrbracket(s, s') = (\llbracket \pi_1 \rrbracket \circ \llbracket \pi_2 \rrbracket)(s, s')$,

- $\llbracket \eta^* \rrbracket(s, s') = \llbracket \eta \rrbracket^*(s, s')$, for $\llbracket \eta \rrbracket^*(s, s') = \sum_{i \ge 0} \llbracket \eta \rrbracket^i(s, s')$ where $\llbracket \eta \rrbracket^0(s, s') = \chi(s, s')$ and for any $i \ge 0$, $\llbracket \eta \rrbracket^{i+1}(s, s') = (\llbracket \eta \rrbracket^i \circ \llbracket \eta \rrbracket)(s, s')$

- $\llbracket \eta + \eta' \rrbracket(s, s') = \llbracket \eta \rrbracket(s, s') + \llbracket \eta' \rrbracket(s, s')$, for $\eta, \eta'$ Petri net programs.

The interpretation of Petri Net composed programs, as presented in Definition 1, where the global composition $\odot$ is considered rather than the sequential composition $;$, can be handled in our logic indirectly by defining $\odot$ as

$$ \eta \odot \eta' \equiv \eta; (\eta + \eta')^* + \eta'; (\eta + \eta')^* \quad (20) $$

where $\eta$ and $\eta'$ are Petri net programs.

# 4 Parametric construction of dynamic logics for Petri nets with failures

This section introduces a parametric method to build Petri-PDL to reason about Petri nets with A-failures, inspired by the construction proposed in [13]. The semantic and satisfaction of these logics are built on top of an arbitrary action lattice $A = (A, +, -, 0, 1, *, \rightarrow, \cdot)$ (c.f. Definition 7). Hence, the resulting logics will be denoted by $GP(A)$. Petri-PDL*, as introduced in [12], is captured as an instance of this construction (by using, as parameter, the lattice 2 of Example 2). Beyond the reliability degrees for transitions, the action lattice also supports the truth space for the (possible multi-valued) outcomes of the logic.

The language for $GP(A)$ is the same of Petri-PDL*, except for formulae, that we define below.

**Definition 12.** Let Prop be a set of propositions. The set of $GP(A)$ formulas for the set of propositions Prop and for the set of place names P, denoted by $Fm^{GP(A)}(Prop, P)$, is defined by the grammar

$$ \rho ::= p \mid \top \mid \bot \mid \rho \wedge \rho \mid \rho \vee \rho \mid \rho \rightarrow \rho \mid \langle \xi \rangle \rho \mid [\xi] \rho $$

where $p \in \text{Prop}$, $\xi ::= \pi; \xi \mid \xi^* \mid \xi + \xi$ for $\pi ::= at_1b \mid abt_2c \mid at_3bc$, and $a, b, c \in P$.

Observe that we denoted the regular programs (with the sequential composition $;$) by letter $\xi$ instead of $\eta$ used for the Petri-net programs (with global composition $\odot$). However, in the sequel, we will relax this convention by using $\eta$ for both cases. The symbol $\odot$ will also be used as meta-syntax of our logic, to be interpreted according to (20). For instance, the expression $\langle \eta \odot \eta' \rangle \varphi$ is just notation for the formula $\langle \eta; (\eta + \eta')^* + \eta'; (\eta + \eta')^* \rangle \varphi$.

Note that, differently from previous work [1], we do not include the negation as a primitive operator, and use, instead, the defined negation $\neg x \equiv x \rightarrow \bot$. Actually, as stated, we intend to deal with generic truth spaces for possible non bivalent interpretation of assertions (e.g. we are not requiring negative involvement).
**Definition 13.** A model for **GP**(A) is a pair $\mathcal{M} = (\mathcal{P}, \mathcal{V})$, where $\mathcal{P}$ is a Petri net with A-failures and $\mathcal{V}$ is a valuation function over a set of propositions Prop, defined as $\mathcal{V} : \text{Prop} \times S \to A$.

Now, we define the semantic notion of satisfaction for **GP**(A).

**Definition 14.** Let $\mathbf{A} = (A, +, -, 0, 1, *, \rightarrow, \cdot)$ be an action lattice. The (graded) satisfaction $\models : (\mathcal{M} \times S) \times \text{Fm}^{\text{GP}(\mathbf{A})}(\text{Prop}) \to \mathbf{A}$ for **GP**(A) is recursively defined for each model $\mathcal{M}$, any marking $s \in S$ and for any formula $\rho \in \text{Fm}^{\text{GP}(\mathbf{A})}(\text{Prop})$ as follows:

$$- (\mathcal{M}, s \models p) = \mathbf{V}(p, s);$$

$$- (\mathcal{M}, s \models \top) = \top;$$

$$- (\mathcal{M}, s \models \bot) = \bot;$$

$$- (\mathcal{M}, s \models \rho \land \rho') = (\mathcal{M}, s \models \rho) \cdot (\mathcal{M}, s \models \rho');$$

$$- (\mathcal{M}, s \models \rho \lor \rho') = (\mathcal{M}, s \models \rho) + (\mathcal{M}, s \models \rho');$$

$$- (\mathcal{M}, s \models \rho \rightarrow \rho') = (\mathcal{M}, s \models \rho) \rightarrow (\mathcal{M}, s \models \rho');$$

$$- (\mathcal{M}, s \models \langle \eta \rangle \rho) = \sum_{s' \in S} (\llbracket \eta \rrbracket(s, s'); (\mathcal{M}, s' \models \rho));$$

$$- (\mathcal{M}, s \models [\eta] \rho) = \bigwedge_{s' \in S} (\llbracket \eta \rrbracket(s, s') \rightarrow (\mathcal{M}, s' \models \rho))$$

*Example 5.* Let us start by revisiting Example 1, by using **GP**(2) (see Example 2). For that, we denote $f_{\ellmt_2x}^{\top}(\ell m, x)$ by $a$ and $f_{xt_3yc}^{\top}(x, yc)$ by $b$ and, in this situation $a = b = \top$. So, we can write the sentence of Example 1 as once we

<figure><img src="image_4.png" /><figcaption>**Fig. 3.** A Petri net for a (possibly) defective chocolate vending machine</figcaption></figure>

turn the machine on and put one coin we have the (total) reliability that we will obtain a chocolate. This expression can, then, be represented in **GP**(2) by the formula $(\mathcal{M}, \ell m \models (\ell mt_2 x \odot xt_3yc) \top) = \top$. Hence:

$$\mathcal{M}, \ell m \models \langle \ell mt_2 x; xt_3yc \rangle \top$$

$$= \sum_{s \in S} (\llbracket \ell mt_2 x; xt_3yc \rrbracket(\ell m, s); (M, s \models \top))$$

$$= \sum_{s \in S} (\llbracket \ell mt_2 x \rrbracket \circ \llbracket xt_3yc \rrbracket)(\ell m, s); (M, s \models \top))$$

$$= \sum_{s \in S} (\left( \sum_{s' \in S} (\llbracket \ell mt_2 x \rrbracket(\ell m, s'); \llbracket xt_3yc \rrbracket(s', s)) \right); (M, s \models \top))$$

$$= \sum_{s \in S} (\left( \llbracket \ell mt_2 x \rrbracket(\ell m, x); \llbracket xt_3yc \rrbracket(x, s) + \llbracket \ell mt_2 x \rrbracket(\ell m, \ell m); \llbracket xt_3yc \rrbracket(\ell m, s) \right); (M, s \models \top))$$
$$
\begin{align*}
&= (([\ellmt_2x](\ell m, x); [xt_3yc](x, y c) + [\ellmt_2x](\ell m, \ell m); [xt_3yc](\ell m, y c)); (M, y c \models \top)) \\
&\quad + ([\ellmt_2x](\ell m, \ell m); [xt_3yc](\ell m, \ell m)); (M, \ell m \models \top) \\
&\quad + ([\ellmt_2x](\ell m, x); [xt_3yc](x, x) + [\ellmt_2x](\ell m, \ell m); [xt_3yc](\ell m, x)); (M, x \models \top) = \top
\end{align*}
$$

Assume now that this machine has a technical problem and it can not assure
with total reliability the release of a chocolate every time a coin is inserted.
Suppose also that we can express such reliability degrees in a 1...10 discrete
scale. Hence, using **GP**(*W*<sub>10</sub>) (see Ex.3), we can express that the machine transits
from marking *lm* to *x* with a reliability 8 and from *x* to *yc* with 9, i.e. *a* = 8
and *b* = 9. Now, the verification of the property *once we turn the machine on*
*and put one coin we have a reliability 7 out of 10 that we will obtain a chocolate,*
from the marking *lm*, can be computed by

$$
\mathcal{M}, \ell m \models \langle \ellmt_2x; xt_3yc \rangle \top = (8; 9 + (8 \to 0); 0); 10 + ((8 \to 0); 0); 10 + (8; (9 \to 0) + (8 \to 0); 0); 10 = 7.
$$

Nevertheless, for some situations, it could be more appropriate to use a con-
tinuous scale. Suppose, for instance, that we want to be more precise, by stating
that the reliability degree of the machine to evolve from marking *lm* to *x* is 0.78
and from *x* to *yc* is 0.93, which corresponds to *a* = 0.78 and *b* = 0.93. This can
be expressed using **GP(L)** (see Ex. 4). In this case we have:

$$
\mathcal{M}, \ell m \models \langle \ellmt_2x; xt_3yc \rangle \top = \max\{\max\{0.78 \odot 0.93, (0.78 \to 0) \odot 0\} \odot 1, ((0.78 \to 0) \odot 0) \odot 1, \max\{0.78 \odot (0.93 \to 0), (0.78 \to 0) \odot 0\} \odot 1\} = 0.71.
$$

Let us now use the global composition operator $\odot$, in place of the simple
sequential composition $;$ . Given the Petri net program $\eta = \ellmt_2x \odot xt_3yc$, we
compute the reliability degree of the formula $\langle \ellmt_2x \odot xt_3yc \rangle \top$, using $\mathbf{GP}(2)$,
as follows:

$$
\begin{align*}
\mathcal{M}, \ell m &\models \langle \ellmt_2 x \odot xt_3yc \rangle \top \\
&= \sum_{s \in S} ( [\ellmt_2 x \odot xt_3yc](\ell m, s); (M, s \models \top) ) \\
&= \sum_{s \in S} ( [\ellmt_2 x; \eta^* + xt_3yc; \eta^*](\ell m, s); (M, s \models \top) ) \\
&= \sum_{s \in S} ( ( [\ellmt_2 x; \eta^*](\ell m, s) + [xt_3yc; \eta^*](\ell m, s) ); (M, s \models \top) ) \\
&= \sum_{s \in S} ( ( ( [\ellmt_2 x] \circ [\eta^*])(\ell m, s) + ( [xt_3yc] \circ [\eta^*])(\ell m, s) ); (M, s \models \top) ) \\
&= \sum_{s \in S} ( ( \sum_{s' \in S} ( [\ellmt_2 x](\ell m, s'); [\eta^*](s', s)) + \sum_{s' \in S} ( [xt_3yc](\ell m, s'); [\eta^*](s', s)) ); (M, s \models \top) ) \\
&= \sum_{s \in S} ( ( [\ellmt_2 x](\ell m, x); [\eta^*](x, s) + [\ellmt_2 x](\ell m, \ell m); [\eta^*](\ell m, s) + [xt_2yc](\ell m, x); [\eta^*](x, s) + [xt_3yc](\ell m, \ell m); [\eta^*](\ell m, s) ); (M, s \models \top) ) \\
&= ((\top \land \top) \lor (\bot \land \top) \lor (\bot \land \top) \lor (\bot \land \top)) \land \top \lor (\bot \land \top) \land \top \lor ((\top \land \top) \lor (\bot \land \top)) \land \top = \top
\end{align*}
$$
# 5 Conclusions and further work

In this work, we contributed with the generalisation of the logic presented in [1], by considering that the firing of a Petri net may fail. The approach taken in order to handle this variation was based on previous work done in [13], where an action lattice is considered to model both the notion of reliability degree of transitions in models and to support the (possible) multi-valued truth degree of a formula. This goal was accomplished by introducing: (i) a new definition of Petri net, where transitions between markings may fail; (ii) an underlying class of Kleene algebras (parametric on an action lattice), suitable for interpreting (composed) Petri net programs; (iii) a parametric method to build Dynamic logics with these semantics.

The extension of this work can be done in several directions. First, the necessity to have supporting computational tools for these logics suggests the development of a proof calculi and model checking algorithms, with their computational complexity. In this line, we expect to obtain characterizations, parametric to the base action lattice adopted in each situation. Moreover, comparing these logics with the literature is also in our agenda, namely to establish a formal relation between the models of $GP(L)$ and the *Fuzzy Petri nets* [17].

The behaviour of Petri nets is concurrent by nature, being defined by the simultaneous firing of sets of transitions. However, in the method introduced, global composition is presented as a derived operator from the base (sequential composition, choice and reflexive transitive closure) Kleene operations. Hence, in future, we intend to adapt the presented construction to another parameter supporting a concurrent computational model like, for instance, a Concurrent Kleene Algebra [9]. An approach in this direction was already addressed in [5], which is based on the well known work on modal semirings [15]. Note however that, although such approach is capable of handling concurrency, it lacks the expressiveness for generating a logic able to reason in a multi-valued truth space.

# References

1. Mario R. F. Benevides, Bruno Lopes, and Edward Hermann Haeusler. Propositional dynamic logic for petri nets with iteration. In Augusto Sampaio and Farn Wang, editors, *Theoretical Aspects of Computing - ICTAC 2016 - 13th International Colloquium, Taipei, Taiwan, ROC, October 24-31, 2016, Proceedings*, volume 9965 of *Lecture Notes in Computer Science*, pages 441–456. Springer, 2016.

2. W. J. Blok and Isabel Ferreirim. On the structure of hoops. *algebra universalis*, 43(2-3):233–257, 2000.

3. Michael Blondin, Alain Finkel, Christoph Haase, and Serge Haddad. The logical view on continuous Petri nets. *ACM Trans. Comput. Log.*, 18(3):24:1–24:28, 2017.

4. J.H. Conway. *Regular Algebra and Finite Machines*. Printed in GB by William Clowes & Sons Ltd., 1971.

5. Han-Hing Dang and Bernhard Möller. Modal algebra and petri nets. *Acta Inf.*, 52(2-3):109–132, 2015.
6. Uffe Engberg and Glynn Winskel. Linear logic on Petri nets. In J. W. de Bakker, W. P. de Roever, and G. Rozenberg, editors, *A Decade of Concurrency Reflections and Perspectives*, pages 176–229. Springer, 1994.

7. Leandro Gomes, Alexandre Madeira, and Luis S. Barbosa. Generalising KAT to verify weighted computations. Technical Report submission under consideration.

8. David Harel, Dexter Kozen, and Jerzy Tiuryn. *Dynamic Logic*. Foundations of Computing Series. MIT Press, 2000.

9. Tony Hoare, Stephan van Staden, Bernhard Möller, Georg Struth, Jules Villard, Huibiao Zhu, and Peter W. O'Hearn. Developments in concurrent kleene algebra. In Peter Höfner, Peter Jipsen, Wolfram Kahl, and Martin Eric Müller, editors, *RAMICS 2014*, volume 8428 of LNCS, pages 1–18. Springer, 2014.

10. Dexter Kozen. On action algebras. *Logic and Information Flow*, pages 78–88, 1994.

11. Bruno Lopes, Mario Benevides, and Edward Hermann Haeusler. Extending Propositional Dynamic Logic for Petri Nets. *ENTCS*, 305(11):67–83, 2014.

12. Bruno Lopes, Mario Benevides, and Hermann Haeusler. Propositional dynamic logic for Petri nets. *Logic Journal of the IGPL*, 22:721–736, 2014.

13. Alexandre Madeira, Renato Neves, and Manuel A. Martins. An exercise on the generation of many-valued dynamic logics. *Journal of Logical and Algebraic Methods in Programming*, 1:1–29, 2016.

14. Alexandre Madeira, Renato Neves, Manuel A. Martins, and Luís Soares Barbosa. A dynamic logic for every season. In Christiano Braga and Narciso Martí-Oliet, editors, *SBMF 2014*, volume 8941 of LNCS, pages 130–145. Springer, 2014.

15. Bernhard Möller and Georg Struth. Modal kleene algebra and partial correctness. In Charles Rattray, Savi Maharaj, and Carron Shankland, editors, *AMAST 2004*, volume 3116 of Lecture Notes in Computer Science, pages 379–393. Springer, 2004.

16. David J. Pym, Peter W. O'Hearn, and Hongseok Yang. Possible worlds and resources: the semantics of BI. *Theor. Comput. Sci.*, 315(1):257–305, 2004.

17. Kai-Qing Zhou and Azlan Mohd Zain. Fuzzy Petri nets and industrial applications: a review. *Artif. Intell. Rev.*, 45(4):405–446, 2016.