A Cutoff Technique for the Verification of Parameterised Interpreted Systems with Parameterised Environments

1 Introduction

With the development and deployment of autonomous agents and multi-agent systems (MAS) in diverse applications such as search-and-rescue [Murphy, 2000] and webservices [Maximilien and Singh, 2004], there is a growing need to study powerful and versatile techniques for the verification of MAS. A key technique that has emerged in the past ten years is that of model checking [Clarke et al., 1999]. Model checking enables us to check whether a model MS representing a system S, satisfies a formula φP encoding a specification P . In the case of MAS a specification expressed by the formula φP may be not just a temporal formula, as is the case in verification of reactive systems, but a specification given in an agent-based logic, such as BDI [Rao, 1996], Desires-Goal-Intention [Dastani et al., 2003], or temporalepistemic logic [Fagin et al., 2003].

Indeed, a number of techniques have been put forward for the efficient model checking of MAS against agent-based specifications including binary decision diagrams [Gammie and Meyden, 2004; Lomuscio et al., 2009], abstraction [Cohen et al., 2009], partial order reduction [Lomuscio et al., 2010], bounded model checking [Lomuscio et al., 2007], parallel model checking [Kwiatkowska and A. Lomuscio, 2010], etc., thereby making it possible to verify systems with large state spaces. Yet, since the number of states is exponential in the number of agents in the system, systems of many agents remain intractable. This is particularly problematic when wishing to reason about open MAS. We may be able to encode a system with a given number of agents and verify that a specification holds. But we cannot draw any conclusion as to whether the specification will still hold should more agents be present. We need a technique that enables us to draw conclusions independently on the number of agents present in a MAS.

Cutoffs have been studied in the analysis of parametric systems precisely to solve this problem, often in the context of networking protocols [Emerson and Namjoshi, 1995; Hanna et al., 2009]. A cutoff is the number of components that need to be analysed with respect to a given specification to be able to draw conclusions on the specification in question irrespective on the number of components a system implements. Although the problem of parameterised verification is, in general, undecidable [Apt and Kozen, 1986], sound and incomplete proposals have been put forward [Clarke et al., 2008; German and Sistla, 1992; Hanna et al., 2009; Pnueli et al., 2002; Wolper and Lovinfosse, 1990] that impose restrictions on the systems and the properties studied. In previous work we have begun addressing this in the context of MAS [Kouvaros and Lomuscio, 2013]. However, [Kouvaros and Lomuscio, 2013] makes strong assumptions on the semantics which effectively entail that all agents evolve in the same way following synchronisation with the environment. This is a severe limitation that makes the technique inapplicable to any scenario where agents evolve differently even if they share a single skeleton. The aim of this paper is to overcome these limitations and present a technique which can be employed to verify systems with arbitrary number of agents that do not necessarily evolve in a lock-step fashion.

After recalling the technical setup in Section 2 for interleaved interpreted systems, in Section 3 we develop a semantics for parameterised interpreted systems in which the environments are equipped with parametric actions. This is explored in Section 4 thereby showing how to derive a cutoff for the verification of temporal-epistemic specifications. Section 5 reports on an implementation of the technique and discusses the experimental results obtained for the train-gatecontroller scenario with an unbounded number of trains.

2 Model Checking Parameterised Systems

We summarise the formalism of interleaved interpreted systems [Lomuscio et al., 2010] (IIS), a variant of interpreted systems [Fagin et al., 2003] to model asynchronous multiagent systems, and we discuss parameterised verification in the context of IIS.

