Formal Verification of Parameterised Neural-symbolic Multi-agent Systems

1 Introduction

Safety concerns stemming from the increasing development of Multi-agent Systems (MAS) have been put under mathematical scrutiny by automated methods that ascertain their correct behaviour. Verification methods based on SAT and BDDs [Kacprzak et al., 2004; Raimondi and Lomuscio, 2005] have resulted in push-button engines such as Verics, MCK and MCMAS [Gammie and van der Meyden, 2004; Kacprzak et al., 2008; Lomuscio et al., 2017]. In conjunction with increasingly sophisticated state-space reduction techniques, such as predicate abstraction [Lomuscio and Michaliszyn, 2015] and partial order reductions [Jamroga et al., 2020], the verifiers have been able to scale to the analysis of systems with very large state spaces.

While the different methods target the provision of effective solutions to different types of analyses, e.g., fast search for counterexamples [Penczek and Lomuscio, 2003] as opposed to fast correctness proofs [Ball and Kupferman, 2006], and for different classes of MAS, e.g., MAS defined over infinite-state as opposed to finite-state variables [Lomuscio and Michaliszyn, 2015], all methods make two fundamental assumptions. The first is that the MAS under analysis is composed of a known number of agents specified at design time. The second is that the agents composing the MAS are specified using traditional programming languages. The approaches cannot therefore be used to verify important classes of MAS, where either the systems have arbitrarily many participants or the agents are endowed with machine learning components. The former class of systems includes open systems, where agents can join and leave the system at runtime, and applications designed irrespective of the number of participants, such as robot swarms and scenarios in the Internet of Things. The latter class comprises forthcoming neuralsymbolic applications such as autonomous vehicles.

More recent methods have addressed the verification of systems with an unbounded number of constituents [Kouvaros and Lomuscio, 2016b; Kouvaros and Lomuscio, 2016a]. While the various verification methods focus on different communication primitives for the agents, most of them rely on abstractions whereby the unbounded verification problem is reduced to analysing a finite state-space. These abstractions formed the backbone of various formal reasoners such as those targeting fault-tolerance [Kouvaros et al., 2018] and data-aware systems [Belardinelli et al., 2017].

In a different line of work, verification methods for MAS comprising agents with neural components were put forward [Akintunde et al., 2020b; Akintunde et al., 2022]. To deal with the real-valued operational domain of the neural network models, the methods recast verification queries for bounded properties into Mixed-Integer-Linear-Programming.

While these two lines of work independently tackle unbounded and neural-symbolic MAS, none of the underlying methods can be used for analysis of systems that are both unbounded and neural-symbolic. In this paper we overcome this limitation. Specifically, we introduce Parameterised NeuralsymbOlic interpreted Systems (PANoS), a formal model for modelling unbounded neural-symbolic MAS. We develop an abstraction methodology for PANoS whereby we derive novel sound and complete procedures for the verification and emergence identification problems with respect to bounded universal and existential CTL formulae. We use these procedures to analyse a social dilemma scenario.

The rest of the paper is organised as follows. After discussing related work below, we present PANoS in Section 2, followed by the development of the verification and emergence identification procedures in Section 3, which we evaluate in Section 4 on a social dilemma scenario. We conclude in Section 5.

Related Work. The contribution is related to the two lines of work discussed above, namely parameterised verification and verification for neural-symbolic MAS. Previous models in parameterised verification targeted either arbitrarily many agents operating in fixed environments [Kouvaros and Lomuscio, 2016b; Kouvaros and Lomuscio, 2016a; Felli et al., 2020] or a fixed number of agents living in environments of arbitrary size [Aminof et al., 2016]. None of these models include neural components. Systems comprising homogeneous agents were also analysed within the framework of Alternating-time Temporal Logic but in a fixed, non-parameterised and purely symbolic setting [Pedersen and Dyrkolbotn, 2013].

Existing verification methods for MAS with neural components [Akintunde et al., 2020b; Akintunde et al., 2022] take as input systems with a known number of agents. The main theoretical finding of this work is that verification for an unbounded number of agents can be reduced to the verification of (abstract) systems with a bounded number of agents.

2 Parameterised Neural-symbolic Interpreted Systems

