# smtbased_safety_checking_of_parameterized_multiagent_systems__05d99841.pdf

SMT-based Safety Checking of Parameterized Multi-Agent Systems

Paolo Felli, Alessandro Gianola, Marco Montali Free University of Bozen-Bolzano, Bolzano, Italy {pfelli,gianola,montali}@inf.unibz.it

We study the problem of verifying whether a given parameterized multi-agent system (PMAS) is safe, namely whether none of its possible executions can lead to bad states. These are captured by a state formula existentially quantifying over agents. As the MAS is parameterized, it only describes the ﬁnite set of possible agent templates, while the actual number of concrete agent instances that will be present at runtime, for each template, is unbounded and cannot be foreseen. We solve this problem via inﬁnite-state model checking based on satisﬁability modulo theories (SMT), relying on the theory of array-based systems. We formally characterize the soundness, completeness and termination guarantees of our approach under speciﬁc assumptions. This gives us a technique that is implementable on top of third-party, SMT-based model checkers. Finally, we discuss how this approach lends itself to richer parameterized and data-aware MAS settings beyond the state-of-the-art solutions in the literature.

Introduction

The automated veriﬁcation of Multi-Agent Systems (MASs) typically amounts to check the existence of execution strategies for the achievement of given goals, or to compute counterexamples as evidence of points of potential failure. Model checking (Clarke et al. 2018) is one of the most common approaches to the veriﬁcation of MASs, often with a focus on strategic abilities (Bulling, Goranko, and Jamroga 2015). However, a common limitation in this literature is the assumption that the system is ﬁnite-state and fully speciﬁed, which in many applications requires to abstract or propositionalize crucial system features. Other approaches have thus tackled the veriﬁcation of MASs in settings that are intrinsically inﬁnite-state (Esparza et al. 2017), for which explicit model-checking techniques cannot be used off-theshelf. In these settings, the model of the MAS is partially speciﬁed or some sort of data component is present. A notable example is that of parameterized MASs (PMASs), addressed by a growing literature (Bloem, Jacobs, and Khalimov 2015; Kouvaros and Lomuscio 2016, 2017; Esparza et al. 2017; De Masellis and Goranko 2020). In PMASs, the number of agents is unbounded and unknown,

Copyright 2021, Association for the Advancement of Artiﬁcial Intelligence (www.aaai.org). All rights reserved.

so that possibly inﬁnitely many concrete MASs must be considered: the task is to check whether a property is satisﬁed by any (or all) concrete MASs that adhere to a ﬁxed behavioral structure (such as a known catalogue of possible agent templates), without ﬁxing their number a priori. In particular, the property we consider is that of safety: a PMAS is said to be safe if bad states, characterized by a state formula (existentially quantifying on agents), can never be reached. Crucially, this must be veriﬁed irrespective of (i) the number of agent instances that will be present at runtime, (ii) the possible interactions they may have and executions they may induce and (iii) the initial setup of the PMAS, i.e., the possible initial interpretation of a read-only, relational data store that is used by PMASs for background data. Safety checking is a key property not only of MASs but of dynamic systems in general, with a long-standing tradition (see, e.g., (Abdulla et al. 1996; Bloem, Jacobs, and Khalimov 2015)). Applications range from veriﬁcation of protocols for swarms to applications for Industry 4.0 and cloud manufacturing , where an unbounded number of manufacturing resources must be considered (Alechina et al. 2019). In this paper we illustrate our theoretical result based on the application of satisﬁability modulo theories (SMT) (Barrett and Tinelli 2018) techniques for array-based systems (ABSs) (Ghilardi et al. 2008; Ghilardi and Ranise 2010a; Alberti, Ghilardi, and Sharygina 2017; Calvanese et al. 2020), and we characterize its soundness and completeness (and decidability of the task). Speciﬁcally, we do so for the notable case of interleaved PMASs. This gives us the theoretical foundation for a practical implementation based on stateof-the-art SMT-based model-checkers, which is showcased in (Felli, Gianola, and Montali 2020b) for a class of PMASs more restricted than the one we study here. The implementation is available at (Felli, Gianola, and Montali 2020a). The paper is organized as follows. We ﬁrst state the contributions and discuss related literature. Then, we introduce PMASs, their interleaved execution semantics, and the (un)safety checking problem. We then encode PMASs into ABSs, which allows us to apply SMT-based techniques for their veriﬁcation. We also show the theoretical guarantees of our veriﬁcation procedure. Finally we discuss future work. A simple example. Consider a scenario in which a swarm of robotic agents intends to reach a protected room denoted as C. To do so, from their initial location they have to ﬁrst

The Thirty-Fifth AAAI Conference on Artificial Intelligence (AAAI-21)

move to a room A, then to a room B, then to C. The doors in corridors between these locations are either open or closed. There is no way a robot can move past a closed door, and the information about the status of these doors is not known nor controllable. Moreover, a security system prohibits to move from room B to room C unless the system is ﬁrst switched off by interacting with a control panel in room A. However, by moving from A to B, the security system automatically turns on again. Moreover, in room C a further security system, when armed, activates an electromagnetic pulse (EMP) to disable robots in that room, and it is armed whenever C is entered. The pulse becomes unarmed after use, but always disables at least one robot. We want to check whether it is possible, after the EMP is activated (hence after a robot entered room C), that there can be robots in C that are not disabled. By careful analysis, we can see that the answer is positive if all doors are open: at least two robots need to move to A, then B. Then, a least one further robot must disable the security system by moving to A and using the control panel in that room. After this, the other robots can move from B to C (this action will arm the EMP). At this point the EMP will be ﬁred in room C, but there are chances that one of the robots will not be disabled, although this is not guaranteed. Note how the existence of this witness of unsafety relies on the ability of considering that more robots are at the same time in C, which is not something that is required by the protocol of robots (a protocol describes the executability of actions).

In this paper we address this type of scenarios, and we discuss at the end of the paper how our technique can be directly extended to account for a number of features left as future work. These include, e.g., considering a number of alternative execution semantics (which is possible within this framework as it is), and most importantly an extension with read/write relational databases that the agents can use during execution for storing data and exchanging messages.

Related Work and Contribution

Our work is related to the existing literature on parameterized veriﬁcation, which has however a number of differences with respect to our approach. The veriﬁcation problem for parameterized systems has been studied extensively, and a number of decidability results are known for various kinds of speciﬁcations. For example, it is decidable for forms of regular speciﬁcations (Esparza et al. 2017) but undecidable even for stuttering-insensitive properties such as LTL\X formulae (Emerson and Kahlon 2003) if asynchronous rendezvous is allowed. As summarized in (Bloem, Jacobs, and Khalimov 2015), decidability results for the veriﬁcation of parameterized systems are based on reduction to ﬁnite-state model checking via abstraction (Pnueli, Xu, and Zuck 2002; John et al. 2012), cutoff computations (a bound on the number of instances that need to be veriﬁed (Emerson and Namjoshi 2003)), or by proving that they can be represented as wellstructured transition systems (Finkel and Schnoebelen 2001; Abdulla et al. 1996). Our veriﬁcation technique, although limited to safety, is not based on (predicate and counter) abstractions, cutoffs nor reductions to ﬁnite-state model checking. Also, the MASs we consider do not assume a particu-

