We present a framework for the speci cation of distributed protocols based on a logic-based presentation of bipartite graphs. For the considered language, we de ne assertions that can be applied to arbitrary con gurations. We apply the language to model the distributed version of the Dining Philosopher Protocol. The protocol is de ned for asynchronous processes distributed over a graph with arbitrary topology. To validate the protocol, we apply permutation schemes, transformation rules, and inductive veri cation.
Veri cation of distributed systems with parametric dimension is a challenging
task. In this setting protocols are de ned on generic con gurations of a network,
e.g., for an arbitrary number of nodes and arbitrary connection topology.
Protocol rules may depend on the current network con guration. For instance, in [
In this paper we present a formalization of distributed protocols with all above mentioned features based on a logic-based presentation of bipartite graphs de ned over two classes of nodes: agent and edges. A agent corresponds to a network agent. An edge corresponds to a potential link between multiple agents. We use bipartite graphs in order to model both complex topologies and asynchronous operations in a more natural way with respect to standard transition systems. Point-to-point links can be obtained by using conditions de ned on update rules. Our speci cation language is based on a predicated logic with quanti cation de ned over a nite set of typed relations without function symbols. The interpretation domain of relations is de ned over an in nite set of agents and edges. In this setting we can model handshaking between two agents via intermediate steps in which agents rst connect to edges and then, by updating the relations connecting them, start an interaction between them. In our model we admit multiple connections to the same edge.
The technical contribution of the paper is as follows. We rst de ne the
syntax and formal semantics of the BLog speci cation language. The language
is based on conditional update rules. Conditions are expressed as rst order
quanti ed formulas de ned over binary predicates without function symbols.
Update rules are de ned by sets of atomic formulas that specify the ground atoms
that have to be removed from the current con guration and those that have to be
added to the new one. BLog can be viewed as a fragment of richer languages for
representing evolving databases like DCDS [
We apply our language to model the distributed version of the Dining
Philosopher Protocol proposed in [
Related Work
We focus our attention on a class of formal models for concurrent and
distributed systems in which synchronization is achieved by using broadcast
communication, a less standard communication primitive than rendez-vous or
pointto-point communication. Rendez-vous communication involves a xed a priori
number of agents (e.g. a sender and a receiver in point-to-point
communication). Properties of rendez-vous communication have been investigated deeply
in the eld of automated veri cation, see e.g. [
Di erently from [16,26] and [
In this section we will de ne a logic-based presentation of evolving bipartite graphs called BLog.
BLog formulas are based on a simple relational calculus that can be used to express updates of con gurations de ned by sets of ground atoms. Ground atoms de ne relations, i.e., labelled links, between agents and edges. More formally, let P be a nite set of names of binary relations, and V be a denumerable set of variables partitioned in two sets Va and Ve, namely variables ranging over agents and edges, respectively. Furthermore, let N and E be denumerable sets of agent and edge identi ers. We consider here typed binary predicates in which the rst argument is of agent type and the second one is of edge type. Our logic has no function symbols but can be instantiated with elements froN and E . De nition 1. An atomic formula is a formula p(x; y), where p 2 P , x 2 Va, and y 2 Ve. A ground formula is a formula p(n; e), where n 2 N , and e 2 E . A literal is either an atomic formula or the negation :A of an atomic formula A. A formula is a Boolean combination of atomic formulas.
De nition 2. The set of free variables of a formula F , namely F V (F ), is the minimal set satisfying F V (p(x; y)) = fx; yg, F V (A _ B) = F V (A) [ F V (B), F V (A ^ B) = F V (A) \ F V (B), F V (:A) = F V (A), F V (8v:A) = F V (A) n fvg, and F V (9v:A) = F V (A) n fvg. Given S = fF1; : : : ; Fng, we de ne F V (S) = F V (F1) [ : : : [ F V (Fn).
Quanti ed formulas will be used as application conditions of rules. Update rules consists of conditions de ned by quanti ed formulas with no function symbols, a deletion and an addition set. The deletion (resp. addition) set de nes the set of ground atoms that have to be cancelled from (resp. added to) the current con guration. We will consider free variables occurring in conditions to restrict the range of identi ers of a con guration.
De nition 3. A rule has the following form hC; D; Ai, where C is a quanti ed formula, D and A are two sets of predicates with variables in V , and such that F V (A) [ F V (D) F V (C).
Con gurations can be viewed as models in which to evaluate a formula. De nition 4. A con guration is a set of ground atomic formulas.
De nition 5. We use j= A to de ne the satis ability relation of a quanti ed formula A s.t. F V (A) = ;. The relation is de ned by induction as follows. { { { { { j= A, if A 2 ; j= A ^ B, if j= A and j= :A, if 6j= A; j= 8X:A (resp. 8E:A), if (resp. e 2 E );
j= 9X:A (resp. 9E:A), if (resp. e 2 E ).
j= B; j= A[n=X] (resp. A[e=X]) for each n 2 N j= A[n=X] (resp. A[e=X]) for some n 2 N To de ne instantiations of free variables, we consider injective mappings. We use injective mappings in order to give a unique interpretation of a formula like p(X; E) ^ p(Y; F ), i.e., X and Y refer to distinct agents and E and F to distinct edges. We allow multiple occurrences of the same variable to implicitly model equality constraints.
De nition 6. An interpretation is an injective mapping from Va [Ve to N [E s.t. (Va) N and (Ve) E.
De nition 7. Given a con guration , we say that the quanti ed formula A is satis ed in , if there exists an interpretation s.t. j= A is satis able. Example 1. The condition 8X: p(X; E) q(X; E), when evaluated on a conguration , is satis able if there exists an edge e such that for all instances p(n; e) 2 , there exists an atom q(n; e) 2 . Based on these considerations, the rule hlink(X; Y ) ^ 8Z:link(Z; Y )
:own(Z; Y ); ;; fown(X; Y )gi de nes a transition in which for a pair n; e such that link(n; e) occurs in the current con guration and such that there are not other agents n0 s.t. own(n0; e) is in the current con guration, own(n; e) is added to the successor con guration. In the operational semantics we assume that all atomic formulas that are not deleted are transferred to the successor con guration.
For a set S = fA1; : : : ; Ang, we use S to denote the set fA1 ; : : : ; An g. 2.1
Transition System A protocol P is a set of rules. The operational semantics of P is given by a transition system TP = hC; !i, where C is the set of possible con gurations, i.e., nite subsets of ground atoms, and ! C C is a relation de ned as follows. For ; 0 2 C and a rule hC; D; Ai 2 P, ! 0 if there exists s.t. j= C and 0 = ( n D ) [ A .
De nition 8. A computation is a sequence of con gurations 0 1 : : : s.t. i ! i+1 for i 0.
We use ! to denote the re exive and transitive closure of !.
Example 2. Let P be a protocol that contains the rule 8X: link(X; E) own(X; E). Consider = flink(n1; e1); link(n2; e1); link(n3; e3); own(n3; e3)g, we rst notice that does not satisfy the condition link(X; Y ) ^ 8Z:link(Z; Y ) 6j= link(n3; e3) ^ 8Z:link(Z; e3) :own(Z; e3); j= link(n3; e3) and 6j= 8Z:link(Z; e3) :own(Z; e3); 6j= 8Z:link(Z; e3) :own(Z; e3); j= link(n1; e3) :own(n1; e3), since own(n1; e3) 62 j= link(n2; e3) :own(n2; e3), since own(n2; e3) 62 , link(n1; e3) 2 , link(n2; e3) 2 ; ; { { { { { { { 6j= link(n3; e3) :own(n3; e3), since own(n3; e3); link(n3; e3) 2
However, satis es the condition link(X; Y ) ^ 8Z:link(Z; Y ) with the interpretation = [n1=X; e1=Y ]. Indeed, we have that :own(Z; Y ) 6j= link(n1; e1) ^ 8Z:link(Z; e1) :own(Z; e1); j= link(n1; e1) and 6j= 8Z:link(Z; e1) :own(Z; e1); 6j= 8Z:link(Z; e1) :own(Z; e1); j= link(n1; e1) :own(n1; e1), since own(n1; e1) 62 j= link(n2; e1) :own(n2; e1), since own(n2; e1) 62 j= link(n3; e3) :own(n3; e1), since own(n3; e1) 62 Starting from 0 = we obtain then a successor con guration , link(n1; e1) 2 , link(n2; e1) 2 , link(n3; e1) 2 ; ; .
Now, let P be a protocol that contains the rule 1 =
0 [ fown(n3; e3)g hlink(X; Y ); fown(X; Y )g; ;i Starting from that 1 =
1, we can reach 0. Indeed, we have that 0 j= link(n3; e3), and 0 n fown(n3; e3)g.
In a single step of the operational semantics a rule is evaluated in the current con guration by taking a sort of closed-word assumption, i.e., ground atoms that do not occur in a con guration are evaluated to false. Furthermore, atomic formulas that are not deleted are transferred from the current to the successor con guration. The latter property can be viewed then as a sort of frame axiom. It is important to notice that, in general, a con guration has several possible successors. Indeed, depending of the chosen interpretation of free variables the same rule can be applied to di erent subsets of ground atoms contained in the same con guration.
For a set S of con gurations, we de ne the following sets:
P ost(S) = f 0 j 9 P re(S) = f 0 j 9 2 S; ! 2 S; 0 ! 0g g We use P ost (S) (resp. P re (S)) to denote the re exive-transitive closure of P ost (resp. P re). 2.2
Derived and Unary Predicates In the rest of the section we will introduce formulas that de ne special conditions on agents and edges. The formula isoN (n) = :9X:(_r2P r(n; X)) speci es an isolated agent n, i.e., that is not involved in any relation in P . Similarly, the formula isoE(e) = :9X:(_r2P r(X; e)) speci es an edge that is not involved in any relation in P . Conditions like isoN (n) and isoE(e) are building blocks for the de nition of other types of derived predicates. This pattern can be applied anytime it is necessary to avoid interference when constructing new predicates and relations. For instance, if isoE(e) holds, then we de ne rules to add predicates like q(n; e) that associate a state/label q to agent n. Similarly, if isoN (n) holds, then we can add predicates like q(n; e) to associate a state/label to edge e. For the sake of simplicity, in the rest of the paper we use unary predicates, e.g. q(X) and q(E), instead of binary predicate in which one of the arguments is used only as placeholder (e.g. associated to an isolated agent/edge) as in the previous examples. 3
We consider decision problems that generalize the standard notion of reachability between con gurations. The key point is to reason about an in nite set of initial con gurations in order to prove properties for protocol instances with an arbitrary number of agents and edges. For this purpose, we introduce the 9-reachability problem de ned as follows.
De nition 9. Given a protocol P, a set of target con gurations T and a possibly in nite set of initial con gurations I, 9-reachability is satis ed for P, I and T , written 9Reach(P; I; T ), if there exists 2 T and a con guration 1 s.t.
1 2 P ost (I) and 1.
In other words 9Reach(P; I; T ) holds if there exists a con guration 0 2 I s.t. 0 ! 1 and 1 for some 2 T .
In the rest of the paper we will generalize the problem by considering patterns de ned via existentially quanti ed formulas. Generalized 9-reachability is de ned as follows.
De nition 10. Given a protocol P and a formula with free variables in S and a set of initial con gurations I, generalized 9-reachability is satis ed for P, I, and , written 9Reach(P; I; ), if there exists an interpretation , a con guration s.t. j= , and a con guration 1 s.t. 1 2 P ost (I) and 1. 3.1
Undecidability The 9-Reachability problem turns out to be undecidable. A proof can be constructed by reducing the halting problem for Turing machines to 9-reachability. The idea of the construction is as follows. Let M = h ; Q; ; q0; F i be a Turing machine in which Q is the set of control states, is the tape alphabet that includes the special blank symbol B, F Q is the set of nal states, q0 is the initial state, and : Q ! Q fL; Rg is the transition relation. Given an input word w 2 without blanks, we rst de ne a bipartite graph that encodes w. We use here three types of relations: { The atomic formula q(n1; e1) is used to represent the state of the head pointing to cell n1. { The atomic formula `(n1; e1) is used to represent a cell n1 containing symbol `. { The atomic formula next(n2; e1) is used to link, via edge e1, a cell to its successor cell identi ed by agent n2.
Creation of the word w = a1 : : : an and initialization of the tape head are de ned by the rule (^in=1isoN (Xi) ^ isoE(Ei); ;; A), where
A = fq0(X1; E1); a1(X1; E1); next(X2; E1); a2(X2; E2); : : : ; an(Xn; En)g This rule selects n isolated agents and edges and de nes a zig-zag graph in which we keep the information about letters and pointers to the adjacent cells.
To simulate a transition (q1; a) = hq2; b; Ri we use the rules r1 = hC1; D1; A1i and r2 = hC2; D2; A2i, where { C1 = q1(X1; E1) ^ a(X1; E1) ^ next(X2; E1) ^ W`2 `(X2; E2), { D1 = fq1(X1; E1); a(X1; E1)g and A1 = fq2(X2; E2); b(X2; E2)g. { C2 = q1(X1; E1) ^ a(X1; E1) ^ isoN (X2) ^ isoE(E2) ^ :9Z:next(Z; E1), { D2 = fq1(X1; E1); a(X1; E1)g, { A2 = fnext(X2; E1); q2(X2; E2); b(X2; E2)g.
The former rule updates the relation associated to the encoding of the cell pointed to by the head assuming that there exists another cell at its right. If there are no representations of cells at its right, i.e., the relation next is not dened, the latter rule can be applied to generate a representation of a blank cell. To simulate a transition (q1; a) = hq2; b; Li we use the rules r3 = hC3; D3; A3i and r4 = hC4; D4; A4i where { C3 = q1(X2; E2) ^ a(X2; E2) ^ next(X2; E1) ^ W`2 `(X1; E1), { D3 = fq1(X2; E2); a(X2; E2)g and A3 = fq1(X1; E1); b(X2; E2)g. { C4 = q1(X1; E1) ^ a(X1; E1) ^ isoN (X2) ^ isoE(E2) ^ :9F:next(X1; F ), { D4 = fq1(X1; E1); a(X1; E1)g, { A4 = fnext(X1; E2); q2(X2; E2); b(X1; E1); B(X2; E2)g.
The former rule updates the relation associated to the encoding of the cell pointed to by the head assuming that there exists another cell at its left. If there are no representations of cells at its left, the latter rule can be applied to generate a representation of a blank cell.
The set of initial con gurations I consists of an arbitrary number of isolated agents and edges, i.e., it contains a con guration n;m for each possible number n of agents and m of edges. Let us indicate with the con guration of the Turing machine represented by .
Namely, if
= fa1(n1; e1); next(n2; e1); a2(n2; e2); : : : ; ak(nk; ek); qi(nj; ej)g then = a1 : : : aj 1qiaj : : : ak. By construction, the application of a rule produced by the encoding preserve the well-formedness of the encoding of con gurations. The following properties then holds.
Proposition 1. Let PM be the encoding of the Turing machine M and If 0 ! 1, then there exists a computation in M from 0 to 1. 0 2 I.
Indeed, by construction, each step of a computation in PM mimics the application of transitions in M . 0 contains nitely many agents and edges, the size of visited part of tape in the computation in M is bounded by the cardinality of 0.
Proposition 2. Let PM be the encoding of the Turing machine M and 0 = q0w an initial con guration of M on input w. If 1 is reachable from 0, then there exists 0 2 I and 1 s.t. 0 = 0, 1 = 1, and 0 ! 1.
If 1 is reachable from 0, then there is a nite upperbound k on the number of cells visited by the machine. Let 0 be an initial con guration with at least n (isolated) agents and edges. By applying a creation rule, we can generate a con guration 00 that represents the initial con guration 0. By construction of PM , a step from i to i+1 can be simulated by the application of a rule in PM . The choice of 0 ensures us that we can always select isolated agents and edges when needed, i.e., when the machine moves to a blank cell to the left or right of the visited part of the tape.
The following property then holds.
Theorem 1. Let PM be the encoding of the Turing machine M . The Halting problem for M can be reduced to 9-Reachability in PM by taking the formula = Wq2F q(X; Y ) as representation of subcon gurations denoting a nal state. 4
In this section we consider possible application of BLog to the speci cation of distributed protocols. The key ingredient of the speci cation language is the combination of complex conditions and update rules to reason on bipartite graphs in which predicates can be viewed as labels of links between agents and edges. We have shown that we can also add labels to individual agents and edges, e.g., to represent their current state. Update rules can be used to dynamically recon gure the graph, i.e., change labels, topology and add or delete agents. The separation between agents and edges is convenient to model asynchronous communication. For instance, let us consider a protocol in which two agents need to establish a connection via a shared bu er.
{ An agent n1 of type A connects to an edge e1 in idle state (the bu er is free) and sets the state of the bu er to ready. { An agent n2 of type B connects to e1 in state ready and changes the state to readyack. { Agent n1 sends message m by changing the state of e1 to msgm. { Agent n2 receive message m and updates the state of the channel to readyack for further communications.
The protocol can be speci ed as follows. We use unary predicates to associate states to edges.
Rule reqA1 = (C1; D1; A1) is s.t. C1 = idle(E) ^ :send(X; E), D1 = fidle(E)g, A1 = fready(E); req(X; E)g Rule reqB1 = (C2; D2; A2) is s.t. C2 = ready(E) ^ :rec(X; E), D2 = fready(E)g, A2 = freadyack(E); rec(X; E)g.
Rule reqA2 = (C3; D3; A3) is s.t. C3 = readyack(E) ^ send(X; E), D3 = freadyack(E); send(X; E)g, A3 = fmsgm(E)g Rule reqA3 = (C4; D4; A4) is s.t. C4 = msgm(E) ^ rec(X; E), D4 = fmsgm(E); rec(X; E)g, A4 = fidle(E)g
An initial state consists of a bipartite graph de ned by the con guration of the following form idle(e1); : : : ; idle(ek), where ei 6= ejfor i 6= j, i; j : 1; : : : ; k.
The model provides other form of interactions. For instance, we can model ordered bu ers by forming lists of messages attached to a given edge as in the representation of the tape of the Turing machine. We can also model synchronous communication by using rules like (C; D; A) de ned as: { C = link(X; E) ^ s1(X; F ) ^ link(Y; E) ^ s2(Y; G) { D = fs1(X; F ); link(X; E); link(Y; E); s2(Y; G)g { A = flink(X; E); s01(X; F ); link(Y; E); s02(Y; G)g where s1(X; F ) is a relation used to denote state of agent X, link(X; E); link(Y; E) is a relation used to share a common bu er E, and s2(Y; G) is a relation used to denote state of agent Y , etc. 5
We consider here a distributed version of the dining philosopher mutual exclusion
problem presented in [
A moves back to idle state.
In a statically de ned topology, agent A gets access to a resource when all neighbors are either idle or are waiting for acquiring some channel. Communication between two neighbors is asynchronous. Indeed, they interact by reading and writing on the shared channel. The protocol should guarantee that two agents that share the same channel cannot acquire and use a resource simultaneosly. The protocol should be robust under dynamic recon gurations of the network.
Correctness Mutual exclusion for the considered protocol can be formulated in its more general form, i.e., for any number of agents, as the negation of an 9-reachability problem. More speci cally, let be the formula
busy(N ) ^ busy(M ) ^ link(N; G) ^ link(M; G) that denotes a con gurations in which two agents share the same channel. We have that 9Reach(PM ; I; ) holds if and only if mutual exclusion does not hold for DDP. 6
In this section we de ne a sort of canonical form for computations in Pddp obtained via permutation and deletion schemes that we can be uses to synthesize derived rules that are equivalent w.r.t. our correctness criteria. 6.1
Permutation and Deletion Schemes We rst consider deletion and permutation properties of rule applications within a given computation. We focus our attention on link and unlink rules, i.e., dynamic recon gurations of the graph topology. Let = 0 1 2 be a computation in Pddp and let r1; r2 be the transitions applied in each step.
{ We rst observe that if r2 is an instance of the unlink rule applied to n1; e1, and r1 is an instance of rule link applied to the same pair, they can be eliminated since 0 = 2. { If r1 is an instance of the getE rule applied to agent n1; e1, and r2 is an application of relE applied to the same pair, then they can be eliminated since 0 = 2. { We now observe that unlink can be permuted with every other rule applied to di erent pairs to its left in a computation. Namely, if r2 is an instance of the unlink rule applied to n1; e1, and r1 is a rule that is not applied to n1; e1, then we can permute the application of the two rules and obtain a new computation leading to the same con guration. { If r1 is an instance of the link rule applied to n1; e1, and r2 is an application of any other rule on a di erent pair, then we can permute the applications of the two rules and obtain a new computation leading to the same con guration. We can now reason on the previous properties in order to consider sets of equivalent computations and infer derived blocks of rules and new permutation rules. More speci cally, given a computation we can obtain an equivalent, w.r.t. our correctness criteria, computation 0 by applying the following steps: { We can eliminate all applications of recon gurations, i.e., link and unlink, performed on the same pair n; e, if in between their occurrences in a computation there are no occurrences of instances of getE on the same pair. The property can be obtained by repeatedly applying permutation rules so as to push applications of link towards the rst occurrence of unlink and then apply the corresponding deletion rules. { We can eliminate all applications of acquire getE and relE on the same pair n; e, if there are no occurrences of acquire involving n in between. Again, the property can be obtained by repeatedly applying permutation rules so as to push applications of relE towards the rst occurrence of getE to its left. { We can push the application of link rules close to the rst occurrence of a corresponding getE rule to its left.
Following from the previous properties, from any computation we can extract a subcomputation in which occurrences of relE occur only after occurrences of acquire on the same pair. Similarly, we can push occurrences of unlink so as to occur only after occurrences of acquire. In other words we can derive rules obtained by combining link and reqE. The resulting pattern, link reqE, is used to simultaneously link an agent to an edge and acquire its ownership. Similarly, since computations in which relE and unlink on speci c pairs occur after acquire, we can use permutations in order to cluster all occurrences of patterns relE unlink occurring before an acquire. In other words, we can use permutations of patterns link reqE with other rules or patterns operating on di erent agents, in order to push all their occurrences close to the rst acquire on their right involving the same agent. This properties leads to patterns of the form (link reqE) acquire. We now observe that the pattern can be used by agent n to simultaneously acquire the ownership of a given set of edges e1; : : : ; en, and update the local state to busy. We can reason on permutations of unlink, relE and release in a similar way, i.e., apply permutations to cluster the sequence of applications of these rules involving the same agent after an acquire. The resulting sequence can be represented by the pattern (relE unlink) release. In other words in the resulting patterns the link relation is updated in parallel with the own relation. The pattern (link reqE) acquire cannot be represented via a single rule in our speci cation language, since it may involve an arbitrary number of edges. To express this pattern, we can use a family frkgk 0 of rules, where rk = (Ck; Dk; Ak) is de ned as: { Ck = idle(X) ^ Vik=1 :link(X; Ei) ^ 8Z: Vik=1 :own(Z; Ei), { Dk = fidle(X)g, { Ak = fbusy(X); link(X; E1); own(X; E1); : : : ; link(X; Ek); own(X; Ek)g. The rule associates agent X to an arbitrary subset of edges. The association is de ned via the ownership predicate.
The pattern (relE unlink) release is expressed by the in nite family fskgk 0 of rules. Rule sk = (Ck; Dk; Ak) is de ned as: { Ck = busy(X) ^ Vik=1 link(X; Ei) ^ own(X; Ei), { Dk = fbusy(X); link(X; E1); own(X; E1); : : : ; link(X; Ek); own(X; Ek)g, { Ak = fidle(X)g.
This rule can be applied to a subset of all edges connected to a given agent. This corresponds to a sequence of applications on release and relE. 6.3
Deductive Reasoning To verify correctness, we have to prove that the formula
= :9X; Y:busy(N ) ^ busy(M ) ^ link(N; G) ^ link(M; G) is an invariant for our system. To prove the property, we will strenghten the invariant proving that 0 = ^ where = (8Z; E:link(Z; E) own(Z; E)), is still an invariant of the resulting rule. By de nition 0 holds in any initial con guration m;n, since initial congurations only contain agents in state idle. The key point is to show that 0 is preserved by applications of rule rk and sk for any k 0.
Consider a con guration with cardinality n and assume that j= 0. Now consider rk s.t. k n. If rk can be applied to , there exists an interpretation s.t. j= Ck where Ck = (idle(X)^Vik=1 :link(X; Ei)^8Z: Vik=1 :own(Z; Ei)). This implies that there exists an agent n s.t. idle(n) 2 , and there exist e1; : : : ; en s.t. link(m; ei); own(m; ei) 62 for i : 1; : : : ; k and for any m occurring in . The application of the rule yields a con guration 0 de ned as 0 =
[ flink(n; e1); : : : ; link(n; ek); own(n; e1); : : : ; own(n; ek); busy(n)g Since by assumption own(m; ei); link(m; ei) 62 for any m occurring in and i : 1; : : : ; k, we have that 0 j= 0.
Now consider a con guration with cardinality n and assume that j= 0. Now consider sk s.t. k n. If sk can be applied to , there exists an interpretation s.t. j= Ck where Ck = (busy(X)^Vik=1 link(X; Ei)^own(X; Ei)). This implies that there exists an agent n s.t. busy(n) 2 , and there exist e1; : : : ; en s.t. link(n; ei); own(n; ei) 2 for i : 1; : : : ; k. The application of the rule yields a con guration 0 de ned as 0 =
n flink(n; e1); : : : ; link(n; ek); own(n; e1); : : : ; own(n; ek)g [ fidle(n)g Although the rule might remove a strict subset of link and own predicates involving n, the resulting con guration still satis es 0.
Since , k, and are chosen in arbitrary way, we have that the considered invariant 0 is an invariant for the whole family of rules of type sk and rk with k 0.
Finally, we observe that for any we have that if j= 0 then j= . This prove that is still an invariant for the model resulting from the transformation described in the previous sections. 7
We have presented a formal language for the speci cation of asynchronous distributed systems based on logic-based update rules for bipartite graphs. For the considered language, we have presented a veri cation approach that combines transformation schemes based on permutation properties and inductive veri cation. The proposed approach can be applied to verify the correctness of a distributed version of the dining philosopher protocol regardless the network topology and the number of nodes. Mechanization of the considered proof method could be an interesting direction for future work. 16. J. Stuckrath. Uncover: Using coverability analysis for verifying graph transformation systems. In Graph Transformation - 8th International Conference, ICGT 2015, Held as Part of STAF 2015, L'Aquila, Italy, July 21-23, 2015. Proceedings, pages 266{274, 2015. 17. https://github.com/pierreganty/mist. 18. http://users.mat.unimi.it/users/ghilardi/mcmt/. 19. http://www.ahmedrezine.com/tools/. 20. http://www.ccs.neu.edu/home/wahl/Research/boom-and-cutoffs.html. 21. http://www.it.uu.se/research/docs/fm/apv/tools/pfs/. 22. http://www.it.uu.se/research/docs/fm/apv/tools/undip/. 23. http://www.liafa.jussieu.fr/~sighirea/trex/. 24. http://www.lsv.ens-cachan.fr/Software/fast/. 25. http://www.montefiore.ulg.ac.be/~boigelot/research/lash/. 26. http://www.ti.inf.uni-due.de/de/research/tools/uncover/.