key: cord-0045114-igg7vvym
authors: Di Stefano, Luca; Lang, Frédéric; Serwe, Wendelin
title: Combining SLiVER with CADP to Analyze Multi-agent Systems
date: 2020-05-13
journal: Coordination Models and Languages
DOI: 10.1007/978-3-030-50029-0_23
sha: d9f2958aa5f1dcc28f926c8917c4c3ccd29cd626
doc_id: 45114
cord_uid: igg7vvym

We present an automated workflow for the analysis of multi-agent systems described in a simple specification language. The procedure is based on a structural encoding of the input system and the property of interest into an LNT program, and relies on the CADP software toolbox to either verify the given property or simulate the encoded system. Counterexamples to properties under verification, as well as simulation traces, are translated into a syntax similar to that of the input language: therefore, no knowledge of CADP is required. The workflow is implemented as a module of the verification tool SLiVER. We present the input specification language, describe the analysis workflow, and show how to invoke SLiVER to verify or simulate two example systems. Then, we provide details on the LNT encoding and the verification procedure.

Multi-agent systems are composed of standalone computational units, the agents, that interact with each other and with an external environment. Computation within each agent may be a composition of multiple interleaving processes. The agents may also interleave their executions and interact with each other, possibly through asynchronous interaction patterns. As a consequence, multi-agent systems typically feature extremely large state spaces, which makes them hard to design and reason about.

Therefore, there is a need for languages that allow to specify these systems in a concise and intuitive fashion, as well as tools that can certify or increase confidence in the correctness of such specifications. This need is felt far beyond the multi-agent community, as agent-based models are gaining popularity in economics [13, 29] , social sciences [3, 4] , and many other research fields. However, the development of tools for such new languages may be a daunting task, as it Work partially funded by MIUR project PRIN 2017FTXR7S IT MATTERS (Methods and Tools for Trustworthy Smart Systems). must keep pace with both the evolution of the language and the state of the art in formal analysis of systems.

An alternative solution is to encode a system specification into an existing language, and reuse mature tools for that language to analyze the encoded system. An example of this approach is given by SLiVER, a prototype tool for the automated verification of multi-agent systems that are described in the simple specification language LAbS [10] . 1 The tool is highly modular: it exploits the formal semantics of LAbS to encode the input system into an emulation program in a given language, through a structural translation procedure, and verifies the emulation program with off-the-shelf tools for that language to reach a verdict on the correctness of the input system. Previously [10] , SLiVER only generated sequential C programs and verified them through bounded model checking [5] , by using tools such as 2LS [8] , CBMC [9] , and ESBMC [14] as back ends.

In this paper, instead, we present a new analysis workflow based on processalgebraic tools. Namely, we choose the process calculus LNT [17] as the target language, and CADP [16] as the back end analysis tool. 2 The workflow is implemented as a SLiVER module and can verify both invariance properties (i.e., all reachable states satisfy a given formula) and inevitable reachability ones (i.e., all executions lead to a state where the given formula is satisfied), over the full state space of the input system. Furthermore, we can use the same workflow to simulate the evolution of the system and return a set of execution traces. This is the first SLiVER module that supports simulation. These two approaches may complement each other: even though simulation can rarely lead to strong conclusions about the correctness of a system [31] , it is a valuable design aid and can provide quick feedback even on very large systems.

The rest of the paper is organized as follows. Section 2 briefly describes the specification language LAbS supported by SLiVER through an example, and contains an overview of LNT and CADP. Section 3 introduces the analysis workflow and its implementation as a SLiVER module, and provides usage examples. In Sect. 4 we describe in further detail how the tool generates emulation programs, and in Sect. 5 we explain how it performs property verification through model checking of such programs. Finally, we discuss related work in Sect. 6 and provide concluding remarks in Sect. 7.