lar topology, and the types of disjunctive guards considered in (Emerson and Kahlon 2003) are here extended toward a FO setting by also allowing relation symbols (please refer to the section on future work for more comments on this point). The approach builds on the model-theoretic framework of ABSs (Ghilardi and Ranise 2010a; Calvanese et al. 2020) and can be seen as a declarative, ﬁrst-order counterpart of theories of well-structured transition systems for which compatible results are known (e.g., (Abdulla et al. 1996; Bloem, Jacobs, and Khalimov 2015)). Regarding speciﬁcally the veriﬁcation of PMASs, the closest model are those of (Kouvaros and Lomuscio 2016, 2017; Belardinelli, Kouvaros, and Lomuscio 2017) and open MASs (De Masellis and Goranko 2020; Kouvaros et al. 2019). In (De Masellis and Goranko 2020), the authors study homogenous, dynamic MASs that are analogous to our definition of PMASs. There, agents join and leave dynamically during the execution and are partitioned into controllable and uncontrollable, so that the main task is to verify strategic properties of coalitions of at least n controllable agents against coalitions of at most m uncontrollable ones. While a mechanism for joining/leaving the system can be captured natively in our formalization of PMASs, our approach is not currently able to verify strategic, temporal properties. The framework of (Kouvaros et al. 2019; Kouvaros and Lomuscio 2016) and related papers is also similar. Again, compared with that work, we restrict to the key task of checking safety, instead of tackling model-checking of modal speciﬁcations. Their results depend on the chosen execution semantics, hence on the combinations of possible action types that are allowed. The same holds for our technique: although not included in this paper, our approach can be directly extended (with the same soundness and completeness guarantees) to the further variants of execution semantics studied there, with the exception of those involving the global execution of synchronous action types. For these, which we leave as future work due space limitations, we can guarantee a weaker notion of soundness (see (Felli, Gianola, and Montali 2020c)), consistently with the results in (Kouvaros and Lomuscio 2016). Crucially, however, their veriﬁcation procedure requires to identify a cutoff even for the PMASs considered in this paper (analogous to the class of systems there called SMR): if a cutoff is found then the veriﬁcation result is correct, otherwise the procedure halts with no result (hence, the procedure is sound but not complete). The existence of a cutoff depends on the existence of a simulation property (between the agent templates and the environment) to be checked on the abstract system, which has to be computed ﬁrst. Conversely, our technique does not require cutoffs: we are able to characterize our results on soundness and completeness for the execution semantics adopted here, while termination (thus a complete decision procedure) can be directly obtained by a syntactic property of the action guards and goal formula. By departing from the literature above, we present here a veriﬁcation technique grounded in an SMT-based (Barrett and Tinelli 2018) approach for ABSs (Ghilardi et al. 2008; Ghilardi and Ranise 2010a; Alberti, Ghilardi, and Sharygina 2017; Calvanese et al. 2020). This is a very well-

understood SMT-based formalism for which a number of results of practical applicability already exist (Calvanese et al. 2019c,a; Ghilardi et al. 2020). Our approach is the ﬁrst to establish a theoretical connection between the veriﬁcation of PMASs and the long-standing tradition of SMT-based model checking for ABSs; moreover, our decidability result, although inspired by an analogous condition in (Calvanese et al. 2020), is a novel contribution for ABSs as well. This result is exploited operationally, by encoding safety-checking of PMASs into the general-purpose model checker MCMT (Ghilardi and Ranise 2010b).

PMASs: parameterised MASs

Let Θ be a set of (semantic) data types (e.g., reals, integers, booleans). Each type θ Θ comes with a (possibly inﬁnite) domain θ, and a type-wise equality operator =θ (we simply write = when the type is clear). Let R be a set of relations over Θ, which we treat as uninterpreted relations (i.e. simple relation symbols), used to model background information in the MAS which is never updated during the execution, thus representing a read-only component. E.g., the information about corridors and doors in the example can be modeled via these relations. We consider the usual notion of FO interpretations I = ( I, I) with I = S Θ θ and I is an FOL interpretation function for symbols in R.

Deﬁnition 1. An agent template is a tuple T = ID, L, l0, V, type, val, Aloc, Asyn, P, δ composed of: an inﬁnite set ID of unique agent identiﬁers of sort ID; a ﬁnite set L of local states, with initial state l0 L; a ﬁnite set V of local (i.e., internal) agent state variables; a variable-type assignment type : V 7 Θ; a variable-value assignment val : L V 7 S Θ θ, with val(l, v) θ for θ = type(v); a non-empty, ﬁnite set of action symbols A .= Aloc Asyn (described later), s.t. Aloc Asyn = ; a protocol function specifying the conditions under which each action is executable. It is a function P : A 7 Ψ, where Ψ are agent formulae, deﬁned below, querying the current state of the whole PMAS; a total transition function δ : L A 7 L, describing how the local state is affected by the execution of an action α: the template moves from a state l to a state l when executing an action α iff δ(l, α) = l , also denoted l α l .

The environment template is a special agent template Te with ﬁxed identiﬁer (i.e., ID = {e}): there is exactly one environment. Intuitively, a (concrete) agent is a triple composed of an agent ID, its template and its current local state. Analogously, a (concrete) environment is a pair consisting of the template Te and its current state. Let {T1, . . . , Tn, Te} be a set of agent (and environment) templates, with Tt = IDt, Lt, l0 t , Vt, typet, valt, Aloc t , Asyn, Pt, δt for t {1, . . . , n, e}. We denote a concrete agent with ID j, template Tt and local state lj by writing j, lj t, and similarly we denote the concrete environment by e, le e. We also denote a vector of k such concrete agents of template Tt as I, L t, where I IDk t and L Lk t are vectors of IDs and local states. We assume unique agent

IDs and disjoint template variables, i.e., IDt IDt = and Vt Vt = for t, t {1, . . . , n, e}, t = t . A PMAS is a tuple M = {T1, . . . , Tn}, Te, R consisting of n agent templates, one environment template and the relations. Note that a PMAS speciﬁes the initial local state of all agents for each template, but does not specify how many concrete agents exist for each template. A conﬁguration is a tuple g = { I1, L1 1, . . . , In, Ln n}, e, le e , which thus identiﬁes the number of agent instances (the size of each It, t [1, n], may differ). A conﬁguration is initial iff all agents are in their initial local state. Inﬁnite possible initial conﬁgurations exist, since the number of concrete agents is unbounded. As shorthand, we denote the local state lj of agent j, lj t in conﬁguration g as g.j, thus writing j, g.j t. We now deﬁne the agent formulae used for protocols in Def. 1 as quantiﬁer-free formulae ψ(j, self, e, v) where j are the free variables of sort ID, self is a special constant used to denote the current agent, e is the special ID (constant) of the concrete environment, v are template variables (for any template). These follow the grammar:

ψ .= (v [j] = k) | (v [j1] 1 = v [j2] 2 ) | | R(x1, , xm) | j1 = j2 | ψ | ψ1 ψ2

