We present a framework for the specification of distributed protocols based on a logic-based presentation of bipartite graphs. For the considered language, we define assertions that can be applied to arbitrary configurations. We apply the language to model the distributed version of the Dining Philosopher Protocol. The protocol is defined for asynchronous processes distributed over a graph with arbitrary topology. To validate the protocol, we apply permutation schemes, transformation rules, and inductive verification.
Verification of distributed systems with parametric dimension is a challenging task. In this setting protocols are defined on generic configurations of a network, e.g., for an arbitrary number of nodes and arbitrary connection topology. Protocol rules may depend on the current network configuration. For instance, in [14] Namjoshi and Trefler introduced a distributed variant of the dining philosopher protocol in which individual nodes interact asynchronously via shared buffers. Global conditions formulated on the state of visible buffers are used to regulate the access to resources shared between adjacent nodes.
In this paper we present a formalization of distributed protocols with all above mentioned features based on a logic-based presentation of bipartite graphs defined 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 defined on update rules. Our specification language is based on a predicated logic with quantification defined over a finite set of typed relations without function symbols. The interpretation domain of relations is defined over an infinite set of agents and edges. In this setting we can model handshaking between two agents via intermediate steps in which agents first 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 first define the syntax and formal semantics of the BLog specification language. The language is based on conditional update rules. Conditions are expressed as first order quantified formulas defined over binary predicates without function symbols. Update rules are defined by sets of atomic formulas that specify the ground atoms that have to be removed from the current configuration 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 [8]. Differently from DCDS, designed for updates of relational databases, we are interested here in a minimal fragment of relational logic to reason about evolving bipartite graphs. Furthermore, we focus our attention on a special class of decision problems that can be viewed as parametric versions of reachability problems. More specifically, in order to reason about families of distributed systems we consider reachability problems existentially quantified over initial configurations as in previous work on formal verification of parameterized systems. Furthermore, we isolate a fragment of BLog in which we show that the considered decision problem is undecidable. The proof is based on an encoding of Turing machines on a special type of bipartite graphs in which we used special links to order the representation of tape cells.
We apply our language to model the distributed version of the Dining Philosopher Protocol proposed in [15]. The protocol is defined for asynchronous processes distributed over a graph with arbitrary topology. We model the protocol by considering dynamic reconfigurations of the topology. To verify the correctness of our model, we apply a proof method that combines two kinds of reasoning. We first apply source to source transformations based on permutation schemes that lead to derived rules. Permutation schemes are obtained via a proof theoretic analysis of computations. Permutation rules can be applied to derive meta rules obtained by composing sequences of rule applications of the original protocol. We use deductive reasoning to prove mutual exclusion on the resulting model. Invariants are expressed using parametric formulas, an extension of the assertional language used in BLog needed to express properties like parametric reachability. The resulting method is based on proof techniques that are complementary to compositional reasoning [15] and symbolic backward exploration [7].
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 fixed 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 field of automated verification, see e.g. [6]. Interactions in models with broadcast communication are usually defined by allowing a finite but arbitrary number of agents to react to a given message or signal. This type of communication is particularly useful to define protocols for replicated systems, e.g. cache coherence protocols, algorithms with global conditions, e.g., simultaneous resets of local variables, and communication in an open environment like an Ad Hoc or Wireless network. Algorithmic verification of models with broadcast communication started receiving more attention after the introduction of the Broadcast Protocols of Emerson and Namjoshi [3]. FAST [2,24], TRex [23], LASH [25], and MIST [17] are tools that can handle counter abstractions of network models given in formal of vector addition systems and their extensions. MAP [4] is a tool based on transformations of constraint logic programs that can be applied to infinite-state systems with linear configurations and relations over data variables. MCMT [18] is a symbolic backward reachability engine based on SMT solvers that can handle parameterized systems with linear configurations. The MCMT tool is based on the EPR fragment of first order logic with arrays and applies different types of heuristics including invariant generation to reduce the state space. PFS [21] and UNDIP [22] are tool specifically devised to handle parameterized systems. AUGUR 2 [11] is a tool devised for the analysis of Graph Transformation Systems using approximated unfoldings based on Petri nets. The approximated systems can then be verified using regular expressions, first order logic and coverability checking techniques. AUGUR 2 does not handle global operations like those needed for modeling broadcast communication. PETRU-CHIO [13] is a tool that extracts a Petri net representation from specifications of dynamic networks based on the π-calculus. Boom [20] is a tool that applies symbolic algorithms, see, e.g., [10,12,1,9], to verify counter abstractions of multithreaded programs. The algorithms behind the tool go beyond backward search. Indeed they combine several types of heuristics like those based on dynamic generation and refinement of over-approximations (defined in terms of upward closed set of states). PCW [19] is a tool that applies ordered counter abstraction [5], a refinement of monotonic abstraction with CEGAR, for the verification of parameterized systems. In this setting over-approximations are refined by using stronger and stronger orderings that can be used to define upward closed sets that "forbid" specific patterns (e.g. they forbid sets of points defined by a given equation). UNCOVER [16,26] is a tool that performs a symbolic backward reachability analysis for GTS with universally quantified conditions. The tool exploits a generalization of monotonic abstraction to quantifications over graph patterns as a heuristic to manipulate infinite sets of configurations using minimal constraints (given in form of graphs) only. UNCONVER can be viewed as the counterpart of UNDIP and PFS for systems in which configurations have a graph structure.
Differently from [16,26] and [14], our specification logic can be applied to define invariants involving an arbitrary but fixed number of nodes. For this purpose, we use assertions with parametric formulas. Global conditions can be defined using universally quantified formulas. The use of SMT solvers for graphbased specification is an interesting direction to explore.
In this section we will define 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 configurations defined by sets of ground atoms. Ground atoms define relations, i.e., labelled links, between agents and edges. More formally, let P be a finite set of names of binary relations, and V be a denumerable set of variables partitioned in two sets V a and V e , namely variables ranging over agents and edges, respectively. Furthermore, let N and E be denumerable sets of agent and edge identifiers. We consider here typed binary predicates in which the first 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. Definition 1. An atomic formula is a formula p(x, y), where p ∈ P , x ∈ V a , and y ∈ V e . A ground formula is a formula p(n, e), where n ∈ N , and e ∈ 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. Definition 2. The set of free variables of a formula F , namely
Quantified formulas will be used as application conditions of rules. Update rules consists of conditions defined by quantified formulas with no function symbols, a deletion and an addition set. The deletion (resp. addition) set defines the set of ground atoms that have to be cancelled from (resp. added to) the current configuration. We will consider free variables occurring in conditions to restrict the range of identifiers of a configuration. Definition 3. A rule has the following form C, D, A , where C is a quantified formula, D and A are two sets of predicates with variables in V , and such that
Configurations can be viewed as models in which to evaluate a formula. -
To define 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. Definition 6. An interpretation is an injective mapping σ from V a ∪V e to N ∪E s.t. σ(V a ) ⊆ N and σ(V e ) ⊆ E.
Definition 7. Given a configuration ∆, we say that the quantified formula A is satisfied in ∆, if there exists an interpretation σ s.t. ∆ |= Aσ is satisfiable.
Example 1. The condition ∀X. p(X, E) ⊃ q(X, E), when evaluated on a configuration ∆, is satisfiable if there exists an edge e such that for all instances p(n, e) ∈ ∆, there exists an atom q(n, e) ∈ ∆. Based on these considerations, the rule
defines a transition in which for a pair n, e such that link(n, e) occurs in the current configuration and such that there are not other agents n s.t. own(n , e) is in the current configuration, own(n, e) is added to the successor configuration.
In the operational semantics we assume that all atomic formulas that are not deleted are transferred to the successor configuration.
For a set S = {A 1 , . . . , A n }, we use Sσ to denote the set {A 1 σ, . . . , A n σ}.
A protocol P is a set of rules. The operational semantics of P is given by a transition system Starting from ∆ 0 = ∆ we obtain then a successor configuration
Now, let P be a protocol that contains the rule
Starting from ∆ 1 , we can reach ∆ 0 . Indeed, we have that ∆ 0 |= link(n 3 , e 3 ), and that
In a single step of the operational semantics a rule is evaluated in the current configuration by taking a sort of closed-word assumption, i.e., ground atoms that do not occur in a configuration are evaluated to false. Furthermore, atomic formulas that are not deleted are transferred from the current to the successor configuration. The latter property can be viewed then as a sort of frame axiom.
It is important to notice that, in general, a configuration ∆ has several possible successors. Indeed, depending of the chosen interpretation of free variables the same rule can be applied to different subsets of ground atoms contained in the same configuration. For a set S of configurations, we define the following sets:
We use P ost * (S) (resp. P re * (S)) to denote the reflexive-transitive closure of P ost (resp. P re).
In the rest of the section we will introduce formulas that define special conditions on agents and edges. The formula isoN (n) = ¬∃X.(∨ r∈P r(n, X)) specifies an isolated agent n, i.e., that is not involved in any relation in P . Similarly, the formula isoE(e) = ¬∃X.(∨ r∈P r(X, e)) specifies an edge that is not involved in any relation in P . Conditions like isoN (n) and isoE(e) are building blocks for the definition 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 define 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.
We consider decision problems that generalize the standard notion of reachability between configurations. The key point is to reason about an infinite set of initial configurations in order to prove properties for protocol instances with an arbitrary number of agents and edges. For this purpose, we introduce the ∃-reachability problem defined as follows.
Definition 9. Given a protocol P, a set of target configurations T and a possibly infinite set of initial configurations I, ∃-reachability is satisfied for P, I and T , written ∃Reach(P, I, T ), if there exists ∆ ∈ T and a configuration ∆ 1 s.t.
In other words ∃Reach(P, I, T ) holds if there exists a configuration ∆ 0 ∈ I s.t.
In the rest of the paper we will generalize the problem by considering patterns defined via existentially quantified formulas. Generalized ∃-reachability is defined as follows.
Definition 10. Given a protocol P and a formula Φ with free variables in S and a set of initial configurations I, generalized ∃-reachability is satisfied for P, I, and Φ, written ∃Reach(P, I, Φ), if there exists an interpretation σ, a configuration ∆ s.t. ∆ |= Φσ, and a configuration ∆ 1 s.t. ∆ 1 ∈ P ost * (I) and ∆ ⊆ ∆ 1 .
The ∃-Reachability problem turns out to be undecidable. A proof can be constructed by reducing the halting problem for Turing machines to ∃-reachability. The idea of the construction is as follows. Let M = Σ, Q, δ, q 0 , F 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 final states, q 0 is the initial state, and δ : Q × Σ → Q × Σ × {L, R} is the transition relation. Given an input word w ∈ Σ * without blanks, we first define a bipartite graph that encodes w. We use here three types of relations:
-The atomic formula q(n 1 , e 1 ) is used to represent the state of the head pointing to cell n 1 . -The atomic formula (n 1 , e 1 ) is used to represent a cell n 1 containing symbol .
-The atomic formula next(n 2 , e 1 ) is used to link, via edge e 1 , a cell to its successor cell identified by agent n 2 .
Creation of the word w = a 1 . . . a n and initialization of the tape head are defined by the rule (∧ n i=1 isoN (X i ) ∧ isoE(E i ), ∅, A), where
This rule selects n isolated agents and edges and defines a zig-zag graph in which we keep the information about letters and pointers to the adjacent cells.
To simulate a transition δ(q 1 , a) = q 2 , b, R we use the rules
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 defined, the latter rule can be applied to generate a representation of a blank cell. To simulate a transition δ(q 1 , a) = q 2 , b, L we use the rules r 3 = C 3 , D 3 , A 3 and r 4 = C 4 , D 4 , A 4 where
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 configurations I consists of an arbitrary number of isolated agents and edges, i.e., it contains a configuration ∆ n,m for each possible number n of agents and m of edges. Let us indicate with ∆ the configuration of the Turing machine represented by ∆. Namely, if ∆ = {a 1 (n 1 , e 1 ), next(n 2 , e 1 ), a 2 (n 2 , e 2 ), . . . , a k (n k , e k ), q i (n j , e j )} then ∆ = a 1 . . . a j−1 q i a j . . . a k . By construction, the application of a rule produced by the encoding preserve the well-formedness of the encoding of configurations. The following properties then holds.
Proposition 1. Let P M be the encoding of the Turing machine M and ∆ 0 ∈ I. If ∆ 0 → * ∆ 1 , then there exists a computation in M from ∆ 0 to ∆ 1 . Indeed, by construction, each step of a computation in P M mimics the application of transitions in M . ∆ 0 contains finitely 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 P M be the encoding of the Turing machine M and γ 0 = q 0 w an initial configuration of M on input w. If γ 1 is reachable from γ 0 , then there exists ∆ 0 ∈ I and ∆ 1 s.t. ∆ 0 = γ 0 , ∆ 1 = γ 1 , and
If γ 1 is reachable from γ 0 , then there is a finite upperbound k on the number of cells visited by the machine. Let ∆ 0 be an initial configuration with at least n (isolated) agents and edges. By applying a creation rule, we can generate a configuration ∆ 0 that represents the initial configuration γ 0 . By construction of P M , a step from γ i to γ i+1 can be simulated by the application of a rule in P M . 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 P M be the encoding of the Turing machine M . The Halting problem for M can be reduced to ∃-Reachability in P M by taking the formula Φ = q∈F q(X, Y ) as representation of subconfigurations denoting a final state.
In this section we consider possible application of BLog to the specification of distributed protocols. The key ingredient of the specification 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 reconfigure 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 buffer.
-An agent n 1 of type A connects to an edge e 1 in idle state (the buffer is free) and sets the state of the buffer to ready. -An agent n 2 of type B connects to e 1 in state ready and changes the state to readyack. -Agent n 1 sends message m by changing the state of e 1 to msg m .
-Agent n 2 receive message m and updates the state of the channel to readyack for further communications.
The protocol can be specified as follows. We use unary predicates to associate states to edges.
Rule
An initial state consists of a bipartite graph defined by the configuration of the following form idle(e 1 ), . . . , idle(e k ), where e i = e j for i = j, i, j : 1, . . . , k.
The model provides other form of interactions. For instance, we can model ordered buffers 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) defined as:
where s 1 (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 buffer E, and s 2 (Y, G) is a relation used to denote state of agent Y , etc.
We consider here a distributed version of the dining philosopher mutual exclusion problem presented in [14]. Agents are distributed on an arbitrary graph and communicate asynchronously via point-to-point channels. Channels are viewed as buffers with state. Distributed dining philosophers (ddp) is defined as follows. The goal is to ensure that agents can access a resource shared in common with their neighbors in mutual exclusion. The protocol from the perspective a single agent consists of the following steps:
-Initially, all agents are in idle state.
-When an agent A wants to get a resource, A has to acquire the control of each buffer shared with his/her neighbors. -To acquire a channel, A marks the channel with its identifier. If the channel is already marked, A has to wait. -A acquires the resources when all channels shared with neighbors are marked with his/her identifier. -To release a resource, A first resets each buffer. When all buffers are reset, A moves back to idle state.
In a statically defined 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 reconfigurations of the network.
In this section we present a formal specification of the DPP protocol. Network configurations are expressed as BLog configurations. The dynamics in a protocol interaction is expressed via a finite set of update rules. We use a predicate link to represent connections from a agent to a possibly shared buffer. To model dynamic reconfigurations, we can non-deterministically add and remove link predicates between pairs of agents and edges. To model buffers with states, we use special relations in which agents are initially isolated. Asynchronous communication is modelled as in the previous example, i.e., agents interact only via a common edge. Communication between two agents is not atomic. Instead of modelling identifiers and buffers with data, we introduce a special relation own that is used to model ownership of a given edge to which a agent is linked. Ownership is normed in the same way as the labelling of buffers in the original protocol, i.e., an agent can acquire ownership only if the edge is not owned by other agents.
In our framework we model this behavior using the following predicates and rules.
An initial state consists of a bipartite graph defined by a configuration of the following form idle(n 1 ), . . . , idle(n k ), where n i = n j for i = j, i, j : 1, . . . , k and k ≥ 1.
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 ∃-reachability problem. More specifically, let Φ be the formula busy(N ) ∧ busy(M ) ∧ link(N, G) ∧ link(M, G) that denotes a configurations in which two agents share the same channel. We have that ∃Reach(P M , I, Φ) holds if and only if mutual exclusion does not hold for DDP.
In this section we define a sort of canonical form for computations in P ddp obtained via permutation and deletion schemes that we can be uses to synthesize derived rules that are equivalent w.r.t. our correctness criteria.
We first consider deletion and permutation properties of rule applications within a given computation. We focus our attention on link and unlink rules, i.e., dynamic reconfigurations of the graph topology. Let θ = ∆ 0 ∆ 1 ∆ 2 be a computation in P ddp and let r 1 , r 2 be the transitions applied in each step.
-We first observe that if r 2 is an instance of the unlink rule applied to n 1 , e 1 , and r 1 is an instance of rule link applied to the same pair, they can be eliminated since ∆ 0 = ∆ 2 . -If r 1 is an instance of the getE rule applied to agent n 1 , e 1 , and r 2 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 different pairs to its left in a computation. Namely, if r 2 is an instance of the unlink rule applied to n 1 , e 1 , and r 1 is a rule that is not applied to n 1 , e 1 , then we can permute the application of the two rules and obtain a new computation leading to the same configuration. -If r 1 is an instance of the link rule applied to n 1 , e 1 , and r 2 is an application of any other rule on a different pair, then we can permute the applications of the two rules and obtain a new computation leading to the same configuration.
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 specifically, given a computation θ we can obtain an equivalent, w.r.t. our correctness criteria, computation θ by applying the following steps:
-We can eliminate all applications of reconfigurations, 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 first 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 first occurrence of getE to its left. -We can push the application of link rules close to the first 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 specific 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 different agents, in order to push all their occurrences close to the first 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 e 1 , . . . , e n , 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 specification language, since it may involve an arbitrary number of edges. To express this pattern, we can use a family {r k } k≥0 of rules, where
The rule associates agent X to an arbitrary subset of edges. The association is defined via the ownership predicate.
The pattern (relE unlink) * release is expressed by the infinite family {s k } k≥0 of rules. Rule s k = (C k , D k , A k ) is defined as:
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.
To verify correctness, we have to prove that the formula Ψ = ¬∃X, 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 k i=1 link(X, E i )∧own(X, E i )). This implies that there exists an agent n s.t. busy(n) ∈ ∆, and there exist e 1 , . . . , e n s.t. link(n, e i ), own(n, e i ) ∈ ∆ for i : 1, . . . , k. The application of the rule yields a configuration ∆ defined as ∆ = ∆ \ {link(n, e 1 ), . . . , link(n, e k ), own(n, e 1 ), . . . , own(n, e k )} ∪ {idle(n)} Although the rule might remove a strict subset of link and own predicates involving n, the resulting configuration still satisfies Ψ .
Since ∆, k, and σ are chosen in arbitrary way, we have that the considered invariant Φ is an invariant for the whole family of rules of type s k and r k with k ≥ 0.
Finally, we observe that for any ∆ we have that if ∆ |= Ψ then ∆ |= Ψ . This prove that Ψ is still an invariant for the model resulting from the transformation described in the previous sections.
We have presented a formal language for the specification of asynchronous distributed systems based on logic-based update rules for bipartite graphs. For the considered language, we have presented a verification approach that combines transformation schemes based on permutation properties and inductive verification. 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.