A Symmetry Reduction Technique for Model Checking Temporal-Epistemic Logic

1 Introduction

Model checking [Clarke and Emerson, 1982] is a wellestablished automated technique for verifying reactive systems against design requirements expressed in temporal logics. More recently model checking has been extended to multi-agent systems (MAS) and design requirements specified in temporal-epistemic logic (cf. [Bordini et al., 2003; Gammie and van der Meyden, 2004; Nabialek et al., 2004; Lomuscio et al., 2009; Wooldridge et al., 2002]).

However, a major obstacle to model checking is the so called state explosion problem: model checking becomes intractable for systems with many agents as the state space that needs to be constructed grows exponentially in the number variables used by agents in the system.

Even worse, for many popular applications of epistemic logic the state space explosion is exasperated by an explosion of initial states; each model includes one initial state for every possible initial configuration of local states. For example, in voting protocols, card games, the muddy children scenario, and the dining cryptographers protocol, we need to consider a different initial state for every distribution of votes/cards/mud/coin tosses and choice of payer. The explosion of initial states leads to an explosion of reachable states.

However, in these applications several agents can be seen as simple variations of a common generic agent. As a result, execution traces starting from different initial states might be the same up to a rearrangement of local states; in other words, the traces are "symmetric". Even so, removing some initial states makes properties of the initial configuration commonly known: if proposition φ holds in all initial states that remain, it is common knowledge among agents that initially φ holds. So, by removing initial states, we obtain unwanted epistemic validities. Amore sophisticated treatment seems required.

In this paper we present a technique for exploiting symmetry when model checking temporal-epistemic properties of multi-agent systems defined in the mainstream interpreted systems framework [Fagin et al., 1995]. The key idea is to abstract the standard Kripke semantics into a counterpart semantics [Lewis, 1968] by permuting agent names along the indistinguishability relation. This allows the initial states to be reduced by keeping a single representative for a group of initial states that are equivalent up to the order of local states. The abstraction is accurate in that the same temporalepistemic specifications hold for both the original and the reduced models; there are neither false positives nor false negatives in the reduced model. Experimental results show that the reduction in model checking time can be dramatic.

Related work Abstraction is a family of techniques for simplifying large models by removing details inessential to the property to be verified [Clarke et al., 1994]. While abstraction of reactive systems for temporal properties is an active research area, abstraction for epistemic properties has so far received little attention. Recently [Dechesne et al., 2008; Enea and Dima, 2007] abstracts Kripke models for epistemic logic by approximating the epistemic possibility relation. However, these models are not computationally grounded [Wooldridge, 2000], hampering concrete applications. In [Cohen et al., 2009] interpreted systems are abstracted by collapsing local states and actions of each agent.

Closer to our contribution, component symmetry reduction is an abstraction technique for temporal logic aiming to reduce the state space by collapsing system states that are equivalent up to a reordering of local states into one representative state [Clarke et al., 1996; Emerson and Sistla, 1996]. Most closely related to our work are the automata-based symmetry reduction techniques that annotate the reduced transition relation with process permutations [Emerson and Sistla, 1995]. The annotation allows processes to be tracked along the transitions, thereby accommodating atomic propositions that specify properties of individual processes (and so break symmetry).

Counterpart semantics has been used before in a computationally grounded setting for epistemic logic [Cohen and Dam, 2007], but without any relation to state space reduction. We could find no attempt in the literature at extending symmetry reduction to epistemic logic.

Overview of paper The rest of the paper is organized as follows. In Section 2 we recall definitions for interpreted systems and the temporal-epistemic specification logic CTLK. In Section 3 we instantiate (component) symmetry to interpreted systems and define formula symmetry for CTLK. In Section 4 we present the counterpart semantics used on the reduced system, and prove that CTLK validity is invariant between the original and reduced systems. In Section 5 we show how to detect symmetries. In Section 6 we report on experimental results. Finally, Section 7 concludes.

2 Interpreted systems and CTLK

We model multi-agent systems in the interpreted systems framework [Fagin et al., 1995] and express requirements in the temporal-epistemic logic CTLK [van der Meyden and Wong, 2003]; this section summarizes the basic definitions.