Interpreted systems are a standard semantics for describing multi-agent systems [Fagin et al., 1995b]. They provide a natural setup to interpret specifications in a variety of languages, including temporal-epistemic logic and alternatingtime temporal logic [Fagin et al., 1995a; Lomuscio and Raimondi, 2006]. Parameterised interpreted systems is a parametric extension of interpreted systems put forward to reason about unbounded multi-agent systems [Kouvaros and Lomuscio, 2015]. The parameter in a system of this kind denotes the number of agents composing the system, each homogeneously constructed from an agent template.

In this section we extend parameterised interpreted systems to Parameterised Neural-symbOlic interpreted Systems (PANoS), where the template for the agents is not purely symbolic but (i) comprises a perception mechanism that is implemented via neural networks, (ii) it is coupled with a symbolic action mechanism. This neural-symbolic treatment of the agents follows the Neural Interpreted Systems (NIS) model from [Akintunde et al., 2020b]. Differently from PANoS however, NIS are limited to standard non-parametric systems with a pre-defined number of agents.

A PANoS consists of the descriptions of an agent template, from which an unbounded number of concrete agents may be constructed, and of an environment in which the agents operate. The agent template is defined as follows.

Definition 1 (Agent template). An agent template is a tuple t = (Lt, ιt, obst, Act t, prot t, tr t), where:

• Lt = Prvt ×Pert is a nonempty (possibly infinite) set of template local states. Each local state is a pair (prv t, per t) of a private state prvt ∈ Prvt ⊆ Rmprv and a percept pert ∈ Pert ⊆ Rmper that encodes a perception of the environment by the agent.
• ιt ∈ Lt is the unique initial template state.
• obst : Lt × Le → Pert is an observation function that maps pairs of template local states Lt ⊆ Rmprv+mper

and environment states Le ⊆ Rme (see below) to percepts Pert ⊆ Rmper . We assume, without loss of generality to the parameterised verification results present in the Secton 3, that the observation function is implemented via a neural network f : Rmprv+mper+me → Rmper .

• Actt is a nonempty and finite set of actions.
• prott : Lt → 2Actt \ {∅} is a local protocol function that returns the set of actions available at a given local state.
• trt : Lt×Actt×2Actt ×Acte →Prvt is a local transition function that determines the next private state for an agent instantiated from the template given its current local state, its action, the set of actions performed by all the agents and the action of the environment.

Example 1. We consider the example of a guarding game, an instance of a collective risk dilemma [Milinski et al., 2008]. In this game there is a colony of agents that needs to be guarded. Guarding duty costs a guard some health Gr (Gr < 0) and resting improves an agent's health by Rr (Rr > 0). If no one is guarding, then all agents in the colony lose some health Ur (Ur < 0). The maximum value of an agent's health is Mh. If an agent does not have any health left, then it expires. We formalise the agent template t = (Lt, ιt, obst, Act t, prot t, tr t) in this game as follows.

