Model checking is an established strategy for automatic verification of software and hardware systems. It supports extensive analyses of the properties 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 communicate 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.
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
correct design poses a significant challenge [
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 [
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 SONCRAFT.
The paper is organised as follows. In Section 2, we provide basic definitions concerning 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 definitions 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
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 2 T , there are p; q 2 P such that pFt and tFq. } For every x 2 P [ T , x = preacnet (x) , fy j yFxg and x = postacnet (x) , fy j xFyg 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 j pj > 1, for some p 2 P) and forward non-determinism (if jp j > 1, for some p 2 P).
Definition 2 (step and marking). Let acnet = (P; T; F) be an acyclic net. 1. steps(acnet) , fU 2 P(T ) n f?g j 8t; u 2 U : t 6= u =)
3. Maincintet , fp 2 P j p = ?g is the default initial marking, and Maficnnet , fp 2 P j p = ?g is the default final marking. } t \ u = ?g are the steps.
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. Definition 3 (enabled and executed step). Let M be a marking of an acyclic net acnet.
Note that markings of acyclic nets are ‘safe’ by definition. The emptiness of the postplaces 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 m be a sequence M0U1M1 : : : Mk 1UkMk (k 0) such that M0; : : : ; Mk are markings and U1; : : : ;Uk are steps.
2. If m is a mixed step sequence from M0 to Mk, then s = U1 : : :Uk is a step sequence from M0 to Mk. This is denoted by M0[s iacnet Mk.
M0 U!1 M1 : : : Mk 1 U!k Mk.
If k = 0 then m = M0 and the corresponding step sequence s is the empty sequence denoted by l . A mixed step sequence M0U1M1 : : : Mk 1UkMk can also be denoted as } Definition 5 (behavioural notions). Let acnet be an acyclic net. 1. sseq(acnet) , fs j Maincintet[s iacnet Mg are the step sequences of acnet.
step sequences of acnet. } We usually treat individual transitions as singleton steps; for instance, a step sequence ftgfugfw; vgfzg can be denoted by tufw; vgz.
Definition 6 (structural notions). Let acnet = (P; T; F) be an acyclic net. 1. Two transitions t 6= u 2 T are in direct (forward) conflict, denoted t#0u, if they have a common place in their presets, i.e., t \ u 6= ?. 2. Two transitions t 6= u 2 T are in direct backward conflict if they have a common place in their postsets, i.e., t \ u 6= ?.
such that t#0u and (t; x); (u; y) 2 F .
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 [
Definition 7 (backward deterministic acyclic net). A backward deterministic acyclic net is an acyclic net acnet = (P; T; F) such that j pj 1, for all p 2 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 sequences.
Occurrence nets and scenarios
An occurrence net [
Definition 9 (scenario and maximal scenario). Let acnet be an acyclic net. 1. A scenario of acnet is an occurrence net ocnet such that: (a) Tocnet Tacnet and Pocnet = Maincintet [ postacnet (Tocnet).
(b) preocnet (t) = preacnet (t) and postocnet (t) = postacnet (t), for every t 2 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. }
Example 2. Figure 3 illustrates the last point by identifying two maximal scenarios, ocnet1 = scenarioacnet(fa; e; g; hg) and ocnet2 = scenarioacnet(fa; f ; g; hg), of the acyclic net acnet in Figure 1. For example, ocnet1 captures the following five executions: a fe;gg h fp0g ! fp1; p2g ! fp3; p5g ! fp4; p5g,
a e g h fp0g ! fp1; p2g ! fp2; p3g ! fp3; p5g ! fp4; p5g,
a e fg;hg fp0g ! fp1; p2g ! fp2; p3g ! fp4; p5g,
a e h g fp0g ! fp1; p2g ! fp2; p3g ! fp2; p4g ! fp4; p5g, and
a g e h fp0g ! fp1; p2g ! fp1; p5g ! fp3; p5g ! fp4; p5g. }
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.
Definition 10 (well-formedness and non-redundant transitions). An acyclic net acnet is well-formed if sseq(acnet) = S sseq(scenarios(acnet)). Moreover, acnet has nonredundant transitions if Tacnet = SfS s j s 2 sseq(acnet)g. }
Proposition 2. acnet is well-formed iff the following hold for every step sequence U1 : : :Uk 2 sseq(acnet): 1. t \ u = ?, for every 1 2. Ui \ U j = ?, for all 1 i i < j k and all distinct t; u 2 Ui.
k. 3
The task of a SAT-solver is to find a satisfying assignment for the variables used in a propositional boolean formula f . That is, the SAT-solver looks for an assignment f : Var ! f0; 1g for the variables Var which occur in f that makes f true, i.e., f [ f ] = 1. And, if such an assignment exists, f is satisfiable. The formula f 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). 3.1 Identifying scenarios For a given acyclic net acnet = (P; T; F), a subset of transitions T 0 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 acnetjT 0 = (P0; T 0; Fj(P0 T 0)[(T 0 P0)), where P0 = Maincintet [ postacnet (T 0), is the restriction of acnet to T 0. } Note that if acnetjT 0 is a scenario, then acnetjT 0 = scenarioacnet(T 0).
Proposition 3. The following statements are equivalent for an acyclic net acnet = (P; T; F) and T 0 T :
2. acnetjT 0 is an occurrence net and preacnet (T 0) n Maincintet postacnet (T 0).
scenarios of an acyclic net acnet, i.e., to construct a formula Scenarioacnet which evaluates 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 2 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 ! t2T ^
_ inu
NoForwardConflictacnet , ^ ^
:(int ^ inu) t2T u2( t) nftg where Vu2( t) nftg :(int ^ inu) is omitted if ( t) = ftg. – To ensure that scenario has no backward conflicts:
NoBackwardConflictacnet , ^ ^
:(int ^ inu) t2T u2 (t )nftg where Vu2 (t )nftg :(int ^ inu) is omitted if (t ) = ftg.
The size of the above formula (in terms of the occurrences of literals) is bounded by jT j + 3 jT j minfjFj2; jPj jT jg.
Proposition 4. Let acnet be an acyclic net.
acnet. 2. For every scenario acnet0 of the acyclic net acnet, there is a satisfying assignment f for Scenarioacnet such that acnetj 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 To characterise well-formed acyclic nets, we introduce formulas capturing the enabledness of transitions, for every t 2 T :
Enabledt ,
^ :inu ^ u2( t) ^
_ inu 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 transition which can be executed after that violating well-formedness.
The size of the above formula is bounded by jT j + 6 jT j minfjFj2; jPj jT jg. t2T p3 p4 p5 c 0 d 1
_ inu u2 (t ) p6 p7 p0 e 1 p1 p2 a 0 b 1
Fig. 4. An acyclic net which is not well-formed. 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 assignment f illustrated in Figure 4 (where f (e) = f (b) = f (d) = 1 and f (a) = f (c) = 0) we have the following: (i) Scenarioacnet evaluates to 1 inducing scenarioacnet(fe; b; dg); (ii) Enableda[ f ] = 1; and (iii) (Wu2 (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. p0 Example 4. Consider the backward deterministic acyclic net in Figure 5. The two transitions g and h are in direct conflict, and so c is in a self-conflict. This means that c can never be executed, i.e., there is no step sequence s 2 sseq(acnet) such that c 2 S s . 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. }
NonRedundanttacnet , int ^ Scenarioacnet :
is satisfiable, for each t 2 T .
Proposition 6. A well-formed acyclic net acnet has non-redundant transitions iff the formula NonRedundanttacnet is satisfiable, for every t 2 T . 3.4
Maximal scenarios Maximal scenarios are complete scenarios, which means that no transitions are enabled.
MaxScenarioacnet , Scenarioacnet ^ ^ :Enabledt The size of MaxScenarioacnet is bounded by jT j + 5 jT j minfjFj2; jPj jT jg. Intuitively, it is satisfiable for all the scenarios that do not enable any transitions.
Proposition 7. Let acnet be a well-formed acyclic net.
scenario of acnet. 2. For every maximal scenario acnet0 of acnet, there is a satisfying assignment f for MaxScenarioacnet such that acnetj 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. p3 p4
t2T p0 1 g 0
Example 5. Figure 6 shows a well-formed acyclic net that exhibits both forward and backward conflict. Observe that all the transitions in fx; e; f ; hg satisfy the causality condition, and have no forward nor backward conflict. They also lead to a marking fp5g where no transitions are enabled. Therefore, the set of transitions fx; e; f ; hg induces 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). }
Marked places and deadlocked scenarios Consider a scenario of a well-formed acyclic net acnet. Then a place p 2 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:
Markp , _ int ^ t2 p u2p ^ :inu where Wt2 p is omitted if p has no input transitions, and Vu2p :inu is omitted if p has no output transitions. The size of the above formula is bounded by 2 jT j, and it can be used to answer questions such as: is a specific marking reachable?
ReachaMcnet , Scenarioacnet ^ ^ p2M
Markp 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 M0 satisfying M M0 iff ReachaMcnet has a satisfying assignment.
No execution of an acyclic net acnet = (P; T; F) can be extended indefinitely.
However, one may consider a scenario as deadlocked if it is maximal and some of the places
it marks does not belong to Maficnnet. (Verification of deadlock-freeness using SAT-solvers
has been studied in, e.g., [
_ p2PnMaficnnet
Markp The size of MaxScenarioacnet is bounded by jT j + 5 jT j minfjFj2; jPj jT jg + 2 jPj jT j. 3.6
Backward deterministic acyclic nets In this case, some formulas defined earlier can be simplified: – Causality: Causalityacnet , Vt2T int ! Vu2 ( t) inu . – Enabling: Enabledt , Vu2( t) :inu ^ Vu2 ( t) inu. – Scenario: Scenarioacnet , Causalityacnet ^ NoForwardConflictacnet. – Place marking (for p 2 P and t 2 T satisfying ftg = p): Markp , int ^ Vu2p :inu. – Checking well-formedness is not needed as acnet is well-formed. 4
Communication structured acyclic nets (CSA-nets) add communication to represent the
interaction among several separated subsystems [
Qcsan , Q Wcsan , W netcsan;i , acneti (for 1
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 tWcsanq.
ii. If tWcsanq and qWcsanu then transitions t and u belong to different acnetis.
precsan (x) , fy j y Fcsan x _ yWcsan xg postcsan (x) , fy j x Fcsan y _ xWcsan yg denote direct predecessors and successors of x. 3. x1 2 precsan (x2); : : : ; xk 1 2 precsan (xk) and x1 = xk imply fx1; : : : ; xkg \ Pcsan = ?, for all x1; : : : ; xk 2 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). 3. Mcinsaitn , Maincintet1 [
Maficnnet1 [ [ Macnetn is the default final marking of csan.
fin 1. steps(csan) , fU 2 P(Tcsan) n f?g j 8t; u 2 U : t 6= u =) precsan (t) \ precsan (u) = ?g are the steps of csan.
[ Maincintetn is the default initial marking of csan, and Mcfisnan , } Definition 14 (enabled and executed step). Let M be a marking of csan.
steps enabled at M.
i
n) : Qcsan) is a set
Definition 15 ((mixed) step sequence). Let m = M0U1M1 : : : Mk 1UkMk (k sequence such that M0; : : : ; Mk are markings and U1; : : : ;Uk are steps of csan. 0) be a 1. m is a mixed step sequence from M0 to Mk if Mi 1[Uiicsan Mi, for every 1 i k. 2. If m is a mixed step sequence from M0 to Mk, then s = U1 : : :Uk is a step sequence from M0 to Mk. This is denoted by M0[s icsan Mk. Also, M0[icsan Mk denotes that Mk is reachable from M0. 3. sseq(csan) , fs j Mcinsaitn[s icsan Mg are the step sequences of csan. 4. maxsseq(csan) , fs 2 sseq(csan) j :9U : sU 2 sseq(csan)g are the maximal step sequences of csan. }
nets. Note that just as acyclic nets, CSA-nets may exhibit backward and forward nondeterminism. 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).
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 initial marking in this case is Mcinsaitn = fp1; p5g. The steps are:
steps(csan1) = fU 2 P(fa; b; c; d; e; f g) n f?g j a 2 U =) c 2= U g ; and all the maximal step sequences are:
maxsseq(csan) = ffa; egb; afb; eg; eab; aeb; abe; ecfd; f g; fe; cgfd; f gg : Also, for example, postacnet (e) = fp6; q1g and the firing of e will produce tokens in those two places. 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. j precsan (q)j = 1 and j postcsan (q)j 1, for every q 2 Q. }
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 2 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 2 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 fe; c; d; f g and no other transitions can be enabled at the final marking fp4; p7g. } Definition 20 (well-formedness and non-redundant transitions). csan is well-formed if sseq(csan) = S sseq(scenarios(csan)). Moreover, csan has non-redundant transitions if Tcsan = SfS s j s 2 sseq(csan)g. }
1. postcsan (t) \ postcsan (u) = ?, for every 1 2. postcsan (Ui) \ postcsan (U j) = ?, for all 1 i k and all distinct t; u 2 Ui. i < j k. 5
The development and intuitive meaning of formulas needed to check the basic properties 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 jT j being sometimes replaced by jSCcsanj (i.e., the number of syn-cycles of csan). Identifying scenarios
– 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.
Definition 21 (restricting communication structured acyclic net). The restriction of csan to T 0 Tcsan is csanjT 0 , (acnet1jT 0 ; : : : ; acnetnjT 0 ; Q0jT 0 ;W j(Q0 T 0)[(T 0 Q0)), where Q0 = Q \ postacnet (T 0). } Proposition 10. The following are equivalent for T 0 Tcsan:
2. csanjT 0 is a CSO-net and precsan (T 0) n Mcinsaitn postcsan (T 0).
the translation into SAT problem.
– For every t 2 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 ,
^ t2Tcsan int ! ^ _
inu p2precsan (t)nMcinsaitn u2precsan (p) – To ensure that scenario has no forward conflicts: – To ensure that scenario has no backward conflicts:
NoForwardConflictcsan , NoBackwardConflictcsan , ^ ^ ^
: int ^ inu t2Tcsan u2postcsan (precsan (t))nftg ^
: int ^ inu t2Tcsan u2precsan (postcsan (t))nftg 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:
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. } 1 p2 q2 p5 q3 d 0
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 2 SCcsan: EnabledS ,
^ u2postcsan (precsan (S)) :inu ^ _
inu : p2precsan (S)n(Mcinsaitn[(Q\postcsan (S))) u2precsan (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 = fB;Cg is a syn-cycle.
scenario of a well-formed csan:
5.1 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 syncacnet1 p1 p4 f 0 acnet2 p5 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:
_
_ u2precsan (postcsan (S)) inu :
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 2 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:
Markcpsan ,
_ t2precsan (p) int ^
^ :inu
p2M ReachcMsan , ^ Scenariocsan ^ Markcpsan
_ p2PcsannMcfisnan
Markp Note that it is not required that the buffer places are empty in non-deadlocked markings. 5.3
Backward deterministic CSA-nets When csan is a backward deterministic CSA-net, some formulas defined earlier can be simplified, for example:
Causalitycsan , Vt2Tcsan int ! Vp2precsan (precsan (t)) inu
EnabledS , Vu2postcsan (precsan (S)):inu ^ Vu2precsan (precsan (S))nS inu
and the formula for marking place p with precsan (p) = ftg is:
^ :inu 6
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 SONCRAFT tool [
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 submitted paper.