Interleaved Interpreted Systems. Consider a MAS composed of n agents A = {1, . . . , n} and a special agent E (the environment in which the agents "live"). Let A′ = A∪ {E}. Each agent i ∈ A′ is encoded with a nonempty set of local states Li and a nonempty set of actions Acti containing a special "null" action ϵi. For each agent i ∈ A′ assume a local protocol Pi : Li → ℘(Acti) governing which actions can be performed in a given state, and a local transition function ti : Li×Acti → Li specifying the evolution of agent i's local states given its action. The "null" action ϵi is used to model the interleaving evolution of agent i; the protocol Pi is such that for every state li ∈ Li we have that ϵi ∈ Pi(li) (i.e., the null action is enabled at every local state); and the transition function ti is such that ti(li, ϵi) = li (i.e., whenever ϵi is performed, agent i's local state does not change). A global state g = (l1, . . . , ln, lE) is a tuple of local states for all the agents in the MAS and gives a description of the system at a particular instance of time. Given a global state g = (l1, . . . , ln, lE) and a set of agents J = {j1, . . . , j|J|}, we write gJ for the tuple of local states (lj1 , . . . , lj|J| ) of the agents in J in g. We often write gi instead of g{i}.

The local protocols and the local evolution functions determine the temporal evolution of the system's global states. Let ACT = ⋃i∈A′ Acti and Agent(a) = {i ∈ A′ | a ∈ Acti} for each action a ∈ ACT . The global (interleaved) transition relation R ⊆ G × G on a set G of global states is defined as (g, g′ ) ∈ R iff there exists a= (act1, . . . , actn, actE) ∈ Act1 × . . . ×Actn ×ActE and a ∈ ACT such that for all i ∈ Agent(a) we have that acti = a and ti(gi, a) = g′i ; and for all i ∈ A′ \ Agent(a), we have that acti = ϵi and ti(gi, acti) = g′i = gi. We often write g a→ g′ to mean that (g, g′ ) ∈ R by means of action a. Note that only one local action is performed in the system at a given round. Furthermore, every agent potentially able to perform the said action has to perform it at that round. Therefore, the agents communicate by means of shared actions. We assume that the joint null action is always enabled; therefore, R is serial. A path is

an infinite sequence g1a1 g2a2 g3 . . . such that gi ai→ gi+1 , for every i ≥ 1. Given a path π, we write π(i) for the i-th state in π. The set of all paths originating from g is denoted by Π(g). We write π[i] for the suffix giai gi+1 . . . of π and [i]π for the prefix g1a1 . . . gi of π. A global state g is said to be reachable from a global state g1 if there is a path g1a1 g2 . . . such that g = gi , for some i ≥ 1.

Model Checking IIS. Model checking techniques have been developed to verify IIS against temporal-epistemic specifications [Lomuscio et al., 2010]. However, a key limitation of the approach remains the state explosion problem: the state space of the system grows exponentially in the number of variables encoding the agents. This renders model checking intractable for systems with many agents. Furthermore, since model checking is typically defined for finite state systems, the approach becomes unfeasible for systems with unbounded number of agents, such as open systems.

Parameterised Systems. To overcome these limitations, parameterised systems have been put forward [Kouvaros and Lomuscio, 2013]. Parameterised systems are composed of arbitrarily many agents each having identical behaviour. The behaviour of the agents is specified by giving a generic agent template. A parameterised system S(n), where the parameter n is the size of the system, represents an infinite collection of IIS each composed of n indexed copies of the template agent. In [Kouvaros and Lomuscio, 2013] a cutoff result is established showing that model checking a certain concrete system (for a certain value of the parameter) suffices to establish correctness for all systems. However, the semantics insist on a lock-step evolution of the agents, thereby confining the technique to systems with agents evolving independently of the environment's actions. The aim of this paper is to overcome these limitations by giving a different semantics and devising a novel verification technique for it.

3 Parameterised Environments