• Lt = {(h, per ) | h ∈ {0, . . . ,Mh}, per ∈ {Gp,Rp,Ep}, where h is the health of the agent and percepts Gp, Rp and Ep indicate what the agent is willing to do (see below).
• ιt = (|Gr|+1,Gp), i.e., at the start each agent has enough health to be able to guard at least once without expiring.
• Actt = {Ga,Ra,Ea}, where Ga, Ra and Ea stand for Guarding, Resting and Expired actions, respectively.
• The observation function is assumed to be given as a neural network. It returns whether the agent volunteers to guard, Gp, can only rest, Rp, or is expired, Ep.

If the percept is Gp, then the agent can both guard and rest. If the percept is Rp or Ep, the only available actions are resting and the dummy action Ea, respectively.

• The local transition function updates the health according to the rules. Formally, for P ∈ {Gp,Rp}:

The environment has a similar description to an agent template but it (i) does not include a perception mechanism, (ii) may include an infinite set of initial local states.

Definition 2 (Environment). An environment is a tuple e = (Le, Ie,Acte, prote, tre), where Le ⊆ Rme is a nonempty set of local states, Ie ⊆ Le is a nonempty set of initial local states, Acte is a nonempty and finite set of actions, prote : Le → 2Acte \ {∅} is a local protocol function, and tre : Le ×Acte × 2Actt → Le is a local transition function.

The agent template and the environment define the main formal structure we will be using in this paper.

Definition 3. A Parameterised Neural Interpreted System (PANoS) is a tuple S = (t, e, ℓ), where t is an agent template, e is an environment, and ℓ : AP → 2 Lt is a labelling function on the agent template states for a set AP of atomic propositions.

Example 2. Consider the agent template t in Example 1. Assume a dummy environment e where Le = Ie = {0} and Act e = {0} are singleton states and actions, prot e(0) = {0} and tre(0, 0,A) = 0 for all A ∈ 2Actt . Suppose AP = {a, d}, where a stands for alive and d for dead, and ℓ is a labelling function defined as ℓ(a) = {(h, S) | h > 0 and S ̸= Ep} and ℓ(d) = Lt \ ℓ(a). Then S = (t, e, ℓ) is a PANoS for the guarding example.

A PANoS S gives a parametric description of an unbounded collection of concrete NIS. In particular, for any value n ≥ 1 of the parameter, the concrete system S (n) composes n copies 1, . . . , n of the agent template with the environment e. We write Ag (n) for the set {1, . . . , n} of concrete agents instantiated from t. A global state in S (n) describes the system at a particular instant of time. It is a tuple q = (l1, . . . , ln, le) of local states for all the agents and the environment in S (n) . For a global state q, we write lprvi(q), lperi(q) and lsi(q) to denote the private part prvi and the perception part peri of the local state lsi(q) = (prvi , peri) of agent i in q. The set G(n) of all possible global states is G(n) = L1 × · · · × Ln × Le. A joint action α = (α1, . . . , αn, αe) in S (n) is a tuple of local actions for all the agents and the environment. For a joint action α, we write lai(α) to denote the local action of agent i in α. The set ACT (n) of all joint actions is ACT (n) = Act1 × · · · × Actn × Acte. We now formally define the concrete NIS generated from PANoS.

Definition 4 (Concrete Neural Interpreted System). Given a PANoS S = (t, e, ℓ) and n ≥ 1, a concrete neural interpreted system is a tuple S (n) = ({1, . . . , n, e} , I (n) , ℓ(n) ), where I (n) = {(ι1, . . . , ιn, ιe) | ιe ∈ Ie} is the set of initial global states and ℓ(n) : AP × {1, . . . , n} → 2 G(n) is the concrete labelling function satisfying q ∈ ℓ(n) (p, i) iff lsi (q) ∈ ℓi (p).

So the atomic propositions in a concrete system are indexed by each of the concrete agents: (p, i) holds in a global state if the agent i is at a local state labelled with p by the template labelling function. This will enable us to construct specifications independently of the size of the concrete system on which they are evaluated.

Given the current global state (l1, . . . , ln, le), where li = (prvi, peri), for i ∈ Ag (n) , of the agents and the environment, the operational cycle of the agents is described as follows. First, every agent i ∈ Ag (n) ∪ {e} selects an action αi that is permitted by its protocol, i.e., αi ∈ proti(li). Then, the agents synchronously perform the joint action α = (α1, . . . , αn, αe). Following the execution of the joint action, each agent i ∈ Ag (n) updates the private component of its local state as per its local transition function to prv ′i = tri(li, αi , α→{}, αe), where α→{} = {αj | j ∈ {1, . . . , n}} is the projection of the joint action for the agents onto a set.

This generates an intermediate local state l′i = (prv ′i , peri) for each of the agents. Similarly, the environment updates its local state to l′e . Finally, every agent i ∈ Ag (n) observes the update on its local state and the update on the local state of the environment via its neural perception module obsi, thus generating a percept per ′i = obsi(l′i , l′e ), with which it updates its perception part thereby obtaining a new local state l′′ i = (prv ′i , per ′i ).

So, differently from the standard treatment of interpreted systems, the transition function of a concrete agent in PANoS does not depend on the joint action performed in the system, but it depends on the local action performed by the agent and on the set of actions performed by all of the agents and the environment. Thus, the identities of the agents are abstracted away in a joint action, thereby reflecting the unbounded nature of PANoS. In other words, whereas a concrete agent can observe which actions were performed in the system at a given time, it cannot observe which agent or how many agents performed each action.

We now formally define the temporal evolution of a concrete system S (n) .

Definition 5 (Global transition function). The global transition function tr (n) : G (n) ×ACT (n) → G (n) of a concrete system S (n) satisfies tr (n) (q, α) = q ′ iff the following hold:

• lae(α) ∈ prote(lse(q)), tre(lse(q), lae(q), α→{}) = lse(q ′ ); i.e., the environment's action is protocol compliant and its local state is updated as per its local transition function and the actions that were performed in the round.
• For all i ∈ {1, . . . , n}, we have that lai(α) ∈ prot i (ls i (q )), tri(lsi(q), lai(α), α→{}, lae(α)) = lprvi(q ′ ), and obsi((lprvi(q ′ ), lperi(q)), lse(q ′ )) = lperi(q ′ ); i.e., the agent's action is protocol compliant, the private part of its local state is updated as per its local transition function and the actions performed at the round, and the perception part of its local state is updated as per its observation function.

Each concrete system is associated with a temporal model that we will use to interpret our specification language.

Definition 6 (Model). Given a concrete NIS S (n) , its (induced) model MS (n) is a tuple (G(n) ,ACT (n) , T (n) , ℓ(n) ), where G(n) is the set of global states, ACT (n) is the set of joint actions, T (n) is the global transition relation defined as (q, α, q′ ) ∈ T (n) iff tr (n) (q, α) = q ′ , and ℓ(n) is the labelling function as in Definition 4.

A path in a model MS (n) is an infinite sequence of global states and joint actions q0α0 q1α1 . . . s.t. (qi , αi , qi+1 ) ∈ T (n) for all i ≥ 0. For a path ρ, we write ρ(i) for the i-th global state in ρ. Given a global state q in MS (n) we write Π(q) for the set of all paths originating from q.

Example 3. Consider a concrete neural interpreted system S (2) = ({1, 2, e} , I (2) , ℓ(2) ) for the agent template in Example 1 and PANoS in Example 2, where ℓ(2) is defined from ℓ, I (2) = {(ι1, ι2, 0)} and ιi = (|Gp| + 1, Gp). A model MS (2) of S (2) is depicted in Figure 1, where for brevity we omit the environment local state le.

We express specifications for PANoS in an indexed and bounded variant of Computation Tree Logic (CTL), henceforth bICTL. The logic (i) introduces indexed atomic propositions that are quantified over the agents of the concrete system on which the formula in question is evaluated, and (ii) permits only the construction of formulae whose evaluation can be realised on paths of bounded lengths. The former extends CTL by allowing the formulation of properties irrespective of the concrete system on which they are evaluated. The latter restricts CTL to bounded formulae [Akintunde et al., 2020a].

Definition 7. Given a set AP of atomic propositions and a set VAR of variables, the bICTL formulae are defined by the following BNF:

The formula AXk φ is read as "for all paths, φ holds at the k-th step", and EXk φ as "there exists a path where φ holds at the k-th step". We note that bounded until A(φU k ψ) can be inductively abbreviated as in [Akintunde et al., 2020a].

The logic bCTL [Akintunde et al., 2022] is the logic obtained from the above BNF, but replacing the first clause with p and removing the last clause. The restriction of the logic to bounded properties follows the undecidability of verification for the unbounded case [Akintunde et al., 2022]. While the parameterised verification results presented in the next section still hold should negation be allowed in our syntax, verification methods for concrete models, including VENMAS used in the present contribution, do not support negation, since its inclusion may hinder the completeness of verification [Akintunde et al., 2022].

A bICTL formula is said to be a sentence if every variable appearing in the formula is in the scope of either a universal or an existential agent quantifier. Hereafter we consider only indexed bICTL sentences of the form ∀v1 · · · ∀vm : φ, or, shortly, ∀v1,...,vm φ, where: (i) vi ∈ VAR for i ∈ {1, . . . ,m}, (ii) φ is either universal in that it contains only universal path quantifiers or existential in that it contains only existential path quantifiers.

We now define the satisfaction relation for bICTL on the temporal models associated with the concrete systems.

Definition 8 (Satisfaction). Given a model MS (n) , a global state q in MS (n) , and a bICTL sentence ∀v1,...,vm φ with m ≤ n, the satisfaction of φ at q, denoted (MS (n) , q) |= φ, or simply q |= φ when MS (n) is clear from the context, is defined as:

By the definition above, a bICTL sentence is evaluated only up to a bounded number of time steps. Given a bICTL sentence, we call this number of steps the temporal depth of the sentence, which we formally define below.

Definition 9. The temporal depth td(φ) of a bICTL sentence ∀v1,...,vm φ is inductively defined as follows:

A sentence ∀v1,...,vm φ is said to be true inMS (n) , denoted MS (n) |= ∀v1,...,vm φ, if (MS (n) , q) |= ∀v1,...,vm φ for all q ∈ I (n) . The sentence is said to be true in S, denoted S |= ∀v1,...,vm φ, if it is true in every model induced by every concrete system instantiated from S with at least m agents, i.e., MS (n) |= ∀v1,...,vm φ for all n ≥ m. The parameterised verification problem is to check whether this holds.

Definition 10 (Parameterised verification problem). Given a PANoS S and a bICTL sentence ∀v1,...,vm φ, determine whether S |= ∀v1,...,vm φ.

While solutions to the parameterised verification problem can be used to establish whether a property holds for any number of agents, some properties, often called emergent properties [Bonabeau et al., 1999], are expected to be realised only after certain conditions on the number of agents are met. For instance, foraging protocols for robot swarms, require a certain number of agents to be present for the underlying formations to be established. A natural number th ∈ N is an emergence thershold for a PANoS S and a bICTL sentence ∀v1,...,vm φ if we have that MS (n) |= ∀v1,...,vm φ for every n ≥ th. The emergence identification problem is to compute an emergence threshold.

Definition 11 (Emergence identification problem). Given a PANoS S and a bICTL sentence ∀v1,...,vm φ, compute an emergence threshold th ∈ {0,m,m+1, . . .} for S and bICTL. (If th = 0, then S admits no threshold for ∀v1,...,vm φ.)

3 Parameterised Verification Procedure

In this section we put forward procedures for solving the parameterised verification and emergence identification problems introduced in the previous section. For ease of presentation, we fix a PANoS S = (t, e, ℓ), where t = (Lt, ιt, obst,Actt, prott, trt), e =

(Le, Ie,Acte, prote, tre), and a bICTL sentence ∀v1,...,vm φ throughout the section.

The verification procedure that we introduce recasts the parameterised verification and emergence identification problems for S and ∀v1,...,vm φ to a number of (standard) verification problems for abstract and concrete NIS against the bCTL formula φ[v1 ↦→ 1, . . . , vm ↦→ m], which for brevity we denote as φ[m]. We show that the satisfaction status of φ[m] on these systems determines the satisfaction and existence of emergence thresholds for ∀v1,...,vm φ on S. This enables us to use previously established methodologies for the verification of NIS against bCTL [Akintunde et al., 2020b] to analyse PANoS. We start by reducing the problem of checking the bICTL sentence in question to that of checking φ[m].

Lemma 1 (Symmetry reduction). S |= ∀v1,...,vm φ iff S |= φ[m].

We next construct the zero-one abstraction of the systems generated from S. The zero-one abstraction is a NIS comprising a zero-one agent, which is an abstraction for arbitrarily many concrete agents, m conrete agents, whose local states determine the satisfaction status of the atomic propositions in φ[m] (see Definition 4), and the environment. In other words, the zero-one agent in this abstract NIS encodes how an arbitrary number of agents may interfere with the temporal evolution of the concrete agents 1, . . . ,m. It is defined in the following.

Definition 12 (Zero-one agent). Given an agent template t = (Lt, ιt, obst, Act t, prot t, tr t) over a set Per t of percepts and a set Prvt of private states, its associated zero-one agent is a tuple zo = (Lzo, ιzo, obszo,Actzo, protzo, trzo) over sets Perzo = 2Pert \ {∅} and Prvzo = 2Prvt \ {∅} of percepts and private states, where:

• Lzo = 2Lt \ {∅} is the set of abstract states. An abstract state represents the projection of global states in systems of any size onto a set.
• ιzo = {ιt} is the unique initial abstract state.
• obszo : Lzo × Le → Perzo is the abstract observation function. It maps pairs of abstract and environment states to sets of percepts, where each set includes the percepts that would be collectively generated in a global state represented by the abstract state. Formally, the observation function satisfies obszo(lzo, le) = perzo if:
• for all lt ∈ lzo we have that obst(lt, le) ∈ perzo;
• for all pert ∈ perzo there is lt ∈ lzo s.t. obst(lt, le) = per t .
• Actzo = 2Lt×Actt \ {∅} is the set of abstract actions. As with abstract states, an abstract action represents the projection of joint actions, paired with the local states at which they are performed, of arbitrarily many agents onto a set.
• protzo : Lzo → 2Actzo \ {∅} is the abstract protocol. The protocol prescribes the sets of template actions that can be collectively performed at a global state represented by a given abstract state. It is defined as protzo(lzo) = ×lt {(lt, A) | A ∈ 2prot t (lt) \ {∅}} .
• trzo : Lzo × Actzo × 2Actt × Acte → Prvzo is the abstract transition function. The function determines the set

of private states that the agents would collectively transition to in any global state represented by a given abstract state and after they have performed a joint action represented by a given abstract action. It is such that trzo(lzo, αzo, A, αe) = prvzo if the following hold:

• αzo ∈ protzo(lzo);
• for all (lt, αt) ∈ αzo, we have trt(lt, αt,A, αe) ∈ prv zo;
• for all prvt ∈ prvzo, there is (lt, αt) ∈ αzo such that tr t(lt, αt, A, αe) = prv t.

The abstract NIS comprises the zero-one agent, m concrete agents, and the environment. Formally, it is a tuple S (m) ab = ({1, . . . ,m, zo, e} , I (m) ab , ℓ(m) ab ), where I (m) ab = {(ι1, . . . , ιm, ιab, ιe) | ιe ∈ Ie} is the set of initial global states and ℓ(m) ab : AP × {1, . . . ,m} → 2 G(m) ab is the abstract labelling function satisfying q ∈ ℓ(m) ab (p, i) iff lsi(q) ∈ ℓi(p). The abstract global transition function is defined as the concrete one but accounting for the zero-one agent:

Definition 13. The abstract global transition function tr (m) ab : G (m) ab ×ACT (m) ab → G (m) ab of the abstract system S (m) ab satisfies tr (m) ab (q, α) = q ′ if the following hold:

• lae(α) ∈ prote(lse(q)), tre(lse(q), lae(q), α→{}) = q ′ , where α→{} = {lai(α) | i ∈ {1, . . . ,m}} ∪ {αt | (lt, αt) ∈ lazo(α) for some lt}.
• For all i ∈ {1, . . . ,m, zo}, we have that lai(α) ∈ proti(lsi(q)), tri(lsi(q), lai(α), α→{}, lae(α)) = lprvi(q ′ ) and obsi((lprvi(q ′ ), lperi(q)), lse(q ′ )) = lper i (q ′ ).

Given the abstract global transition function we can associate an (abstract) model MS (m) ab = (G(m) ab ,ACT (m) ab , T (m) ab , ℓ(m) ab ) to the abstract NIS in a similar manner to the concrete case.

We now establish a correspondence between the abstract model and the concrete models. We show in particular that: (i) the abstract model simulates every concrete model with at least m+ 1 agents; (ii) there is always a concrete model with a sufficient number of agents that simulates the abstract model; (iii) a concrete model always simulates a smaller concrete model. A model simulates another model if every behaviour exhibited by the latter is also admitted by the former. As specifications for PANoS are bounded, we consider simulation up to a bounded number of steps as defined below.

Definition 14 (Bounded simulation.). A b-bounded simulation between two models M = (G, ACT, T, ℓ) and M′ = (G′ ,ACT ′ ,T ′ , ℓ′ ) with sets of initial global states I and I ′ is inductively defined on b ≥ 0 as follows.

• A relation ∼0⊆ G×G′ is 0-bounded simulation if for every ι ∈ I, there is ι′ ∈ I ′ with (ι, ι′ ) ∈∼0, and whenever (q, q′ ) ∈∼0, we have that q ∈ ℓ(p, i) implies that q′ ∈ ℓ′ (p, i).
• A relation ∼b⊆ G×G′ is b-bounded simulation if for every ι ∈ I, there is ι′ ∈ I ′ with (ι, ι′ ) ∈∼b, and whenever (q, q′ ) ∈∼b, the following hold:

1. (q, q′ ) ∈∼0.
2. If (q, α, q1 ) ∈ T for a joint action α ∈ ACT and global state q1 ∈ G, then there is a joint action α′ ∈ ACT ′ and global state q′1 ∈ G′ such that (q′ , α′ , q′1 ) ∈ T ′ and (q1 , q′1 ) ∈∼b-1.

We say that a model M′ simulates a model M up to b time steps, denotedM≤b M′ , if there is a b-bounded simulation relation between M and M′ . Universal bCTL formulae are preserved from the simulating model to the simulated model and existential bCTL formulae are preserved from the simulated model to the simulating model whenever their temporal depth is at most b.

Theorem 1. LetMandM′ be two models such thatM≤b M′ . Then, the following hold.

1. If M′ |= φ for a universal bCTL formula φ with td(φ) ≤ b, thenM |= φ.
2. If M |= φ for an existential bCTL formula φ with td(φ) ≤ b, thenM′ |= φ.

We can now show the simulation results pertaining to the abstract and concrete models. We start by showing that the abstract model simulates every concrete model with at least m + 1 agents up to any depth.

Next, we show that irrespective of the temporal depth of the specification under analysis there is always a concrete model that simulates the abstract model up to that depth.

Finally, we show that every concrete model simulates every smaller concrete model up to any depth.

The above results enable the derivation of procedures for solving the parameterised verification and emergence identification problems. In the case of universal formulae, the emergence identification procedure simply concerns checking the abstract model, and the parameterised verification procedure additionally involves checking a single concrete model against the formula in question.

Corollary 1. For a universal bCTL formula φ[m]:

• If MS (m) ab |= φ[m], then m+ 1 is an emergence threshold for ∀v1,...,vm φ. Otherwise, there is no emergence threshold for ∀v1,...,vm φ.
• MS (m) ab |= φ[m] andMS (m) |= φ[m] iff S |= ∀v1,...,vm φ.

Theorems 2, 3 and 4, additionally enable the derivation of procedures for the verification of existential properties.

Corollary 2. If φ[m] is an existential bCTL formula with temporal depth b and n = mini (MS (m) ab ≤b MS (i) ), then:

• If MS (n) |= φ[m], then n is an emergence threshold for ∀v1,...,vm φ. Otherwise, there is no emergence threshold for ∀v1,...,vm φ.
• MS (i) |= ∀v1,...,vm φ, for all i ∈ {m, . . . , n}, iff S |= ∀v1,...,vm φ.

In summary, Corollaries 1 and 2 provide constructive, sound and complete methodologies for checking universal and existential bICTL formulae for PANoS. For the case of universal properties, verification can be conducted by constructing and checking the abstract model and the concrete model with m agents, where m is the number of index variables present in the specification in question. The specification is satisfied by the abstract and concrete models if and only if the specification is satisfied in general for any number of agents. The satisfaction of the specification by the abstract model is also connected by biconditional implication with the existence of an emergence threshold for the specification. For the case of existential properties, verification can be performed by enumerating all concrete models, identifying the smallest one that simulates the abstract model, and checking all concrete models up to the simulating one. The specification is satisfied by all these concrete models if and only if the specification is satisfied in general for any number of agents. The satisfaction of the specification by the concrete model that simulates the abstract model is also connected by biconditional implication with the existence of an emergence threshold for the specification.

4 Evaluation

In this section we present an evaluation of the parameterised verification procedures described in Section 3 on the guarding game presented in Example 1.

The guarding game is an instance of a social dilemma game, a class of MAS characterised by tension between individual and collective rationality [Van Lange et al., 2013]. The game simulates the fundamental forces of a collective risk dilemma (CRD), a type of social dilemma where a guaranteed "tragedy of the commons" [Hardin, 1968] is avoided by personal sacrifice by a population of agents, or brought on by free riding if all the agents neglect the collective interests [Santos and Pacheco, 2011]. Namely, guarding can be considered equivalent to cooperation (acting in collective interest), and resting to defection (acting in selfish interest).

We train a neural observation function using deep Qlearning, a type of reinforcement learning (RL) algorithm. During the training, the game was played by 4 agents, and the parameters were set as Mh = 4, Gr = -2, Rr = 1 and Ur = -3. The rewards were assigned to reflect the tension between individual and collective interests. All agents shared the same neural network, and thus were learning to play against exact copies of themselves. The produced neural network has two hidden layers of four ReLU activated neurons, takes as input a single neuron, representing the normalised health points of the agent, and outputs the estimated Q-values of the two actions 'rest' and 'guard'.

Given the learned neural network, we implemented a template agent and a zero-one agent for the guarding game. We then used Corollaries 1 and 2 to verify whether it is possible for a colony of agents to survive after a number of time steps. Specifically, recall from Example 2 that proposition a labels all states with positive health ("alive") and proposition d labels all other states with no health ("dead"). We considered two specifications (for vi ∈ VAR):

1. The existential property ∀v1,v2 φkE , where φkE = EXk ((a, v1) ∧ (a, v2)). The property expresses that there is an evolution where at least 2 agents are alive after k time steps.
2. The universal property ∀v1,...,vm φkA, where φkA = AXk ∧mi=1 (a, vi). The property expresses that in every possible evolution at least m agents are alive after k time steps, for m ∈ {2, 3}.

We used the VENMAS toolkit [Akintunde et al., 2020b] for checking the conrete and abstract systems prescribed by Corollaries 1 and 2. The experiments were performed on a standard PC running Ubuntu 22.04 with 16GB RAM and processor Intel(R) Core i5-4460. We relied on Gurobi v10.0 [Gu et al., 2016] to solve the mixed integer linear programs generated by VENMAS.

Let S be the PANoS for the guarding example. For the existential property, we check whether at least two agents can stay alive for k time steps (S |= φkE ), and whether there is a minimal number (an emergence threshold) of agents that can guarantee that. We vary the temporal depth k from 2 to 5. To verify whether S |= ∀v1,v2 φkE , we use Corollary 2 and check whetherMS (i) |= φkE [2] for every i ∈ {2, . . . , n}, where n is the minimal i such that MS (i) k-bounded simulates MS (2) ab . We have that n = 2 for k = 2, and n = 3 for k ≥ 3.

Table 1 presents the outcomes of the verification queries MS (i) |= φkE [2] for i ∈ {2, . . . , 4}. For k = 2, since MS (2) |= φ2E [2], we conclude that S |= ∀v1,v2 φ2E . This of course additionally implies that n = 2 is an emergence threshold for ∀v1,v2 φ2E . For k ≥ 3, sinceMS (2) ̸|= φkE [2], we conclude that S ̸|= ∀v1,v2 φkE . Still, since MS (3) |= φkE [2], we obtain that n = 3 is an emergence threshold for ∀v1,v2 φkE , so there need to be at least 3 agents present in the colony to ensure a temporal evolution whereby the colony is viable. The verification results for i ∈ {4, 5, 6} reported by the table (which are not used to reason about parameterised verification) demonstrate the increasing computational cost of verifying concrete systems for increasing number of agents, thereby empirically justifying the need for parameterised verification.

Concerning the universal property, we verified φkA[m] against the abstract model MS (m) ab for the temporal depths k ∈ {1, . . . , 6} and m ∈ {2, 3}. The verification times and results can be found in Table 2. We observe that because of the presence of the zero-one agent, the verification times are longer than the ones observed in Table 1. We additionally notice that the property in question is not satisfied even after 1 time step, which is expected given that there exist paths where no agent is guarding even when there are volunteers.

In summary, our experimental results confirm the intractability of verification for concrete models as the number of agents grows, thereby motivating the need for the parameterised verification methods that we put forward.

5 Conclusions

Advances in interconnectivity of autonomous services and machine learning fuel the development of MAS with arbitrarily many neural-symbolic components, thereby creating a pressing need for their verification.

Towards addressing this need, in this paper we put forward a number of automated procedures for the formal analysis of parameterised, neural-symbolic MAS. The procedures enable conclusions to be drawn on the satisfaction of temporal properties irrespective of the number of agents composing the MAS. They can additionally identify emergence thresholds expressing sufficient conditions on the number agents for a property to be realised.

The theoretical results have driven the implementation of a parameterised, neural-symbolic verifier, which we used to reason about a simple social dilemma game. More generally, the techniques here developed can be used to analyse properties of policies learned to deal with real-life challenges that come in the form of collective risk dilemmas, as well as properties in swarm scenarios and open systems in general.

In future work we target the development of parameterised methods for interleaved semantics for neural-symbolic MAS and strategic properties.