Consider a set Ag = {1...n} of agents. For each agent i, assume a non-empty set Li of local states that agent i can be in, and a non-empty set ACTi of actions that agent i can perform. Assume also a non-empty set LE of states for the environment and a non-empty set ACTE of actions. Let S = L1 × · · · × Ln × LE be the set of all possible global states and ACT = ACT1 × · · · × ACTn × ACTE the set of all possible joint actions. For each agent i assume a local protocol Pi : Li -→ 2ACTi selecting actions depending on the current local state of i, and a local evolution function ti : ACT × Li -→ Li specifying how agent i evolves from one local state to another depending on its action, the actions of the other agents, and the action of the environment. Analogously, assume an environment protocol PE : LE -→ 2ACTE , and an environment evolution function tE : ACT ×LE -→LE. Let P = 〈P1, · · · , Pn, PE〉 be the joint protocol and t = 〈t1, · · · , tn, tE〉 be the joint evolution function. Finally, consider a non-empty set I0 ⊆ S of initial states, and an evaluation function V : S -→ 2A for some non-empty set A of propositional atoms.

Definition 2.1. An interpreted system is a tuple I = 〈S, ACT, P, t, I0, V 〉 with a global state space S, a joint actions space ACT, a joint protocol P, a joint evolution function t, a set I0 of initial states and an evaluation function V .

For any global state g = 〈l1, . . . , ln, lE〉 ∈ S, we write li(g) for the the local state li of agent i in g, and lE(g) for the environment state lE in g.

The local protocols and the local evolution functions together determine how the system of agents proceeds from one global state to the next. The global transition relation R ⊆ S × S is such that 〈g, g′ 〉 ∈ R if and only if there exists a = 〈a1, . . . , an, aE〉 ∈ ACT such that tE(a, lE(g)) = lE(g′ ) and aE ∈ PE(lE(g)), and for all agent i, ti(a, li(g)) = li(g′ ) and ai ∈ Pi(li(g)). We assume throughout the paper that the global transition relation R is serial, i.e., for every g ∈ S, there is g′ ∈ S such that gRg′ .

A path in I is an infinite sequence g0 , g1 , . . . of global states in S such that every pair of adjacent states forms a transition, i.e., gj Rgj+1 for all j. The set G of reachable states in I contains all global states g ∈ S for which there is a path g0 , g1 , . . . , g, . . . starting from an initial state g0 ∈ I0.

Intuitively, the local state li(g) contains all the information available to agent i. We say that g′ ∈ G is epistemically possible for agent i at g ∈ G, written g ∼i g′ , if the local state of i in g is the local state of i in g′ , i.e., li(g) = li(g′ ). We refer to [Fagin et al., 1995] for more details.

We consider specifications expressed in the temporalepistemic logic CTLK which extends Computation Tree Logic (CTL) with epistemic modalities.

Definition 2.2. Assume a set Ag = {1..n} of agents i and a non-empty set A of propositional atoms p. CTLK formulae are defined by the following BNF expresion:

The knowledge modality Ki is read "Agent i knows that", the quantifier E is read "For some computation path" and the temporal operators X, G and U are read "In the next state", "Always" and "Until" respectively. We assume customary abbreviations: Ki encodes the diamond modality ¬Ki¬; AGφ represents ¬E(true U ¬φ) ("For all paths, always φ"); AF φ abbreviates ¬EG¬φ ("For all paths, eventually φ").

Given an interpreted system I, the modality Ki is interpreted by the epistemic possibility relation ∼i as follows:

· (I, g) |=Kiφ iff (I, g′ ) |= φ for all g′ such that g ∼i g′ . The CTL modalities are interpreted by means of the global transition relation R in the usual way: (I, g) |= EXφ iff for some path g0 , g1 , . . . in I such that g = g0 , we have (I, g1 ) |= φ; (I, g) |= EGφ iff for some path g0 , g1 , . . . in I such that g = g0 , we have (I, gi ) |= φ for all i ≥ 0; (I, g) |= E(φUφ′ ) iff for some path g0 , g1 , . . . in I such that g = g0 , there is a natural number i such that (I, gi ) |= φ′ and (I, gj ) |= φ for all 0 ≤ j < i. We write [[φ]] for the extension of formula φ in I, i.e., the set of reachable states g ∈ G such that (I, g) |= φ. We say that formula φ is true in system I, written I |= φ, iff I0 ⊆ [[φ]].