We introduce a semantics for parameterised systems in which the environment closely synchronises with the agents' actions. We use two parameters to describe a MAS: the number of agents in the system and the set of actions of the environment. A Parameterised Interpreted System with Parameterised Environment (or PISPE) is given as follows. Firstly we define a template agent T = 〈L, ι,Act, P, t〉 and a template environment E = 〈LE, ιE,ActE, PE, tE〉. T and E are encoded as interleaved agents for which we respectively assume an initial state ι ∈ L and ιE ∈ LE. The set Act = S ∪NS of actions of the template agent is decomposed into disjoint sets of shared actions S and of non-shared actions NS . Shared actions are actions shared with the template environment (encoded with these actions; i.e., ActE = S) and they are further decomposed into a set NPS of nonparameterised actions and a set PS of parameterised actions. We assume that non-parameterised actions are shared by all the agents and the environment in a concrete system, whereas parameterised actions are shared by exactly one agent and the environment. Therefore, in compliance with the interleaved semantics, a global transition from a global state g can only happen in three cases: (i) an NS action is enabled for some agent at g; (ii) an NPS action is enabled for the environment and all the agents at g; (iii) a PS action is enabled for the environment and some agent at g. We assume that for each action a ∈ S, the set {l ∈ LE | a ∈ PE(l)} is a singleton; i.e., shared actions are enabled by the protocol at exactly one template state in E.

Let n ≥ 1 and [n] = {1, . . . , n}. We now describe the construction of a concrete system S(n) from the templates T and E. S(n) results from n instantiations A(n) = {T (1), . . . , T (n)}, or simply A(n) = [n], of the template agent and an instantiation E(n) of the template environment. Each agent i ∈ A(n) is instantiated as follows: Li = L×{i}; Acti = NS i ∪ PS i ∪ NPS ∪ {ϵi}, where NS i = NS × {i}, PSi = PS×{i}; Pi : Li → ℘(Acti) is defined by a ∈ Pi(li) iff tl(a) ∈ P (l), where tl(x), x ∈ Li ∪Acti, refers to the corresponding template state or action; ti : Li ×Acti → Li is defined by ti(li, a) = l′i iff t(l, tl(a)) = l′ . The concrete environment E(n) = 〈LE, ιE,ActE(n), PE(n), tE(n)〉 is obtained by instantiating each template parameterised action for every concrete agent: ActE(n) = NPS ∪ PS1 ∪ · · · ∪ PSn ; PE(n) : LE → ℘(ActE(n)) is defined by a ∈ (PE(n))(l) iff tl(a) ∈ PE(l); tE(n) : LE ×ActE(n) → LE is defined by (tE(n))(l, a) = l′ iff tE(l, tl(a)) = l′ .

We can now formally define the semantic structures we will be using in this paper.

• (a) Template Agent (Train)
• (b) Template Environment (Controller)

Figure 1: A PISPE of parameterised TGC.

Definition 3.1 (Parameterised system). Given T and E, assume a template labelling function h : L → ℘(AP) for a set AP of atomic propositions, and let n ≥ 1. A parameterised (interleaved) interpreted system with parameterised environment (PISPE, or a model), composed of n concrete agents, is a tuple S(n) = 〈G(n), ι(n),R(n), V (n)〉, where G(n) ⊆ L1×· · ·×Ln×LE is a set of reachable global states from ι(n) = (ι1, . . . , ιn, ιE), R(n) is a global transition relation, and V (n) : G(n) → ℘(AP × A(n)) is a labelling function such that pi ∈ (V (n))(g) iff p ∈ h(tl(gi)).

The above gives a concise description of an infinite collection of concrete systems (or system instances). Each value of the parameter n defines a system composed of a different number of agents and an environment suitable for synchronisation with each of the agents.

Example 3.2. Figure 1 presents a parametric variant of the untimed version of the Train-Gate-Controller (TGC) [Alur et al., 1998] composed of a controller and arbitrarily many trains encoded as a PISPE. Each train runs along a circular track and all tracks pass through a narrow tunnel (template state "T"). The tunnel has enough space for only one train to be in it at any time. The controller operates the colour (template states "G" (Green) and "R" (Red)) of the traffic lights to let the trains enter and exit the tunnel (to state "A" (Away)). Initially, the trains are in state "W" (Waiting) and the controller is in state "G". In the figure enter, exit ∈ PS and approach ∈ NS; the ϵ actions are omitted.