where v, v1 Vt, v2 Vt for templates t, t {1, . . . , n, e}, k is a constant in θ for θ = typet(v), R is a relation symbol in R of arity m 1 (over types θ1, . . . , θm), each xi is either a variable v [j] of some template or a constant ki θi, and j, j1, j2 are either the variables of sort ID in j or the constant self or the ID constant e for the environment (with a little abuse of notation, in this paper we use symbols j to denote variables of sort ID or concrete IDs). The usual logical abbreviations apply. Note that, differently from the restricted model in (Felli, Gianola, and Montali 2020b), terms of the form R(x1, , xm) can mention more than one variable of sort ID and make comparisons of the form v [j1] 1 = v [j2] 2 , possibly with j1 = j2. This detail will play an important role for our termination guarantees (see Thm. 2). Intuitively, agent formulae are implicitly quantiﬁed existentially over agent IDs. As we will formalize next, they allow to test (dis)equality of agent variables w.r.t. other agent variables and agent constants (IDs), and to check whether a tuple is in a relation (whose elements are agent variables or constants). For instance, (v [j] = k) informally means that there exists an agent ID j so that v = k for such an agent. An ID grounding of a formula ψ(j, self, e, v) in g is an assignment σ which assigns each variable j of sort ID in j, and the constant self, to a concrete agent ID in g (denoted σ(j) and σ(self), resp.). It also assigns the constant e to itself, i.e. σ(e) = e. Intuitively, for a formula to be true in g, one needs to ﬁnd a suitable σ that makes the formula true.

Deﬁnition 2. Given an interpretation I0, a conﬁguration g satisﬁes a formula ψ under I0, denoted g |=I0 ψ, iff there exists an ID grounding σ of ψ in g s.t. g, σ |=I0 ψ, with: g, σ |=I0 (v [j] = k) iff valt(g.σ(j), v) = k, where v Vt; i.e. the concrete agent σ(j), g.σ(j) t, i.e. with ID σ(j) and template Tt, is so that v = k;

g, σ |=I0 (v [j1] 1 = v [j2] 2 ) iff valt(g.σ(j1), v1) = valt (g.σ(j2), v2), where v1 Vt, v2 Vt ; i.e. the agents σ(j1), g.σ(j1) t and σ(j2), g.σ(j2) t with IDs σ(j1), σ(j2) and templates Tt and Tt , are so that v1 = v2; g, σ |=I0 R(x1, , xm) iff RI0(yi, . . . , ym), where yi is as follows for each i [1, m]. If xi is a constant k, then yi is k; if instead xi is a variable v [j] with vi Vt for some template t {1, . . . , n, e} then yi is valt(g.σ(j), v). Intuitively, R holds under I0 for the constants and values of variables, where the value of v [j] is taken from the local state of agent with ID σ(j); g, σ |=I0 (j1 = j2) iff σ(j1) = σ(j2); g, σ |=I0 ψ iff g, σ |=I0 ψ; g, σ |=I0 ψ1 ψ2 iff g, σ |=I0 ψ1 or g, σ |=I0 ψ2.

Note that self is freely assigned to an agent ID: if g satisﬁes a formula with self, then an agent exists that can be taken as self. Hence we write g |=j I0 ψ, if needed, to denote that there exists σ with σ(self) = j so that g, σ |=I0 ψ. This informally reads as ψ is true in g for agent with ID j. E.g., assuming g is s.t. v1 = 6 for agent with ID 3, and v1 = 5 for agent with ID 7, then g |=3 I0 (v [self] 1 = 6) (v [j] 1 = 5). A (global) transition of a PMAS describes its evolution when a vector of actions α (one for each concrete agent and one for the environment) are executed from conﬁguration g = { I1, L1 1, . . . , In, Ln n}, e, le , so that a new conﬁguration of the form g = { I1, L 1 1, . . . , In, L n n}, e, l e is reached. This is denoted by g α g . Since each concrete agent and the environment may either perform an action (in Aloc t Asyn) or remain idle, multiple executions semantics can be deﬁned, depending on the constraints we impose on α, and in this paper we consider one of these, i.e., interleaved MASs. First, we describe the set Aloc t Asyn used in Def. 1. Symbols in Aloc t , for each t, are called local actions, and those in Asyn synchronization actions. Actions in Aloc t can only affect the local state of the concrete agent which executes them, whereas actions in Asyn represent the synchronization between one or more agents and the environment and thus can affect the local state of each agent involved. Intuitively, synchronization actions in Asyn are used to model explicit communication actions or any action with effects that are not private to the single agent or to the environment. Therefore, not every vector α is meaningful: typically, one wants to constrain the possible evolutions so that synchronization actions and local actions do not happen at the same time, so that we can distinguish those steps in which the PMAS evolves in response to public actions, events, messages, from those in which agents update their local state.

Interleaved PMASs. They are characterized by the following notion of legal transition. First, we consider a special no-op action nop so that δt(l, nop) = l for each template t and local state l. Hence, at each step, either: (i) a (possibly not proper) subset of concrete agents and the environment perform a (non nop) action in Aloc t on their local state or (ii) the environment and a subset of the agents synchronize by executing the same action in Asyn. Local (non-nop) and

synchronization actions are not mixed. α.j denotes the action of the agent with ID j, or of the environment if j = e.

Deﬁnition 3. For an interpretation I0, g α g is legal iff: g .j = δt(g.j, α.j) for every j, g.j t, t {1, . . . , n, e}, i.e., agents and environment evolve as per their template; g |=j I0 Pt( α.j) for every j, g.j t, i.e., each action is executable and self is replaced by j for evaluating protocols; either only local actions are executed (by some agents and the environment), or the environment and at least one agent synchronize through action α Asyn. All other agents perform nop. Formally, either: no j exists so that α.j Asyn, that is, no synchronization action is executed; or the environment and at least one agent synchronize, while other agents can either synchronize as well or freely decide to remain idle. Formally, α.e = α Asyn and i = e exists with α.i = α, while α.j {α, nop} and g |=j I0 Pt( α.j) for every j, g.j t. Example 1. In the scenario, we use a template Tatt for robots, with variables room (enumeration [init,A,B,C]) and disabled (boolean). For the environment template Te, sec ON and armed are used for specifying whether the security system is active, and whether the pulse is armed. Template Tatt has actions go A, go B and go C, plus additional actions off and pulse representing the action of switching off the security system and of being disabled by the pulse. The environment also has actions go B, go C and off, as the robot template. Indeed, these are synchronization actions which have an effect on the environment as well: respectively, the security system is re-activated, the EMP is armed, the security system is disabled. The fact that corridors between rooms are either open or closed is captured by elements in a binary relation over rooms (e.g. Corr(A,B)). As we quantify over initial interpretations, this captures the fact that the status of doors is not known, but all possibilities are considered. For example, the protocol of action go C in Tatt is