Example 2.3 (Muddy children). [Fagin et al., 1995] A group of n children have been out playing in the mud, and k of them now have mud on their forehead. They sit in a circle and see only the foreheads of other children. Their father announces "At least one of you is muddy!", and then asks: "Does any one of you know whether you are muddy?". The father repeats the question over and over. After each question, the children answer simultaneously; all children say "I do not know" until round k when the muddy children say that they know they are muddy.

The scenario can be modeled as an interpreted system I (see [Fagin et al., 1995] for details). We would like to verify by means of a model checker that the children are truthful:

where the propositional atom saysknows(i) holds if child i says it knows whether it is muddy.

Example 2.4 (Dining cryptographers). [Chaum, 1988] A group of n cryptographers share a meal around a circular table. Either one of them paid for the meal or their employer did. They would like to make it known if one of them paid without revealing the identity of the payer (if one of them did pay). To this end, every cryptographer tosses a coin and shows the outcome to his right-hand neighbour. Comparing his own coin to the coin shown to him, each cryptographer announces if the two coins agree or not; if a cryptographer paid for the meal, he announces the opposite of what he sees.

The scenario can be modeled as an interpreted system (see [van der Meyden and Su, 2004] for details). We would like to verify that no agent i can ever come to know that a particular other agent j is the payer:

and each agent comes to know whether the employer paid:

3 Symmetry

In this section we instantiate agent (component) symmetry [Clarke et al., 1996; Emerson and Sistla, 1996] to interpreted systems, and generalise formula symmetry [Emerson and Sistla, 1995] from CTL to CTLK.

Informally, an agent symmetry is an interchange of local states preserving the behaviors of the system. Formally, a symmetry, or automorphism, of a set X ⊆ S of global states, or of a relation X ⊆ S × S between global states, is a bijection π : S -→ S that leaves X unchanged: π(X) = X, where π(X) = {π(g) : g ∈ X} if X is a set, and π(X) = {〈π(g), π(g′ )〉 : 〈g, g′ 〉 ∈ X} if X is a relation. An automorphism of the system I is an automorphism of both the global transition relation R and the set I0 of initial states.

In this paper we consider only agent symmetries, i.e., automorphisms induced by a reordering of local states in global states. We identify a reordering of local states with an agent permutation, i.e., a bijection π : Ag -→ Ag. An agent permutation π extends naturally to global states by moving each local state li(g) of agent i to that of agent π(i): π(g) = 〈lπ-1 (1)(g), . . . , lπ-1 (n)(g), lE(g)〉. For example, π(〈A,A,B,B, lE(g)〉) = 〈B,A,A,B, lE(g)〉 if π is the right-shift permutation defined by π(i) = i+1 modulo 4. The set Aut(X) of agent permutations that are automorphisms of X ∈ {R, I0, I} is a group with respect to function composition, function inverse, and identity. We write Sym(Ag) for the group of all agent permutations.

In some applications we might want the agent permutations to act on variables inside the local states being reshuffled: π(g) = 〈π(lπ-1 (1)(g)), . . . , π(lπ-1 (n)(g)), π(lE(g))〉, where π(l) is the result of substituting π(i) for i in local state l. For example, if variable X in local state l stores an agent identity i, l(X) = i, then π(l)(X) = π(l(X)) = π(i). The state reduction technique presented in this paper generalises to symmetries obtained under this finer definition of π(g), but we only discuss the former definition for ease of presentation given that the formal results are equivalent.

We assume that propositional atoms have the form p(i), where p is an agent predicate, and i ∈ Ag⋆ respects the arity of p. Intuitively, p(i) states that property p holds of agents i. To reflect this we require that any evaluation function V is such that:

for any agent permutation π and any states g, π(g) ∈ S. For example, the interpretation of the unary agent predicate mud must satisfy: g |=mud(i) if and only if π(g) |=mud(π(i)).

We apply the agent permutation π on formula φ by substituting π(i) for agent name i inside the formula.

Definition 3.1. π(φ) is defined inductively over φ as follows: π(p(i)) = p(π(i)), π(φ ∧ φ′ ) = π(φ) ∧ π(φ′ ), π(¬φ) = ¬π(φ), π(Ki φ) = Kπ(i)π(φ), π(EX φ) = EX π(φ), etc.