We use the temporal-epistemic logic ACTL∗K-X [Lomuscio et al., 2010] to expresses properties of MAS to be interpreted on PISPE. The logic combines epistemic modalities with the universal fragment of CTL∗-X (the logic CTL∗ without the next-time operator in which: (i) the existential state modality does not appear in any formula; and (ii) the negation is only allowed for atomic propositions). The restriction to a next-step free logic is typical in parameterised verification; the next-step operator can be used to count the number of agents in the system resulting in the verification problem being undecidable [Emerson and Kahlon, 2003]. The restriction to universal path quantification is essential in establishing the behavioural equivalence results in Section 4.

Definition 3.3 (Syntax of ACTL∗K-X). State formulae and path formulae of ACTL∗K-X over a set AP of propositions and a set A of agents are defined by the following BNF expressions:

where φ and ψ are state and path formulae and p ∈ AP. As usual [Fagin et al., 2003] the knowledge modality Ki stands for "agent i knows that", the path quantifier A is read "for all paths" and the temporal operators U, R are read "until" and "release" respectively. ACTL∗K-X formulae are interpreted in a model S(n) as standard: the temporal modalities are interpreted by means of the global transition relation; the epistemic modalities are interpreted over epistemic accessibility relations defined on local equalities for the agents' states.

Definition 3.4 (Satisfaction). Let S(n) be a PISPE, let π = g1 , a1 , g2 , . . . be a path of S(n), let g ∈ G(n) be a state of S(n), and let φ be an ACTL∗K-X formula. Satisfaction of φ at g, denoted (S(n), g) |= φ, or simply g |= φ, and satisfaction of φ on π, denoted (S(n), π) |= φ, or π |= φ, is inductively defined as follows:

We say that a formula φ is true in a system S(n), denoted S(n) |= φ, if (S(n), ι(n)) |= φ. We assume the customary abbreviations for Fφ ("Eventually φ") and Gφ ("Always φ") from until and release.

We would like to establish whether or not a certain ACTL∗K-X specification is satisfied by a MAS irrespective of how many agents are present. To do this we consider formulae with atomic propositions and epistemic modalities indexed with variables taking pairwise distinct values in A(n). We write φ(J) to indicate that each variable j ∈ J appears in the formula φ. We verify the PISPE encoding the MAS against properties of the form ∧J ϕ(J). In other words ∧J φ(J) is a shortcut for the ACTL∗K-X formula expressing the conjunction of all φ(J) under any assignment for J. Note that formulae of this form are implicitly parametric; i.e., the domain A(n) of J depends on the concrete system S(n) at which the formula is evaluated. For example consider the property "whenever a train is in the tunnel, it knows that no other train is in the tunnel at the same time" for the TGC. We express this property with the formula φTGC = ∧{i,j} AG(Ti → Ki¬Tj) which, when evaluated at S(2), is a shortcut for AG(T1 → K1¬T2) ∧ AG(T2 → K2¬T1).

Similar properties, but specified in CTL∗ , are considered in some approaches to parameterised verification [Clarke et al., 1989].

Definition 3.5 (Parameterised model checking problem). Given a PISPE S(n) and an ACTL∗K-X formula φ(J), the parameterised model checking problem (PMCP) concerns establishing whether or not the following holds:

The above amounts to checking an unbounded number of systems. This is a task that in principle involves an unbounded state space which is clearly unfeasible for traditional model checking techniques.

4 MAS Cutoffs

In this section we put forward a cutoff-based abstraction methodology for the PMCP. Cutoffs have been studied to circumvent the aforementioned difficulties in parameterised verification by reducing the number of systems to consider [Emerson and Namjoshi, 1995; Emerson and Kahlon, 2000; Hanna et al., 2009; Siirtola, 2010; Kaiser et al., 2010; Kouvaros and Lomuscio, 2013]. A cutoff for a system is the number of components that is sufficient to consider when evaluating a given specification.

Definition 4.1 (MAS Cutoff). Consider a PISPE S(n) and let Γ(I) = {∧J φ(J) | φ(J) ∈ ACTL∗K-X and J ⊆ I} be a set of specifications for S(n). A natural number c is a MAS cutoff for S(n) with respect to Γ(I) if for any φ ∈ Γ(I) we have that S(c) |= φ ⇔ ∀n ≥ c : S(n) |= φ.