System Specifications. LAbS [10] is a domain-specific language to describe the behavior of agents in a multi-agent system. A behavior is made of basic actions, which tell the agent to assign a value to a variable. There are three kinds of assignments: to an internal variable, denoted by x ← E (where x is a variable identifier and E a value expression); to a shared variable, denoted by x E; and to a stigmergic variable, denoted by x E. Stigmergic variables are a distinguishing feature of LAbS. Their value is bound to a timestamp and stored on a decentralized data structure, allowing agents to share their knowledge with the rest of the system by exchanging asynchronous messages [26] . In brief, agents send propagation messages after updating a stigmergic variable. A propagation message contains the name of this variable, its new value, and its associated timestamp. An agent that receives a message checks whether its timestamp is newer than the local one for the same variable. If this is the case, the local value and timestamp are overwritten by the received ones; furthermore, the receiver will in turn propagate this new value to others. Otherwise, the message is simply discarded. Agents also send confirmation messages after reading the value of a stigmergic variable (i.e., by using it as part of a value expression). The contents of a confirmation message are the same as those of a propagation message. However, a receiver of a confirmation message that stores a value with a higher timestamp will react by propagating its own value. This mechanism facilitates the spread of up-to-date values through the system.

A single action may specify multiple assignments to variables of the same kind: for instance, an assignment to multiple internal variables is denoted by x 1 , . . . , x n ← E 1 , . . . , E n . Multiple assignments to variables of different kinds (e.g., an internal one and a shared one) are not allowed. Actions may be composed with traditional process-algebraic operators: sequential composition (;), nondeterministic choice (+), interleaving (|), and calls to other behaviors (possibly including recursive calls). Furthermore, a behavior B may be guarded by a condition g (denoted as g → B), meaning that the agent may start behaving as B only if g holds.

SLiVER takes as input a system specification in a machine-readable version of LAbS, which is extended with constructs to specify the property of interest and the initial state of the system through (possibly nondeterministic) variable initialization expressions. Furthermore, the input format allows to parameterize systems in one or more external variables. Figure 1a shows an example specification describing the well-known dining philosophers scenario. The system is parameterized in the number n of agents (line 2), and features an array forks, which is shared by all the agents and whose elements are all initialized to 0 (line 3: the set of shared variables within a system is called its environment). Each element of the array models a fork: a value 0 means that the fork is available, while a value 1 means that it is currently held by one of the agents. The (recursive) behavior of the agents is specified at lines 10-21. Each agent repeatedly tries to acquire two forks, by checking and updating the elements id and (id+1)% n of the array forks. The special variable id has a different value for each agent, and % denotes the modulo operator. After acquiring both forks, the agent releases them and starts over. Each agent maintains an internal variable status, initially set to 0, which describes its current situation (line 8: the set of internal variables of an agent is called its interface). When status is set to either 0, 1, or 2, it denotes the number of forks currently held by the agent. When status is set to 3, it means that the agent has just released one fork and is going to release the other one during its next action. Lastly, invariant NoDeadlock (lines 25-27) states that the system should never reach a state where all agents are waiting for the second fork. Figure 1b contains a simple leader election system, which we will use to illustrate stigmergic variables. Lines 6-9 define a stigmergy Election containing a single variable leader. The link predicate is, in general, a Boolean expression over the state of two agents: an agent may only send a stigmergic message to another one if they satisfy this predicate. In this case, the predicate is simply true, so any two agents may communicate at any time. The stigmergic variable leader is initially set to the value of external parameter n. The definition of Node agents states that they can access the Election stigmergy (line 12). Their behavior (lines 13-16) simply tells them to repeatedly update the variable leader to their own id as long as it contains a greater value. Finally, property LeaderIs0 (lines 20-22) specifies that the system should eventually reach a state where all Node agents agree on a value of 0 for variable leader.

Supported Properties. SLiVER currently supports invariants and inevitable reachability properties. A property is expressed by a modality keyword (always for invariants, eventually for inevitability properties), followed by a predicate over the state of agents. The predicate may contain existential (exists) or universal (forall) quantifiers. Alternation of existential and universal quantifiers in the same property is not supported yet.