Applying an agent permutation to a CTL formula modifies only atomic sub-formulae. Here, by contrast, an agent permutation modifies epistemic modalities as well. For example, if π transposes 1 with 2, i.e., π(1) = 2 and π(2) = 1, then, π(K1 mud(2)) = K2 mud(1).

An automorphism of a formula φ is an agent permutation π such that φ is semantically equivalent to π(φ), i.e., [[φ]] = [[π(φ)]] in all systems I. For example, an agent permutation that transposes 1 with 2 is an automorphism of K1 mud(2) ∧ K2 mud(1). Every agent permutation is an automorphism of specifications (1), (2), and (3) (cf. lemma 5.3). As before, the set Aut(φ) of automorphisms of φ is a group.

4 Agent symmetry reduction

As highlighted in the introduction, multi-agent systems in key applications of epistemic logic exhibit considerable agent symmetry. In this section we present a technique that exploits agent symmetries to reduce the initial states.

Assume a group Γ ⊆ Aut(I) of symmetries of the system I. Let I/Γ = 〈S, ACT, P, t, I ′0 , V 〉 be the result of replacing the set I0 of initial states with a minimal I ′0 ⊆ I0 such that I0 = Γ(I ′0 ) = {π(g) | π ∈ Γ, g ∈ I ′0 }, i.e., the result of leaving a single representative initial state g for each equivalence class {π(g) | π ∈ Γ} of initial states.

Example 4.1. For the system I of muddy children from Example 2.3, we can choose Γ such that I/Sym(Ag) contains a single initial state where 1 child is muddy, a single initial state where 2 children are muddy, etc. While I has 2n initial states, I/Sym(Ag) has only n + 1 initial states.

We show that the original system I and the reduced system I/Γ can be seen to validate the same CTLK formulae. To achieve this invariance, we use a counterpart semantics for the epistemic modalities in the reduced system I/Γ.

4.1 Abstract semantics

In counterpart semantics [Lewis, 1968] the modal accessibility relation is indexed by a counterpart relation C which identifies individuals across states. If a state g′ is accessible from a state g under a counterpart relation C, then each individual i at state g has a counterpart ( "equivalent") individual C(i) at the accessible state g′ ; in a sense, the individual i at g "is" the individual C(i) at g′ . Accordingly, a proposition φ(i) about the individual i is possible at state g, g |= ✸φ(i), if the proposition φ(C(i)) about the counterpart individual C(i) holds at the accessible state g′ , g′ |= φ(C(i)).

In the abstract semantics we define below, individuals i are agents and counterpart relations C are agent permutations.

Definition 4.2. Assume an interpreted system I and a group Γ of agent permutations. A state g′ ∈ G is (epistemically) accessible to agent i from state g ∈ G under agent permutation π ∈ Γ, written g ≈πi g′ , if and only if, g ∼i π-1 (g′ ).

Intuitively, if g ≈πi g′ then agent j at state g could, for all agent i knows, be agent π(j) at g′ . Therefore, agent i holds fact φ(j) as possible at state g if the counterpart fact φ(π(j)) holds at the accessible state g′ .

Definition 4.3 (Abstract semantics). Truth of φ at g in interpreted system I under Γ, written (I, g) |=Γ φ, is defined inductively by:

• (I, g) |=Γ Kiφ iff (I, g′ ) |=Γ π(φ) for all g′ ∈ G and π ∈ Γ such that g ≈πi g′

All other cases are unchanged from Section 2.

Note that the abstract semantics involves the counterpart formula π(φ) at the accessible state g′ , rather than the formula φ itself; the formula π(φ) may have different propositional atoms as well as different epistemic modalities from φ. Note also that when Γ contains only the identity permutation, the abstract semantics coincides with the basic Kripke semantics of Section 2: (I, g) |= φ, if and only if, (I, g) |={id} φ.

