Vol-3170/paper4
Jump to navigation
Jump to search
Paper
| Paper | |
|---|---|
 edit
| |
| description | |
| id | Vol-3170/paper4 |
| wikidataid | Q117351466→Q117351466 |
| title | Information Flow among Transitions of Bounded Equal-Conflict Petri Nets |
| pdfUrl | https://ceur-ws.org/Vol-3170/paper4.pdf |
| dblpUrl | https://dblp.org/rec/conf/apn/AdobbatiBSP22 |
| volume | Vol-3170→Vol-3170 |
| session | → |
Information Flow among Transitions of Bounded Equal-Conflict Petri Nets
Information Flow Among Transitions of Bounded
Equal-Conflict Petri Nets
Federica Adobbati1 , Luca Bernardinello1 , Görkem Kılınç Soylu1 and Lucia Pomello1
1
Dipartimento di Informatica, Sistemistica e Comunicazione, Università degli Studi di Milano - Bicocca, viale Sarca
336 U14, Milano, Italia
Abstract
In a distributed system, in which an action can be either “hidden” or “observable”, an unwanted infor-
mation flow might arise when occurrences of observable actions give information about occurrences of
hidden actions. A collection of relations, i.e. reveals and its variants, is used to model such information
flow among transitions of a Petri net. This paper introduces a parametrised generalisation to the exist-
ing reveals relations and provides a formal basis for information-flow analysis of bounded equal-conflict
PT systems.
Keywords
Information flow, noninterference, bounded equal-conflict Petri nets, reveals relations, distributed sys-
tems.
1. Introduction
In distributed systems, it is often the case that some actions are confidential, and it is not desired
that a user is able to deduce information about occurrences of these confidential actions, while
still being able to interact with the system. This kind of unwanted information flow can form a
security concern for systems. Noninterference is a formal notion which guarantees that a system
does not suffer from such information flow.
The concept of noninterference was introduced by Goguen and Meseguer for deterministic
state machines in [1]. In this concept, a system is viewed as consisting of components at two
distinct levels of confidentiality: high (hidden) and low (observable). A system is then said to
be secure with respect to noninterference if a user, who knows the structure of the system,
cannot deduce information about high actions by interacting only via low actions. Sutherland
and McCullough moved the concept to the nondeterministic and concurrent systems in [2] and
[3]. Since then, various noninterference properties have been proposed in the literature based
on different system models, e.g., [4, 5, 6, 7]. An overview on information-flow security and
noninterference is provided in [8].
Busi and Gorrieri moved the notion of noninterference to 1-safe Petri nets by studying obser-
vational equivalences and structural properties in [9]. In [10], the authors investigate structural
properties, such as absence of certain places, for defining noninterference in elementary net sys-
PNSE’22: International Workshop on Petri Nets and Software Engineering, Bergen, Norway, 2022
" f.adobbati@campus.unimib.it (F. Adobbati); luca.bernardinello@unimib.it (L. Bernardinello);
gorkemklnc@gmail.com (G. Kılınç Soylu); lucia.pomello@unimib.it (L. Pomello)
© 2022 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
CEUR
Workshop
Proceedings
http://ceur-ws.org
ISSN 1613-0073 CEUR Workshop Proceedings (CEUR-WS.org)
60
�Federica Adobbati et al. CEUR Workshop Proceedings 60–79
tems. In [11], Best et. al. study the decidability of noninterference in Petri nets. In [12], Baldan
and Carraro give a characterisation of noninterference in terms of causalities and conflicts on
unfoldings of 1-safe Petri nets. In [13], the authors work on the minimal solutions for enforcing
noninterference on bounded Petri nets.
The work presented in [14] and [15] distinguish two kinds of information flow in Petri nets,
i.e. positive and negative information flow. The first one arises when the occurrence of a low
transition gives information about the occurrence of a high transition whereas the second arises
when the occurrence of a low transition allows one to deduce the non-occurrence of a high
transition. The authors introduce two families of relations, namely reveals and excludes, to
model positive and negative information flow among transitions of a Petri net. Reveals relation
was originally defined for the events of an occurrence net by Haar in [16] to be used in fault
diagnosis [17]. The reveals relation was then redefined for the transitions of Petri nets in [14, 15]
and was used, together with its variants and excludes relation, to define various noninterference
properties for distributed systems modelled with Petri nets.
In [18], a formal basis is provided for modelling and analysing information flow with 1-safe
free-choice Petri nets by computing reveals and excludes relations. The authors introduce a
notion of maximal-step computation tree, which represents the behaviour of a 1-safe free-choice
net under maximal-step semantics. They define a finite prefix, named full prefix, on the tree
and provide methods for computing reveals and excludes relations on the prefix.
In this paper, we extend the results in [18] to bounded equal-conflict Petri nets, which are
a weighted generalisation of (extended) free-choice nets and were introduced in [19]. We
introduce two new parametric reveals relations and provide methods for computing them on
bounded equal-conflict PT systems for positive information flow.
The paper is organised as follows. Section 2 provides the necessary background on Petri
nets. Section 3 recalls some definitions of reveals relation in the context of information flow
and introduces new parametric variants. Section 4 formalises maximal-step computation tree
and its full prefix for bounded equal-conflict PT systems and provides methods for computing
reveals relations for positive information-flow analysis on full prefix. Section 5 concludes the
paper and discusses some possible future work.
2. Petri nets
In this section we recall basic definitions concerning Petri nets and net unfoldings that will be
useful in the rest of the paper, see also [20, 21, 22, 23, 24].
A net is a triple 𝑁 = (𝑃, 𝑇, 𝐹 ), where 𝑃 and 𝑇 are disjoint sets. The elements of 𝑃 are
called places and are represented by circles, the elements of 𝑇 are called transitions and are
represented by squares, 𝐹 ⊆ (𝑃 × 𝑇 ) ∪ (𝑇 × 𝑃 ) is the flow relation, represented by directed
arcs. The pre-set of an element 𝑥 ∈ 𝑃 ∪ 𝑇 is the set ∙ 𝑥 = {𝑦 ∈ 𝑃 ∪ 𝑇 : (𝑦, 𝑥) ∈ 𝐹 }; the
post-set of 𝑥 is the set 𝑥∙ = {𝑦 ∈ 𝑃 ∪ 𝑇 : (𝑥, 𝑦) ∈ 𝐹 }. Let 𝑋 ⊆ 𝑃 ∪ 𝑇 be a subset of
elements, its pre-set is defined as ∙ 𝑋 = {𝑦 ∈ 𝑃 ∪ 𝑇 : ∃𝑥 ∈ 𝑋 : (𝑦, 𝑥) ∈ 𝐹 }, and its post-set as
𝑋 ∙ = {𝑦 ∈ 𝑃 ∪ 𝑇 : ∃𝑥 ∈ 𝑋 : (𝑥, 𝑦) ∈ 𝐹 }.
A net (𝑃, 𝑇, 𝐹 ) is a subnet of another net (𝑃 ′ , 𝑇 ′ , 𝐹 ′ ) if 𝑃 ⊆ 𝑃 ′ , 𝑇 ⊆ 𝑇 ′ and 𝐹 is the
restriction of 𝐹 ′ to (𝑃 × 𝑇 ) ∪ (𝑇 × 𝑃 ).
61
�Federica Adobbati et al. CEUR Workshop Proceedings 60–79
A net is finite if 𝑃 ∪ 𝑇 is finite, and infinite otherwise. A net is T-restricted if for any 𝑡 ∈ 𝑇 ,
∙ 𝑡 ̸= ∅ and 𝑡∙ ̸= ∅.
A Place Transition (PT) system, Σ = (𝑃, 𝑇, 𝐹, 𝑊, 𝑚0 ) is defined by a finite net (𝑃, 𝑇, 𝐹 ),
a map 𝑊 : 𝐹 → N which assigns a positive weight to each arc, and an initial marking
𝑚0 : 𝑃 → N. We write 𝑊 (𝑥, 𝑦) = 0 when (𝑥, 𝑦) ∈ / 𝐹 . The tuple (𝑃, 𝑇, 𝐹, 𝑊 ) will be called
PT net. In graphical representations, arcs are inscribed by their weights, if the weight is greater
than one, and markings 𝑚 are represented by 𝑚(𝑝) dots, called tokens, in each place 𝑝.
Let Σ be a PT net and 𝑚 : 𝑃 → N be a marking. A transition 𝑡 is enabled at 𝑚, denoted
𝑚[𝑡⟩, if, for any 𝑝 ∈ 𝑃 , 𝑚(𝑝) ≥ 𝑊 (𝑝, 𝑡). Let 𝑡 be enabled at 𝑚; then, 𝑡 can occur (or fire) in
𝑚 producing the new marking 𝑚′ , denoted 𝑚[𝑡⟩𝑚′ and defined as follows: ∀𝑝 ∈ 𝑃 , 𝑚′ (𝑝) =
𝑚(𝑝) − 𝑊 (𝑝, 𝑡) + 𝑊 (𝑡, 𝑝).
A finite or infinite sequence of transitions 𝑡1 𝑡2 ... 𝑡𝑘 ... is an occurrence sequence enabled
at 𝑚0 , denoted 𝑚0 [𝑡1 ... 𝑡𝑘 ... ⟩, if there are intermediate markings 𝑚1 ... 𝑚𝑘 ... such that:
𝑚0 [𝑡1 ⟩𝑚1 ... [𝑡𝑘 ⟩𝑚𝑘 ....
Let 𝑚 be a marking of Σ, the set [𝑚⟩ is the smallest set of markings such that: 𝑚 ∈ [𝑚⟩, and
if 𝑚′ ∈ [𝑚⟩ and 𝑚′ [𝑡⟩𝑚′′ , then 𝑚′′ ∈ [𝑚⟩. The set [𝑚0 ⟩ is the set of reachable markings of Σ.
A multiset of transitions 𝑈 ∑︀: 𝑇 → N is concurrently enabled at 𝑚 ∈ [𝑚0 ⟩, denoted 𝑚[𝑈 ⟩,
and called step, iff ∀𝑝 ∈ 𝑃 , 𝑡∈𝑇 𝑈 (𝑡) · 𝑊 (𝑝, 𝑡) ≤ 𝑚(𝑝); if 𝑈 is enabled at 𝑚, it can occur
producing ∑︀ the new marking 𝑚 ∑︀
′ , denoted 𝑚[𝑈 ⟩𝑚′ and defined as follows: ∀𝑝 ∈ 𝑃 , 𝑚′ (𝑝) =
𝑚(𝑝) − 𝑡∈𝑇 𝑈 (𝑡) · 𝑊 (𝑝, 𝑡) + 𝑡∈𝑇 𝑈 (𝑡) · 𝑊 (𝑡, 𝑝).
A multiset 𝑈∑︀ : 𝑇 → N is a maximal-step ′at 𝑚 ∈ [𝑚0 ⟩ iff 𝑚[𝑈 ⟩ and ∀𝑡 ∈ 𝑇 , ∃𝑝 ∈ 𝑃 such
′
that: 𝑚(𝑝) < 𝑡∈𝑇 𝑈 (𝑡) · 𝑊 (𝑝, 𝑡) + 𝑊 (𝑝, 𝑡 ).
Analogously to occurrence sequences, a finite or infinite sequence of steps (or maximal-
steps) 𝑈1 𝑈2 ...𝑈𝑘 ... is a step sequence (or a maximal-step sequence) enabled at 𝑚0 , denoted
𝑚0 [𝑈1 ...𝑈𝑘 ...⟩, if there are intermediate markings 𝑚1 ...𝑚𝑘 ... such that: 𝑚0 [𝑈1 ⟩𝑚1 ...[𝑈𝑘 ⟩𝑚𝑘 ....
Two transitions 𝑡1 and 𝑡2 are in conflict at a marking 𝑚 ∈ [𝑚0 ⟩ iff they are both enabled
at 𝑚, 𝑚[𝑡1 ⟩ and 𝑚[𝑡2 ⟩, however they are not concurrently enabled at 𝑚, ¬(𝑚[{𝑡1 , 𝑡2 }⟩), the
occurrence of one of them disables the other one.
In some situations concurrency and conflicts overlap in such a way that it is not clear if in
the execution of concurrent transitions a conflict has been solved or not. This is a so called
situation of ‘confusion’ which has been introduced by C.A. Petri and discussed in several papers
as for example in [25, 26], and which can be formalised in the following way. Let 𝑚 ∈ [𝑚0 ⟩,
𝑡1 , 𝑡2 ∈ 𝑇 such that: 𝑚[{𝑡1 , 𝑡2 }⟩, then (𝑚, 𝑡1 , 𝑡2 ) is a confusion at 𝑚 if cfl(𝑡1 , 𝑚) ̸= cfl(𝑡1 , 𝑚2 ),
where cfl(𝑡1 , 𝑚) = {𝑡′ ∈ 𝑇 : 𝑚[𝑡′ ⟩ ∧ ¬(𝑚[{𝑡1 , 𝑡′ }⟩)}, and 𝑚2 is such that 𝑚[𝑡2 ⟩𝑚2 . In Fig. 1,
the two main situations of confusion are illustrated, namely asymmetric confusion, on the left
side, and symmetric confusion, on the right side. In the particular case of asymmetric confusion,
the occurrence of the step {𝑡1 , 𝑡2 } hides the information whether the conflict in-between 𝑡1 and
𝑡3 has been solved or not; moreover, in this case, maximal-step semantics is not equivalent to
step semantics, since transition 𝑡3 will never occur in any sequence of maximal steps, whereas
the step sequence 𝑚0 [{𝑡2 }⟩{𝑏1 , 𝑏3 , 𝑏4 }[{𝑡3 }⟩ may occur.
The relation between step semantics and maximal-step semantics has been studied for example
in [27], where it is shown that they are equivalent in the case of systems without asymmetric
confusion.
A general class of nets in which confusion cannot arise is the class of equal-conflict PT nets,
62
�Federica Adobbati et al. CEUR Workshop Proceedings 60–79
Figure 1: Asymmetric confusion (on the left) and symmetric confusion (on the right side).
studied by various authors, see for example [19]. A PT net (𝑃, 𝑇, 𝐹, 𝑊 ) is an equal-conflict PT
net, also called EC PT net, iff ∀𝑡, 𝑡′ ∈ 𝑇 , ∙ 𝑡∩∙ 𝑡′ ̸= ∅ ⇒ (∙ 𝑡 = ∙ 𝑡′ ∧ ∀𝑝 ∈ ∙ 𝑡, 𝑊 (𝑝, 𝑡) = 𝑊 (𝑝, 𝑡′ )).
From the definition, it follows that in EC PT systems, if two transitions share a pre-place,
then any given marking enables either both transitions or neither. All the figures in this paper,
except for Fig. 1, provide examples of EC PT systems.
A PT system Σ is bounded if there is a finite number 𝑛 such that: for any reachable marking
𝑚 ∈ [𝑚0 ⟩ and for any place 𝑝, 𝑚(𝑝) ≤ 𝑛. If Σ is bounded, its set of reachable markings [𝑚0 ⟩
is finite. A marking 𝑚 is a deadlock if no transition is enabled in 𝑚. Σ is 1-live if for all 𝑡 ∈ 𝑇
there exists 𝑚 ∈ [𝑚0 ⟩ such that 𝑚[𝑡⟩.
In the rest of the paper, we will consider finite, bounded, and 1-live PT systems, whose
underlying nets are T-restricted.
We now introduce two technical relations that will be useful to define the partial order
semantics of PT systems. The ≺ relation on the elements of a net 𝑁 is the transitive closure of
𝐹 and ⪯ is the reflexive closure of ≺. Let 𝑥, 𝑦 ∈ 𝑃 ∪ 𝑇 , 𝑥#𝑦, iff there exist 𝑡1 , 𝑡2 ∈ 𝑇 : 𝑡1 ̸=
𝑡2 , 𝑡1 ⪯ 𝑥, 𝑡2 ⪯ 𝑦 and there exists 𝑝 ∈ ∙ 𝑡1 ∩ ∙ 𝑡2 .
A net 𝑁 = (𝐵, 𝐸, 𝐹 ), possibly infinite, is an occurrence net if the following restrictions hold:
1. ∀𝑥 ∈ 𝐵 ∪ 𝐸 : ¬(𝑥 ≺ 𝑥)
2. ∀𝑥 ∈ 𝐵 ∪ 𝐸 : ¬(𝑥#𝑥)
3. ∀𝑒 ∈ 𝐸 : {𝑥 ∈ 𝐵 ∪ 𝐸 | 𝑥 ⪯ 𝑒} is finite
4. ∀𝑏 ∈ 𝐵 : |∙ 𝑏| ≤ 1
In an occurrence net, the elements of 𝐵 are called conditions and the elements of 𝐸 are called
events; the transitive and reflexive closure of 𝐹 , ⪯, forms a partial order. The set of minimal
elements of an occurrence net 𝑁 with respect to ⪯ will be denoted by min(𝑁 ). Since we only
consider T-restricted nets the elements of min(𝑁 ) are conditions.
A configuration of an occurrence net 𝑁 = (𝐵, 𝐸, 𝐹 ) is a, possibly infinite, set of events
𝐶 ⊆ 𝐸 which is causally closed (for every 𝑒 ∈ 𝐶, 𝑒′ ⪯ 𝑒 ⇒ 𝑒′ ∈ 𝐶) and free of conflicts
(∀𝑒1 , 𝑒2 ∈ 𝐶, ¬(𝑒1 #𝑒2 )). 𝐶 is maximal if it is maximal with respect to set inclusion.
On the elements of an occurrence net the relation of concurrency, co, is defined as follows:
let 𝑥, 𝑦 ∈ 𝑃 ∪ 𝑇 , 𝑥 co 𝑦, if neither (𝑥 ≺ 𝑦) nor (𝑦 ≺ 𝑥) nor (𝑥#𝑦).
63
�Federica Adobbati et al. CEUR Workshop Proceedings 60–79
A B-cut of 𝑁 is a maximal set of pairwise concurrent elements of 𝐵, and can be intuitively
seen as a global state of the net in a certain moment. An E-cut of 𝑁 is a maximal set of pairwise
concurrent elements of 𝐸, that corresponds to a maximal step on 𝑁 .
A branching process of a bounded 1-live PT system Σ = (𝑃, 𝑇, 𝐹, 𝑊, 𝑚0 ), whose underlying
net is T-restricted, is a pair (𝑂, 𝜆), where 𝑂 = (𝐵, 𝐸, 𝐹 ′ ) is an occurrence net, and 𝜆 is a map
from 𝐵 ∪ 𝐸 to 𝑃 ∪ 𝑇 such that:
1. 𝜆(𝐵) ⊆ 𝑃 ; 𝜆(𝐸) ⊆ 𝑇
2. ∀𝑒 ∈ 𝐸, ∀𝑝 ∈ 𝑃 , 𝑊 (𝑝, 𝜆(𝑒)) = |𝜆−1 (𝑝) ∩ ∙ 𝑒| and 𝑊 (𝜆(𝑒), 𝑝) = |𝜆−1 (𝑝) ∩ 𝑒∙ |
3. ∀𝑝 ∈ 𝑃 𝑚0 (𝑝) = |𝜆−1 (𝑝) ∩ min(𝑂)|
4. ∀𝑥, 𝑦 ∈ 𝐸, if ∙ 𝑥 = ∙ 𝑦 and 𝜆(𝑥) = 𝜆(𝑦), then 𝑥 = 𝑦
We extend the definition of 𝜆 to the set of configurations of the branching process: for each
configuration 𝐶, 𝜆(𝐶) is the multiset of the transitions ∑︀ whose occurrences are recorded in
𝐶 and is called the footprint of 𝐶; formally 𝜆(𝐶) = 𝑒𝑖 ∈𝐶 𝜆(𝑒𝑖 ). If a transition 𝑡 belongs to
the support set of 𝜆(𝐶), i.e.: at least an occurrence of 𝑡 is in 𝐶, 𝜆(𝐶)(𝑡) ≥ 1, then we use the
notation 𝑡 ∈ 𝜆(𝐶). If 𝐶 is infinite, it records the infinite occurrence of some transitions, and the
multiset 𝜆(𝐶) is such that the multiplicity of those transitions is infinite, whereas its support
set is obviously finite, being a subset of 𝑇 .
A branching process (𝑂1 , 𝜆1 ) is a prefix of a branching process (𝑂2 , 𝜆2 ) if 𝑂1 is a subnet
of 𝑂2 containing all minimal elements (min(𝑂2 )) and such that: if 𝑒 ∈ 𝐸1 and (𝑏, 𝑒) ∈ 𝐹2 or
(𝑒, 𝑏) ∈ 𝐹2 then 𝑏 ∈ 𝐵1 ; if 𝑏 ∈ 𝐵1 and (𝑒, 𝑏) ∈ 𝐹2 then 𝑒 ∈ 𝐸1 ; and 𝜆1 is the restriction of 𝜆2
to 𝐵1 ∪ 𝐸1 .
Any finite PT system Σ = (𝑃, 𝑇, 𝐹, 𝑊, 𝑚0 ) has a unique branching process which is maximal
with respect to the prefix relation. This maximal branching process, called the unfolding of Σ,
will be denoted by Unf(Σ) = ((𝐵, 𝐸, 𝐹 ′ ), 𝜆), where 𝜆 is the map from (𝐵, 𝐸, 𝐹 ′ ) to (𝑃, 𝑇, 𝐹 ).
A run records a possible non sequential behaviour of the system, it is a branching process,
whose occurrence net is free of conflicts, i.e., its set of events is a configuration. A run is
maximal if the corresponding configuration is maximal. Let 𝜌 be a run, its footprint 𝜆(𝜌) is
equal to the footprint of its set of events.
Example 1. Figure 2 represents an equal-conflict PT system Σ and a branching process, which
is a prefix of the unfolding of Σ. A maximal run of the branching process is the labelled subnet
whose elements are grey, the set of its events is the configuration 𝐶 = {𝑒1 , 𝑒2 , 𝑒3 , 𝑒4 , 𝑒5 , 𝑒6 }, The
footprint of 𝐶 is the multiset 𝜆(𝐶) = {𝑎, 𝑒, 𝑓, 𝑔, 2.ℎ}.
3. Formal relations for the analysis of information flow
In [14] and [15], a family of relations, i.e., reveals and its variants, were introduced to express
information flow among transitions of a Petri net. These relations were then used to define
several noninterference properties for specification of security requirements. In this section,
after recalling the existing reveals relations we introduce two new variants which are parametric.
These new relations give the opportunity to specify security requirements of a distributed system
in a way that is more tailored to the needs of the system.
64
�Federica Adobbati et al. CEUR Workshop Proceedings 60–79
Figure 2: A bounded equal-conflict PT system and a branching process of it (a prefix of Unf(Σ)).
Let Σ = (𝑃, 𝑇, 𝐹, 𝑊, 𝑚0 ) be a PT system (bounded, 1-live PT system with T-restricted un-
derlying net) and Unf(Σ) = ((𝐵, 𝐸, 𝐹 ), 𝜆) be its unfolding. In the following, 𝐶𝑚𝑎𝑥 will denote
the set of all maximal configurations of Unf(Σ). The set of events of Unf(Σ) corresponding to
a specific transition 𝑡 of a given PT system Σ will be denoted by 𝐸𝑡 = {𝑒 ∈ 𝐸 : 𝜆(𝑒) = 𝑡}.
We will assume progress of the system, i.e., an enabled transition either fires or gets disabled
by another transition in conflict with it; the set of configurations satisfying this assumption
coincides with 𝐶𝑚𝑎𝑥 .
The reveals relation was originally introduced for events of an occurrence net in [16], and in
[17] it was applied in the field of fault diagnosis. In [15], reveals relation was redefined for the
transitions of a 1-live Petri net in order to express positive information flow: transition 𝑡1 reveals
transition 𝑡2 if each maximal configuration which contains an occurrence of 𝑡1 also contains at
least one occurrence of 𝑡2 . This means that the occurrence of 𝑡1 implies the occurrence of 𝑡2 ,
either in the past or in the future. Hence, if a low transition reveals a high transition, this might
cause a positive information flow endangering the security of the system.
Definition 1. Let 𝑡1 , 𝑡2 ∈ 𝑇 be two transitions; 𝑡1 reveals 𝑡2 , denoted 𝑡1 ▷ 𝑡2 , iff ∀ 𝐶 ∈
𝐶𝑚𝑎𝑥 𝑡1 ∈ 𝜆(𝐶) =⇒ 𝑡2 ∈ 𝜆(𝐶).
Since we consider 1-live nets, there is at least one maximal configuration in which 𝑡1 occurs.
If there exists a maximal configuration in which 𝑡1 occurs and 𝑡2 does not occur, then 𝑡1 ̸▷ 𝑡2 .
Sometimes, even if a transition alone does not give much information about the occurrence of
another transition, a set of transitions together might imply the occurrence of some transitions
in another set. This relation was originally defined for the events of an occurrence net in
[28], and later in [15] was redefined for the transitions of a Petri net in order to be used in
information-flow analysis. Set 𝑋 extended reveals set 𝑌 if each maximal configuration which
65
�Federica Adobbati et al. CEUR Workshop Proceedings 60–79
has all the transitions of 𝑋 also has at least one transition of 𝑌 . It can violate the security of a
system if a group of low transitions extended reveals a group of high transitions.
Definition 2. Let 𝑋, 𝑌 ⊆ 𝑇 . If there is at least one maximal configuration in which all transi-
tions of 𝑋 appear, then we say 𝑋 extended reveals 𝑌 , denoted 𝑋 _ 𝑌 , iff ∀ 𝐶 ∈ 𝐶𝑚𝑎𝑥
⋀︁ ⋁︁
𝑡𝑖 ∈ 𝜆(𝐶) =⇒ 𝑡𝑗 ∈ 𝜆(𝐶).
𝑡𝑖 ∈𝑋 𝑡𝑗 ∈𝑌
Note that 𝑋 _ 𝑌 is not defined if the transitions of 𝑋 never appear together.
Remark 1. Extended reveals relation between two singletons coincides with reveals relation.
The next relation takes the repeated occurrences of a transition into account. In some cases,
the occurrence of a transition does not give information while several occurrences of the
transition imply the occurrence of another transition. This relation was defined in [15] without
progress assumption, thus considering all configurations. Here, we alter the definition for the
setting in which maximal configurations are considered. We say that 𝑡1 𝑛-repeated reveals
𝑡2 if each maximal configuration which has at least 𝑛 occurrences of 𝑡1 , also has at least one
occurrence of 𝑡2 . It can violate the security of a system if a number of occurrences of a low
transition imply occurrence of a high transition.
Definition 3. Let 𝑡1 , 𝑡2 ∈ 𝑇 be two transitions, and 𝐶𝑚𝑎𝑥 be the set of all maximal configurations
of Unf(Σ). Let 𝑛 be a positive integer. If there exists a maximal configuration in which 𝑡1 occurs
at least 𝑛 times, then we say 𝑡1 𝑛-repeated reveals 𝑡2 , denoted 𝑛.𝑡1 ▷ 𝑡2 , iff
∀𝐶 ∈ 𝐶𝑚𝑎𝑥 |𝐶 ∩ 𝐸𝑡1 | ≥ 𝑛 =⇒ 𝐶 ∩ 𝐸𝑡2 ̸= ∅.
Note that 𝑛-repeated reveals is not defined if there is no maximal configuration in which 𝑡1
occurs at least 𝑛 times.
The following statements are direct consequences of Def. 3.
Remark 2. Reveals relation (as in Def. 1) coincides with 1-repeated reveals.
Remark 3. If 𝑛.𝑡1 ▷ 𝑡2 and ∃𝐶 ∈ 𝐶𝑚𝑎𝑥 such that |𝐶 ∩ 𝐸𝑡1 | ≥ 𝑛 + 1 then (𝑛 + 1).𝑡1 ▷ 𝑡2 .
Remark 4. 𝑛.𝑡1 ̸▷ 𝑡2 =⇒ (𝑛 − 1).𝑡1 ̸▷ 𝑡2 .
Example 2. A bounded equal-conflict PT system is illustrated in Fig. 3. In this system, the occur-
rence of 𝑏 implies the occurrence of 𝑎 since every maximal configuration which has 𝑏 also has 𝑎.
However, vice versa is not correct since there is a maximal configuration in which 𝑎 occurs without
𝑏. Thus, 𝑏 ▷ 𝑎 and 𝑎 ̸▷ 𝑏. Some other reveals relations are 𝑐 ▷ 𝑑, 𝑑 ▷ 𝑐, 𝑓 ▷ ℎ, ℎ ▷ 𝑓 , 𝑑 ▷ 𝑎 and
ℎ ▷ 𝑒.
Examples of extended reveals are as follows. The occurrence of 𝑐 alone or 𝑓 alone is not sufficient
to say something about the occurrence of 𝑘, but the occurrence of 𝑐 and 𝑓 together implies the
occurrence of 𝑘, i.e., {𝑐, 𝑓 } _ {𝑘}. Although 𝑎 ̸▷ 𝑐 and 𝑎 ̸▷ 𝑏, the occurrence of 𝑎 implies the
occurrence of either 𝑏 or 𝑐, i.e., {𝑎} _ {𝑏, 𝑐}. Similarly, {𝑒} _ {𝑓, 𝑔}.
Examples of repeated reveals are as follows. Only one occurrence of 𝑎 does not give informa-
tion about 𝑑, but if 𝑎 occurs twice, this implies the occurrence of 𝑑, i.e., 2.𝑎 ▷ 𝑑. Similarly, two
occurrences of 𝑒 imply the occurrence of ℎ, i.e., 2.𝑒 ▷ ℎ.
66
�Federica Adobbati et al. CEUR Workshop Proceedings 60–79
Figure 3: A bounded equal-conflict PT system.
The following variant of reveals relation is parametric and it generalises all the variants above.
This relation is more expressive and allows one to specify the expected security requirements
in a more tailored fashion.
Definition 4. Let 𝑖, 𝑘 ≥ 1 and {𝑛1 , ..., 𝑛𝑘 } be positive integers. Let {𝑡1 , ..., 𝑡𝑘 }, 𝑌 ⊆ 𝑇 . If there
is at least one maximal configuration in which each transition 𝑡𝑖 of {𝑡1 , ..., 𝑡𝑘 } occurs at least 𝑛𝑖
times, then we say {𝑛1 .𝑡1 , ..., 𝑛𝑘 .𝑡𝑘 } extended-repeated reveals 𝑌 denoted {𝑛1 .𝑡1 , ..., 𝑛𝑘 .𝑡𝑘 } _
𝑌 iff ∀ 𝐶 ∈ 𝐶𝑚𝑎𝑥
⋀︁ ⋁︁
(|𝐶 ∩ 𝐸𝑡𝑖 | ≥ 𝑛𝑖 ) =⇒ (𝐶 ∩ 𝐸𝑡 ̸= ∅).
𝑡𝑖 ∈{𝑡1 ,...,𝑡𝑘 } 𝑡∈𝑌
Note that {𝑛1 .𝑡1 , ..., 𝑛𝑘 .𝑡𝑘 } extended-repeated reveals 𝑌 is not defined if there is no maximal
configuration in which each transition 𝑡𝑖 of {𝑡1 , ..., 𝑡𝑘 } occurs at least 𝑛𝑖 times.
Remark 5. Reveals, extended reveals and repeated reveals can be expressed by Def. 4.
𝑡1 ▷ 𝑡2 ⇐⇒ {1.𝑡1 } _ {𝑡2 },
{𝑡1 , 𝑡2 } _ {𝑡3 , 𝑡4 } ⇐⇒ {1.𝑡1 , 1.𝑡2 } _ {𝑡3 , 𝑡4 },
𝑛.𝑡1 ▷ 𝑡2 ⇐⇒ {𝑛.𝑡1 } _ {𝑡2 }.
Example 3. In the system net illustrated in Fig. 3, let us examine the relation between the transi-
tions 𝑎, 𝑒 and 𝑘. Neither 𝑎 nor 𝑒 reveals 𝑘 alone. There is no extended reveals or repeated reveals
67
�Federica Adobbati et al. CEUR Workshop Proceedings 60–79
Figure 4: A bounded equal-conflict system.
relation between them either. However, there is still some information flow. Two occurrences of 𝑎
together with two occurrences of 𝑒 extended-repeated reveal 𝑘, i.e., {2.𝑎, 2.𝑒} _ {𝑘}. This might
cause a security violation in a system where the occurrence of 𝑘 is supposed to be a secret.
Let us consider a case in which the total number of occurrences of a set of transitions gives
information about another set of transitions. In other words, if the total number of occurrences
of the transitions in the first set is more than a certain number, this implies that at least one
transition of the second set must have occurred or will occur inevitably. The next relation
defines such situation. If a set of low transitions collectively reveal some high transitions this
might cause a security violation.
Definition 5. Let 𝑛 ≥ 1 and 𝑋, 𝑌 ⊆ 𝑇 . If there is at least one maximal configuration in which
the total number of occurrences of the transitions in set 𝑋 is at least 𝑛, then we say 𝑋 𝑛-collective
reveals 𝑌 , denoted 𝑛.𝑋 _ 𝑌 , iff ∀ 𝐶 ∈ 𝐶𝑚𝑎𝑥
∑︁ ⋁︁
|𝐶 ∩ 𝐸𝑡 | ≥ 𝑛 =⇒ (𝐶 ∩ 𝐸𝑡 ̸= ∅).
𝑡∈𝑋 𝑡∈𝑌
Note that 𝑋 𝑛-collective reveals 𝑌 is not defined if there is no maximal configuration in
which the total number of occurrences of the transitions in set 𝑋 is at least 𝑛.
Remark 6. Reveals and repeated reveals can be expressed by Def. 5.
𝑡1 ▷ 𝑡2 ⇐⇒ 1.{𝑡1 } _ {𝑡2 },
𝑛.𝑡1 ▷ 𝑡2 ⇐⇒ 𝑛.{𝑡1 } _ {𝑡2 }.
Example 4. In the net in Fig. 4, if the total number of occurrences of 𝑑 and 𝑒 is at least 3, this
implies the occurrence of ℎ, i.e., 3.{𝑑, 𝑒} _ {ℎ}.
In the net in Fig. 5, if the total number of occurrences of 𝑏 and 𝑐 is at least 2, this implies
occurrence of either 𝑒 or 𝑓 , i.e., 2.{𝑏, 𝑐} _ {𝑒, 𝑓 }.
68
�Federica Adobbati et al. CEUR Workshop Proceedings 60–79
Figure 5: A bounded equal-conflict system.
4. Computing information flow on bounded equal-conflict nets
In this section, we consider bounded equal-conflict PT systems and show how to compute the
relations introduced in Sec. 3 by exploiting the equal-conflict structure of the net.
The relations in Sec. 3 consider the unfolding of a system Unf(Σ) and analyse their max-
imal configurations checking footprints, the multisets of transitions occurring in maximal
configurations. Here, we consider maximal-step semantics, since, as recalled in Sec. 2, it is
equivalent to step semantics in the case of equal-conflict systems, where there is no asymmetric
confusion [27].
Moreover, thanks to the results in [22], it is possible to show a strict relation between
footprints of step sequences of a system Σ and footprints of configurations of Unf(Σ).
In fact, in [22], the authors studied the relationships between various classes of non-sequential
processes (runs of an unfolding), occurrence sequences and step sequences. They showed that,
in the special case of countable, T-restricted nets of finite synchronisation (i.e., where any
transition has a finite set of pre- and post-places) with finite initial marking, and then also in
the case of the nets here considered, the distinction between occurrence sequences and step
sequences disappears. Moreover, for the same class of nets, they showed that it is possible
to consider equivalence relations both on the set of occurrence sequences and on the set of
processes such that there is a bijection between the induced equivalence classes.
In the case of occurrence sequences, the equivalence relation abstracts w.r.t. the total order
arbitrarily chosen when transitions are concurrent; in the case of processes, the equivalence
abstracts from the distinction among several tokens on the same place.
From the construction of the equivalence classes both of occurrence sequences and of pro-
cesses, it is possible to observe that the elements in each class have the same footprints, i.e., the
same multiset of transitions which can be observed through the corresponding behaviour, and
that elements of an equivalence class in bijective correspondence with a class of the other sort
69
�Federica Adobbati et al. CEUR Workshop Proceedings 60–79
have the same footprint too.
Given this correspondence, in the next subsections we introduce a tree, whose paths record
the set of maximal-step sequences of Σ, and show that a particular prefix of this tree is sufficient
to compute the reveals relations. Note that since we are interested in maximal configurations,
we cannot directly work on the marking graph of the net, since its maximal paths are not
necessarily associated with maximal configurations in the unfolding.
The tree and its prefix were first introduced in [18] for 1-safe free-choice Petri nets, here we
adapt them to the class of bounded equal-conflict PT systems, to study their information flow.
4.1. The tree of maximal-step computations
Definition 6. Let Σ = (𝑃, 𝑇, 𝐹, 𝑊, 𝑚0 ) be a bounded equal-conflict PT system. We define the
tree of maximal-step computations, denoted as msct(Σ) or msc-tree, as follows.
• Each node of the tree is labelled with a reachable marking.
• The root of the tree is labelled with the initial marking 𝑚0 .
• From each node labelled with marking 𝑚, for each maximal step 𝑈 enabled at 𝑚, there is
an outgoing arc, labelled with 𝑈 , and leading to a node labelled with 𝑚′ , where 𝑚[𝑈 ⟩𝑚′ .
A path in msct(Σ) is a sequence 𝜋 = 𝑣1 𝑈1 𝑣2 𝑈2 · · · , such that, for each 𝑖, there is an arc from
𝑣𝑖 to 𝑣𝑖+1 , labelled with 𝑈𝑖 . A path is initial if it starts in the root of the tree. A path can be
either finite or infinite. Let 𝑣, 𝑟 be two nodes on the same path 𝜋, 𝑣 < 𝑟 iff 𝑣 is closer to the
root than 𝑟. The footprint of the path 𝜋 is the (multiset) union of all steps occurring in 𝜋.
We define an inclusion relation between footprints: let 𝜋1 and 𝜋2 be paths on msct(Σ);
then 𝜆(𝜋1 ) ⊆ 𝜆(𝜋2 ) iff ∀𝑡 ∈ 𝑇 , 𝜆(𝜋1 )(𝑡) ≤ 𝜆(𝜋2 )(𝑡), i.e., for each transition 𝑡, the number of
occurrences in the footprint of 𝜋1 is less than or equal to that in the footprint of 𝜋2 .
To simplify the notation, we will write 𝑡 ∈ 𝜆(𝜋) when 𝜆(𝜋)(𝑡) ≥ 1, namely when 𝑡 occurs in
some step of path 𝜋.
From the considerations in the first part of Sec. 4, each maximal path in msct(Σ) can be
associated to at least one maximal configuration of the unfolding, with the same footprint; and
vice versa, each configuration of Unf(Σ) is represented in the msct(Σ) by a path with the same
footprint.
Example 5. Fig. 6 represents a PT system and a prefix of its maximal computation tree. In the
tree, the markings are represented as multisets of places. In each marking, if a place appears only
once, its multiplicity is omitted; if a place 𝑝 appears 𝑛 times, for the sake of clarity in the figure, it
is denoted with 𝑝𝑛 . For example, the initial marking of the net is represented with 1, 62 . Note that
the PT system is the same of Ex. 1, and in Fig. 2 a branching process of Σ is shown.
Let 𝑉 = {𝑣1 , 𝑣2 , ..., 𝑣𝑛 , ...} be the set of nodes in msct(Σ), and 𝜇 : 𝑉 → [𝑚0 ⟩ the labelling
function, mapping to each node the corresponding marking. Two nodes 𝑣1 and 𝑣2 are equivalent
if 𝜇(𝑣1 ) = 𝜇(𝑣2 ). Let 𝜋1 = 𝑣1 𝑈1 𝑣2 𝑈2 ...𝑣𝑛 𝑈𝑛 ... and 𝜋2 = 𝑣1′ 𝑈1′ 𝑣2′ 𝑈2′ ...𝑣𝑛′ 𝑈𝑛′ ... be two paths on
the tree, where the elements 𝑣𝑗 represent nodes of the tree, and the elements 𝑈𝑗 represent the
labels of the arcs. The path 𝜋1 is isomorphic to the path 𝜋2 (in symbols 𝜋1 ≃ 𝜋2 ) iff for each 𝑗,
𝜇(𝑣𝑗 ) = 𝜇(𝑣𝑗′ ), and 𝜆(𝑈𝑗 ) = 𝜆(𝑈𝑗′ ). Finally, two subtrees 𝐿1 and 𝐿2 are isomorphic iff for each
maximal path 𝜋 on 𝐿1 there is a maximal path 𝜋 ′ in 𝐿2 such that 𝜋 ≃ 𝜋 ′ , and vice versa.
70
�Federica Adobbati et al. CEUR Workshop Proceedings 60–79
Figure 6: A bounded equal-conflict PT system and a prefix of its associated maximal-step computation
tree.
Let 𝜋 be a maximal path on the tree, and 𝑣𝑛 one of its nodes. We denote with ↓ 𝜋(𝑣𝑛 ) the
path from the root to 𝑣𝑛 , and with ↑ 𝜋(𝑣𝑛 ) the subpath 𝜋 starting from 𝑣𝑛 .
Lemma 1. Let 𝑣𝑛 and 𝑣𝑘 be two nodes of an msc-tree such that 𝜇(𝑣𝑛 ) = 𝜇(𝑣𝑘 ). The subtree with
𝑣𝑛 as root and the one with 𝑣𝑘 as root are isomorphic.
Proof. Since 𝜇(𝑣𝑛 ) = 𝜇(𝑣𝑘 ), the arcs leaving from 𝑣𝑛 and from 𝑣𝑘 have the same labels. Then,
by construction the children of 𝑣𝑛 are equivalent to the children of 𝑣𝑘 , and the same reasoning
can be applied to each of them.
On the maximal paths of the msc-tree, we can define a peeling operation as follows [18, 17].
Let 𝜋 = 𝑣1 𝑈1 𝑣2 𝑈2 · · · be a maximal path on the msc-tree, 𝑣𝑛 and 𝑣𝑘 be two nodes in 𝜋 with
𝑛 < 𝑘 and 𝜇(𝑣𝑛 ) = 𝜇(𝑣𝑘 ). Let 𝜋𝑛,𝑘 be the subpath between 𝑣𝑛+1 and 𝑣𝑘 . The peeling of 𝜋 with
respect to 𝜋𝑛,𝑘 is the path 𝜋 ′ =peel(𝜋, 𝜋𝑛,𝑘 ) such that ↓ (𝜋(𝑣𝑛 )) = ↓ (𝜋 ′ (𝑣𝑛 )), 𝜋𝑛,𝑘 is deleted
from 𝜋, and ↑ (𝜋(𝑣𝑘 )) is equivalent to ↑ (𝜋 ′ (𝑣𝑛 )). In words, peeling 𝜋 means to consider the
execution in which the cycle 𝜋𝑛,𝑘 has not been executed. The path 𝜋 ′ constructed in this way is
also maximal in the msc-tree.
4.2. The full prefix of the maximal-step computation tree
In this section we recall the definition of full prefix given in [18] and some results that will be
useful when presenting the algorithm.
71
�Federica Adobbati et al. CEUR Workshop Proceedings 60–79
Definition 7. Let Σ be a bounded equal-conflict PT system. The full prefix of msct (Σ), denoted
fp(Σ), is a labelled rooted tree defined by the following clauses.
1. The root of fp(Σ) is the root of msct (Σ).
2. Let 𝑣 be a node of fp(Σ). If there is no 𝑣 ′ such that 𝑣 ′ < 𝑣 and 𝜇(𝑣 ′ ) = 𝜇(𝑣), then all the
children of 𝑣 in the msct (Σ) are nodes in fp(Σ); otherwise 𝑣 is a leaf in fp(Σ).
Example 6. The tree in Fig. 6 is a full prefix. Each node is labelled with a marking, and each arc
is labelled with a multiset of transitions. The leaves are either deadlocks, and in this case they are
denoted with a black thick line, or repeated markings, and in this case the leaves are in the same
colour of the node that they repeat. Moreover, some nodes have a second label: in particular, the
leaves are labelled with 𝑙𝑖 , 𝑖 ∈ {1, ..., 8}, and, for each leaf corresponding to a repeated marking
labelled with 𝑙𝑖 , its repetition is labelled rep(𝑙𝑖 ).
The full prefix fp(Σ) is finite, since the length of a path cannot exceed the number of markings
of the net system, and every node has a finite number of children.
For each maximal path 𝜋 on 𝐿 = fp(Σ), we will denote with 𝑙(𝜋) the leaf of the path, and,
if 𝑙(𝜋) is not a deadlock, we will denote as rep(𝑙(𝜋)) the node preceding 𝑙(𝜋) and such that
𝜇(𝑙(𝜋)) = 𝜇(rep(𝑙(𝜋))). In addition, we will denote as 𝐿rep(𝑙(𝜋)) the subtree of 𝐿 with root
rep(𝑙(𝜋)).
Lemma 2. Let 𝜋 be a path on msct (Σ), and 𝑡 ∈ 𝑇 a transition. If 𝑛 ≤ 𝜆(𝜋)(𝑡), but 𝑡 ̸∈
𝜋 ∩ fp(Σ), then there is another path 𝜋 ′ ∈ msct (Σ) such that 𝜆(𝜋 ′ ) ⊆ 𝜆(𝜋), 𝑛 ≤ 𝜆(𝜋 ′ )(𝑡), and
𝑡 ∈ 𝜋 ′ ∩ fp(Σ).
Proof. Let 𝑙(𝜋1 ) be the leaf of 𝜋1 = 𝜋 ∩ fp(Σ) and rep(𝑙(𝜋1 )) its repetition in the prefix. We
can construct the run 𝜋1′ = 𝑝𝑒𝑒𝑙(𝜋, 𝜋rep(𝑙(𝜋1 )),𝑙(𝜋1 ) ). If 𝑡 ∈ 𝜋2 = 𝜋1′ ∩ fp(Σ) we can stop
the construction, otherwise we repeat the procedure by considering 𝑙(𝜋2 ). Since the distance
between the root and the first occurrence of 𝑡 is finite, and every step of the peeling reduces it,
after a finite number of peeling operations the thesis must be satisfied.
Let 𝜋 ′ be a maximal path on msct(Σ), and 𝜋 its prefix on fp(Σ). If 𝑙(𝜋) is not a deadlock,
there must be a prefix of 𝜋 ′ extending 𝜋 with a segment isomorphic to another segment in
fp(Σ) starting from rep(𝑙(𝜋)) and arriving to a leaf of fp(Σ). Let 𝜋1 be such a segment; we
denote with 𝜋 + 𝜋1 the prefix of 𝜋 ′ obtained by concatenating 𝜋 with a segment isomorphic to
𝜋1 . If 𝑙(𝜋1 ) is not a deadlock, then 𝜋 + 𝜋1 can be extended further by looking in fp(Σ) which
segments start from rep(𝑙(𝜋1 )). Among them, there must be a segment 𝜋2 such that 𝜋 + 𝜋1 can
be extended with a segment isomorphic to 𝜋2 , obtaining a longer prefix of 𝜋 ′ : 𝜋 + 𝜋1 + 𝜋2 .
Proceeding in this way, we can obtain an arbitrarily long prefix of 𝜋 ′ from fp(Σ).
4.3. An algorithm for the collective reveals relations
In this section, we propose an algorithm to compute the collective reveals relation, defined in
Def. 5, on a bounded equal-conflict PT system Σ, through the full prefix fp(Σ). Its pseudo-code
is presented in Algorithm 1. Since reveals (Def. 1) and repeated reveals (Def. 3) can be expressed
as special cases of collective reveals (see Remark 6), the algorithm allows to compute also
72
�Federica Adobbati et al. CEUR Workshop Proceedings 60–79
these relations. At the end of the section, we will discuss how to modify it to compute also
extended-repeated reveals (Def. 4).
Algorithm 1 takes as input the full prefix 𝐿 = fp(Σ), two sets of transitions, 𝑋 and 𝑌 ,
and a positive number 𝑛. If there is no path in the msct(Σ) with at least 𝑛 occurrences of
transitions of 𝑋, then the algorithm returns undefined. Otherwise, it returns true if 𝑛.𝑋 _ 𝑌 ,
false if 𝑛.𝑋 ̸_ 𝑌 . The main function of the algorithm is repex. The variable ‘Paths’ includes all
the prefixes of the paths of msct(Σ) that we need to check to verify the relation. Initially, it
includes all the paths in fp(Σ) with at least an occurrence of a transition of 𝑋 (this is justified by
Lemma 2). The variable ‘empty’ is true if a path with at least 𝑛 occurrences of transitions of 𝑋
has not been found, false otherwise. ‘Paths’ and ‘empty’ are the input arguments of the function
extendPaths. This function checks which input paths already include at least 𝑛 occurrences of
transitions of 𝑋, and, if it finds a path with 𝑛 occurrences of 𝑋 and none of 𝑌 , it sets the value
of ‘stop’ to true, and stops the execution. In this case, also the main function will stop, and
return false, since the path could be extended to a maximal path of msct(Σ) without adding any
new transition label. If the path has at least 𝑛 occurrences of 𝑋 and an occurrence in 𝑌 , then it
does not need to be elongated further, and the algorithm must continue with the analysis of the
other paths.
Let 𝜋 be a path with less than 𝑛 occurrences of 𝑋; then the algorithm needs to check which
extensions could be useful to add more occurrences of transitions of 𝑋. If 𝜋 ends with a deadlock,
it is not possible to extend it further, and since there are no 𝑛 occurrences of 𝑋 we are not
interested in it. Otherwise, rep(𝑙(𝜋)) is well defined, and all the paths extending 𝜋 are labelled
as one of the paths starting from rep(𝑙(𝜋)). Let ext be any path starting from rep(𝑙(𝜋)). If 𝑒𝑥𝑡
does not have any occurrence of 𝑋 and ends with a deadlock, then we do not need to consider it,
since the concatenation 𝜋 + 𝑒𝑥𝑡 of 𝜋 and 𝑒𝑥𝑡 does not have 𝑛 occurrences of 𝑋. Also, we do not
consider the extension of 𝜋 with no occurrence of 𝑋, and such that rep(𝑙(𝜋)) ≤ rep(𝑙(𝑒𝑥𝑡)),
since each path with such a prefix and 𝑛 occurrences of 𝑋 can be peeled removing 𝑒𝑥𝑡 and still
have 𝑛 occurrences of 𝑋. All the other extensions are put in the variable ‘newPaths’, and will
be considered in the next round. If there are no paths left to analyse, and in all those with at
least 𝑛 occurrences of 𝑋 there is an occurrence in 𝑌 , then the algorithm returns true.
Example 7. Consider the net in Fig. 6 and its full prefix. Assume that we want to check the
relation 2.{𝑎, 𝑐} _ {𝑏}. We can easily see that the relation is verified. The first part of the
relation is satisfied if we observe 𝑎 or 𝑐 at least twice, or both 𝑎 and 𝑐 once. In all these cases, 𝑏
must have occurred to bring the token back in 1. We simulate some steps of the algorithm to see
how to arrive at this conclusion. First, we need to consider all the paths with at least an occurrence
of 𝑎 or of 𝑐. In this case, these are all the paths of the full prefix. Since none of them has two
occurrences, we need to check the possible extensions for all of them. The two paths ending in a
deadlock cannot be extended further, therefore we can stop to consider them. In what follows, if a
transition has multiplicity 1 in a footprint, we will omit the 1. Consider the path with footprint
{𝑎, 𝑒, 2.ℎ, 𝑓, 𝑔}. Its possible extensions are isomorphic to the segments starting with rep(𝑙2 ): these
have labels {𝑓 } and {𝑔, ℎ}. In none of them an occurrence of 𝑎 or 𝑐 appears; the segment labelled
{𝑓 } ends in a deadlock, and the leaf of the segment labelled {𝑔, ℎ} (𝑙2 ) coincides with rep(𝑙2 ),
therefore none of these extensions is useful to observe a second occurrence in {𝑎, 𝑐} and we can
discard the path. Analogously for the path with footprint {𝑐, 𝑑, 𝑒, 𝑓, 𝑔, 2.ℎ}. A similar reasoning
73
�Federica Adobbati et al. CEUR Workshop Proceedings 60–79
Algorithm 1 Computing collective reveals
function 𝑟𝑒𝑝𝑒𝑥(𝐿: full prefix, 𝑋, 𝑌 ⊆ 𝑇, 𝑛 ∈ N) ∈ {true, false, undefined}
Paths = The list of maximal paths in 𝐿 with at least an element of 𝑋
empty = True
while Paths ̸= []
Paths, empty, stop = 𝑒𝑥𝑡𝑒𝑛𝑑𝑃 𝑎𝑡ℎ𝑠(Paths, empty)
if stop == true
return false
end if
end while
if empty == true
return undefined
else
return true
end if
end function
function 𝑒𝑥𝑡𝑒𝑛𝑑𝑃 𝑎𝑡ℎ𝑠(Paths, empty)
# returns a triple (𝑥, 𝑦, 𝑧), where 𝑥 is a list of paths, and 𝑦 and 𝑧 are boolean values
newPaths = []
for 𝜋 ∈ Paths
if |𝜋 ∩ 𝑋| ≥ 𝑛
empty = false
if 𝑌 ∩ 𝜋 == ∅
return [], false, true
end if
else if 𝑙(𝜋) is not a deadlock
for 𝑒𝑥𝑡 ∈ 𝐿𝑟𝑒𝑝(𝑙(𝜋))
if 𝑒𝑥𝑡 ∩ 𝑋 ̸= ∅ ∨ (𝑟𝑒𝑝(𝑙(𝑒𝑥𝑡)) < 𝑟𝑒𝑝(𝑙(𝜋)))
newPaths.append(𝜋 + 𝑒𝑥𝑡)
end if
end for
end if
end for
return newPaths, empty, false
end function
# | 𝜋 ∩ 𝑋 | is equivalent to 𝑡∈𝑋 𝜆(𝜋)(𝑡)
∑︀
can be done for the paths with footprints {𝑎, 𝑒, ℎ, 𝑔} and {𝑐, 𝑑, 𝑒, ℎ, 𝑔}: in these cases, the possible
extensions start from the nodes rep(𝑙6 ) and rep(𝑙4 ) respectively, but none of them has an other
occurrence of 𝑎 or 𝑐, and the repetition of the non-deadlock leaves coincides or follows these nodes.
Hence, the only paths that we can extend are those ending with the nodes 𝑙7 and 𝑙5 ({𝑎, 𝑏} and
{𝑐, 𝑑, 𝑏} respectively). The extensions of these paths start from the root, therefore in all of them
74
�Federica Adobbati et al. CEUR Workshop Proceedings 60–79
there is an occurrence of 𝑎 or one of 𝑐, and these extended paths have two occurrences in {𝑎, 𝑐}.
Since in all of them there is already an occurrence of 𝑏, we can stop, and conclude 2.{𝑎, 𝑐} _ {𝑏}.
Lemma 3. The leaf of every path constructed by the algorithm is a deadlock, or is associated with
a marking that is already present in the path.
Proof. First we observe that every path constructed by the algorithm ends with a node equivalent
to a leaf in the prefix tree. For each leaf, the path in the tree starting from the root and arriving
to it is unique.
Let 𝑟 be the root of the tree, 𝜋0 𝜋1′ ...𝜋𝑛′ be a path constructed by the algorithm, where 𝜋0
is a maximal path in the prefix tree and 𝜋𝑖′ is an added segment isomorphic to a segment 𝜋𝑖
starting from rep(𝑙(𝜋𝑖−1 )) (the repetition of the leaf 𝑙(𝜋𝑖−1 ) of the segment 𝜋𝑖−1 ) and ending
in 𝑙(𝜋𝑖 ), a leaf of the prefix tree. We have to prove that, if the leaf of the constructed path is not
a deadlock, then the repetition rep(𝑙(𝜋𝑛′ )) of the leaf 𝑙(𝜋𝑛′ ) of the path belongs to the path itself,
i.e., rep(𝑙(𝜋𝑛′ )) is in 𝜋0 𝜋1′ ...𝜋𝑛′ .
We prove it by induction. Let 𝑙(𝜋1′ ) be the leaf of 𝜋0 𝜋1′ ; if it is not a deadlock, then rep(𝑙(𝜋1′ ))
is either in 𝜋1′ or inside [𝑟, rep(𝑙(𝜋0 ))], where [𝑟, rep(𝑙(𝜋0 ))] is the path from the root 𝑟 to the
repetition of the leaf of 𝜋0 and then it is contained in 𝜋0 . Then rep(𝑙(𝜋1′ )) ∈ 𝜋0 𝜋1′ .
We now assume the constructed path 𝜋0 𝜋1′ ...𝜋𝑖′ ends either with a deadlock, or with a node
whose repetition rep(𝑙(𝜋𝑖′ )) is either in 𝜋𝑖′ or in the segment [𝑟, rep(𝑙(𝜋𝑖−1 ′ ))], which is contained
in 𝜋0 𝜋1′ ...𝜋𝑖−1
′ , and then rep(𝑙(𝜋 ′ )) ∈ 𝜋 𝜋 ′ ...𝜋 ′ .
𝑖 0 1 𝑖
We prove that the path 𝜋0 𝜋1′ ...𝜋𝑖+1 ′ ends either with a deadlock, or with a node whose
repetition rep(𝑙(𝜋𝑖+1 ′ )) is either in 𝜋 ′
𝑖+1 or in the segment [𝑟, rep(𝑙(𝜋𝑖 ))], which is contained in
′
𝜋0 𝜋1 ...𝜋𝑖 , and therefore rep(𝑙(𝜋𝑖+1 )) ∈ 𝜋0 𝜋1 ...𝜋𝑖+1 . In fact, 𝜋𝑖+1 is isomorphic to a segment
′ ′ ′ ′ ′ ′
𝜋𝑖+1 in the prefix tree starting from rep(𝑙(𝜋𝑖 )), which is between 𝑟 and 𝑙(𝜋𝑖 ), and ending in a
leaf 𝑙(𝜋𝑖+1 ) of the prefix tree. This last leaf is either a deadlock, or has a repetition, which is
either in 𝜋𝑖+1 or in [𝑟, rep(𝑙(𝜋𝑖 ))]; since rep(𝑙(𝜋𝑖′ )) is by inductive hypothesis in 𝜋0 𝜋1′ ...𝜋𝑖′ , we
get the thesis.
Lemma 4. Let 𝜋 be any maximal path in the msc-tree. If 𝜋 has in total at least 𝑛 occurrences of
transitions belonging to 𝑋, then there is at least a path 𝜋 ′ analysed by the algorithm with in total
at least 𝑛 occurrences of transitions of 𝑋, such that 𝜆(𝜋 ′ ) ⊆ 𝜆(𝜋).
Proof. We show that we can peel 𝜋 and obtain a maximal path of the msc-tree such that its prefix
is analysed. For Lemma 2, we can peel 𝜋 and obtain a path 𝜋1 such that at least an occurrence of
𝑋 appears in its prefix in fp(Σ). Let 𝜋1′ be such prefix. If 𝜋1′ has 𝑛 occurrences of 𝑋, we don’t
need to proceed further; otherwise 𝜋1′ must be followed in 𝜋1 by a path isomorphic to a path
starting from rep(𝑙(𝜋1′ )). Let 𝜋2′ be this segment. If 𝜋2′ has at least an occurrence of a transition
of 𝑋, or rep(𝑙(𝜋2′ )) precedes rep(𝑙(𝜋1′ )), this elongation of the prefix has been considered by
the algorithm. If 𝜋2′ has no occurrences of 𝑋 and rep(𝑙(𝜋2′ )) ≥ rep(𝑙(𝜋1′ )), then we can peel 𝜋1
of the part between rep(𝑙(𝜋2′ )) and 𝑙(𝜋2′ ), obtaining 𝜋12 . Since in 𝜋2′ there are no elements of
𝑋, this cannot influence their number in 𝜋12 , and 𝜆(𝜋12 ) ⊆ 𝜆(𝜋1 ). The path 𝜋12 has also a prefix
made by 𝜋1′ concatenated with a segment starting from rep(𝑙(𝜋1′ )). Let 𝜋3′ be this segment. If
rep(𝑙(𝜋3′ )) ≥ rep(𝑙(𝜋1′ )), we repeat the peeling procedure. Since 𝜋1 has 𝑛 occurrence of 𝑋 by
hypothesis, after a finite number 𝑖 of steps, we will obtain a peeled maximal run 𝜋1𝑖 such that
75
�Federica Adobbati et al. CEUR Workshop Proceedings 60–79
rep(𝑙(𝜋𝑖′ )) < rep(𝑙(𝜋1′ )), with 𝜋𝑖′ segment starting from rep(𝑙(𝜋1′ )) elongating the segment 𝜋1′ ,
or 𝜋𝑖′ has at least an occurrence of 𝑋. We can repeat this reasoning until obtaining a prefix with
at least 𝑛 occurrences of 𝑋. Since in our steps we never remove any of those, and 𝜋 includes
them by hypothesis, this procedure ends after a finite number of steps. By construction, all the
transitions in the constructed prefix are also in 𝜋, therefore we produced a prefix as required
from the thesis.
Theorem 1. Algorithm 1 is correct.
Proof. As first step we show that if the algorithm returns false, then 𝑛.𝑋 ̸_ 𝑌 . The algorithm
returns false if the variable ‘stop’ is true. The value of ‘stop’ is selected into the function
extendPaths, and it is set to true if a path is found with 𝑛 occurrences of 𝑋 and none in 𝑌 . Each
prefix is constructed so that the final leaf is a deadlock for the path, or it is repeated previously;
in the first case the path is already maximal, in the second case, the path can be extended to
a maximal path without adding any new transition by repeating infinitely often the segment
between the leaf of the prefix and its repetition. The existence of such a repetition is guaranteed
by Lemma 3. In both cases there is a maximal run with at least 𝑛 occurrences of 𝑋 and none in
𝑌 , therefore 𝑛.𝑋 ̸_ 𝑌 .
We now show that if the algorithm returns true, then 𝑛.𝑋 _ 𝑌 . This is a consequence of
Lemma 4: if there were a path with 𝑛 occurrences of 𝑋 and none in 𝑌 , Lemma 4 guarantees
that we would analyse a prefix with the same feature, but if this happens, the algorithm returns
false. If the algorithm returns undefined, then there cannot be any run in the msc-tree with 𝑛
occurrences of transitions of 𝑋 as a consequence of Lemma 4.
Theorem 2. Algorithm 1 terminates.
Proof. The algorithm ends when the variable ‘Paths’ becomes empty, or when a path with 𝑛
occurrences of 𝑋 and none in 𝑌 was found. We show that ‘Paths’ becomes empty after a finite
number of steps. The variable ‘Paths’ is a list of prefixes of paths in the msc-tree. Its content in
each iteration of the while loop is entirely determined by the function extendPaths, that elongate
some of its elements. In particular, the function elongates the paths with less of 𝑛 occurrences
of 𝑋. Each path can be elongated in two ways: adding at least an additional occurrence of 𝑋,
and this happens only finitely many times, since when the path has at least 𝑛 occurrences of
𝑋 it is not extended anymore, or with a segment whose repetition of the leaf is strictly closer
to the root than the repetition of the previous leaf. Also in this second case the number of
extension is finite, since the distance between each node and the root is finite.
Remark 7. To compute the reveals relation, the algorithm needs to analyse only the maximal
runs of the prefix tree, without further extensions. This is coherent with the result in [18], where
the authors show that for 1-safe free-choice Petri nets, ∀𝑎, 𝑏 ∈ 𝑇 , 𝑎 ▷ 𝑏 iff for each maximal path
𝜋 in the prefix, if 𝑎 ∈ 𝜋, then 𝑏 ∈ 𝜋.
Algorithm 1 can be adapted to compute the relation presented in Def. 4. Here we give only a
sketch of how this can be done. Let 𝑋 = {𝑡1 , ..., 𝑡𝑘 } and 𝑌 be the input sets. Instead of having
just a single threshold 𝑛 in input as for repeated reveals, the input must include all the thresholds
{𝑛1 , ..., 𝑛𝑘 } related to transitions of 𝑋, and the information about how they are associated to
76
�Federica Adobbati et al. CEUR Workshop Proceedings 60–79
these transitions. Since the number of observations in which we are interested changes for
every transition, when the algorithm needs to decide whether a path can stop or needs to be
extended, it must consider all transitions of 𝑋 separately, each with its threshold. In addition,
if a path has already reached the number of required occurrences of a certain transition, we
should stop to consider this transition as useful when we evaluate the possible extensions.
Since extended reveals (Def. 2) can be expressed as a special case of extended-repeated reveals,
modifying the algorithm as described would allow for its computation.
5. Conclusion
In this paper, we have introduced two new variants of reveals relation, namely extended-repeated
reveals and collective reveals. The relations are defined for transitions of general PT nets and
they express positive information flow. Existence of reveals relation (or its variants) between
transitions means that the occurrence of one gives information about the other one. It can
violate security of a system when a low transition reveals a high transition. The new variants
introduced in this paper are parametric and they allow one to specify security requirements
of a distributed system based on the specific needs of the system. They provide scalability by
allowing one to specify different levels of security.
Building upon the results from [18], we have provided a formal basis for information-flow
analysis of distributed systems that are modelled with bounded equal-conflict PT nets. We
have adapted the formalisation of maximal-step computation tree and its full prefix to bounded
equal-conflict PT systems. We have shown that maximal-step computation tree represents the
behaviour of a bounded equal-conflict PT system under maximal-step semantics and its full
prefix forms an adequate basis for analysis of positive information flow by computing reveals
relation and its variants. We have provided an algorithm to compute collective reveals on the
full prefix and shown how to adapt the algorithm for computing extended-repeated reveals.
The methods provided in this paper cover the computation of all reveals variants and can be
used to perform information-flow analysis on bounded equal-conflict PT systems.
One of our next steps will be performing a complexity analysis of the proposed methods and
working on improving the efficiency. This includes investigation of a shorter prefix and more
efficient algorithms. We plan to work on extending our results to more general classes of Petri
nets such as unbounded equal-conflict PT systems. We will explore the practical use of our meth-
ods for both information-flow analysis and verification of other desired behavioural properties
of complex distributed systems. We will also explore different approaches to information-flow
analysis on Petri nets by considering games like in [29, 30].
6. Acknowledgements
This work is partially supported by the Italian MUR.
77
�Federica Adobbati et al. CEUR Workshop Proceedings 60–79
References
[1] J. A. Goguen, J. Meseguer, Security policies and security models, in: Proc. IEEE Symp. on
Secur. and Privacy, 1982, pp. 11–20.
[2] D. Sutherland, A model of information, in: Proc. 9th Nat. Comput. Sec. Conf., volume 247,
1986, pp. 175–183.
[3] D. McCullough, Specifications for multi-level security and a hook-up, in: Proc. IEEE Symp.
on Secur. and Privacy, 1987, pp. 161–161. doi:10.1109/SP.1987.10009.
[4] R. Focardi, R. Gorrieri, A taxonomy of security properties for process algebras, Journal of
Computer Security 3 (1995) 5–34.
[5] J. McLean, A general theory of composition for a class of "possibilistic" properties, IEEE
Transactions on Software Engineering 22 (1996) 53–67. doi:10.1109/32.481534.
[6] G. Boudol, I. Castellani, Noninterference for concurrent programs and thread systems,
Theor. Comput. Sci. 281 (2002) 109–130. URL: https://doi.org/10.1016/S0304-3975(02)
00010-5. doi:10.1016/S0304-3975(02)00010-5.
[7] H. Mantel, A uniform framework for the formal specification and verification of information
flow security, Ph.D. thesis, Saarland University, Saarbrücken, Germany, 2003. URL: http:
//scidok.sulb.uni-saarland.de/volltexte/2004/202/index.html.
[8] H. Mantel, Information flow and noninterference, in: H. C. A. van Tilborg, S. Jajodia (Eds.),
Encyclopedia of Cryptography and Security, 2nd Ed, Springer, 2011, pp. 605–607. URL: https:
//doi.org/10.1007/978-1-4419-5906-5_874. doi:10.1007/978-1-4419-5906-5\_874.
[9] N. Busi, R. Gorrieri, A survey on non-interference with Petri nets, in: Lectures on Concur.
and Petri Nets, Advances in Petri Nets, volume 3098 of LNCS, Springer, 2003, pp. 328–344.
[10] N. Busi, R. Gorrieri, Structural non-interference in elementary and trace nets, Math. Struct.
Comput. Sci. 19 (2009) 1065–1090.
[11] E. Best, P. Darondeau, R. Gorrieri, On the decidability of non interference over unbounded
Petri nets, in: K. Chatzikokolakis, V. Cortier (Eds.), Proc. 8th SecCo, Paris, France, volume 51
of EPTCS, 2010, pp. 16–33. URL: https://doi.org/10.4204/EPTCS.51.2. doi:10.4204/EPTCS.
51.2.
[12] P. Baldan, A. Carraro, Non-interference by unfolding, in: G. Ciardo, E. Kindler (Eds.), Proc.
PETRI NETS 2014, Tunis, Tunisia, volume 8489 of LNCS, Springer, 2014, pp. 190–209. URL:
http://dx.doi.org/10.1007/978-3-319-07734-5_11. doi:10.1007/978-3-319-07734-5_
11.
[13] F. Basile, G. De Tommasi, C. Sterle, Noninterference enforcement via supervisory control
in bounded Petri nets, IEEE Trans. Automat. Contr. 66 (2021) 3653–3666. doi:10.1109/
TAC.2020.3024274.
[14] G. Kılınç, Formal Notions of Non-interference and Liveness for Distributed Systems, Ph.D.
thesis, Univ. Milano-Bicocca, DISCo, Milano, Italy, 2016.
[15] L. Bernardinello, G. Kılınç, L. Pomello, Non-interference notions based on reveals and
excludes relations for Petri nets, ToPNoC 11 (2016) 49–70. URL: https://doi.org/10.1007/
978-3-662-53401-4_3. doi:10.1007/978-3-662-53401-4\_3.
[16] S. Haar, Unfold and cover: Qualitative diagnosability for Petri nets, in: Proc. 46th IEEE
Conf. Decis. Control, 2007.
[17] S. Haar, C. Rodríguez, S. Schwoon, Reveal your faults: It’s only fair!, in: Proc. 13th ACSD,
78
�Federica Adobbati et al. CEUR Workshop Proceedings 60–79
Barcelona, Spain, 2013, pp. 120–129.
[18] F. Adobbati, G. Kilinç Soylu, A. Puerto Aubel, A finite prefix for analyzing information
flow among transitions of a free-choice net, IEEE Access 10 (2022) 38483–38501. URL:
https://doi.org/10.1109/ACCESS.2022.3165185. doi:10.1109/ACCESS.2022.3165185.
[19] E. Teruel, M. Silva, Liveness and home states in equal conflict systems, in: M. Aj-
mone Marsan (Ed.), Application and Theory of Petri Nets 1993, Springer Berlin Heidelberg,
Berlin, Heidelberg, 1993, pp. 415–432.
[20] T. Murata, Petri nets: Properties, analysis and applications, Proceedings of the IEEE 77
(1989) 541–580. doi:10.1109/5.24143.
[21] U. Goltz, W. Reisig, The non-sequential behaviour of Petri nets, Information
and Control 57 (1983) 125–147. URL: https://www.sciencedirect.com/science/article/pii/
S0019995883800400. doi:https://doi.org/10.1016/S0019-9958(83)80040-0.
[22] E. Best, R. Devillers, Sequential and concurrent behaviour in Petri net theory, Theoretical
Computer Science 55 (1987) 87–136. URL: https://www.sciencedirect.com/science/article/
pii/0304397587900909. doi:https://doi.org/10.1016/0304-3975(87)90090-9.
[23] J. Engelfriet, Branching processes of Petri nets., Acta Inf. 28 (1991) 575–591. doi:10.1007/
BF01463946.
[24] J. Esparza, S. Römer, W. Vogler, An improvement of McMillan’s unfolding algorithm,
Formal Methods in System Design 20 (2002) 285–310. doi:10.1023/A:1014746130920.
[25] E. Smith, On the border of causality: Contact and confusion, Theoretical Com-
puter Science 153 (1996) 245–270. URL: https://www.sciencedirect.com/science/article/pii/
0304397595001239. doi:https://doi.org/10.1016/0304-3975(95)00123-9.
[26] P. S. Thiagarajan, Elementary net systems, in: W. Brauer, W. Reisig, G. Rozenberg
(Eds.), Petri Nets: Central Models and Their Properties, Advances in Petri Nets 1986,
Part I, Proceedings of an Advanced Course, Bad Honnef, Germany, 8-19 September 1986,
volume 254 of Lecture Notes in Computer Science, Springer, 1986, pp. 26–59. URL: https:
//doi.org/10.1007/BFb0046835. doi:10.1007/BFb0046835.
[27] R. Janicki, P. E. Lauer, M. Koutny, R. Devillers, Concurrent and maximally concurrent
evolution of nonsequential systems, Theoretical Computer Science 43 (1986) 213–238.
[28] S. Balaguer, T. Chatain, S. Haar, Building tight occurrence nets from reveals relations,
in: B. Caillaud, J. Carmona, K. Hiraishi (Eds.), Proc. 11th ACSD, Newcastle Upon Tyne,
UK, IEEE, 2011, pp. 44–53. URL: http://doi.ieeecomputersociety.org/10.1109/ACSD.2011.16.
doi:10.1109/ACSD.2011.16.
[29] L. Bernardinello, G. Kılınç, L. Pomello, Weak observable liveness and infinite games
on finite graphs, in: W. M. P. van der Aalst, E. Best (Eds.), Application and Theory of
Petri Nets and Concurrency - 38th International Conference, PETRI NETS 2017, Zaragoza,
Spain, June 25-30, 2017, Proceedings, volume 10258 of Lecture Notes in Computer Science,
Springer, 2017, pp. 181–199. URL: https://doi.org/10.1007/978-3-319-57861-3_12. doi:10.
1007/978-3-319-57861-3\_12.
[30] F. Adobbati, L. Bernardinello, L. Pomello, A two-player asynchronous game on fully
observable Petri nets, Trans. Petri Nets Other Model. Concurr. 15 (2021) 126–149. URL:
https://doi.org/10.1007/978-3-662-63079-2_6. doi:10.1007/978-3-662-63079-2\_6.
79