LNT and CADP. LNT is a formally defined language for the description of asynchronous concurrent systems [17] . A system is modeled as a process, generally composed of several, possibly concurrent processes, which may perform communication actions on gates and exchange information by multiway (value-passing) rendezvous, in the style of the Theoretical CSP [19] and LOTOS [20] process algebras. The syntax of LNT is inspired from both imperative languages (assignments, sequential composition, loops) and functional languages (pattern matching, recursion), with many static checks, such as binding, typing, and dataflow analysis ensuring the proper definition of variables and function results.

CADP [16] is a software toolbox for the analysis of asynchronous concurrent systems, in particular systems described in LNT. It contains a wide range of tools for simulation, test generation, verification (model checking and equivalence checking), performance evaluation, etc. We briefly describe two CADP tools named Evaluator and Executor. Evaluator is a model checker that can evaluate properties expressed in the language MCL [25] , a temporal logic based on the modal μ-calculus [21] extended with regular action formulas and valuepassing constructs. 3 Executor, on the other hand, performs a bounded random exploration of the state space of a given program. Starting from the initial state, it repeatedly enumerates and then randomly chooses one of the transitions going out of the current state, until it has generated a sequence of the requested length. Explorations can be made reproducible by manually providing a seed for the internal pseudo-random number generator. 4

Workflow. The analysis workflow is shown in Fig. 2 . First, a front end parses the input file and substitutes external parameters with the values provided in the command line, to obtain a system specification S and a property of interest ϕ. After that, we perform a two-step encoding procedure. The first step is independent of the target language and builds a structural symbolic representation T of the behaviors of the agents within S. This representation is used in the second step to encode S and ϕ into an LNT program P. At this point, a wrapper invokes a specific program from the CADP toolbox, depending on the analysis task requested by the user. In verification mode, the tool invokes Evaluator to model-check P. If a counterexample is found, a translation module converts it to a LAbS-like syntax and shows it to the user; otherwise, the user is notified that ϕ holds in S. In simulation mode, instead, we call Executor to obtain one or more random traces of P. Each trace is then translated and shown to the user. Simulation traces will also display a message whenever an invariant is violated or an eventually property is satisfied. where specfile is the name of the input specification file. If the input system is parameterized, the user must provide a sequence params in the form param=val to assign a value to each parameter. Argument --backend cadp is needed to force SLiVER to use the CADP analysis module. As an example, if we invoke SLiVER on the system of Fig. 1a with the command sliver.py philosophers.labs n=5 --backend cadp we obtain the counterexample of Fig. 3a , disproving property NoDeadlock. By default, the tool assumes that there are no constraints on the interleaving of agents. However, in some cases it might be convenient to restrict the analysis to traces where interleaving is restricted according to some policy. Currently, SLiVER allows to enforce round-robin execution of agents through the optional --fair flag.

If the optional arguments --simulate <n> --steps <s> are omitted, the tool attempts to verify the input property on the given system. Otherwise, it returns n execution traces, each one containing at most s transitions. As an example, Fig. 3b contains part of a simulation trace for the leader election system of Fig. 1b , with three agents 5 . This trace shows the asynchronous nature of stigmergic messages. Notice that all stigmergic assignments within the trace show both the value and its attached timestamp. In the first steps, nodes 0 and 2 update leader to their respective ids. Then, node 0 sends a confirmation message for leader. It does so because it had to compute the guard leader > id. Node 1 picks up the message and updates its value of leader accordingly (lines 8-10). On the other hand, node 2 ignores the message, since its own value of leader has a higher timestamp. After a sequence of messaging rounds, during which node 0 sets leader to 2 (line 16), the same node updates yet again leader to 0 (line 21). Then, a propagation messages from node 0 forces the other nodes to accept that value for leader, and property LeaderIs0 becomes satisfied (line 26).