room[self] = B sec ON[e] = false Corr(B, C). Note that it is not required to specify the template of variables, as these sets are disjoint. Therefore, given a global state in which an agent instance of Tatt (i.e., a robot) is in local state l and Te is in local state le, the robot can execute a transition l go C l only if Corr(B,C) is in I0, valatt(l, room) = B and vale(le, sec ON) = false in Te. The resulting local state l of the robot is such that valatt(l , room) = C while the environment reaches a local state l e so that vale(l e, armed) = true (plus further assignments for inertia). Other actions are deﬁned in a similar manner. E.g., the protocol of off in Tatt is

room[self] = A. The formula expressing the unwanted condition is given at the end of this section.

Runs and the Safety Checking Problem. Based on the one-step deﬁnition of (legal) global transition, we now deﬁne the notion of runs for interleaved PMASs. Given a PMAS M = {T1, . . . , Tn}, Te, R , a (global) run is a pair ρ, I0 where ρ is a sequence ρ = g0 α1 g1 α2 and I0 is an interpretation for relation symbols as before. We restrict to runs that (i) are legal and (ii) start from an initial conﬁguration, i.e., with all concrete agents in their initial lo-

cal state. A transition as above speciﬁes how each concrete agent g.j evolves depending on the nature of the action α.j. As already stated, once ﬁxed at the start of ρ, I0 does not change and is used at each step for evaluating formulae.

Deﬁnition 4. An agent formula ψgoal is reachable in M iff I0 and an initial conﬁguration g0 exist such that a conﬁguration g with g |=I0 ψgoal is reachable through a run ρ, I0 from g0.

If a formula is not reachable then it is so for any number of agents and all possible interpretations. Finally, we can formally state the task at hand.

Deﬁnition 5. Given a PMAS M and an agent formula ψgoal, the safety checking problem is to check whether ψgoal is not reachable in M. If this is the case then M is said to be safe w.r.t. ψgoal, otherwise it is unsafe w.r.t. ψgoal.

Example 2. In our running example, the agent formula expressing the unwanted condition is room[j] = C destroyed[j] = false armed[e] = false.

PMASs as Array-based Systems

Array-based Systems (ABSs) is a generic term used to refer to inﬁnite-state transition systems implicitly speciﬁed using a declarative, logic-based formalism in which arrays are manipulated via logical formulae. They are described using a multi-sorted theory: one kind of sorts for the indexes of arrays and another for the elements stored therein. The content of an array is unbounded and updated during the evolution. Nonetheless, note that our technique does not distinguish between unboundedness and inﬁniteness, and ABSs enjoy the ﬁnite model property (Calvanese et al. 2020). In order to introduce veriﬁcation problems in the symbolic setting of ABSs, one ﬁrst has to specify the FO theories TInd and T (equipped with FO signatures ΣInd and Σ, resp.) for array indexes and for the array elements. In this paper, TInd will be the empty theory where ΣInd contains only equality, and T will be EUF (the theory of uninterpreted symbols), i.e., the empty theory with signature Σ containing sorts S, relation symbols Rel and constants C. This is a standard, common setting in the ABS literature. Then, one needs to write the formulae representing the set of initial states and the system evolution. We denote by z a tuple z1, . . . , zm and by φ(x, a) the formula with x as free individual variables and a as free array variables. In the following we use the notation F(x) := case of {κ1(x) : t1; κn(x) : tn} (where κi(x) are quantiﬁer-free Σ-formulae and ti are generic terms), or, equivalently, nested if-then-else expressions: we call one such F case-deﬁned function. We also use λ-abstractions like b = λj.F(j, z) in place of j. b(j) = F(j, z), where typically F is a case-deﬁned function or a constant assignment. We consider three types of formulae: An initial formula ι(x, a) initializes individual and array variables via assignments and λ-abstractions: (Vm i=1 xi = ci) (Vk i=1 ai = λj.di), with ci,di constants from Σ; A state formula of the form j φ(j, x, a) speciﬁes conditions on variables, where φ is a quantiﬁer-free Σ-formula and j are individual variables of the index sort;

