=Paper=
{{Paper
|id=Vol-2907/paper10
|storemode=property
|title=Verification of Communication Structured Acyclic Nets Using SAT
|pdfUrl=https://ceur-ws.org/Vol-2907/paper10.pdf
|volume=Vol-2907
|authors=Nadiyah Almutairi,Maciej Koutny
|dblpUrl=https://dblp.org/rec/conf/apn/AlmutairiK21
}}
==Verification of Communication Structured Acyclic Nets Using SAT==
https://ceur-ws.org/Vol-2907/paper10.pdf
Verification of Communication Structured Acyclic Nets
Using SAT
Nadiyah Almutairi and Maciej Koutny
School of Computing, Newcastle University
1 Science Square, Newcastle Helix, Newcastle upon Tyne NE4 5TG, U.K.
{n.m.r.almutairi2,maciej.koutny}@newcastle.ac.uk
Abstract. Model checking is an established strategy for automatic verification
of software and hardware systems. It supports extensive analyses of the proper-
ties of states and behaviours of computing systems. Petri net verification using
SAT -solvers has already received considerable attention and effective tools based
on it have been developed. In this paper, we are concerned with the verification
of communication structured acyclic nets (CSA-nets) which so far lacked robust
verification methodology. CSA-nets are sets of acyclic nets which can communi-
cate by means of synchronous and asynchronous interactions. In this paper, we
introduce several propositional formulas which can be used to verify properties
of CSA-nets using SAT-solvers.
Keywords: Petri net, acyclic net, communication structured acyclic net, model
checking, reachability, deadlock, SAT-solver
1 Introduction
Model checking is a verification approach that, for example, performs a search of the
system state space to examine whether certain property is satisfiable. This technique
is often used for automatic verification of both hardware and software systems. It is
a powerful method for detecting bugs in, for example, concurrent systems whose cor-
rect design poses a significant challenge [4]. For instance, [7] proposed an approach
using SAT-solver to detect state encoding conflicts in Signal Transition Graphs which
are converted into equivalent Petri nets and the verification is performed on the finite
complete prefixes of their unfoldings ([6] extends this approach to model-checking for
merged processes). [4] introduced a general study of model-checking based on Petri net
unfoldings. A similar work has been done for the verification of contextual nets in [14].
A complex evolving system (CES) is composed of a number of concurrently-acting
subsystems interacting with each other and with the environment. Such systems suffer
from a very high complexity in terms of design and behaviour. The approach [9,10,1]
based on communication structured acyclic nets (CSA-nets) — and their direct precur-
sors communication structured occurrence nets (CSO-nets) — which employs different
types of formally-defined types of abstraction can play an important role regarding the
Copyright © 2021 for this paper by its authors. Use permitted under Creative Commons Li-
cense Attribution 4.0 International (CC BY 4.0).
176 Nadiyah Almutairi and Maciej Koutny
representation of behaviours of CESs using structure to reduce the complexity of rep-
resentations. A recently designed and implemented tool S ONCRAFT [11] (based on the
W ORKCRAFT platform [13,15] providing a flexible common underpinning for graph-
based models) extensive powerful support for dealing with models of CESs based on
CSO -nets, including visualization and verification. Previous work on CSO -nets provided
a framework for visualising and analysing behaviour of CESs [10], modelling cyber-
crime investigation [1], provenance [12], and timed behaviours [2].
A satisfactory property verification for CSA-nets is still missing. To address this,
our main contribution in this paper is to fill this gap by providing SAT-encoding of the
most significant behavioural properties of CSA-nets, such as reachability. This is the
first paper to propose a model checking solution of this kind. The proposed verification
algorithms will be added as a plug-in to S ONCRAFT.
The paper is organised as follows. In Section 2, we provide basic definitions con-
cerning acyclic nets. In Section 3, we introduce formulas characterising various basic
properties of acyclic nets, such as well-formedness and scenarios (valid executions)
which can then be checked for satisfiability using SAT-solvers. In Section 4, basic defi-
nitions concerning communication structured acyclic nets are introduced. In Section 5,
we extend the property formulas to CSA-nets. We conclude in Section 6. Due to the
page limit proofs of formal results are not included.
2 Acyclic nets
In this section we introduced basic notions concerning acyclic nets.
Definition 1 (acyclic net). An acyclic net is a triple acnet = (P, T, F), where P and T
are finite disjoint sets of places and transitions, respectively, and F ⊆ (P × T ) ∪ (T × P)
is a flow relation such that F is acyclic and, for every t ∈ T , there are p, q ∈ P such that
pFt and tFq. ♦
For every x ∈ P ∪ T , • x = preacnet (x) , {y | yFx} and x• = postacnet (x) , {y | xFy}
are the elements directly preceding and directly following x. We denote P, T , and F
by Pacnet , Tacnet , and Facnet , respectively, to indicate explicitly the net acnet. An acyclic
net can exhibit backward non-determinism (if |• p| > 1, for some p ∈ P) and forward
non-determinism (if |p• | > 1, for some p ∈ P).
Definition 2 (step and marking). Let acnet = (P, T, F) be an acyclic net.
1. steps(acnet) , {U ∈ P(T ) \ {∅} | ∀t, u ∈ U : t 6= u =⇒ •t ∩ • u = ∅} are the steps.
2. markings(acnet) , P(P) are the markings.
init , {p ∈ P | • p = ∅} is the default initial marking, and M fin , {p ∈ P | p• =
3. Macnet acnet
∅} is the default final marking. ♦
Graphically, places are represented by circles, transitions by boxes, and arcs represent
the flow relation F. Markings are shown by placing tokens within the circles. For acyclic
nets we introduce step sequence semantics as such a semantics is used in the model of
communication structured occurrence nets.
Verification of Communication Structured Acyclic Nets Using SAT 177
Definition 3 (enabled and executed step). Let M be a marking of an acyclic net acnet.
1. enabledacnet (M) , {U ∈ steps(acnet) | •U ⊆ M} are the steps enabled at M.
2. A step U ∈ enabledacnet (M) can be executed yielding a new marking given by M 0 ,
(M ∪U • ) \ •U. This is denoted by M[Uiacnet M 0 . ♦
Note that markings of acyclic nets are ‘safe’ by definition. The emptiness of the post-
places of an executed U will hold for the well-formed acyclic nets introduced later.
Definition 4 ((mixed) step sequence). Let acnet be an acyclic net and µ be a sequence
M0U1 M1 . . . Mk−1Uk Mk (k ≥ 0) such that M0 , . . . , Mk are markings and U1 , . . . ,Uk are
steps.
1. µ is a mixed step sequence from M0 to Mk if Mi−1 [Ui iacnet Mi , for every 1 ≤ i ≤ k.
2. If µ is a mixed step sequence from M0 to Mk , then σ = U1 . . .Uk is a step sequence
from M0 to Mk . This is denoted by M0 [σ iacnet Mk .
Also, M0 [iacnet Mk denotes that Mk is reachable from M0 . ♦
If k = 0 then µ = M0 and the corresponding step sequence σ is the empty sequence
denoted by λ . A mixed step sequence M0U1 M1 . . . Mk−1Uk Mk can also be denoted as
U
1 U
k
M0 −→ M1 . . . Mk−1 −→ Mk .
Definition 5 (behavioural notions). Let acnet be an acyclic net.
init [σ i
1. sseq(acnet) , {σ | Macnet acnet M} are the step sequences of acnet.
2. maxsseq(acnet) , {σ ∈ sseq(acnet) | ¬∃U : σU ∈ sseq(acnet)} are the maximal
step sequences of acnet. ♦
We usually treat individual transitions as singleton steps; for instance, a step sequence
{t}{u}{w, v}{z} can be denoted by tu{w, v}z.
Acyclic nets allow one to define conflicts between transitions in a structural way.
Definition 6 (structural notions). Let acnet = (P, T, F) be an acyclic net.
1. Two transitions t 6= u ∈ T are in direct (forward) conflict, denoted t#0 u, if they have
a common place in their presets, i.e., •t ∩ • u 6= ∅.
2. Two transitions t 6= u ∈ T are in direct backward conflict if they have a common
place in their postsets, i.e., t • ∩ u• 6= ∅.
3. Two nodes x, y ∈ P ∪ T are in conflict, denoted x#y, if there are transitions t and u
such that t#0 u and (t, x), (u, y) ∈ F ∗ .
4. A transition t ∈ T is in self-conflict if t#t. ♦
Note that conflicts between transitions emerge from having a common pre-place (in the
case of forward non-determinism) or a common post-place (in the case of backward
non-determinism), while concurrency results from multiple post-places emerging from
a transition [10].
178 Nadiyah Almutairi and Maciej Koutny
e
p1 p3 p4
h
p0
a f
p2 p5
g
Fig. 1. An acyclic net.
Example 1. Figure 1 shows an acyclic net acnet, where P = {p0 , p1 , p2 , p3 , p4 , p5 },
T = {a, e, f , g, h}, and F = {(p0 , a), (a, p1 ), (a, p2 ), . . . , (h, p4 )}. The initial and final
markings are {p0 } and {p4 , p5 }, respectively. Two possible steps sequences are σ1 =
a{e, g}h and σ2 = a{ f , g}h. In this acyclic net, transitions e and f are involved both in
direct forward conflict and direct backward conflict. ♦
If backward conflicts are not allowed, one can characterise structurally transitions
which can be executed.
Definition 7 (backward deterministic acyclic net). A backward deterministic acyclic
net is an acyclic net acnet = (P, T, F) such that |• p| ≤ 1, for all p ∈ P. ♦
Proposition 1. Let acnet be a backward deterministic acyclic net.
1. No step sequence contains multiple occurrences of transitions.
2. Each transition which is not in self-conflict occurs in at least one of the step se-
quences.
Figure 2 shows an example of backward deterministic acyclic net, where no transition
is in self-conflict and it can be executed.
c4 c5
g
c0 c3
h e
c1
c2
f
Fig. 2. A backward deterministic acyclic net.
Verification of Communication Structured Acyclic Nets Using SAT 179
2.1 Occurrence nets and scenarios
An occurrence net [9] is a Petri net describing a single execution of some concurrent
system in such a way that only the details of causality and concurrency between transi-
tions are captured. It is deterministic and can represent an execution history of a system
with a clear interpretation of causal dependencies between transitions.
Definition 8 (occurrence net). An occurrence net is an acyclic net onet = (P, T, F)
such that |• p| ≤ 1 and |p• |≤ 1, for every p ∈ P. ♦
We use occurrence nets embedded in an acyclic net to provide a characterisation of
its potential executions.
Definition 9 (scenario and maximal scenario). Let acnet be an acyclic net.
1. A scenario of acnet is an occurrence net ocnet such that:
init ∪ post
(a) Tocnet ⊆ Tacnet and Pocnet = Macnet acnet (Tocnet ).
(b) preocnet (t) = preacnet (t) and postocnet (t) = postacnet (t), for every t ∈ Tocnet .
2. A maximal scenario of acnet is a scenario ocnet such that there is no other scenario
ocnet0 satisfying Tocnet ⊂ Tocnet0 .
The sets of all scenarios and maximal scenarios of acnet are scenarios(acnet) and
maxscenarios(acnet), respectively. ♦
Figure 3 shows the only two maximal scenarios of the acyclic net in Figure 1.
Different step sequences may generate the same scenario, and each scenario is gen-
erated by at least one step sequence. Two step sequences generate the same scenario
iff their executed transitions are identical. Each scenario is identified by the set of its
transitions, and we denote by scenarioacnet (V ) the unique scenario with the transition
set V .
A maximal scenario can be seen as a deterministic process, which captures an equiv-
alence class of maximal step sequences that are distinguishable only in the order of
concurrent transitions [7].
Example 2. Figure 3 illustrates the last point by identifying two maximal scenarios,
ocnet1 = scenarioacnet ({a, e, g, h}) and ocnet2 = scenarioacnet ({a, f , g, h}), of the acyclic
net acnet in Figure 1. For example, ocnet1 captures the following five executions:
a {e,g} h
{p0 } →
− {p1 , p2 } −−−→ {p3 , p5 } →
− {p4 , p5 },
a e g h
{p0 } →
− {p1 , p2 } →
− {p2 , p3 } →
− {p3 , p5 } →
− {p4 , p5 },
a e {g,h}
{p0 } →
− {p1 , p2 } →
− {p2 , p3 } −−−→ {p4 , p5 },
a e h g
{p0 } →
− {p1 , p2 } →
− {p2 , p3 } →
− {p2 , p4 } →
− {p4 , p5 }, and
a g e h
{p0 } →
− {p1 , p2 } →
− {p1 , p5 } →
− {p3 , p5 } →
− {p4 , p5 }. ♦
Not every acyclic net can be seen as a valid representation of causal dependencies
in some execution of a concurrent system. The next definition introduces the notion
of well-formedness which basically means that all the executions an acyclic net are
the executions of its scenarios. In addition, an acyclic net has no redundant transitions
whenever each of its transitions can be executed.
180 Nadiyah Almutairi and Maciej Koutny
e
p1 p3 p4
h
p0
a
p2 p5
(a) g
p1 p3 p4
h
p0
a f
p2 p5
(b) g
Fig. 3. Maximal scenarios of the acyclic net in Figure 1: ocnet1 = scenarioacnet ({a, e, g, h}) in (a),
and ocnet2 = scenarioacnet ({a, f , g, h}) in (b).
Definition 10 (well-formedness and non-redundant transitions). An acyclic net acnet
S
is well-formed if sseq(acnet) =S S sseq(scenarios(acnet)). Moreover, acnet has non-
redundant transitions if Tacnet = { σ | σ ∈ sseq(acnet)}. ♦
Each backward deterministic acyclic net, and so also each occurrence net, is well-
formed. Moreover, each occurrence net has non-redundant transitions. As the result
shows, in a given execution a well-formed acyclic net no token can be created ‘more
than once’.
Proposition 2. acnet is well-formed iff the following hold for every step sequence U1 . . .Uk ∈
sseq(acnet):
1. t • ∩ u• = ∅, for every 1 ≤ i ≤ k and all distinct t, u ∈ Ui .
2. Ui• ∩U j• = ∅, for all 1 ≤ i < j ≤ k.
3 Verifying properties of acyclic nets
The task of a SAT-solver is to find a satisfying assignment for the variables used in
a propositional boolean formula φ . That is, the SAT-solver looks for an assignment
f : Var → {0, 1} for the variables Var which occur in φ that makes φ true, i.e., φ [ f ] = 1.
And, if such an assignment exists, φ is satisfiable. The formula φ is often expressed in
conjunctive normal form (CNF), i.e., a conjunction of clauses which are disjunctions of
literals (where a literal is either a variable or the negation of a variable).
Verification of Communication Structured Acyclic Nets Using SAT 181
3.1 Identifying scenarios
For a given acyclic net acnet = (P, T, F), a subset of transitions T 0 ⊆ T induces a sce-
nario whenever the following three properties hold:
– Causality: all non-initial pre-places of T 0 received tokens from T 0 .
– No Forward Conflict: the transitions in T 0 are free from forward conflicts.
– No Backward Conflict: the transitions in T 0 are free from backward conflicts.
The next definition and proposition make this formal, by identifying the scenarios of an
acyclic net with occurrence net restrictions induced by subsets of transitions.
Definition 11 (restricting acyclic net). Let acnet = (P, T, F) be an acyclic net and
T 0 ⊆ T . Then acnet|T 0 = (P0 , T 0 , F|(P0 ×T 0 )∪(T 0 ×P0 ) ), where P0 = Macnet
init ∪ post 0
acnet (T ), is
0
the restriction of acnet to T . ♦
Note that if acnet|T 0 is a scenario, then acnet|T 0 = scenarioacnet (T 0 ).
Proposition 3. The following statements are equivalent for an acyclic net acnet =
(P, T, F) and T 0 ⊆ T :
1. acnet|T 0 ∈ scenarios(acnet).
2. acnet|T 0 is an occurrence net and preacnet (T 0 ) \ Macnet
init ⊆ post 0
acnet (T ).
We want to obtain a propositional formula which can be used to identify all the
scenarios of an acyclic net acnet, i.e., to construct a formula Scenarioacnet which eval-
uates to 1 iff all the transitions assigned 1 induce a scenario of acnet (note that acnet
is not assumed to be well-formed). The following boolean variables will be used in the
construction of Scenarioacnet and the translation into SAT :
– For every t ∈ T , we have a variable int tracing that t belongs to a scenario.
The constraints on the above variables are defined, following Proposition 3, as follows:
– To ensure that all non-initial pre-places of T 0 received tokens from T 0 :
^ ^ _
Causalityacnet , int → inu
t∈T init u∈ p •
p∈• t\Macnet
• init
u∈• p inu is set to 1 if t ⊆ Macnet .
V W
where p∈• t\Macnet
init
– To ensure that scenario has no forward conflicts:
^ ^
NoForwardConflictacnet , ¬(int ∧ inu )
t∈T u∈(• t)• \{t}
where u∈(• t)• \{t} ¬(int ∧ inu ) is omitted if (•t)• = {t}.
V
– To ensure that scenario has no backward conflicts:
^ ^
NoBackwardConflictacnet , ¬(int ∧ inu )
t∈T u∈• (t • )\{t}
• (t • ) = {t}.
u∈• (t • )\{t} ¬(int ∧ inu ) is omitted if
V
where
182 Nadiyah Almutairi and Maciej Koutny
Then the formula which characterises all the scenarios of acnet is:
Scenarioacnet , Causalityacnet ∧ NoForwardConflictacnet ∧ NoBackwardConflictacnet
The size of the above formula (in terms of the occurrences of literals) is bounded by
|T | + 3 · |T | · min{|F|2 , |P| · |T |}.
Proposition 4. Let acnet be an acyclic net.
1. If f is a satisfying assignment for Scenarioacnet then acnet| f −1 (1) is a scenario of
acnet.
2. For every scenario acnet0 of the acyclic net acnet, there is a satisfying assignment
f for Scenarioacnet such that acnet| f −1 (1) = acnet0 .
Hence, we can use Scenarioacnet to find all the subsets T 0 of transitions of acnet inducing
scenarios after translating it into CNF and feeding into a SAT-solver.
3.2 Well-formedness
To characterise well-formed acyclic nets, we introduce formulas capturing the enabled-
ness of transitions, for every t ∈ T :
^ ^ _
Enabledt , ¬inu ∧ inu
u∈(• t)• init u∈ p•
p∈• t\Macnet
where the second clause is omitted if •t ⊆ Macnet
init . We then define:
_ _
NotWellFormedacnet , Scenarioacnet ∧ Enabledt ∧ inu
t∈T u∈• (t • )
Intuitively, in the above formula, Scenarioacnet ‘selects’ one of the executions of acnet
which does not violate well-formedness, and the second part means that there is a tran-
sition which can be executed after that violating well-formedness.
The size of the above formula is bounded by |T | + 6 · |T | · min{|F|2 , |P| · |T |}.
p0 e p1 a p4 c p6
1 0 0
p3
p2 b d p7
1 1
p5
Fig. 4. An acyclic net which is not well-formed.
Verification of Communication Structured Acyclic Nets Using SAT 183
Proposition 5. An acyclic net acnet is well-formed iff NotWellFormedacnet does not
have a satisfying assignment.
Hence we can use NotWellFormedacnet to find out whether acnet is well-formed after
translating it into CNF and feeding into a SAT-solver.
Example 3. The acyclic net in Figure 4 is not well-formed. This is so because for the as-
signment f illustrated in Figure 4 (where f (e) = f (b) = f (d) = 1 and f (a) = f (c) = 0)
we have the following: (i) Scenario W acnet
evaluates to 1 inducing scenarioacnet ({e, b, d});
(ii) Enableda [ f ] = 1; and (iii) ( u∈• (a• ) inu )[ f ] = (ina ∨ inb )[ f ] = (0 ∨ 1) = 1. Hence,
NotWellFormedacnet [ f ] = 1. ♦
3.3 Non-redundant transitions
Definition 10(2) asserts that a well-formed acnet has non-redundant transitions if each
transition is guaranteed to occur in at least one of its steps sequences. In other words, if
for each transition t there is a valid scenario in scenarios(acnet) that contains t.
g p5
0
p1 c p7
1
p0 x h p6
1 1
p2 f p4
1
Fig. 5. A well-formed acyclic net with a redundant transition c (see Example 4).
Example 4. Consider the backward deterministic acyclic net in Figure 5. The two tran-
sitions g and h are in direct conflict, and so c is in a self-conflict. This means that cScan
never be executed, i.e., there is no step sequence σ ∈ sseq(acnet) such that c ∈ σ .
Therefore, c is not included in any scenario of scenarios(acnet), and can be seen as an
irrelevant part of acnet.
For the example in Figure 5, we can see that the boolean formula Scenarioacnet is not
satisfiable for an assignment r such that r(inc ) = 1 since
Causalityacnet = (inx → 1) ∧ (ing → inx ) ∧ (inh → inx )∧
(in f → inx ) ∧ (inc → (ing ∧ inh ))
NoForwardConflictacnet = ¬(ing ∧ inh ) ∧ ¬(inh ∧ ing ) .
Hence, if r(inc ) = 1 and Causalityacnet [r] = 1 then we have r(ing ) = r(inh ) = 1, and so
NoForwardConflictacnet [r] = 0. This means there is no scenario induced by transitions
whose associated variables are assigned 1 and c belongs to such a scenario. ♦
184 Nadiyah Almutairi and Maciej Koutny
Checking whether a transition t belongs to at least one scenario can be done using
the following formula:
NonRedundanttacnet , int ∧ Scenarioacnet .
As a result, a well-formed acyclic net has non-redundant transitions if NonRedundantt
is satisfiable, for each t ∈ T .
Proposition 6. A well-formed acyclic net acnet has non-redundant transitions iff the
formula NonRedundanttacnet is satisfiable, for every t ∈ T .
3.4 Maximal scenarios
Maximal scenarios are complete scenarios, which means that no transitions are enabled.
In this case, we assume that acnet is a well-formed acyclic net, and define:
^
MaxScenarioacnet , Scenarioacnet ∧ ¬Enabledt
t∈T
The size of MaxScenarioacnet is bounded by |T | + 5 · |T | · min{|F|2 , |P| · |T |}. Intuitively,
it is satisfiable for all the scenarios that do not enable any transitions.
Proposition 7. Let acnet be a well-formed acyclic net.
1. If f is a satisfying assignment for MaxScenarioacnet then acnet| f −1 (1) is a maximal
scenario of acnet.
2. For every maximal scenario acnet0 of acnet, there is a satisfying assignment f for
MaxScenarioacnet such that acnet| f −1 (1) = acnet0 .
Hence we can use MaxScenarioacnet to find the subsets T 0 of transitions of acnet
inducting maximal scenarios after translating it into CNF and feeding into a SAT-solver.
p1 e p3 g
1 0
p0 x p5
1
p2 f p4 h
1 1
Fig. 6. A well-formed acyclic net in Example 5.
Example 5. Figure 6 shows a well-formed acyclic net that exhibits both forward and
backward conflict. Observe that all the transitions in {x, e, f , h} satisfy the causality
condition, and have no forward nor backward conflict. They also lead to a marking
{p5 } where no transitions are enabled. Therefore, the set of transitions {x, e, f , h} in-
duces a maximal scenario in maxscenarios(acnet). Thus, the MaxScenarioacnet formula
is satisfied by the assignment indicated in Figure 6 (the situation is the same if g is used
instead of h). ♦
Verification of Communication Structured Acyclic Nets Using SAT 185
3.5 Marked places and deadlocked scenarios
Consider a scenario of a well-formed acyclic net acnet. Then a place p ∈ P is marked
when at least one transition in its preset has been executed and no transitions in its
postset have been executed. This can be captured as follows:
_ ^
Mark p , int ∧ ¬inu
t∈• p u∈p•
where t∈• p is omitted if p has no input transitions, and u∈p• ¬inu is omitted if p has
W V
no output transitions. The size of the above formula is bounded by 2 · |T |, and it can be
used to answer questions such as: is a specific marking reachable?
The following formula can be used to check whether there is a reachable marking
in which all places in a non-empty set M ⊆ P are marked:
^
ReachM
acnet , Scenarioacnet ∧ Mark p
p∈M
Proposition 8. Let acnet be a well-formed acyclic net and M be a non-empty set of its
places. Then there is a reachable marking M 0 satisfying M ⊆ M 0 iff ReachM
acnet has a
satisfying assignment.
No execution of an acyclic net acnet = (P, T, F) can be extended indefinitely. How-
ever, one may consider a scenario as deadlocked if it is maximal and some of the places
fin
it marks does not belong to Macnet . (Verification of deadlock-freeness using SAT-solvers
has been studied in, e.g., [14,6,5]). All the deadlocked scenarios can be captured by the
following formula:
_
DeadlockScenarioacnet , MaxScenarioacnet ∧ Mark p
fin
p∈P\Macnet
The size of MaxScenarioacnet is bounded by |T |+5·|T |·min{|F|2 , |P|·|T |}+2·|P|·|T |.
3.6 Backward deterministic acyclic nets
In this case, some formulas defined earlier can be simplified:
– Causality: Causalityacnet , t∈T int → u∈• (• t) inu .
V V
– Enabling: Enabledt , u∈(• t)• ¬inu ∧ u∈• (• t) inu .
V V
– Scenario: Scenarioacnet , Causalityacnet ∧ NoForwardConflictacnet .
– Place marking (for p ∈ P and t ∈ T satisfying {t} = • p): Mark p , int ∧ u∈p• ¬inu .
V
– Checking well-formedness is not needed as acnet is well-formed.
4 Communication structured acyclic nets
Communication structured acyclic nets (CSA-nets) add communication to represent the
interaction among several separated subsystems [10]. Each CSA-net is a set of acnets
186 Nadiyah Almutairi and Maciej Koutny
with synchronous or asynchronous communication between their transitions imple-
mented using extra nodes called buffer places (which provided a motivation for a/syn
connections discussed, e.g., in [8]). When two transitions are subject to synchronous
communication, they are always executed together, but under asynchronous communi-
cation they may be executed simultaneously or one of them after the other.
Definition 12 (communication structured acyclic net). A communication structured
acyclic net (or CSA-net) is a tuple csan , (acnet1 , . . . , acnetn , Q,W ) (n ≥ 1) such that:
1. acnet1 , . . . , acnetn are well-formed acyclic nets with disjoint sets of nodes (i.e.,
places and transitions). We also denote:
Pcsan , Pacnet1 ∪ · · · ∪ Pacnetn Qcsan , Q
Tcsan , Tacnet1 ∪ · · · ∪ Tacnetn Wcsan , W
Fcsan , Facnet1 ∪ · · · ∪ Facnetn netcsan,i , acneti (for 1 ≤ i ≤ n) .
2. Qcsan is a set of buffer places and Wcsan ⊆ (Qcsan × Tcsan ) ∪ (Tcsan × Qcsan ) is a set
of arcs adjacent to the buffer places satisfying the following:
(a) Qcsan ∩ (Pcsan ∪ Tcsan ) = ∅.
(b) For every buffer place q:
i. There is at least one transition t such that tWcsan q.
ii. If tWcsan q and qWcsan u then transitions t and u belong to different acneti s.
Moreover, for every x ∈ Pcsan ∪ Tcsan ∪ Qcsan :
precsan (x) , {y | y Fcsan x ∨ yWcsan x}
postcsan (x) , {y | x Fcsan y ∨ xWcsan y}
denote direct predecessors and successors of x.
3. x1 ∈ precsan (x2 ), . . . , xk−1 ∈ precsan (xk ) and x1 = xk imply {x1 , . . . , xk } ∩ Pcsan = ∅,
for all x1 , . . . , xk ∈ Pcsan ∪ Tcsan ∪ Qcsan .
The set of all CSA-nets is denoted by CSAN. ♦
Note that the structure of a CSA-net may include cycles which are a means to implement
synchronous communication. Each such cycle can only involve buffer places. In what
follows, csan = (acnet1 , . . . , acnetn , Q,W ) (n ≥ 1) is a fixed CSA-net.
Definition 13 (step and marking).
1. steps(csan) , {U ∈ P(Tcsan ) \ {∅} | ∀t, u ∈ U : t 6= u =⇒ precsan (t) ∩ precsan (u) =
∅} are the steps of csan.
2. markings(csan) , P(Pcsan ∪ Qcsan ) are the markings of csan.
init , M init init fin
3. Mcsan acnet1 ∪ · · · ∪ Macnetn is the default initial marking of csan, and Mcsan ,
fin fin
Macnet 1
∪ · · · ∪ Macnet n
is the default final marking of csan. ♦
Definition 14 (enabled and executed step). Let M be a marking of csan.
1. enabledcsan (M) , {U ∈ steps(csan) | precsan (U) ⊆ M ∪ (postcsan (U) ∩ Q)} are the
steps enabled at M.
Verification of Communication Structured Acyclic Nets Using SAT 187
2. A step U ∈ enabledcsan (M) can be executed yielding a new marking given by M 0 ,
(M ∪ postcsan (U)) \ precsan (U). This is denoted by M[Uicsan M 0 . ♦
The definition that follow introduce notion similar to those introduced earlier for
acyclic nets.
Definition 15 ((mixed) step sequence). Let µ = M0U1 M1 . . . Mk−1Uk Mk (k ≥ 0) be a
sequence such that M0 , . . . , Mk are markings and U1 , . . . ,Uk are steps of csan.
1. µ is a mixed step sequence from M0 to Mk if Mi−1 [Ui icsan Mi , for every 1 ≤ i ≤ k.
2. If µ is a mixed step sequence from M0 to Mk , then σ = U1 . . .Uk is a step sequence
from M0 to Mk . This is denoted by M0 [σ icsan Mk . Also, M0 [icsan Mk denotes that Mk
is reachable from M0 .
init [σ i
3. sseq(csan) , {σ | Mcsan csan M} are the step sequences of csan.
4. maxsseq(csan) , {σ ∈ sseq(csan) | ¬∃U : σU ∈ sseq(csan)} are the maximal step
sequences of csan. ♦
Thus, in csan the buffer places pass tokens between the different component acyclic
nets. Note that just as acyclic nets, CSA-nets may exhibit backward and forward non-
determinism. Moreover, they can additionally contain cycles involving buffer places.
Within such cycles tokens can be produced and consumed in a single executed step. This
provides a mechanism enabling synchronous communication, and is a feature which is
not supported by acyclic nets (and the standard Petri net models).
acnet1
p2
p1 a b p4
p3
c d
q1 q2 q3
acnet2
e f
p5 p6 p7
Fig. 7. A communication structured acyclic net.
Example 6. In Figure 7, transitions e and c communicate asynchronously, so they can
be executed together, or e then c (but not c before e). On the other hand, d and f must
be executed simultaneously as they are involved in synchronous communication. The
init = {p , p }. The steps are:
initial marking in this case is Mcsan 1 5
steps(csan1 ) = {U ∈ P({a, b, c, d, e, f }) \ {∅} | a ∈ U =⇒ c ∈
/ U} ,
188 Nadiyah Almutairi and Maciej Koutny
and all the maximal step sequences are:
maxsseq(csan) = {{a, e}b, a{b, e}, eab, aeb, abe, ec{d, f }, {e, c}{d, f }} .
Also, for example, postacnet (e) = {p6 , q1 } and the firing of e will produce tokens in
those two places. ♦
Definition 16 (backward deterministic CSA-net). csan is backward deterministic if
the following hold:
1. acnet1 , . . . , acnetn are backward deterministic acyclic nets.
2. | precsan (q)| = 1, for every q ∈ Q. ♦
Definition 17 (sync-cycle). A sync-cycle of csan is a maximal non-empty set of transi-
tions S ⊆ T such that, for all t 6= u ∈ S, (t, u) ∈ W + . The set of all sync-cycles is denoted
by SCcsan . ♦
Note that {t} ∈ SCcsan , for every t ∈ Tcsan . The idea behind the notion of sync-cycles
is to represent maximum number of synchronised communication sub-systems [10]. In
Figure 7, there is one non-singleton sync-cycle S = {d, f }.
4.1 Scenarios of CSA-nets
Scenarios of CSA-nets are based on CSA-nets which involve occurrence nets rather than
acyclic nets.
Definition 18 (communication structured occurrence net). csan is a communication
structured occurrence net (or CSO-net) if the following hold:
1. acnet1 , . . . , acnetn are occurrence nets.
2. | precsan (q)| = 1 and | postcsan (q)| ≤ 1, for every q ∈ Q. ♦
The scenarios of CSA-nets are subnets which are both backward and forward deter-
ministic.
Definition 19 (scenario and maximal scenario).
1. A scenario of csan is a CSO-net cson with n component occurrence nets such that:
(a) netcson,i ∈ scenarios(netcson,i ), for every 1 ≤ i ≤ n.
(b) Qcson ⊆ Q and Wcson ⊆ W .
(c) precson (t) = precsan (t) and postcson (t) = postcsan (t), for every t ∈ Tcson .
2. A maximal scenario of csan is a scenario cson such that there is no scenario cson0
satisfying Tcson ⊂ Tcson0 .
The set of all scenarios of csan is scenarios(csan), and the set of all maximal scenarios
of csan is maxscenarios(csan). ♦
Scenarios represent possible deterministic executions (concurrent histories). Maximal
scenarios are complete in the sense that they cannot be extended any further. Note that
Definition 19(1.a) requires that each component net of cson is a scenario (and so, in
particular, an occurrence net) of the corresponding component acyclic net of csan.
Example 7. Figure 8 represents a CSO-net for csan in Figure 7 which is also one of
its maximal scenarios whose transitions are {e, c, d, f } and no other transitions can be
enabled at the final marking {p4 , p7 }. ♦
Verification of Communication Structured Acyclic Nets Using SAT 189
p1 p4
p3
c d
q1 q2 q3
e f
p5 p6 p7
Fig. 8. A communication structured occurrence net.
4.2 Well-formed CSA-nets
Definition 20 (well-formedness
S
and non-redundant transitions). csan is well-for-
med if sseq(csan)S=S sseq(scenarios(csan)). Moreover, csan has non-redundant tran-
sitions if Tcsan = { σ | σ ∈ sseq(csan)}. ♦
As shown in [9], all CSO-nets are well-formed.
Proposition 9. csan is well-formed iff, for every U1 . . .Uk ∈ sseq(csan):
1. postcsan (t) ∩ postcsan (u) = ∅, for every 1 ≤ i ≤ k and all distinct t, u ∈ Ui .
2. postcsan (Ui ) ∩ postcsan (U j ) = ∅, for all 1 ≤ i < j ≤ k.
5 Verifying properties of CSA-nets
The development and intuitive meaning of formulas needed to check the basic prop-
erties of CSA-nets are similar as in the case of acyclic nets. Therefore, we will avoid
repeating some of the explanations and formal properties. Also, the sizes of formulas
introduced for CSA-nets are similar to those developed for acyclic nets with |T | being
sometimes replaced by |SCcsan | (i.e., the number of syn-cycles of csan).
Identifying scenarios
We say that a set of transitions T 0 ⊆ Tcsan induces a scenario of csan if the following are
satisfied:
– Causality: all non-initial pre-places of T 0 received tokens from T 0 .
– No Forward Conflict: transitions in T 0 are free from forward conflicts.
– No Backward Conflict: transitions in T 0 are free from backward conflicts.
The next definition and proposition make this more formal.
190 Nadiyah Almutairi and Maciej Koutny
Definition 21 (restricting communication structured acyclic net). The restriction of
csan to T 0 ⊆ Tcsan is csan|T 0 , (acnet1 |T 0 , . . . , acnetn |T 0 , Q0 |T 0 ,W |(Q0 ×T 0 )∪(T 0 ×Q0 ) ), where
Q0 = Q ∩ postacnet (T 0 ). ♦
Proposition 10. The following are equivalent for T 0 ⊆ Tcsan :
1. csan|T 0 ∈ scenarios(csan).
2. csan|T 0 is a CSO-net and precsan (T 0 ) \ Mcsan
init ⊆ post 0
csan (T ).
The following boolean variables will be used in the construction of Scenariocsan and
the translation into SAT problem.
– For every t ∈ Tcsan , we have a variable int tracing that t belongs to a scenario.
The constraints on the above variables are defined, following Proposition 3, as follows:
– To ensure that all non-initial pre-places of T 0 received tokens from T 0 :
^ ^ _
Causalitycsan , int → inu
t∈Tcsan init u∈pre
p∈precsan (t)\Mcsan csan (p)
– To ensure that scenario has no forward conflicts:
^ ^
NoForwardConflictcsan , ¬ int ∧ inu
t∈Tcsan u∈postcsan (precsan (t))\{t}
– To ensure that scenario has no backward conflicts:
^ ^
NoBackwardConflictcsan , ¬ int ∧ inu
t∈Tcsan u∈precsan (postcsan (t))\{t}
Note that sometimes parts of the above formulas may be omitted, similarly as in the
case of acyclic nets. Then the formula which characterises all the scenarios of csan is:
Scenariocsan , Causalitycsan ∧ NoForwardConflictcsan ∧ NoBackwardConflictcsan
The satisfying assignments of Scenariocsan identify precisely all the scenarios of csan
which is not necessary well-formed.
Example 8. All the transitions in Figure 9 which have value 1 assigned by the indicated
assignment f represent a scenario for csan because each part of Scenariocsan is satisfied:
Causalitycsan [ f ]
= ((ind → inA ) ∧ (ine → in f ) ∧ (inA → ine )∧
(inB → (ine ∧ inC )) ∧ ((inC → (in f ∧ inB ))) ∧ (in f → 1))[ f ]
= (0 → 0) ∧ (1 → 1) ∧ (0 → 1) ∧ (1 → (1 ∧ 1)) ∧ (1 → (1 ∧ 1)) ∧ (1 → 1) = 1
NoForwardConflictcsan [ f ]
= (¬(inA ∧ inB ) ∧ ¬(inB ∧ inA ))[ f ] = ¬(0 ∧ 1) ∧ ¬(1 ∧ 0) = 1
NoBackwardConflictcsan [ f ]
= (¬(inA ∧ inB ) ∧ ¬(inB ∧ inA ))[ f ] = ¬(0 ∧ 1) ∧ ¬(1 ∧ 0) = 1 .
Hence, Scenariocsan [ f ] = 1 ∧ 1 ∧ 1 = 1. ♦
Verification of Communication Structured Acyclic Nets Using SAT 191
acnet3
p7 d p8
0
q3
acnet1
0 A
p1 e p2 p3
1
1 B
q0 q2 q1
acnet2
p4 f p5 C p6
1 1
Fig. 9. A CSA-net with a scenario indicated by transitions assigned 1.
The formula Scenariocsan represents a scenario in general, which not necessarily
maximal. In order to evaluate the maximality of a scenario, we need to evaluate the
enabledness property as any scenario is maximal iff there are no enabled steps that can
be executed. In this case, however, sync-cycles (which include individual transitions)
rather than individual transitions need to be checked for enabledness.
The following formula captures the enabledness of a syn-cycle, for every S ∈ SCcsan :
^ ^ _
EnabledS , ¬inu ∧ inu .
u∈postcsan (precsan (S)) init ∪(Q∩post
p∈precsan (S)\(Mcsan csan (S))) u∈precsan (p)
Thus S is a set of synchronised transitions whose enabledness depends on each other.
In Figure 9, B and C are transitions involved in synchronous communication and S =
{B,C} is a syn-cycle.
Finally, the following formula represents the set of transitions that induce a maximal
scenario of a well-formed csan:
^
MaxScenariocsan , Scenariocsan ∧ ¬EnabledS .
S∈SCcsan
Evaluating the property of well-formedness is discussed in the next section.
5.1 Well-formedness
Informally speaking, csan in not well-formed if there is a subset of transitions that
induce a scenario which does not violate well-formedness and there is an enabled sync-
192 Nadiyah Almutairi and Maciej Koutny
acnet3
p7 d p8
1
q1
acnet1 acnet2
p1 e p2 p4 f p5
1 0
Fig. 10. A communication structured acyclic net which is not well-formed.
cycle which violates well-formedness after its execution and the definition of a scenario
is violated as well. The following formula detects that a given csan is not well-formed:
_ _
NotWellFormedcsan , Scenariocsan ∧ EnabledS ∧ inu .
S∈SCcsan u∈precsan (postcsan (S))
5.2 Non-redundant transitions, marked places, and deadlocked scenarios
The absence of redundant transitions of csan can be verified in the same way as for an
acyclic net, by checking that, for every t ∈ Tcsan , the following formula has a satisfying
assignment:
NonRedundanttcsan , int ∧ Scenariocsan
The formula for checking whether a place is marked by a scenario is also similar as
before:
_ ^
Markcsan
p , int ∧ ¬inu
t∈precsan (p) u∈postcsan (p)
Moreover, checking whether a set of places is marked by a scenario is achieved by:
^
ReachM
csan , Scenariocsan ∧ Markcsan
p
p∈M
Detecting deadlocked scenarios can then be done using the following formula:
_
DeadlockScenariocsan , MaxScenariocsan ∧ Mark p
fin
p∈Pcsan \Mcsan
Note that it is not required that the buffer places are empty in non-deadlocked markings.
Verification of Communication Structured Acyclic Nets Using SAT 193
5.3 Backward deterministic CSA-nets
When csan is a backward deterministic CSA-net, some formulas defined earlier can be
simplified, for example:
Causalitycsan , t∈Tcsan int → p∈precsan (precsan (t)) inu
V V
, u∈postcsan (precsan (S))¬inu ∧ u∈precsan (precsan (S))\S inu
V V
EnabledS
Then, the formula of Scenariocsan is reduced to:
Scenariocsan , Causalitycsan ∧ NoForwardConflictcsan
and the formula for marking place p with precsan (p) = {t} is:
^
Mark p , int ∧ ¬inu
u∈postcsan (p)
6 Concluding remarks
We presented fundamentals of SAT-based verification of CSA-nets (we also intend to
discuss the acyclicity constraint later on). In the future work, we plan to extend the set of
formulas capturing behavioural properties of CSA-nets, and so enhance the applicability
of the proposed model checking method.
The ongoing work is concerned with an implementation of formulas developed here
in the S ONCRAFT tool [11]. This would allow comparisons of the efficiency of the pro-
posed model checking technique with other approaches (note that verification problems
considered here are NP-complete; see, e.g., [3]). In particular, a comparison with model
checking based on finite prefixes of net unfoldings [4,5] after adapting it to CSA-nets
and their step sequence execution semantics. However, even the unfolding of acyclic
nets, where the forward and backward conflict are allowed, would in the worst case
generate exponential finite prefixes [6]. The method proposed in this paper does not
suffer from a similar problem.
Finally, we expect the model checking approach presented in this paper to be amen-
able to further, relatively straightforward, extensions. In particular, to structured acyclic
nets based on the behavioural structured occurrence nets [9], where the dynamic be-
haviour of a concurrent system is represented at different levels of abstraction.
Acknowledgement
The authors acknowledge financial support provided by University of Hafr Al Batin.
Also, we would like to thank the reviewers for their insightful comments on the submit-
ted paper.
194 Nadiyah Almutairi and Maciej Koutny
References
1. Talal Alharbi. Analysing and visualizing big data sets of crime investigations using structured
occurrence nets (PhD thesis), 2016.
2. Anirban Bhattacharyya, Bowen Li, and Brian Randell. Time in structured occurrence nets.
In Lawrence Cabac, Lars Michael Kristensen, and Heiko Rölke, editors, Proceedings of the
International Workshop on Petri Nets and Software Engineering 2016, Toruń, Poland, June
20-21, 2016, volume 1591 of CEUR Workshop Proceedings, pages 35–55. CEUR-WS.org,
2016.
3. Javier Esparza. Decidability and complexity of Petri net problems - an introduction. In
Wolfgang Reisig and Grzegorz Rozenberg, editors, Lectures on Petri Nets I: Basic Models,
Advances in Petri Nets, the volumes are based on the Advanced Course on Petri Nets, held
in Dagstuhl, September 1996, volume 1491 of Lecture Notes in Computer Science, pages
374–428. Springer, 1996.
4. Javier Esparza and Keijo Heljanko. Unfoldings: A Partial-Order Approach to Model Check-
ing (Monographs in Theoretical Computer Science. An EATCS Series). Springer, 2008.
5. Victor Khomenko. Model checking based on prefixes of Petri net unfoldings (PhD thesis),
2003.
6. Victor Khomenko, Alex Kondratyev, Maciej Koutny, and Walter Vogler. Merged processes:
a new condensed representation of Petri net behaviour. Acta Informatica, 43(5):307–330,
2006.
7. Victor Khomenko, Maciej Koutny, and Alexandre Yakovlev. Detecting state encoding con-
flicts in STG unfoldings using SAT. Fundam. Informaticae, 62(2):221–241, 2004.
8. Jetty Kleijn, Maciej Koutny, and Marta Pietkiewicz-Koutny. Regions of Petri nets with a/sync
connections. Theor. Comput. Sci., 454:189–198, 2012.
9. Maciej Koutny and Brian Randell. Structured occurrence nets: A formalism for aiding sys-
tem failure prevention and analysis techniques. Fundam. Informaticae, 97(1-2):41–91, 2009.
10. Bowen Li. Visualisation and analysis of complex behaviours using structured occurrence
nets (phd thesis), 2017.
11. Bowen Li, Brian Randell, Anirban Bhattacharyya, Talal Alharbi, and Maciej Koutny. Son-
craft: A tool for construction, simulation, and analysis of structured occurrence nets. In 18th
International Conference on Application of Concurrency to System Design, ACSD 2018,
Bratislava, Slovakia, June 25-29, 2018, pages 70–74. IEEE Computer Society, 2018.
12. Paolo Missier, Brian Randell, and Maciej Koutny. Modelling provenance using structured
occurrence networks. In Paul Groth and James Frew, editors, Provenance and Annotation of
Data and Processes - 4th International Provenance and Annotation Workshop, IPAW 2012,
Santa Barbara, CA, USA, June 19-21, 2012, Revised Selected Papers, volume 7525 of Lec-
ture Notes in Computer Science, pages 183–197. Springer, 2012.
13. Ivan Poliakov, Victor Khomenko, and Alexandre Yakovlev. Workcraft - A framework for
interpreted graph models. In Giuliana Franceschinis and Karsten Wolf, editors, Applications
and Theory of Petri Nets, 30th International Conference, PETRI NETS 2009, Paris, France,
June 22-26, 2009. Proceedings, volume 5606 of Lecture Notes in Computer Science, pages
333–342. Springer, 2009.
14. César Rodríguez and Stefan Schwoon. Verification of Petri nets with read arcs. In Ma-
ciej Koutny and Irek Ulidowski, editors, CONCUR 2012 - Concurrency Theory - 23rd In-
ternational Conference, CONCUR 2012, Newcastle upon Tyne, UK, September 4-7, 2012.
Proceedings, volume 7454 of Lecture Notes in Computer Science, pages 471–485. Springer,
2012.
15. Workcraft. https://workcraft.org/, 2018.