By definition, if a cutoff exists, then the PMCP can be reduced to model checking all system instances up to the cutoff instance S(c). Note that by definition a cutoff c is always greater than the number of agents that any φ ∈ Γ(I) can refer to via local propositions and epistemic modalities. Note, also, that Γ(I) contains all ACTL∗K-X formulae with at most |I| index variables; this is in line with the standard treatment of cutoffs in the literature where a cutoff is defined with respect to the logic under analysis.

Theorem 4.2. There are PISPE S(n) and specifications Γ(I) ∈ ACTL∗K-X that admit no cutoff.

Proof. (Sketch) Let S(n) be the PISPE specified in Figure 2, where a, b ∈ PS and d ∈ NS. Suppose that there is a c such that S(c) |= φ ⇔ ∀n ≥ c : S(n) |= φ, for any φ ∈ Γ({i, j}). Inductively define a formula δc as follows: δc = si if c = 1; δc = si ∧ F(ui ∧ Fδc-1) if c > 1. Let φ = ∧{i,j} A(δc → G¬uj) expressing that for each path, if an agent does at least c - 1 loops through the cycle (s, u, s), then every other agent never reaches the state u in the path. It is easy to see that whenever an agent moves to state u, a different agent had moved to state t in a preceding step. Therefore S(c) |= ψ and S(c + 1) ⊭ ψ. The latter contradicts that c is cutoff.

While the result above is negative, we now proceed to identify a sufficient condition for the existence of cutoffs.

4.1 Environment Loops

We introduce the notion of shared-simulation between the agent and environment templates. Informally, there is a shared-simulation between T and E if E can simulate T only by means of the template states in which an S action is enabled. In the following, let l →X l′ , where l, l′ are template states, denote that there exists an action a ∈ X such that t(l, a) = l′ . Analogously, let g →X g′ , where g, g′ are global states, denote that there exists an action a ∈ X such that g a→ g′ . Finally, let →X∗ denote the reflexive and transitive closure of →X.

Definition 4.3 (Shared-simulation). A relation ∼P⊆ L × LE is a shared-simulation between T and E if ι ∼P ιE and whenever l ∼P lE the following condition holds: if there is l′ , l′′ ∈ L such that l →NS∗ l′ →{a} l′′ for some a ∈ S, then a ∈ PE(lE) and l′′ ∼P tE(lE, a).

We write T ≤P E to denote that there is a sharedsimulation between T and E. If T ≤P E, then a looping behaviour is induced on the concrete environment whenever it synchronises between two different agents.

Definition 4.4. A subsequence giai . . . gj , j > i, of a path g1a1 . . . in S(n) is an environment loop if giE = gjE .

As we clarify below, following synchronisation between the environment and an agent through a PS action, the environment can only synchronise with the same agent unless an environment loop occurs. Therefore, an environment loop occurs whenever the system moves to a state g in which the environment is able to synchronise with more than one agent.

Definition 4.5. A global state π(i) in a path π in S(n) has the environment loop condition, denoted ELC(π(i), r, q), if there exist r ̸= q ∈ A(n) and π(j), π(j ′ ), j < j ′ ≤ i, such that π(j) →PSr π(j ′ ) →NSr∗ π(i), and ∃g, g′ ∈ G(n) : π(i) →NSq∗ g →Sq g′ .

In other words, a global state π(i) has the environment loop condition if (i) the environment lastly synchronises with an agent r through a PS action earlier in π; and (ii) a different agent q can asynchronously move from its local state in π(i) to a state in which it can synchronise with the environment through a shared action.

Example 4.6. Consider the path π = (W1W2G) enter1 -→ (T1W2R) exit1 -→ (A1W2G) enter2 -→ (A1T2R) of the concrete TGC composed of two trains. The global state (A1,W2,G) in π has the environment loop condition whereas the global state (T1W2R) does not.