A transition formula ˆτ relates current and new (primed) values of individual and array variables: e (γ(e, x, a) (Vm i=1 x i := c) (Vk i=1 a i = λj.Fi(j, e, x, a))), where e are individual variables (of both element and index sorts); γ (the guard ) is a quantiﬁer-free Σ-formula; x and a are renamed copies of x and a; c is a constant from Σ and Fj (the conditional update") is a case-deﬁned function. We now give a general deﬁnition of array-based systems, one that helps us to narrow down the scope and consider the kind that is suitable for our purposes (e.g. having the notion of action), in place of a generic notion of array-based system, that is extremely general. Then we show how a PMAS can be encoded as a special case of such deﬁnition (in Def. 7). Known results on ABS (Ghilardi and Ranise 2010a; Calvanese et al. 2020) can directly be adapted to this variant. Deﬁnition 6. An abstract AB-PMAS is a tuple: Σ, Sind, x, arr Y, act, ιa, τa (i) Σ := S, Rel, C is a multi-sorted FO signature as before, such that there exists a speciﬁc sort Aa S called actions sort ; (ii) Sind is a set of sorts of index type; (iii) x is a set of individual variables (containing the global variables encoding the states of the environment); (iv) arr Y is a set of arrays, one for each variable y Y, where Y is an abstract set of variables; (v) act is a set of arrays, with codomain of type Aa; (vi) ιa is an initial formula, whose individual variables are x and whose array variables are arr Y and act; (vii) τa is a disjunction of transition formulae, with individual and array variables x, x and arr Y, act, arr Y, act , resp.

Formally, a FO interpretation of Σ can be thought as an instance of the elements domain of an abstract AB-PMAS, the individual variables are assigned to values taken from this interpretation, Aa is interpreted over a ﬁnite set of elements called actions and the sorts Sind are interpreted over disjoint sets of concrete indexes. The array variables are assigned to functions from these sets of indexes to the instance of the elements domain. In what follows, we show how a speciﬁc abstract ABPMAS (simply called AB-PMAS) can be used to model a PMAS as in the previous section. To this end, we consider the different sorts and relations as in that section, and we encode the set of agent and environment templates. Instead of the abstract set arr Y of arrays, for each template Tt with t {1, . . . , n, e} we consider a set arr Vt of arrays, one for each variable in Vt, that is used to store the current value of that variable for each concrete agent of type t. Intuitively, the cell for index j in the array for variable v Vt of template Tt holds the value of v for the agent with ID (in correspondence to) j in the current global state (see Fig. 1). Since only one concrete environment exists, instead of arrays arr Ve we use individual global variables of the form env Ve. Accordingly, the set Aa of generic actions is now t Aloc t Asyn. Additional global variables x, which we now denote by glob for readability, are needed for book-keeping (that is, to model any required low-level detail in the PMAS that is needed to encode its execution, such as ﬂags, counters, turn indicators, etc). The global variable Phase, discussed later, is an example of such variables.

Deﬁnition 7. Given a PMAS M := {T1, . . . , Tn}, Te, R and a set of initial states, its AB-PMAS is a tuple:

Σ, {SIDt}t [1,n], glob, {arr Vt}t [1,n], {arr At}t [1,n], ι, τ

where: (i) Σ := S, R, C , where S are sorts (including sorts SAloc t and SAsyn), R are the relation symbols of M and C a set of constants (including all values valt(l, v) for every t, l, v); (ii) {SIDt}t [1,n] is a set of sorts of indexes type, one for each IDt. (iii) glob is a set of individual variables used to encode the local state of the environment plus any book-keeping info (see later); (iv) {arr Vt}t [1,n] is a set of sets of arrays, one for each variable in Vt of each Tt, whose elements range over θ for θ = type(v); (v) {arr At}t [1,n] is a set of arrays, one for each Tt, whose codomain has type SAloc t or SAsyn; (vi) ι is an initial formula, with individual variables glob and array variables arr Vt, arr At; (vii) τ is a disjunction of transition formulae, with individual variables glob, glob , and array variables arr Vt, arr At, arr Vt, arr At. A model of an AB-PMAS is a FO interpretation of Σ accounting for the elements domain, equipped with an assignment of the individual variables to elements of that interpretation; the action sorts SAloc t and SAsyn are resp. interpreted over sets Aloc t and Asyn; the index sorts {SIDt}t [1,n] are interpreted over the disjoint sets of concrete agents IDs IDt, for every t [1, n]. Array variables are assigned to functions from these sets of IDs to the elements domain. Next, we ﬁnally encode a PMAS into an AB-PMAS, which constitutes our ﬁrst main contribution. As shown in Fig. 1, for each t [1, n] there are kt arrays for local variables {v t 1, , v t kt} = Vt plus one array storing the current chosen action (in Asyn Aloc t or nop as default value). The environment is modeled with global variables: there is one global variable for each template variable and one action variable storing the current synchronization action in Asyn (or nop). The initial formula is trivial to write (it has the very same shape given before). The formula τ in Def. 7 is the disjunction of transition formulae ˆτ, shown next.

Encoding interleaved PMAS as ABSs In this section we present the ABS formulae that are needed for capturing the execution semantics of our interleaved PMASs. These formulae can be directly implemented into MCMT, a inﬁnite-state model checker that can verify ABSs: the encoding into MCMT input ﬁles matches exactly the reduction from PMASs to AB-PMAS described here. Each global transition of the PMAS is encoded as a sequence of steps of the AB-PMAS, each speciﬁed by a disjunction of transition formulae, ordered by means of an additional global variable Phase used to guide the progression. This is intuitively shown in Figure 1 (Below). The variables in each agent template are encoded by array variables, so that the value of each v for an agent with ID j can be written in the position j of that array arrv (the length and content of arrays is unbounded). An additional array arr At, one for each template Tt, stores the action currently declared" by agents. So the local state l of a concrete agent j, l t is encoded by the values written for index j in the arrays for template Tt (e.g., the red area in Figure 1). The environment variables

arrv 1 1 arrv 1 k1 arr A1

envv1 envvkeenvact

Figure 1: Above, a depiction of the encoding of an agent template T1 and of the environment template Te. Below, the phases used to capture the execution of an AB-PMAS.

are instead encoded via global variables, because only one concrete environment exists. In the same ﬁgure (Below), we show the how transition formulae of the ABS are used to encode the execution semantics of interleaved PMASs. Nodes correspond to phases and edges to (disjunctions of) transition formulae. There are two kinds of progressions, corresponding to the two semantics in Def. 3: either some nonempty subset of concrete agents execute local actions on their local state (upper branch) or a synchronization action is performed by the environment and at least one concrete agent (lower branch). The former case is realized by a nonempty sequence of steps following formula (1), in which local actions are written ( declared ) in the appropriate position j of array arr At for some t, followed by a single step in which the local state of all concrete agents that declared an action is updated in bulk (by applying the function in the λ-abstraction) as in (2). As transitions (ˆτ formulae) are taken nondeterministically, this will capture all possible sequences of (1)-steps followed by a (2)-step. The latter case is analogous: the formula in (3) makes sure that the environment and at least one concrete agent with ID j and type t can execute a synchronization action, which is then written in a global variable envact as well as in the array position arr At[j]. Then, a number of concrete agents can declare the same action, updating their action array as speciﬁed by (4). Nondeterministically, a bulk update is performed as in formula (5), which also updates the environment. In both cases, when the initial phase is reached again, the action arrays arr At of each template Tt are reset to contain nop values. As a result a possible evolution of an AB-PMAS template corresponds to a possible path in this intuitive diagram. We now list the transition formulae, numbered as in Figure 1 (Below). For encoding the ﬁrst step of the upper branch we use a disjunction of transition formulae as (1) below, for each t {1, . . . , n, e} and local action α Aloc t : Phase = 0 Phase = L

arr At[jself] = nop Pt(α) Phase := L arr At[jself] := α

where a disjunction is used for compactness: we can write this as two distinct formulae. Here, as in the rest of the paper, when a primed array variable a does not appear explicitly, the current content of a is propagated, as is, to the next state. Remark 2. Above we denoted by Pt(α) the transformation of the (quantiﬁer-free) agent formula Pt(α) =

ψ(j, self, e, v) into a (quantiﬁer-free) formula φ(j, x, a) for AB-PMASs, with the same syntactic shape of state formulae. This is required because agent formulae, e.g., make use of local template variables, whereas array-based formulae make use of individual and array variables. Such transformation is trivial and it is not formalized further: we simply need to replace the variables of sort ID in ϕ with index variables from the sort used for agents in the AB-PMAS. As a special case, we impose that self is always replaced with a special index jself that is existentially quantiﬁed in (1): there must exist an agent with index jself and template Tt that we can take as self to evaluate Pt(α). If other index variables j are present, these are existentially quantiﬁed as well. The step above is repeated an unbounded number of times (see the loop on state L in Fig. 1), as long as a new index jself exists. Then, nondeterministically, a further step can be executed, characterized by the transition formula below. Here, as in the remainder of the section, we write arr Vt[j] = l as a shorthand to denote that, for each variable v Vt for some t {1, . . . , n, e}, arrv[j] = val(l, v), namely the set of arrays arr Vt[j] for the concrete agent with ID j of type t encode the local state l Lt (see Fig. 1, in red). The same for arr Vt := λj. case of {. . . , κi : val(l, v), . . . }. In this formula, we perform a bulk update of all instances (indexes j) by applying the transition function of each Tt (below, one case is listed for each couple of local state-action):

Phase = L Phase := 0 V

t {1,...,n,e} arr At := λj. nop

t {1,...,n,e} arr Vt:=λj.

arr Vt[j]=l1 arr At[j]=α1 : δt(l1, α1)

arr Vt[j]=lm arr At[j]=αk : δt(lm, αk)

(2) Above, for each j one possible case applies. E.g., if α1 was declared and the state is l1, then arr Vt[j] = δt(l1, α1). For synchronization actions, for each α Asyn and template Tt we have the following formula, making sure that at least one concrete agent and the environment can perform the same action, then written in the global variable envact:

Phase=0 jself

arr At[jself] = nop envact = nop

Pt(α) Pe(α) arr At[jself]:=α env act:=α Phase :=S

(3) Then two possibilities exist: either an unbounded number of agents participate in the synchronization (via (4)), or the bulk progression is performed by applying the formula (5) further below. Again, this is encoded as a disjunction of formulae. For each t [1, n] and α Asyn:

Phase = S jself

envact = α Pt(α) arr At[jself] = nop Phase :=S arr At[jself]:=α

(4) Phase = S envact = α env Ve = le env Ve := δe(le, α) env act := nop arr At := λj. nop Phase := 0

t [1,n] arr Vt := λj.

arr Vt[j] = l1 arr At[j] = α : δt(l1, α)

arr Vt[j] = lm arr At[j] = α : δt(lm, α)}

