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.