We call an NP-free section of a path π a subsequence giai . . . gj of π such that tl(ai-1 ) ∈ NPS (when i > 1), tl(ak ) /∈ NPS for i ≤ k ≤ j - 1 and tl(aj ) ∈ NPS. In other words the agents either perform asynchronous actions, or they synchronise with the environment only. The following lemma shows that the environment loop condition is a sufficient (but not necessary) condition for the occurrence of an environment loop in an NP-free section. Specifically, whenever ELC(g, r, q) holds, the environment's local state in g is equal to its local state at the initial global state of the NP-free section in which g occurs.

Lemma 4.7. Suppose that T ≤P E and let ρ = g1a1 , . . . , gj be an NP-free section of a path in S(n), n ≥ 2. If ELC(gk , r, q), 1 < k ≤ j, then [k]ρ is an environment loop.

Proof. (Sketch) By induction on k. Base step: [k]ρ = g1a1 g2 . Suppose that ELC(g2 , r, q). We have that a1 /∈ Sq and ∃g, g′ : g2 →NSq∗ g →Sq g′ . Obviously, g2E = gE and there is an aq ∈ Sq such that tl(aq) ∈ PE(gE). T ≤P E gives that tl(g1 q ) ∼P g1E . Therefore, as tl(g1 q ) →NSq∗ tl(gq), T ≤P E gives that tl(aq) ∈ PE(g1E ). It follows that g1E = gE (recall that the set {l ∈ LE | tl(aq) ∈ PE(l)} is a singleton) which gives that g1E = g2E . Assume for the inductive step that the claim is true for 2 ≤ k ≤ m- 1 and suppose that ELC(gm, r, q). Let l = maxy∈[m-1](ay ∈ PSq). If such a maximum does not exist, then the claim follows as in the base step; if it exists, then it is easy to see that ELC(gl+1 , q, z) for some z ∈ A(n). The inductive hypothesis gives that g1E = gl+1 E ; T ≤P E gives that tl(gl+1 q ) ∼P gl+1 E . The latter can be used in a similar argument to the base step and conclude gl+1 E = gm E . Hence, g1E = gm E .

4.2 Cutoff Theorem

We now show that if there is a shared-simulation between the agent and environment templates, then the cutoff c for a set of specifications Γ(I) being considered is c = max(2,m), where m = |I|. We achieve this result by means of three observations. Firstly, we show that by symmetry considerations [Emerson and Sistla, 1996] a formula ∧J φ(J) ∈ Γ(I) can be evaluated simply by considering the ground instantiation φ([|J|]) obtained by assigning the variables in J to any set of distinct values in A(n); for clarity we take the set of values simply to be {1, . . . , |J|}.

Proof. (Sketch) This follows by suitably extending the result in [Emerson and Sistla, 1996].

For example, the formula φTGC can be evaluated simply by considering its single conjunct AG(T1 → K1¬T2).

Secondly, we show that the cutoff instance S(c) admits the behaviour of any larger system S(n), n ≥ c. This requires a notion of equivalence between system instances. Recall that ACTL∗K-X formulae are preserved under stutteringsimulation [Lomuscio et al., 2010]; i.e., if a model M′ stuttering-simulates a model M, denoted M ≤ss M′ , then M′ |= φ([m]) implies that M |= φ([m]). We say that M ≤ss M′ if there is a relation ∼ss⊆ G × G′ such that ι ∼ss ι′ and whenever g ∼ss g′ then: (i) if g ∼i g1 (i ∈ [m]), then g′ ∼i g′1 for some g′1 such that g1 ∼ss g′1 ; (ii) V (g)∩{pi | p ∈ AP∧i ∈ [m]} = V ′ (g′ )∩{pi | p ∈ AP∧i ∈ [m]} and for every π ∈ Π(g), there is a π′ ∈ Π(g′ ), a partition B1,B2 . . . of the states in π, and a partition B′1 ,B′2 , . . . of the states in π′ such that for each j ≥ 1, Bj and B′j are nonempty and finite, and every state in Bj is related by ∼ss to every state in B′j .

Lemma 4.9. If T ≤P E and S(c) |= φ([m]), then S(n) |= φ([m]), for all n ≥ c ≥ m.