Veriﬁcation

We denote by ab(M) the AB-PMAS obtained by encoding a PMAS M as in the previous section. An unsafety formula for ab(M) is a state formula φ of the form j.φ(j, x, a). These formulae are used to characterize undesired states of ab(M). By adopting a customary terminology for array-based systems, we say that ab(M) is safe with respect to φ if intuitively the system has no ﬁnite run leading from ι to φ. Formally, this means that there is no interpretation I0 of relations, no k 0 and no possible assignment to the individual and array variables x0, a0, . . . , xk, ak such that the formula

ι(x0, a0) τ(x0, a0, x1, a1) τ(xk 1, ak 1, xk, ak) φ(xk, ak)

is valid in any model of ab(M). The safety problem for ab(M) is the following: Given an unsafety formula φ as before, decide whether ab(M) is safe with respect to φ. It is immediate to see that this matches Def. 4: the AB-PMAS cannot be safe w.r.t φ if there exists an initial interpretation I0 so that a global state g with g |=I0 ψ, where ψ is an agent formula with ψ = φ, is reachable through a run ρ, I0 , and vice-versa (recall the description of in Remark 2).

Proposition 1. An agent formula ψgoal is reachable in a PMAS M iff the AB-PMAS ab(M) is unsafe w.r.t. ψgoal.

Soundness, Completeness, Termination

The algorithm described in Fig. 1 shows the SMT-based backward reachability procedure (or, backward search) for handling the safety problem for an AB-PMAS ab(M). An integral part of the algorithm is to compute symbolic preimages. For that purpose, for any τ(z, z ) and φ(z) (where z are renamed copies of z), we deﬁne Pre(τ, φ) as the formula z (τ(z, z ) φ(z )). The preimage of the set of states described by a state formula φ(x) is the set of states described by Pre(τ, φ) (notice that, when τ = W ˆτ, then Pre(τ, φ) = W Pre(ˆτ, φ)). Backward search computes iterated preimages of an unsafety formula φ, until a ﬁxpoint is reached (in that case, ab(M) is safe w.r.t. φ) or until a set intersecting the initial states (i.e., satisfying ι) is found (in that case, ab(M) is unsafe w.r.t. φ) . Inclusion (Line 2) and disjointness (Line 3) tests can be discharged via proof obligations to be handled by SMT solvers. The ﬁxpoint is reached when the test in Line 2 returns unsat: the preimage of the set of the current states is included in the set of states reached by the backward search so far (represented as the iterated application of preimages to the unsafety formula φ). The test at Line 3 is satisﬁable when the states visited so far by the backward search includes a possible initial state (i.e., a state satisfying ι). If this is the case, then ab(M) is unsafe w.r.t. φ. We call PMAS-Backward search the procedure that takes as input a PMAS M and a goal formula ψgoal, transforms them into its corresponding array-based system ab(M) and into ψgoal resp., and then applies the backward search BReach(ab(M), ψgoal). This procedure either does not terminate or returns a SAFE/UNSAFE result. Given a PMAS M and an agent formula ψgoal, a SAFE (resp. UNSAFE) result is correct iff M is safe (resp. unsafe) w.r.t. ψgoal.

Algorithm 1: backward search BReach(ab(M), φ)

2 while φ B is satisﬁable do

3 if (ι φ is satisﬁable) then return UNSAFE;

5 φ Pre(τ, φ); // τ is as in Def. 7

6 return SAFE;

Theorem 1. PMAS-Backward search for the reachability problem for interleaved PMASs is so that, (i) when it terminates, it returns a correct result, and (ii) whenever UNSAFE is the correct result, then UNSAFE is indeed returned.

Proof Sketch. Thanks to Proposition 1, establishing reachability of ψgoal in M is equivalent to establishing the unsafety of ab(M) w.r.t. ψgoal: hence, we can focus on the latter. For both (i) and (ii) we need to prove, by taking inspiration from (Ghilardi and Ranise 2010a; Calvanese et al. 2019b), that every step in Alg. 1 can be effectively executed: for doing so, we need suitable decision procedures for the satisﬁability tests at Lines 2-3. First, in order to guarantee the regressability of the procedure, the fact that φ is a state formula needs to be a loop invariant: this is obtained by showing that the pre-image of a state formula can be converted to a state formula. Then, to perform the tests at Lines 2-3, we can show that entailment between state formulae can be decided via ﬁnite instantiation techniques: this is possible thanks to the speciﬁc shape of these formulae (which are called -formulae in (Felli, Gianola, and Montali 2020c)). For (ii), we conclude the proof by noticing that ﬁnite unsafe traces are found after ﬁnitely many steps. The full proof is reported in (Felli, Gianola, and Montali 2020c).

Backward search for interleaved AB-PMAS is thus a semi-decision procedure for checking that a PMASs is unsafe. However, there is no guarantee of termination because the pre-image computation can diverge on a safe AB-PMAS. We show under which (sufﬁcient) condition we can guarantee termination of the backward search, which will gives us a decision procedure for unsafety. Although technical proofs are quite involved at the syntactic level, they can be intuitively understood as based on this locality condition: the states visited by the backward search can be represented by state formulae which do not include direct/indirect comparisons and joins" of distinct state variables for different agent IDs. E.g., we cannot use direct comparisons of the form (v [j1] 1 = v [j2] 2 ), i.e., comparing template variables for agent IDs j1 = j2. Similarly, we cannot (indirectly) correlate v [j1] 1 and v [j2] 2 by writing R(v [j1] 1 , v [j2] 2 ) for some relation R. We can however write v [j1] 1 = k, v [j2] 2 = k for a constant k. Of course, if this property is true for φ, it does not necessary hold for the formula obtained by regressing" φ w.r.t. some transition formula ˆτ, i.e., Pre(ˆτ, φ): ˆτ includes translations Pt(α) of template protocols Pt(α) for action α. Formally, we call a state formula local if it is a disjunction of

the formulae of the form:

j1 jm (Eq(j1, . . . , jm)

k=1 φk(jk, x, a)) (6)

Here, Eq is a conjunction of variable (dis)equalities, φk are quantiﬁer-free formulae, and j1, . . . , jm are individual variables of index sort. Moving all the existential quantiﬁers externally, it is easy to see that a local state formula is a state formula. Note how each φk in (6) can contain only the existentially quantiﬁed index variable jk. As said before, this limitation has an impact on transition formulae as well: we say that a transition formula ˆτ is local if whenever a formula φ is local, so is Pre(ˆτ, φ).

Theorem 2. BReach(ab(M), ψgoal) always terminates for an interleaved AB-PMAS if its transition formula τ = W ˆτ is a disjunction of local transition formulae and ψgoal is local.

