A Logic-based Approach to Verify Distributed Protocols Giorgio Delzanno DIBRIS, University of Genova, Italy Abstract. 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. 1 Introduction 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. Proto- col 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 net- work agent. An edge corresponds to a potential link between multiple agents. We use bipartite graphs in order to model both complex topologies and asyn- chronous 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 sym- bols. 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 up- dating 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 Philoso- pher Protocol proposed in [15]. The protocol is defined for asynchronous pro- cesses distributed over a graph with arbitrary topology. We model the protocol by considering dynamic reconfigurations of the topology. To verify the correct- ness 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 theo- retic analysis of computations. Permutation rules can be applied to derive meta rules obtained by composing sequences of rule applications of the original pro- tocol. 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 com- plementary to compositional reasoning [15] and symbolic backward exploration [7]. 1.1 Related Work We focus our attention on a class of formal models for concurrent and dis- tributed systems in which synchronization is achieved by using broadcast com- munication, a less standard communication primitive than rendez-vous or point- to-point communication. Rendez-vous communication involves a fixed a priori number of agents (e.g. a sender and a receiver in point-to-point communica- tion). 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 communi- cation 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 communi- cation 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 vari- ables. 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 pa- rameterized 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 multi- threaded 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 us- ing 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 back- ward 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 graph- based specification is an interesting direction to explore. 2 BLog 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 Va and Ve , 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 ∈ Va , and y ∈ Ve . 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 F V (F ), is the minimal set satisfying F V (p(x, y)) = {x, y}, 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 (∀v.A) = F V (A) \ {v}, and F V (∃v.A) = F V (A) \ {v}. Given S = {F1 , . . . , Fn }, we define F V (S) = F V (F1 ) ∪ . . . ∪ F V (Fn ). 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 hC, D, Ai, where C is a quantified 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). Configurations can be viewed as models in which to evaluate a formula. Definition 4. A configuration is a set ∆ of ground atomic formulas. Definition 5. We use ∆ |= A to define the satisfiability relation of a quantified formula A s.t. F V (A) = ∅. The relation is defined by induction as follows. – ∆ |= A, if A ∈ ∆; – ∆ |= A ∧ B, if ∆ |= A and ∆ |= B; – ∆ |= ¬A, if ∆ 6|= A; – ∆ |= ∀X.A (resp. ∀E.A), if ∆ |= A[n/X] (resp. A[e/X]) for each n ∈ N (resp. e ∈ E); – ∆ |= ∃X.A (resp. ∃E.A), if ∆ |= A[n/X] (resp. A[e/X]) for some n ∈ N (resp. e ∈ E). 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 Va ∪Ve to N ∪E s.t. σ(Va ) ⊆ N and σ(Ve ) ⊆ 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 con- figuration ∆, 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 hlink(X, Y ) ∧ ∀Z.link(Z, Y ) ⊃ ¬own(Z, Y ), ∅, {own(X, Y )}i 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 n0 s.t. own(n0 , 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 = {A1 , . . . , An }, we use Sσ to denote the set {A1 σ, . . . , An σ}. 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 configurations, i.e., finite subsets of ground atoms, and →⊆ C × C is a relation defined as follows. For ∆, ∆0 ∈ C and a rule hC, D, Ai ∈ P, ∆ → ∆0 if there exists σ s.t. ∆ |= Cσ and ∆0 = (∆ \ Dσ) ∪ Aσ. Definition 8. A computation is a sequence of configurations ∆0 ∆1 . . . s.t. ∆i → ∆i+1 for i ≥ 0. We use →∗ to denote the reflexive and transitive closure of →. Example 2. Let P be a protocol that contains the rule ∀X. link(X, E) ⊃ own(X, E). Consider ∆ = {link(n1 , e1 ), link(n2 , e1 ), link(n3 , e3 ), own(n3 , e3 )}, we first no- tice that ∆ does not satisfy the condition link(X, Y ) ∧ ∀Z.link(Z, Y ) ⊃ ¬own(Z, Y ) with the interpretation σ = [n3 /X, e3 /Y ]. Indeed, we have that – ∆ 6|= link(n3 , e3 ) ∧ ∀Z.link(Z, e3 ) ⊃ ¬own(Z, e3 ); – ∆ |= link(n3 , e3 ) and ∆ 6|= ∀Z.link(Z, e3 ) ⊃ ¬own(Z, e3 ); – ∆ 6|= ∀Z.link(Z, e3 ) ⊃ ¬own(Z, e3 ); – ∆ |= link(n1 , e3 ) ⊃ ¬own(n1 , e3 ), since own(n1 , e3 ) 6∈ ∆, link(n1 , e3 ) ∈ ∆; – ∆ |= link(n2 , e3 ) ⊃ ¬own(n2 , e3 ), since own(n2 , e3 ) 6∈ ∆, link(n2 , e3 ) ∈ ∆; – ∆ 6|= link(n3 , e3 ) ⊃ ¬own(n3 , e3 ), since own(n3 , e3 ), link(n3 , e3 ) ∈ ∆. However, ∆ satisfies the condition link(X, Y ) ∧ ∀Z.link(Z, Y ) ⊃ ¬own(Z, Y ) with the interpretation σ = [n1 /X, e1 /Y ]. Indeed, we have that – ∆ 6|= link(n1 , e1 ) ∧ ∀Z.link(Z, e1 ) ⊃ ¬own(Z, e1 ); – ∆ |= link(n1 , e1 ) and ∆ 6|= ∀Z.link(Z, e1 ) ⊃ ¬own(Z, e1 ); – ∆ 6|= ∀Z.link(Z, e1 ) ⊃ ¬own(Z, e1 ); – ∆ |= link(n1 , e1 ) ⊃ ¬own(n1 , e1 ), since own(n1 , e1 ) 6∈ ∆, link(n1 , e1 ) ∈ ∆; – ∆ |= link(n2 , e1 ) ⊃ ¬own(n2 , e1 ), since own(n2 , e1 ) 6∈ ∆, link(n2 , e1 ) ∈ ∆; – ∆ |= link(n3 , e3 ) ⊃ ¬own(n3 , e1 ), since own(n3 , e1 ) 6∈ ∆, link(n3 , e1 ) ∈ ∆. Starting from ∆0 = ∆ we obtain then a successor configuration ∆1 = ∆0 ∪ {own(n3 , e3 )} Now, let P be a protocol that contains the rule hlink(X, Y ), {own(X, Y )}, ∅i Starting from ∆1 , we can reach ∆0 . Indeed, we have that ∆0 |= link(n3 , e3 ), and that ∆1 = ∆0 \ {own(n3 , e3 )}. 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: P ost(S) = {∆0 | ∃∆ ∈ S, ∆ → ∆0 } P re(S) = {∆0 | ∃∆ ∈ S, ∆0 → ∆} We use P ost∗ (S) (resp. P re∗ (S)) to denote the reflexive-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 define special condi- tions 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 predi- cates 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 Decision Problem We consider decision problems that generalize the standard notion of reacha- bility 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. ∆1 ∈ P ost∗ (I) and ∆ ⊆ ∆1 . In other words ∃Reach(P, I, T ) holds if there exists a configuration ∆0 ∈ I s.t. ∆0 →∗ ∆1 and ∆ ⊆ ∆1 for some ∆ ∈ 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 configu- ration ∆ s.t. ∆ |= Φσ, and a configuration ∆1 s.t. ∆1 ∈ P ost∗ (I) and ∆ ⊆ ∆1 . 3.1 Undecidability The ∃-Reachability problem turns out to be undecidable. A proof can be con- structed by reducing the halting problem for Turing machines to ∃-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 final states, q0 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(n1 , e1 ) is used to represent the state of the head point- ing 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 identified by agent n2 . Creation of the word w = a1 . . . an and initialization of the tape head are defined by the rule (∧ni=1 isoN (Xi ) ∧ isoE(Ei ), ∅, A), where A = {q0 (X1 , E1 ), a1 (X1 , E1 ), next(X2 , E1 ), a2 (X2 , E2 ), . . . , an (Xn , En )} 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 δ(q1 , a) = hq2 , b, Ri we use the rules r1 = hC1 , D1 , A1 i and r2 = hC2 , D2 , A2 i, where W – C1 = q1 (X1 , E1 ) ∧ a(X1 , E1 ) ∧ next(X2 , E1 ) ∧ `∈Σ `(X2 , E2 ), – D1 = {q1 (X1 , E1 ), a(X1 , E1 )} and A1 = {q2 (X2 , E2 ), b(X2 , E2 )}. – C2 = q1 (X1 , E1 ) ∧ a(X1 , E1 ) ∧ isoN (X2 ) ∧ isoE(E2 ) ∧ ¬∃Z.next(Z, E1 ), – D2 = {q1 (X1 , E1 ), a(X1 , E1 )}, – A2 = {next(X2 , E1 ), q2 (X2 , E2 ), b(X2 , E2 )}. 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 de- fined, 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 , A3 i and r4 = hC4 , D4 , A4 i where W – C3 = q1 (X2 , E2 ) ∧ a(X2 , E2 ) ∧ next(X2 , E1 ) ∧ `∈Σ `(X1 , E1 ), – D3 = {q1 (X2 , E2 ), a(X2 , E2 )} and A3 = {q1 (X1 , E1 ), b(X2 , E2 )}. – C4 = q1 (X1 , E1 ) ∧ a(X1 , E1 ) ∧ isoN (X2 ) ∧ isoE(E2 ) ∧ ¬∃F.next(X1 , F ), – D4 = {q1 (X1 , E1 ), a(X1 , E1 )}, – A4 = {next(X1 , E2 ), q2 (X2 , E2 ), b(X1 , E1 ), B(X2 , E2 )}. 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 ∆ = {a1 (n1 , e1 ), next(n2 , e1 ), a2 (n2 , e2 ), . . . , ak (nk , ek ), qi (nj , ej )} then ∆ = a1 . . . aj−1 qi aj . . . ak . By construction, the application of a rule pro- duced by the encoding preserve the well-formedness of the encoding of configu- rations. The following properties then holds. Proposition 1. Let PM 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 PM mimics the applica- tion 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 PM be the encoding of the Turing machine M and γ0 = q0 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 ∆0 →∗ ∆1 . 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 ∆00 that represents the initial configuration γ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 W for M can be reduced to ∃-Reachability in PM by taking the formula problem Φ = q∈F q(X, Y ) as representation of subconfigurations denoting a final state. 4 Modelling In this section we consider possible application of BLog to the specification of distributed protocols. The key ingredient of the specification language is the com- bination 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 re- configure the graph, i.e., change labels, topology and add or delete agents. The separation between agents and edges is convenient to model asynchronous com- munication. For instance, let us consider a protocol in which two agents need to establish a connection via a shared buffer. – An agent n1 of type A connects to an edge e1 in idle state (the buffer is free) and sets the state of the buffer 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 specified as follows. We use unary predicates to associate states to edges. 1 Rule reqA = (C1 , D1 , A1 ) is s.t. C1 = idle(E) ∧ ¬send(X, E), D1 = {idle(E)}, A1 = {ready(E), req(X, E)} 1 Rule reqB = (C2 , D2 , A2 ) is s.t. C2 = ready(E) ∧ ¬rec(X, E), D2 = {ready(E)}, A2 = {readyack(E), rec(X, E)}. 2 Rule reqA = (C3 , D3 , A3 ) is s.t. C3 = readyack(E) ∧ send(X, E), D3 = {readyack(E), send(X, E)}, A3 = {msgm (E)} 3 Rule reqA = (C4 , D4 , A4 ) is s.t. C4 = msgm (E) ∧ rec(X, E), D4 = {msgm (E), rec(X, E)}, A4 = {idle(E)} An initial state consists of a bipartite graph defined by the configuration of the following form idle(e1 ), . . . , idle(ek ), where ei 6= ej for i 6= 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: – C = link(X, E) ∧ s1 (X, F ) ∧ link(Y, E) ∧ s2 (Y, G) – D = {s1 (X, F ), link(X, E), link(Y, E), s2 (Y, G)} – A = {link(X, E), s01 (X, F ), link(Y, E), s02 (Y, 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 buffer E, and s2 (Y, G) is a relation used to denote state of agent Y , etc. 5 Distributed Dining Philosophers 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 neigh- bors 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. 5.1 Formal Specification of DDP 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. Rule link = (C1 , D1 , A1 ) is defined s.t. C1 = ¬link(X, E), D1 = ∅, A1 = {link(X, E)}. Rule unlink = (C2 , D2 , A2 ) is defined s.t. C2 = link(X, E), D2 = {link(X, E)}, A2 = ∅. Rule getE = (C3 , D3 , A3 ) is s.t. C3 = link(X, E) ∧ ∀Z.¬own(Z, E), D3 = ∅, A3 = {own(X, E)}. Rule relE = (C4 , D4 , A4 ) is s.t.: C4 = D4 = {own(X, E)}, A4 = ∅. Rule acquire = (C5 , D5 , A5 ) is s.t. C5 = idle(X)∧∀E.(link(X, E) ⊃ own(X, E)), D5 = {idle(X)}, A5 = {busy(X)}. Rule release = (C6 , D6 , A6 ) is defined s.t. C6 = D6 = {busy(X)}, A6 = {idle(X)}. An initial state consists of a bipartite graph defined by a configuration of the following form idle(n1 ), . . . , idle(nk ), where ni 6= nj for i 6= 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(PM , I, Φ) holds if and only if mutual exclusion does not hold for DDP. 6 Verification via Transformation Rules In this section we define 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 first consider deletion and permutation properties of rule applications within a given computation. We focus our attention on link and unlink rules, i.e., dy- namic reconfigurations 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 first 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 different 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 configuration. – If r1 is an instance of the link rule applied to n1 , e1 , and r2 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 equiv- alent 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 θ0 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 compu- tation 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 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. 6.2 Derived Rules 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 ex- press this pattern, we can use a family {rk }k≥0 of rules, where rk = (Ck , Dk , Ak ) is defined as: Vk Vk – Ck = idle(X) ∧ i=1 ¬link(X, Ei ) ∧ ∀Z. i=1 ¬own(Z, Ei ), – Dk = {idle(X)}, – Ak = {busy(X), link(X, E1 ), own(X, E1 ), . . . , link(X, Ek ), own(X, Ek )}. 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 {sk }k≥0 of rules. Rule sk = (Ck , Dk , Ak ) is defined as: Vk – Ck = busy(X) ∧ i=1 link(X, Ei ) ∧ own(X, Ei ), – Dk = {busy(X), link(X, E1 ), own(X, E1 ), . . . , link(X, Ek ), own(X, Ek )}, – Ak = {idle(X)}. 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 Ψ = ¬∃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 Ψ0 = Υ ∧ Ψ where Υ = (∀Z, E.link(Z, E) ⊃ own(Z, E)), is still an invariant of the resulting rule. By definition Ψ 0 holds in any initial configuration ∆m,n , since initial con- figurations 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 configuration ∆ with cardinality n and assume that ∆ |= Ψ 0 . Now consider rk s.t. k ≤ n. If rk can be appliedVk to ∆, there exists V an interpretation σ k s.t. ∆ |= Ck σ where Ck = (idle(X)∧ i=1 ¬link(X, Ei )∧∀Z. i=1 ¬own(Z, Ei )). This implies that there exists an agent n s.t. idle(n) ∈ ∆, and there exist e1 , . . . , en s.t. link(m, ei ), own(m, ei ) 6∈ ∆ for i : 1, . . . , k and for any m oc- curring in ∆. The application of the rule yields a configuration ∆0 defined as ∆0 = ∆ ∪ {link(n, e1 ), . . . , link(n, ek ), own(n, e1 ), . . . , own(n, ek ), busy(n)} Since by assumption own(m, ei ), link(m, ei ) 6∈ ∆ for any m occurring in ∆ and i : 1, . . . , k, we have that ∆0 |= Ψ 0 . Now consider a configuration ∆ with cardinality n and assume that ∆ |= Ψ 0 . Now consider sk s.t. k ≤ n. If sk can be applied Vk to ∆, there exists an interpreta- tion σ s.t. ∆ |= Ck σ where Ck = (busy(X)∧ i=1 link(X, Ei )∧own(X, Ei )). This implies that there exists an agent n s.t. busy(n) ∈ ∆, and there exist e1 , . . . , en s.t. link(n, ei ), own(n, ei ) ∈ ∆ for i : 1, . . . , k. The application of the rule yields a configuration ∆0 defined as ∆0 = ∆ \ {link(n, e1 ), . . . , link(n, ek ), own(n, e1 ), . . . , own(n, ek )} ∪ {idle(n)} Although the rule might remove a strict subset of link and own predicates involving n, the resulting configuration still satisfies Ψ 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 ∆ |= Ψ 0 then ∆ |= Ψ . This prove that Ψ is still an invariant for the model resulting from the transformation described in the previous sections. 7 Conclusions and Related Work We have presented a formal language for the specification of asynchronous dis- tributed systems based on logic-based update rules for bipartite graphs. For the considered language, we have presented a verification approach that com- bines 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 net- work topology and the number of nodes. Mechanization of the considered proof method could be an interesting direction for future work. References 1. P. Liu andT. Wahl. Infinite-state backward exploration of boolean broadcast pro- grams. In Formal Methods in Computer Aided Design, FMCAD ’14, pages 155–162, 2014. 2. Sébastien Bardin, Alain Finkel, Jérôme Leroux, and Laure Petrucci. FAST: accel- eration from theory to practice. STTT, 10(5):401–424, 2008. 3. E. A. Emerson and K. S. Namjoshi. On model checking for non-deterministic infinite-state systems. In Thirteenth Annual IEEE Symposium on Logic in Com- puter Science, Indianapolis, Indiana, USA, June 21-24, 1998, pages 70–80, 1998. 4. F. Fioravanti, A. Pettorossi, M. Proietti, and V. Senni. Improving reachability analysis of infinite state systems by specialization. Fundam. Inform., 119(3-4):281– 300, 2012. 5. P. Ganty and A. Rezine. Ordered counter-abstraction - refinable subword relations for parameterized verification. In Language and Automata Theory and Applications - 8th International Conference, LATA 2014, Madrid, Spain, March 10-14, 2014. Proceedings, pages 396–408, 2014. 6. S. M. German and A. P. Sistla. Reasoning about systems with many processes. J. ACM, 39(3):675–735, 1992. 7. S. Ghilardi and S. Ranise. Backward reachability of array-based systems by SMT solving: Termination and invariant synthesis. Logical Methods in Computer Sci- ence, 6(4), 2010. 8. B. Bagheri Hariri, D. Calvanese, G. De Giacomo, A. Deutsch, and M. Montali. Verification of relational data-centric dynamic systems with external services. In Proceedings of the 32nd ACM SIGMOD-SIGACT-SIGART Symposium on Princi- ples of Database Systems, PODS 2013, New York, NY, USA - June 22 - 27, 2013, pages 163–174, 2013. 9. A. Kaiser, D. Kroening, and T. Wahl. Lost in abstraction: Monotonicity in multi- threaded programs. In CONCUR 2014 - Concurrency Theory - 25th International Conference, CONCUR 2014, Rome, Italy, September 2-5, 2014. Proceedings, pages 141–155, 2014. 10. A. Kaiser, D. Kroening, and Thomas Wahl. A widening approach to multithreaded program verification. ACM Trans. Program. Lang. Syst., 36(4):14, 2014. 11. B. König and V. Kozioura. Augur 2 - A new version of a tool for the analysis of graph transformation systems. Electr. Notes Theor. Comput. Sci., 211:201–210, 2008. 12. D. Kroening. Automated verification of concurrent software. In Reachability Prob- lems - 7th International Workshop, RP 2013, Uppsala, Sweden, September 24-26, 2013 Proceedings, pages 19–20, 2013. 13. R. Meyer and T. Strazny. Petruchio: From dynamic networks to nets. In Computer Aided Verification, 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010. Proceedings, pages 175–179, 2010. 14. K. S. Namjoshi and R. J. Trefler. Uncovering symmetries in irregular process networks. In VMCAI, pages 496–514, 2013. 15. Kedar S. Namjoshi and Richard J. Trefler. Analysis of dynamic process networks. In Tools and Algorithms for the Construction and Analysis of Systems - 21st Inter- national Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings, pages 164–178, 2015. 16. J. Stückrath. Uncover: Using coverability analysis for verifying graph transfor- mation 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/.