Example 4.4. Consider the system I of muddy children from Example 2.3. Let I ′ be the result of removing the initial state g1 where only child 1 is muddy. Observe that under the standard semantics at the initial state g0 where no child is muddy, child 1 knows she is not muddy: (I ′ , g0 ) |= K1¬mud(1). In fact, since we removed initial state g1 , the only state reachable in I ′ which is epistemically possible for child 1 at g0 is g0 itself. By contrast, under the abstract semantics, child 1 does not know she is not muddy: (I ′ , g0 ) ̸|=Sym(Ag) K1 ¬mud(1). This is seen as follows. By assumption, I ′ contains some initial state g2 where exactly one child, say child 2, is muddy: g2 |= mud(2). Choose an agent permutation π that transposes 1 and 2. Then, π-1 (g2 ) = g1 , i.e., g0 ∼1 π-1 (g2 ), i.e., g0 ≈π1 g2 . The claim follows by definition 4.3, since g2 |= π(mud(1)).

4.2 Reduction theorem

We reach the reduction result by way of two lemmas. Firstly, applying a system automorphism π on the epistemic relation for agent i yields the epistemic relation for agent π(i).

Secondly, applying a system automorphism π to the extension of a formula φ produces the extension of π(φ).

Proof. (Sketch) We show that (I, g) |= φ, if and only if, (I, π(g)) |= π(φ), by induction on φ. Base step: From requirement (4). Induction step, temporal modalities: Since π ∈ Aut(I), gRg′ , if and only if, π(g)Rπ(g′ ). Induction step, epistemic modalities: From Lemma 4.5.

Theorem 4.7 (Reduction). Let Γ be a subgroup of both Aut(I) and Aut(φ). Then, I |= φ if and only if I/Γ |=Γ φ.

Proof. (Sketch) Since Γ ⊆ Aut(I) it follows that G = {π(g) | π ∈ Γ, g ∈ G′ } where G and G′ are the sets of reachable states in I and I/Γ respectively. Therefore, we can evaluate the epistemic modality in I by scanning the reduced space G′ and apply agent permutations "on the fly", expanding each state g′ into its equivalence class {π-1 (g′ ) | π ∈ Γ}. So, (I, g) |= Kiφ, if and only if, ∀g′ ∈ G′ : ∀π ∈ Γ : g ∼i π-1 (g′ ) ⇒ (I, π-1 (g′ )) |= φ. In fact, by Lemma 4.6, we can replace the test of the property φ at π-1 (g′ ) with the test of the counterpart property π(φ) at g′ , and so obtain: (I, g) |= Kiφ, if and only if, ∀g′ ∈ G′ : ∀π ∈ Γ : g ∼i π-1 (g′ ) ⇒ (I, g′ ) |= π(φ). But g ∼i π-1 (g′ ) means g ≈πi g′ . By induction over φ, therefore, we obtain: (I, g) |= φ, if and only if, (I/Γ, g) |=Γ φ, for all g ∈ G′ . The theorem follows since Γ ⊆ Aut(φ).

Following Theorem 4.7 we can reduce the initial states before feeding a system to a model checker.

Example 4.8. Applying Theorem 4.7 to the system I of muddy children from Example 2.3, I |= (1) if and only if I/Sym(Ag) |=Sym(Ag) (1).

5 Symmetry detection

To Theorem 4.7, we need to find a group Γ of symmetries of the system I and of the specification φ. In this section we show how to compute a group Γ directly from the description of I and the shape of φ.

Intuitively, system symmetries arise from similarities in the agents. To exploit this intuition, we extend the notion of symmetry to joint protocols and joint evolution functions.

Definition 5.1. An automorphism of the joint protocol P is an agent permutation π such that Pi = Pπ(i). An automorphism of the joint evolution function t is an agent permutation π such that ti(l, a) = tπ(i)(l, π(a)) and tE(l, a) = tE(l, π(a)), where π(a) = 〈aπ-1 (1), . . . , aπ-1 (n), aE〉.

It can be checked that the sets Aut(P) and Aut(t) of automorphisms of the joint protocol P and the joint evolution function t are groups.

We can now make precise the intuition that symmetries arise from similarities in the agents. Any symmetry of the joint protocol and the joint evolution function is a symmetry of the global transition relation R.

Proof. Let 〈g, g′ 〉 ∈ R and π ∈ Aut(P) ∩ Aut(t). So there is a such that ti(a, li(g)) = li(g′ ) with ai ∈ Pi(li(g)), and so tπ(i)(π(a), li(g)) = li(g′ ) with ai ∈ Pπ(i)(li(g)).

Using Lemma 5.2, we can detect automorphisms of the global transition relation R without constructing R explicitly.