Proof Sketch. Although involved, the proof relies on the use of a suitable well-quasi-order (wqo) deﬁnable thanks to locality. After introducing the algebraic notion of cyclic FO structure (see (Felli, Gianola, and Montali 2020c) for the formal deﬁnition), one can notice that, since our language is relational, there are only ﬁnitely many cyclic FO structures that can be built. The particular format of local formulae implies that it is sufﬁcient to check the validity of a local formula in cyclic structures in order to know if a local formula holds in a generic model of AB-PMASs. This allows us to introduce a speciﬁc wqo based on counting how many copies of cyclic FO-structures every model of AB-PMASs contains. We can show that a non-terminating backward search would destroy the well-foundedness of this wqo. The full proof is in (Felli, Gianola, and Montali 2020c).

Theorem 2 (with Thm. 1) gives a sufﬁcient condition for termination, inspired to a condition well-known in the literature of veriﬁcation of data-aware processes (Calvanese et al. 2020). There, an analogous result holds, and decidability in the general case is still unknown. Our model of PMASs does not require the restriction imposed by locality, and indeed we proved only soundness and completeness of backward search (Thm. 1), making it a semi-decision procedure for checking unsafety. This is consistent with our focus, which is not on decidability, but on the effectiveness of employing the backward reachability procedure. Nevertheless, when locality is imposed, Thm. 2 proves that backward search, thanks to termination, becomes a full decision procedure. In particular, when relations and agent state variables comparisons are disregarded, locality (thus decidability) is always guaranteed: this in line with the models/results in (Emerson and Kahlon 2000, 2003; Emerson and Namjoshi 1996) when only reachability is considered. The structure of the proof of the theorem follows the schema of that of Thm. 5.4 in (Calvanese et al. 2020), with a signiﬁcant difference: decidability is there based on locality and applies to ABSs whose FO-signatures do not have relational symbols, while ABSs have free relational symbols. It is immediate to verify that the transition formulae and goal formula ψgoal for our running scenario are both lo-

cal, hence checking safety is decidable. The PMAS can be proved to be unsafe w.r.t. ψgoal as in Example 2.

Implementation

In this section, we illustrate our implementation approach and the tool called SAFE, which makes available the thirdparty model checker MCMT (Ghilardi and Ranise 2010b) for checking the safety of PMASs. A thorough description of SAFE and of its use in connection with MCMT for the safety checking of PMASs is presented in (Felli, Gianola, and Montali 2020b): we report here a brief discussion on this implementation in order to show the feasibility of our theoretical approach, and what follows is not intended either as a proper tool description or as an experimental validation. MCTM is a symbolic model checker for safety properties of inﬁnite-state systems, based on backward reachability and ﬁxpoints computations (computed relying on an SMT solver): every ABS can be processed by MCMT (with the correct syntax). By using this tool-chain, the user is able to (i) model a PMAS M in a concrete syntax using SAFE, (ii) generate its encoding into MCMT (this encoding follows exactly the formalization presented in this paper) (iii) check the safety of M w.r.t. a given agent formula via MCMT (which also provides a witness in case of an unsafe verdict). For lack of space, in this paper we do not describe the MCMT input ﬁles, as these are only used as the internal representation in our implementation. Instead, we brieﬂy describe SAFE (Felli, Gianola, and Montali 2020a), i.e., our implementation of a user interface allowing to use in practice the results presented in this paper. SAFE automatizes the textual encoding of the PMAS into MCMT input ﬁles, by relying on a MAS-oriented modeling approach. This allows the user to focus on modeling the PMAS, i.e., the agent and environment templates, without worrying about how their constructs can be encoded for MCMT. The tool also allows to convert the witnesses for unsafety that MCMT returns (for unsafe ABSs) back into executions of the original PMAS. SAFE Agent templates. In its present version, the representation of agent and environment templates used by SAFE differs slightly from the one used here, although it is equivalent. Instead of an explicit state-transition representation as in Def. 1, SAFE assumes a more succinct representation, namely a STRIPS-like approach where actions are speciﬁed by means of preand postconditions. Execution of SAFE-MCMT. We run here our tool-chain over the example. As the PMAS is unsafe, this allows us to comment in practice on how a witness of unsafety is returned by MCMT. More examples (including safe ones) are available through the GUI of SAFE (Felli, Gianola, and Montali 2020a) and in (Felli, Gianola, and Montali 2020b), and they are all reproducible running SAFE and then MCMT. The textual encoding of the ABS corresponding to the PMAS in the running example is solved by MCMT v.3.0, on a machine with Ubuntu 18.04, 3.60 GHz Intel Core i7-7700 CPU, in 2 minutes and 22 seconds and in 56 seconds respectively using Yices (version 1.0.40) and Z3 (version 4.8.9.0) as background SMT solvers. MCMT correctly