Proof. (Sketch) Define a relation ∼ss= {(g, g′ ) ∈ G(n) × G(c) | g[c] = g′ }. We show that S(n) ≤ss S(c). Simulation requirement (i): let g1 ∼ss g′1 . Suppose that g1 ∼i g2 for some i ∈ [m] and let g′2 = g2 [c] . We get that g′1 ∼i g′2 and g2 ∼ss g′2 . Simulation requirement (ii): let π = g1a1 g2 . . . ∈ Π(g1 ) and let ρ = g1 [c]a′1 g2 [c] . . ., where a′j = aj if aj ∈ ⋃i∈[c] Acti and a′j = ϵ otherwise. Note that for every subsequence giai gi+1 . . . gj aj gj+1 of an NPfree section in π such that ai , aj ∈ PSq, for some q ∈ [c], and az /∈ PSq, i < z < j, we have that gi+1 E = gjE by Lemma 4.7. Therefore the environment allows for the transitions in ρ, hence ρ ∈ Π(g′1 ). Let B1,B2, . . . and B′1 ,B′2 , . . . be a partition of π and ρ respectively into singleton blocks. We have that Bj ∼ss B′j , j ≥ 1; therefore, S(n) ≤ss S(c).

Finally, we show that any system S(n + 1), n ≥ c, admits the behaviour of the system S(n) obtained by removing one component. Repeated application of the following lemma gives that any system S(n), n ≥ c, simulates the cutoff instance S(c).

Lemma 4.10. If T ≤P E and S(n + 1) |= φ([m]), then S(n) |= φ([m]), for all n ≥ c ≥ m.

Proof. (Sketch) The idea is to allow the extra agent n+ 1 in S(n+1) to mimic agent 1. Define a relation R1 = {(g, g′ ) ∈ G(n) × G(n + 1) | g = g′ [n] and tl(g′n+1 ) →(NS∪PS)∗ tl(g′1 )}; if R1(g, g′ ), then agent n + 1 in S(n + 1) is able to reach the state of agent 1 via PS and NS transitions. We ensure that the environment allows this. Define a relation R2 = {(g, g′ ) ∈ G(n)×G(n+1) | if ∃g1 : g →NPS g1 , then tl(g′n+1 ) ∼P g′E , else g′E = gE}; so, if R2(g, g′ ) and there is an NPS action enabled at g, then tl(g′n+1 ) ∼P g′E thereby allowing agent n + 1 to reach the state of agent 1 in g′ . Now define a relation ∼ss= R1 ∩ R2. We show that S(n) ≤ss S(n + 1). Let g1 ∼ss g′1 . Simulation requirement (i): follows by a similar argument used in the proof of Lemma 4.9. Simulation requirement (ii): let π = g1a1 g2 · · · ∈ Π(g1 ). We inductively construct a path ρ = g′1a′1 g′2 · · · ∈ Π(g′1 ) as required by stuttering-simulation. Assume that we have already constructed a prefix [j]ρ, a prefix [i]π such that ρ(j) ∼ss π(i), and a partition of the states in [j]ρ and [i]π into corresponding blocks. We now define the next blocks B and B′ . There are two cases depending on the next action ai in π. Case 1: tl(ai ) /∈ NPS. Then B = gi+1 and B′ = g′j+1 , where g′j ai→ g′j+1 . Case 2: tl(ai ) ∈ NPS. Then B = gi+1 and B′ = g′j+1 g′j+2 . . . g′j+d , where

Proof. By Lemma 4.8 it suffices to prove the claim for φ([m]). (⇒) Repeated application of Lemma 4.10. (⇐) Lemma 4.9.

Following Corollary 4.11 we can reduce the PMCP (Definition 3.5) to the simple check of the cutoff instance S(c) against φ([m]).

5 Implementation and Experimental Results