The tool supports other flags, not shown above. If an invocation is enriched with --verbose, SLiVER will print the full output from the back end. The --debug flag enables the output of additional messages for diagnostic purposes. Finally, the --show flag forces SLiVER to print the emulation program and quit without performing any analysis.

In this section we describe how we encode a LAbS system S and a property ϕ into an LNT emulation program P by using the intermediate representation T.

We illustrate our description with simplified excerpts of LNT code generated from the tool. 6 Intermediate Representation. The intermediate representation of an agent behavior B contains one record for each basic action within B. Each record is decorated with an entry condition and an exit condition. An entry condition is a predicate over a set of symbolic variables, which we call the program counter of the agent. Intuitively, the program counter tracks the actions which the agent can perform at any given time. An exit condition, on the other hand, is a (possibly nondeterministic) assignment to the program counter. Exit conditions are constructed so as to preserve the control-flow of B. We use multiple variables for the program counter to compactly represent parallel compositions of LAbS processes within a single behavior.

Program Stub. Once the intermediate representation T is obtained, the generation of the emulation program P starts from a stub, containing a type definition Sys that encodes the full state of S. A system is composed of a collection of agents, an environment env, and a global clock time (Listing 1, lines 1-3). The latter is needed to model the semantics of stigmergic variables. Throughout Listing 1, the with "get", "set" construct implements standard functions for accessing and updating elements (for array types) or fields (for record types). The LNT type Agent models a LAbS agent: each agent has an identifier id, a program counter pc, two stores I and L respectively used for local and stigmergic variables, two stores Zprop and Zconf to keep track of pending propagation and confirmation messages, and an init field that tracks whether the agent has been initialized (lines 4-8). Agents, Env, PC, Iface, Lstig, and Pending are all implemented as arrays (lines [10] [11] [12] .

Their sizes are determined by SLiVER through static analysis of the input specifications. #spawn is the total number of agents within the system, as specified in the spawn section (e.g., at line 4 in Fig. 1a) . #I, #L, and #E respectively denote the number of internal, stigmergic, and shared variables within the behavioral specifications. #P is the number of program counter variables, which is computed during the construction of T. Finally, type ID is a natural number strictly less than the number of agents in the system (line 16). The stub also contains LNT functions and processes that implement the semantics of LAbS, and thus never change (see Sect. 4.1 for an example of such a process). Notice that SLiVER is able to alter this stub according to the features of S. For instance, if the system does not feature any stigmergic variables, the emulation program will not contain Lstig, Pending, nor the functions that implement stigmergic messaging, and the Sys type will not have a time field.

Emulation Functions. We populate the stub by encoding each record within T as a separate LNT process. We call these processes emulation functions. An emulation function for a given record alters the state of the system according to the semantic rule of its action, and then updates the program counter of the selected agent according to its exit condition. The main section of the program (Listing 3) implements a scheduler, that repeatedly selects an agent and calls an emulation function. Agent selection happens by assigning a value to a variable id. If the tool is invoked with the --fair flag, the variable is simply incremented modulo the number of agents; otherwise, a nondeterministic assignment is performed (lines 34-37). Listing 4 shows the LNT process implementing an iteration of the scheduler. Notice that an emulation function may only be called if the program counter of the selected agent satisfies its corresponding entry condition (see e.g. lines 48-50). This prevents spurious executions. At each iteration, instead of calling an emulation function, the scheduler may call one of several system functions implementing other semantic rules of the language, e.g., communication between agents (line 39).

Listing 2: An emulation function.

Listing 3: Main section of P.

Property Instrumentation. The generated program is then instrumented for the verification of ϕ. First, we obtain a propositional formula ϕ from ϕ by quantifier elimination. Then, we add a monitor process to P, which is executed before each iteration of the scheduler (Line 23 of Listing 3). A stub of the monitor process is shown in Listing 5. If ϕ is an invariant and ϕ is violated, the monitor emits a false value over a gate m (line 63). On the other hand, if ϕ is an inevitable reachability property and ϕ holds, a true value will be emitted over m (line 68).

In any case, when the monitor emits a value, it also terminates P by means of a stop instruction, since there is no need to further explore the evolution of P. This instruction is only added to the program when in verification mode: in simulation mode, the program will keep running until it reaches either a deadlocked state or the user-provided bound.

Listing 4: A scheduler iteration. Listing 5: Property encoding.

Size of Emulation Programs. The behavior of multiple identical agents is only encoded once, by parameterizing all emulation functions in the id of the agent. Therefore, the number of lines of code in P scales well with the number of agents in the input system. To show that, we consider the systems of Fig. 1a -1b, as well as the boids and majority systems introduced in [10] . For each one, we build a 10-agent and a 100-agent emulation program, and compare their sizes. Table 1 shows the size of the input specification and of the two programs. Dining philosophers is the only system where the size of P increases, roughly by a factor of 1.5. This is due to initialization code for array forks, whose length depends on the number of agents. The other systems have a fixed-size state, and thus their encodings have the same size, regardless of the number of agents. The growth of the dining philosophers program may be avoided by improving the LNT code generator, e.g., by initializing LAbS arrays within a loop. We plan to implement improvements of this kind in a future release of SLiVER. Listing 6: Propagation of stigmergic variables in LNT.

Listing 6 contains an LNT process that implements LAbS propagation messages. This process may be called at each iteration of the scheduler of the emulation program (line 39 of Listing 3). A similar function, not shown here, implements confirmation messages.

The process first selects an agent with at least one pending message, i.e., with a non-empty Zprop field. The selection happens via a nondeterministic assignment of an agent identifier to a variable senderId (line 4). Once a suitable sender is found, an element of Zprop is nondeterministically selected and stored in the key variable (line 6). This value is the index of the stigmergic variable that will be propagated. The process then finds all potential receivers of the message: sender and receiver must be different agents, and they have to satisfy the link predicate for the stigmergic variable that is being sent (line 9).

If an agent satisfies all the above requirements, it can receive the message. Furthermore, if its own timestamp for key is less than the one of the sender (line 10), it will update its value and timestamp for key with the ones from the message (otherwise, it will just discard it). Notice that multiple stigmergic variables may actually be updated (lines [12] [13] [14] . This is because LAbS allows the user to put multiple stigmergic variables together in a tuple, and its semantics guarantee that variables within a tuple are always propagated together [10] . The loop in the LNT process enforces these guarantees. In lines 15-17, the state of the receiver is updated, and key is added to its set of pending propagation messages. Additionally, key is removed from its pending confirmation messages: intuitively, the agent needs no further confirmation for that variable, since it has just received a newer value. Finally, the value key is removed from the pending propagation messages of the sender (line 20).

Listing 7 contains all LNT emulation functions for the dining philosophers example. The name of each emulation function is constructed from its entry condition. For instance, function action 0 2 has entry condition pc[0] == 2. A comment within each process reports its corresponding LAbS action. Updates to local and shared variables are implemented through the attr and env processes, respectively. Notice how the assignments to the program counter at the end of each function preserve the control flow of the input specification.

In this section we explain how we determine whether a system S satisfies a property ϕ by model-checking the emulation program generated from (S, ϕ). We use the Evaluator tool to verify the values emitted by the monitor process (Listing 5). If ϕ is an invariant, we check that the program never emits a false value over m. This property is encoded as the MCL query Listing 7: Emulation functions for the dining philosopherssystem. When ϕ is an inevitability property, instead, we check that all fair executions [27] of P emit a value of true over m at some point. To do that, we use the following MCL query:

[ (not ("M !TRUE"))* ]<true * . "M !TRUE">true To trust that the outcome of the model checker is also a verdict on the original problem (namely, whether ϕ holds in S), we need to prove that intermediate representation T preserves all traces of each behavior in the system, and also that the emulation program P correctly interleaves these traces with calls to system functions, without introducing spurious executions. We cannot include a detailed proof for reasons of space, but this procedure adapts a previous structure-aware encoding [11] (which was tied to explicit-state model checking) to the semantics of LAbS, and makes it independent of the verification technique. Thus, our argument for correctness closely follows the one for that encoding.

There are several specialized tools for the formal analysis of multi-agent systems. MCMAS [24] verifies multi-agent systems of unbounded size with synchronous communication. Its language lacks value-passing actions, so it is not clear whether their technique could be applied to LAbS. AJPF [7] can perform explicit-state model-checking on a variety of agent-oriented languages. Differently from AJPF, SLiVER is modular with respect to the analysis back end, and may support explicit-state techniques as well as symbolic ones, such as SAT-based bounded model checking [10] . Peregrine [6] can verify and simulate population protocols, i.e. collections of identical mobile agents [2] . It can check that a population of unbounded size inevitably ends up satisfying a given predicate over its initial state. SLiVER cannot reason over unbounded-size systems, but it allows for the verification of invariants in addition to inevitable reachability properties.

The concept of verifying domain-specific languages by means of a structural translation into more amenable formalisms is not new. For instance, in [18] hardware specifications are translated into LOTOS and verified with CADP, while [11] shows a translation from an attribute-based process algebra [1] to UMC [30] .

We have presented an automated analysis workflow for multi-agent systems based on CADP and implemented as part of the SLiVER tool. Through an LNT encoding, the workflow allows to formally verify the input system via model checking, as well as generate random execution traces. The end user does not need to be familiar with either LNT or CADP: knowledge of the input language LAbS is the only requirement.

Future work may improve the presented workflow at several levels. We currently represent the whole system as a sequential LNT program: one might instead represent agents as parallel processes and apply compositional verification [15, 22, 23] to improve model checking performance. We could verify much more expressive properties than the current ones, by devising a translation into MCL queries with data variables [25] to be passed to the model checker. This would require an extension of the property language currently understood by the tool, as well as a correct encoding of this (state-based) language into MCL, which is action-based [12] . Finally, we could use the new trace generation capability to implement simulation-based analysis techniques, such as statistical model checking [28] .

A calculus for collective-adaptive systems and its behavioural theory

An introduction to population protocols

Population growth and collapse in a multiagent model of the Kayenta Anasazi in Long House Valley

Modeling the decline of labor-sharing in the semi-desert region of Chile

Symbolic model checking without BDDs

Peregrine: a tool for the analysis of population protocols

Automated verification of multi-agent programs

Synthesising interprocedural bit-precise termination proofs

A tool for checking ANSI-C programs

Multi-agent systems with virtual stigmergy

Verifying properties of systems relying on attribute-based communication

Action versus state based logics for transition systems

The economy needs agent-based modelling

ESBMC 5.0: an industrial-strength C model checker

Compositional verification of asynchronous concurrent systems using

CADP 2011: a toolbox for the construction and analysis of distributed processes

On the semantics of communicating hardware processes and their translation into LOTOS for the verification of asynchronous circuits with

Communicating Sequential Processes

LOTOS -A formal description technique based on the temporal ordering of observational behaviour

Results on the propositional µ-Calculus

Compositional verification of concurrent systems by combining bisimulations

Sharp congruences adequate with temporal logics combining weak and strong modalities

MCMAS: an open-source model checker for the verification of multi-agent systems

A model checking language for concurrent valuepassing systems

A tuple space for data sharing in robot swarms

Fairness and related properties in transition systems -a temporal logic to deal with fairness

Statistical model checking of black-box probabilistic systems

Heterogeneous interacting agent models for understanding monetary economies

A state/event-based modelchecking approach for the analysis of abstract system properties

Specification and Verification of Multi-Agent Systems