reports that the system is unsafe.1 The generated input ﬁle ( download MCMT input") contains 501 lines of code and has 3 local variables for Tatt, 4 global variables and 15 transitions formulae. MCMT returns this witness for unsafety: [t1_3][t2_2][t2_1][t3][t5_2][t9_1][t13][t6_3][t14] [t4_2][t8_1][t12][t7_2][t15], where each tn_m represents the execution of the n-th transition in the input ﬁle, in the order in which they appear, with m instantiated index variables. In this case, this is sequence of actions go A,go A,go A,go B,go B,off,go C,go C,pulse, where each action is executed by one agent (and/or by the environment).

Conclusion and Future Work We have presented a model of PMASs, deﬁned the veriﬁcation task of checking safety, and provided a custom, MASoriented tool that allows to make use of a generic SMTmodel checker off-the-shelf. Our tool supports a concrete syntax for PMASs, and automatically encodes it into the input format accepted by the MCTM model checker for ABSs. The generality of our approach allows in principle any tool accepting ABS inputs to be used, e.g. Cubicle (Conchon et al. 2012). Cubicle, however, crucially does not support data-aware veriﬁcation, like relations with primary and foreign keys: MCMT, instead, will allow us to exploit these features when, as commented below, data-aware extensions of PMASs are considered. To the best of our knowledge, this is the ﬁrst paper that establishes a theoretical connection between the veriﬁcation of PMASs and SMT-based model checking for ABSs, opening up the possibility of solving the former via advanced techniques and tools for the latter. This allows a number of interesting extensions. From the foundational perspective, data-aware extensions of our framework can be directly incorporated, along the line studied in (Calvanese et al. 2020). This supports ﬁnite action signatures with inﬁnite number of possible parameter values, and also to store and inspect inﬁnite data values. For instance, this will allow us to model and check for safety extended models of PMASs where agents are given read and write access to private and public databases, hence allowing us to model complex systems in which data is stored and exchanged. Also, the background theories employed by the SMT-solver in this paper are only the empty theory or EUF, whereas further ones may be considered. Adding data extensions, theories, possibly arithmetics and cardinality constraints, are all future directions. From the applied perspective, the SMT technology brings effective techniques for symbolic reasoning, like decision procedures for combined theories or quantiﬁer handling through instantiation and quantiﬁer elimination. At the same time, it features advanced heuristics and approximation techniques, like acceleration, predicate abstraction and invariant synthesis. This triggers a natural extension of our implementation, tailored for efﬁciency. In fact, it is well-known that the performance of symbolic veriﬁcation techniques can be substantially improved when such techniques are suitably developed for the domain at hand (Conchon et al. 2013).

1The example, modeled with SAFE, is publicly available at the address: http://safeswarms.club/page/mcmt/rooms

Acknowledgements This work was supported by the Unibz projects SMARTEST, VERBA and REKAP.

References Abdulla, P. A.; Cerans, K.; Jonsson, B.; and Tsay, Y.-K. 1996. General decidability theorems for inﬁnite-state systems. In Proc. of LICS, 313 321. IEEE. Alberti, F.; Ghilardi, S.; and Sharygina, N. 2017. A Framework for the Veriﬁcation of Parameterized Inﬁnite-state Systems. Fund. Inform. 150(1): 1 24. Alechina, N.; Brázdil, T.; De Giacomo, G.; Felli, P.; Logan, B.; and Vardi, M. Y. 2019. Unbounded Orchestrations of Transducers for Manufacturing. In Proc. of AAAI, 2646 2653. Barrett, C. W.; and Tinelli, C. 2018. Satisﬁability Modulo Theories. In Handbook of Model Checking., 305 343. Belardinelli, F.; Kouvaros, P.; and Lomuscio, A. 2017. Parameterised Veriﬁcation of Data-aware Multi-Agent Systems. In Proc. of IJCAI, 98 104. Bloem, R.; Jacobs, S.; and Khalimov, A. 2015. Decidability of Parameterized Veriﬁcation. Morgan & Claypool Publishers. Bulling, N.; Goranko, V.; and Jamroga, W. 2015. Logics for Reasoning About Strategic Abilities in Multi-player Games. In Models of Strategic Reasoning - Logics, Games, and Communities, 93 136. Calvanese, D.; Ghilardi, S.; Gianola, A.; Montali, M.; and Rivkin, A. 2019a. Formal Modeling and SMT-Based Parameterized Veriﬁcation of Data-Aware BPMN. In Proc. of BPM, 157 175. Springer. Calvanese, D.; Ghilardi, S.; Gianola, A.; Montali, M.; and Rivkin, A. 2019b. From model completeness to veriﬁcation of data aware processes. In Description Logic, Theory Combination, and All That, 212 239. Springer. Calvanese, D.; Ghilardi, S.; Gianola, A.; Montali, M.; and Rivkin, A. 2019c. Model Completeness, Covers and Superposition. In Proc. of CADE, 142 160. Springer. Calvanese, D.; Ghilardi, S.; Gianola, A.; Montali, M.; and Rivkin, A. 2020. SMT-based Veriﬁcation of Data-Aware Processes: a Model-Theoretic Approach. Math. Struct. Comp. Sci. 30(3): 271 313. Clarke, E. M.; Henzinger, T. A.; Veith, H.; and Bloem, R., eds. 2018. Handbook of Model Checking. Springer. Conchon, S.; Goel, A.; Krstic, S.; Mebsout, A.; and Zaïdi, F. 2012. Cubicle: A Parallel SMT-Based Model Checker for Parameterized Systems - Tool Paper. In Proc. of CAV, LNCS, 718 724. Springer. Conchon, S.; Goel, A.; Krstic, S.; Mebsout, A.; and Zaïdi, F. 2013. Invariants for ﬁnite instances and beyond. In Proceedings of FMCAD, 61 68. IEEE. De Masellis, R.; and Goranko, V. 2020. Logic-based speciﬁcation and veriﬁcation of homogeneous dynamic multiagent systems. Auton. Agents Multi Agent Syst. 34(2): 34.

Emerson, E. A.; and Kahlon, V. 2000. Reducing Model Checking of the Many to the Few. In Proc. of CADE, 236 254. Springer. Emerson, E. A.; and Kahlon, V. 2003. Model Checking Guarded Protocols. In Proc. of LICS, 361 370. IEEE. Emerson, E. A.; and Namjoshi, K. S. 1996. Automatic Veriﬁcation of Parameterized Synchronous Systems (Extended Abstract). In Proc. of CADE, LNCS, 87 98. Springer. Emerson, E. A.; and Namjoshi, K. S. 2003. On Reasoning About Rings. International Journal of Foundations of Computer Science 14(4): 527 550. Esparza, J.; Ganty, P.; Leroux, J.; and Majumdar, R. 2017. Veriﬁcation of population protocols. Acta Inf. 54(2): 191 215. Felli, P.; Gianola, A.; and Montali, M. 2020a. SAFE: the Swarm Safety Detector. www.safeswarms.club. Accessed: 2020-12-15. Felli, P.; Gianola, A.; and Montali, M. 2020b. A SMTbased Implementation for Safety Checking of Parameterized Multi-Agent Systems. In Proc. of PRIMA, LNCS, 259 280. Springer. Felli, P.; Gianola, A.; and Montali, M. 2020c. SMT-based Safety Veriﬁcation of Parameterised Multi-Agent Systems. Technical Report ar Xiv:2008.04774, ar Xiv.org. Finkel, A.; and Schnoebelen, P. 2001. Well-structured transition systems everywhere! Theoretical Computer Science 256(1): 63 92. ISSN 0304-3975. Ghilardi, S.; Gianola, A.; Montali, M.; and Rivkin, A. 2020. Petri Nets with Parameterised Data: Modelling and Veriﬁcation. In Proc. of BPM, 55 74. Springer. Ghilardi, S.; Nicolini, E.; Ranise, S.; and Zucchelli, D. 2008. Towards SMT Model Checking of Array-Based Systems. In Proc. of IJCAR, 67 82. Ghilardi, S.; and Ranise, S. 2010a. Backward Reachability of Array-based Systems by SMT Solving: Termination and Invariant Synthesis. Log. Methods Comput. Sci. 6(4). Ghilardi, S.; and Ranise, S. 2010b. MCMT: A Model Checker Modulo Theories. In Proc. of IJCAR, 22 29. Springer. John, A.; Konnov, I.; Schmid, U.; Veith, H.; and Widder, J. 2012. Counter Attack on Byzantine Generals: Parameterized Model Checking of Fault-tolerant Distributed Algorithms. Technical Report ar Xiv:1210.3846, ar Xiv.org. Kouvaros, P.; and Lomuscio, A. 2016. Parameterised veriﬁcation for multi-agent systems. Artif. Intell. 234: 152 189. Kouvaros, P.; and Lomuscio, A. 2017. Parameterised Veriﬁcation of Inﬁnite State Multi-Agent Systems via Predicate Abstraction. In Proc. of AAAI, 3013 3020. Kouvaros, P.; Lomuscio, A.; Pirovano, E.; and Punchihewa, H. 2019. Formal Veriﬁcation of Open Multi-Agent Systems. In Proc. of AAMAS, 179 187. Pnueli, A.; Xu, J.; and Zuck, L. 2002. Liveness with (0,1, infty)- Counter Abstraction. In Proc. of CAV, 107 122. Springer.