We implemented the cut-off based abstraction methodologies presented earlier in an experimental toolkit that we built from the open-source model checker MCMAS [Lomuscio et al., 2009]. We extended ISPL, MCMAS's input language, to allow for the definition of the semantic structures and the parametric specifications considered here. A PISPE is described by giving declarations for the template agent and the template environment. These extend ISPL's semantics by considering, among other concepts, the different kind of actions that PISPE are defined on. We refer to [MCMAS-P, 2013] for more details.

Given the input descriptions for T and E, the model checker MCMAS-P first attempts to establish whether T ≤P E. To do this, the tool constructs the concrete system S(1). The states in S(1) are assigned atomic propositions by the valuation function V (1) : G(1) → ℘(AP), where AP = {aT , aE | a ∈ S}, defined as aT ∈ (V (1))(g) iff a ∈ P(tl(g1)) and aE ∈ (V (1))(g) iff a ∈ PE(gE). In other words a state g is labelled with aT (respectively, aE) if the shared action a is enabled for the agent (respectively, the environment) at g. Following this, MCMAS is called to check S(1) against the formulae in ∆ = {AG(aT → aE) | a ∈ S}. It is easy to see that T ≤P E iff ∀δ ∈ ∆ : S(1) |= δ; so if the formulae are satisfied we can conclude that T ≤P E. Following a successful simulation test MCMAS-P employs Corollary 4.11 by means of five steps: (i) the cutoff c is computed from the cardinality of the set of indices used in the specifications Λ ⊂ Γ(I) to check; (ii) the reachable state-space of the cutoff system S(c) is computed and encoded symbolically; (iii) given an (input) valuation of the template states, atomic propositions are assigned to global states as in Definition 3.1; (iv) the specification formulae are reduced to their ground instantiations Λ([c]) as in Lemma 4.8; (v) finally, MCMAS is called to verify S(c) against Λ([c]). Following these calculations the user can conclude whether or not the specifications hold for any number of agents in the system.

We tested the cutoff technique on the TGC against the specification φTGC, a commonly used benchmark [Lomuscio et al., 2010; Hoek and Wooldridge, 2002]. Note that the state-space grows exponentially with the number of agents in the system. To the best of our knowledge all current techniques would have to consider an unbounded number of systems each with different number of trains. This is unfeasible as illustrated by Table 1: time and space requirements grow exponentially in the number of trains to consider, hence model checking quickly becomes intractable. In our case the base model checker we used could not verify a system composed of 80 trains within the timeout of one hour. In comparison MCMAS-P established the simulation as above and verified the cutoff instance S(2) in under 0.1 seconds. The MAS cutoff MCMAS-P found corresponds to a MAS with 2 agents; the formula checked, and found to be true, was AG(T1 → K1¬T2). This establishes the correctness of the TGC for systems with any number of agents.

6 Conclusions and FurtherWork

As discussed in the Introduction, irrespective of recent progress in the area of verification for MAS, a number of open problems remain, including verification of open systems with an unbounded number of components. Given MAS are often open systems, it seems of particular importance to develop techniques for these setups.

In this paper we put forward a cutoff technique for MAS which enabled us to reason about interleaved interpreted systems in which the agents may synchronise more effectively with the environment. The results we obtained on the sharedsimulation relation here defined enabled us to identify a sufficient condition for the cutoff generation. This enabled us to implement a toolkit for the technique which pointed to very significant advantages over conventional model checking. While the results here obtained share the specification language and the general notion of parameterised interpreted system used in [Kouvaros and Lomuscio, 2013], the semantics and the abstraction notion here put forward is different. Most importantly, and differently from [Kouvaros and Lomuscio, 2013], we can here deal with systems in which exactly one concrete agent may synchronise with the environment at a tick of the clock. This enables us to check rich scenarios such as the TGC which are not supported in [Kouvaros and Lomuscio, 2013].

Much work remains to be done in this line. While we can now verify unbounded systems, we can only operate on one abstract template agent. Our future work includes supporting more than one template agent so that we may be able to verify unbounded systems with agents of any kind. This at present remains a considerable challenge due to the complexity of the setup required.

Acknowledgments. The research described in this paper was supported by the EPSRC Research Project "Trusted Autonomous Systems" (grant No. EP/I00520X/1).