With respect to the detection of formula symmetries we observe that the specifications we are interested in are often universal formulae of the form ∧j φ(j/i), where i is the tu-

ple of agent names appearing in φ, and j ranges over tuples of distinct agent names. In other words, universal formulae either have the form ∧i φ(i), or the form ∧ i̸=jφ(i, j), etc. For

example, (1), (2), and (3) are universal. According the following lemma, universal formulae are fully symmetric.

So, the group Γ = Aut(P )∩Aut(t)∩Aut(I0) can be used to form the reduced system I/Γ in Theorem 4.7 when verifying a universal specification φ. Similar results can be obtained for other types of specifications, e.g. existential specifications of the form ∨i φ(i), or semi-universal specifications

6 Experimental results

To show the effectiveness of the proposed reduction technique, we implemented the abstract semantics from Section 4.1 on MCMAS [Lomuscio et al., 2009], an open-source, symbolic model checker for the verification of temporal-epistemic properties of interpreted systems described in ISPL. We modified the interpretation of the epistemic modality in MCMAS as follows:

where G is the set of states reachable in the supplied system (i.e., the reduced system I/Γ). Note that the loop-body computes the extension of π(φ) rather than φ. Of course, when π, π′ ∈ Γ agree on the agent names in the formula Kiφ, the loop need not consider both of them. Since the algorithm may revisit the same sub-formula several times, we store constructed extensions in a BDD cache.

We tested our reduction technique on the dining cryptographers (Example 2.4) and the muddy children (Example 2.3) on a machine running Linux Fedora 10 x86 64 version with Intel Core 2 Duo E4500 2.2GHz and 4GB memory. In the ISPL program for the dining cryptographers, every rotation

(sideways shift π(i) = i + k modulo n, for some k) is an automorphism of the joint protocol, joint evolution function and the initial states. By Proposition 5.4 and Theorem 4.7, we can thus form the ISPL program for a reduced system by requiring (in the program section defining the initial states) that either agent 1 pays or no agent pays, thereby obtaining a portion 2/(n + 1) of initial states of the original ISPL program. Verification times (in seconds) for the universal anonymity specification (2) and different number of cryptographers are presented in Table 1, showing a linear reduction. The running time for 11 cryptographers is less than for 10 because the BDDs generated in the former are more compact. This is a known feature of symbolic techniques for this example [Kacprzak et al., 2006].

In the ISPL program for the muddy children all agent permutations (not only rotations as in the dining cryptographers) are automorphisms of the joint protocol, joint evolution function and the initial states. By Proposition 5.4 and Theorem 4.7, we can simplify the program section defining the initial states by keeping only one initial state from each group of initial states with the same number of muddy children. Table 2 shows the verification times (in seconds) and the BDD memory usage (in MB) for the universal specification (1); we obtain an exponential reduction in verification time. However, the memory consumption is not significantly reduced, as the reduction generates extra BDDs.

7 Conclusion

While model checking epistemic logic has received considerable attention in the AI community, there has been little work so far on techniques for tackling the state explosion problem. But, if model checking for MAS and AI logics is to succeed, it is essential that attention is dedicated to this.

In this paper we have introduced an agent symmetry reduction technique for MAS specified in temporal-epistemic logic. By means of this technique we abstract the standard interpreted systems semantics into a counterpart semantics, by permuting agent names along the epistemic accessibility relation. This allows the initial states to be reduced by keeping a single representative for a group of symmetric initial states. The abstraction technique is shown to be sound and complete, i.e., there are neither false positives nor false negatives in the reduced model.

Experiments with the muddy children and the dining cryptographers show substantial reductions in verification time under symbolic model checking. The time is reduced by one to two orders of magnitude for moderate numbers of agents. Since BDDs are a form of symbolic optimisation, one may expect even bigger reductions for any implementation on top of an explicit model checker.

Looking ahead, we intend to transfer the reduction technique to data symmetry and to automate the symmetry detection method in Section 5 for ISPL programs. Automation of symmetry detection is a relatively recent area in mainstream verification with significant open problems. However, the very structured nature of ISPL might prove helpful.

Acknowledgments The research described in this paper is partly supported by EPSRC funded project EP/E035655, by the European Commission Framework 6 funded project CONTRACT (IST Project Number 034418), and by grant 2003-6108 from the Swedish Research Council.