-We address the problem of decentralized runtime verification of interaction protocols in multiagent systems by means of MAS-DRiVe, an algorithm for partitioning a multiagent system (MAS) into sub-MASs which can be monitored independently. Given a global interaction protocol named AIP (for A“gent Interaction Protocol”) describing all the interactions which can take place in the MAS, the MAS-DRiVe algorithm extracts the interaction graph from AIP , identifies the clusters of agents which cannot be split during the decentralized monitoring as the interactions they are involved in are not independent, collapses each of those clusters into a single node in the interaction graph, and finally partitions the collapsed graph obtained so far. Although the “unsplittable agents identification” stage is still in its early design and prototyping phases and requires a better formalization and a deeper analysis, the MAS-DRiVe algorithm pipeline has been fully implemented and demonstrated on two simple MASs. Once the independently monitorable sub-MASs have been identified by MAS-DRiVe, the global interaction protocol AIP can be projected onto the subsets of agents belonging to each graph partition, thus obtaining local versions of AIP which can be monitored in a decentralized way.
Runtime verification (RV) is a software verification technique that complements formal static verification and testing.
In RV, dynamic checking of the correct behavior of a system is performed by a monitor which is generated from a formal specification of the properties to be verified.
Distributed runtime verification (DRV), as described by S.
Rajsbaum in his keynote speech at the SSS 2015 Symposium [25], tackles the problem of building a decentralized runtime monitor for a distributed system and involves designing a distributed algorithm that coordinates the monitors in order for them to correctly verify the dynamic behavior of the whole system.
With respect to RV, DRV techniques are more complex and less developed, since they involve designing a distributed algorithm that monitors another distributed algorithm. Nevertheless, they are gaining more and more attention, as shown by the recent Distributed Runtime Verification Workshop organized in Bertinoro in May 20161.
Once the formal specification of the global pattern of events is given, however, distributing the monitoring activity can be resorted to decomposing the global specification into “subspecifications”, involving less events than the global one, which can be monitored in an independent way from each other and such that the union of their independent monitoring gives the same guarantees as the monitoring of the whole system w.r.t. the original specification.
Given a global specification of the expected system behavior S, the challenge to face is then to compute a set of n subspecifications S1, . . . , Sn derived from S in such a way that the following properties hold: • decentralized monitoring against the sub-specifications
S1, . . . , Sn is equivalent to centralized monitoring against
S; • the decomposition of S into S1, . . . , Sn is balanced according to some weighting criterion, to get, ideally, the best monitoring performances.
These sub-specifications do not necessarily induce a partition of the monitored events: indeed, it might be necessary that some monitored events belong to more than one specification, and hence must be checked by more monitors. Let us suppose for example that the formal specification of the event pattern states that when the alarm rings, Mary stops it and either she wakes up, washes, has breakfast and goes to work (then the monitoring is allowed to stop), or she continues to sleep.
The events “wake up”, “wash”, “have breakfast”, “go to work” are independent from the event “sleep”, so a good way to decentralize the monitoring activity between two monitors m1 and m2 could be to have m1 in charge of the “active” behavior (m1 would check that “when the alarm rings, Mary stops it and then either she wakes up, washes, has breakfast, goes to work – then the monitoring can stop –, or the monitoring can stop immediately”) and m2 in charge of the lazy one (m2 would check that “when the alarm rings, Mary stops it and then either she continues to sleep, or the monitoring can stop immediately”).
It would be convenient that the events “the alarm rings” and “Mary stops it” were monitored by both m1 and m2, in order to avoid a further monitor ensuring the correct sequence of initial events, whatever Mary’s attitude towards the new day.
Due to events which may be monitored by more than one monitor, the total amount of monitored events in the decentralized setting may be larger than in the centralized case. However, decentralized monitors can be run in parallel on different machines, so the workload is more balanced than in the centralized setting. Also, sometimes a centralized approach is unfeasible, as in the motivating scenario discussed in our previous work presented at EMAS 2014 [2]. There, we of agents in a MAS which provide formal guarantees that supposed that the safety of a humanitarian convoy was guar- verification through projected types and decentralized monitors anteed by unmanned aerial vehicles whose behavior is critical is equivalent to verification performed by a single centralized for the success of the mission and hence subject to runtime monitor with a single global type. verification, but which might not be monitorable by a single This paper addresses that problem by presenting MASmonitor for network connectivity reasons and for failures of DRiVe, an algorithm for partitioning a MAS in such a way some computational entities. In cases like that, decentralizing that the identified subsystems can be safely monitored in the runtime verification activity is no longer an option, but a decentralized way. The paper is structured as follows: the only viable solution. The possibility to exchange protocol Section II discusses the related work, Section III introduces specifications, dealt with as first class entities that can be sent background knowledge, Section IV presents the design of and received [3], allows us to apply our approach to oppor- MAS-DRiVe, Section V discusses its implementation and tunistic networks (Wireless Sensor Networks, drone ferries, experiments, Section VI concludes. and the like) where the actual communication protocols are unknown until deployment, and mobility dynamically changes II. RELATED WORK them.
Finding a set of sub-specifications S1, . . . , Sn of S DRV lies at the crossroad where decentralized algorithms meeting the requirements for decentralizing the monitoring and formal methods meet [25]. It must cope both with the activity heavily depends on the way S has been specified. problems intrinsic to distributed systems, and with those RV specifications are typically expressed using trace predicate related to formalization of properties to be verified at runtime. formalisms. Many of them, such as finite state machines, reg- Furthermore, the distribution of the monitoring activity itself ular expressions, context free grammars, linear-time temporal poses new problems and raises new challenges. (LTL) logic, have been originally introduced for other aims One of the most severe and most studied problems which and then exploited for RV; others, such as trace expressions characterize decentralized systems is the lack of a global clock [6], have been expressly devised for RV. Different formalisms and the need to tag events with a timestamp which, although may have different expressive power, which impacts on the local to the node where the event took place or was observed, types of patterns that can be described and on the meaning of can be compared with the timestamps of the other events to “independent” sub-specifications. check their relative order. In this paper we assume that each
Although the MAS-DRiVe algorithm proposed in this paper monitor observes the events it is in charge of, in the same for decentralizing the monitoring activity is general enough to order as they actually took place in the environment. This be adopted whatever the formalism and the kind of monitored condition is enough for our approach to work. As mentioned events are, it has only been experimented for the specific in the introduction, some events may be observed by more formalism of trace expressions, for specific decentralized than one monitor so the condition we pose implicitly means systems, that is, multiagent systems (MASs), and for specific that event ordering is always preserved in all monitors. A large events, namely interactions between pairs of agents. Also, as body of literature addresses this problem; the two most widely we will see later on, the “unsplittable agents identification” is used approaches are to connect the different physical clocks almost naif and requires a refinement and a better theoretical of the decentralized nodes to one common logical clock, by support. exploiting causality in communication between nodes (Lam
Trace expressions are an evolution of global types [5], which ports “happened before” relation [22]), and to synchronize the have been initially proposed for RV of interactions in MASs. local clocks to provide a full ordering of events as proposed Trace expressions are an expressive formalism based on a set for example by M. Maro´ti et al. [23]. of operators (including prefixing, concatenation, shuffle, union, Formalizing the system properties in order to dynamically and intersection) to denote finite and infinite traces of events. verify them requires that a suitable formal language is availTheir semantics is based on a labeled transition system defined able. Among the first efforts in this direction we may cite one by a simple set of rewriting rules which directly drive the paper by A. Bauer, M. Leucker, and C. Schallhart [7] where behavior of monitors generated from them. They have been the use of LTL in the context of RV was explored. When used used to model and monitor (in a simulated setting) both fail- for RV, the expressive power of LTL is reduced, because at uncontrolled and ambient intelligence systems [4], as well as runtime only finite traces can be checked. To provide a formal medical guidelines for remote patient monitoring [16]. account for this limitation, a three-valued semantics for LTL,
In the already cited EMAS 2014 paper, we tackled the called LTL3, has been proposed later on [8]. A third truth problem of projecting a global specification of an interaction value “ ?” is introduced to specify that after a finite trace of protocol expressed in the global types formalism onto subsets events has been occurred, the outcome of a monitor can be of agents in the MAS. The projection function is a key element inconclusive. for moving from a global specification of the protocol to a The generation of efficient monitors for properties specified localized one, which involves less agents and hence hopefully in a variety of formal languages was firstly addressed by less interaction events. However, in our previous work we M. Kim et al. [21, 18] and many proposals exist for RV faced only one of the issues involved in distributing the of object-oriented systems (jassda [11], PQL [24], JavaMOP RV activity, that of projecting the interaction protocol, and [13], LARVA [14], SAGA [15], just to cite a few) and MASs did not consider the problem of finding suitable partitions [1, 17]. A large community of researchers works on RV and in 2001 the Runtime Verification Workshop/Conference series was initiated (http://www.runtime-verification.org), and workshops/conferences have occurred each year since then.
When moving from RV to DRV, however, the situation dramatically changes: no introductory papers and surveys on the topic exist, which demonstrates the youth of this research field. W.r.t. DRV of MASs, we were not able to find any related work except for one paper of ours [10] where the projection mechanism introduced in our previous EMAS 2014 work had been integrated with JADE [9].
Trace expressions are a specification formalism expressly designed for RV. They are based on the notions of event and its abstraction, event type.
Events. In the following we denote by E a fixed universe of events. An event trace over E is a possibly infinite sequence of events in E. As an example, we might have E = { msg(bob, alice, tell, m1), msg(alice, bob, tell, a1), msg(bob, carol, tell, m2), msg(carol, bob, tell, a2), msg(bob, dave, tell, m3), msg(dave, bob, tell, a3) } where the interaction event msg(S, R, P, C) corresponds to the interaction between agent S and agent R, with S sending a message with performative P and content C to R. In this example, contents m1, m2 and m3 correspond to actual messages, and contents a1, a2 and a3 correspond to acknowledges of reception. • τ1·τ2 (concatenation), denoting the set of all traces obtained by concatenating the traces of τ1 with those of τ2. • τ1∧τ2 (intersection), denoting the intersection of the traces of τ1 and τ2. • τ1∨τ2 (union), denoting the union of the traces of τ1 and τ2. • τ1|τ2 (shuffle ), denoting the set obtained by shuffling the traces in τ1 with the traces in τ2.
To support recursion without introducing an explicit construct, trace expressions are regular (a.k.a. rational or cyclic) terms. A regular term can be represented by a finite set of syntactic equations, as happens, for instance, in most modern Prolog implementations where unification supports cyclic terms. A trace expression τ is contractive if all its infinite paths from the root contain the prefix operator.
From the operators above we can derive the filter operator, useful for making trace expressions more compact and readable. The expression ϑ τ denotes the set of all traces contained in τ , when deprived of all events that do not match ϑ. Assuming that event types are closed by complementation, the expression above is a convenient syntactic shortcut for T |τ , where T = ∨ϑ:T , and ϑ is the complement event type of ϑ, that is, JϑK = E \ JϑK.
In the context of RV, where the three-valued semantics is considered for LTL, trace expressions are strictly more expressive than LTL [6]: every LTL formula can be encoded into a trace expression with an equivalent three-valued semantics, whereas the opposite property does not hold, since trace expressions are also able to specify all context-free languages, and also some non context-free ones.
Although trace expressions can define protocols involving events of any kind, in the sequel we will limit our investigation to interaction events like msg(S, R, P, C) and interaction types that we will identify with α.
Event types. To be more general, trace expressions are built on top of event types (chosen from a set ET), rather than of single events; an event type denotes a subset of E.
For example, if we were interested only in the type of the message content (actual message or acknowledge), we might define the two event types Msg= { msg(bob, alice, tell, m1), msg(bob, carol, tell, m2), msg(bob, dave, tell, m3) } and Ack= { msg(alice, bob, tell, a1), msg(carol, bob, tell, a2), msg(dave, bob, tell, a3) }, and use them for describing interaction patterns.
The projection function was first introduced in [2]. Given the finite set AGS of all the agents that could play a role in the MAS and an interaction type α, senders(α) is the set of all the agents in AGS that could play the role of sender in actual interactions having type α, and receivers(α) is the set of all the agents in AGS that could play the role of receiver
Trace expressions. A trace expression τ represents a set of in interactions of type α. The involves predicate holds on one possibly infinite event traces, and is defined on top of the interaction type α and one set of agents Ags, involves(α, Ags), following operators (binary operators associate from left, and iff (senders(α) ∩ Ags 6= ∅) ∨ (receivers(α) ∩ Ags 6= ∅). are listed in decreasing order of precedence, that is, the first Projection can be described as a function Π : T × operator has the highest precedence): P(AGS) → T where T is the set of trace expressions. Π is • (empty trace), denoting the singleton set { } containing driven by the syntax of the trace expression to project; since the empty event trace . Π is defined on cyclic terms, the simplest way to define it • ϑ:τ (prefix ), denoting the set of all traces whose first event would be by coinduction2 as follows: e matches the event type ϑ (e ∈ ϑ), and the remaining (i) Π( , Ags) = part is a trace of τ . For example, if our communication protocol just required that an interaction from the set 2Coinduction is a technique for defining and proving properties of systems Msg must take place, no matter which one, and then an of concurrent interacting objects. It is the mathematical dual to structural interaction from Ack must occur, no matter which one, isnudcuhctaiosn.stCreoaimndsu.cStieveelyhtdtpe:fi//ncseedwteybp.uescsadr.eedtuy/pgircoaullpys/tiantfia mniit/ehadnadtdaesmtrousc/tduorce/s, we could express it as Msg:Ack: . coind.htm for a more technical formalization. (ii) Π(α : τ, Ags) = α : Π(τ, Ags) if involves(α, Ags) (iii) Π(α : τ, Ags) = Π(τ, Ags) if ¬involves(α, Ags) (iv) Π(τ 0 op τ 00, Ags) = Π(τ 0, Ags) op Π(τ 00, Ags), where op ∈ {·, ∧, ∨, |}.
This definition works properly only on all non cyclic terms and on some, but not all, cyclic terms. To guarantee that the projection function always returns a contractive type and that the correct coinductive definition is implemented, it is necessary to keep track of all types visited by Π along a path; each type is associated with its depth in the path, and with a fresh variable which will be unified with the corresponding computed projection. During the visit, the depth DeepestSeq of the deepest visited sequence operator is kept. If a type τ has been already visited, then a cycle is detected: if its depth is less than DeepestSeq then the cycle contains an occurrence of the sequence constructor, therefore the projected type associated with τ is contractive and, hence, is returned; otherwise, the projection would not be contractive, therefore is returned.
The graph partitioning problem (GPP) is defined in the following way [12]: given a number k ∈ N>1 and an undirected graph G = (V, E) with non-negative node and edge weights, GPP asks for a partition of V , that is, with blocks of nodes (V1, ..., Vk) such that all edges in the CI G have weight 1, but the approach works also in case edge weights are different: a higher edge weight would model a preferential communication channel; 4) partition the new graph obtained so far using some suitable graph partition method; 5) project the interaction protocol onto these agents’ partitions.
The algorithm is explained by means of two running examples introduced in [2].
1) V1 ∪ V2 ∪ ... ∪ Vk = V 2) Vi ∩ Vj = ∅ ∀i 6= j
A balance constraint may be required, demanding that all blocks have about equal weights. To be more precise, a good Fig. 1. The “Socks and Shoes” MAS partition is the one where the sum of the node weights in each Vi is “about the same” and the sum of all edge a) Socks and Shoes (SaS): Let us consider the simple weights of edges connecting all different pairs Vi and Vj is scenario illustrated in Figure 1 where two robots (right minimized. Applications of graph partitioning include parallel and left), two monitors (right and left) associated with processing, road networks, image processing, VLSI design, each robot, and a plan monitor which supervises them, social networks, and bioinformatics. Among the many existing must reach the goal to put the right and left socks and tools for graph partitioning we opted for using METIS [20], shoes in the correct way (socks first!). As robots are a set of serial programs for partitioning graphs, partitioning autonomous, they could perform the two actions in the wrong finite element meshes, and producing fill reducing orderings order: monitors are there to ensure that wrong actions are for sparse matrices (http://glaros.dtc.umn.edu/gkhome/views/ immediately rolled back. Robots communicate their actions metis, accessed on June 2016). The choice of METIS was due to their corresponding monitors, which, in turn, notify the to the efficiency of the multi-level Kernighan/Lin approach it plan monitor when the robots accomplish their goal. The builds upon [19] and to the ease of its installation and usage. interaction types involving the right robot and the right node monitor are defined as msg(right robot, right node monitor, IV. MAS-DRIVE: DESIGN tell, put sock) ∈ put right sock; msg(right robot, right node monitor, tell, put shoe) ∈ put right shoe; msg(right robot, right node monitor, tell, removed shoe) ∈ removed right shoe; msg(right node monitor, right robot, tell, oblige remove shoe) ∈ oblige remove right shoe; msg(right node monitor, plan monitor, tell, ok) ∈ ok right.
Those for the left robot and left node monitor are symmetrical.
Given an interaction protocol expressed in some suitable formalism, the MAS-DRiVe algorithm for partitioning a MAS in such a way that the identified subsystems can be safely monitored in a decentralized way is the following: 1) extract the interaction graph I G from the interaction
protocol; 2) identify the sets of agents which cannot be split during the decentralized monitoring (unsplittable agents), since the interactions they are involved in are not independent; 3) compute the collapsed interaction graph CI G by collapsing each of those sets into a single node with weight equal to the cardinality of the collapsed set, and by computing the collapsed edges consistently; for simplicity,
The right robot (RIGHT branch in the protocol description below) can start by putting the sock, which is the correct action to do, or (∨ operator) by putting the shoe, which requires a recovery by the right robot monitor and looping back to the RIGHT branch. The left robot has the same behavior (LEFT branch in the protocol description). The SaS protocol is described by the shuffle of the actions of the right and left verify MA2, and if an event has type msg3 or ack3 , then it must verify MA3.
As already introduced in the beginning of this section, the
MAS-DRiVe algorithm consists of five steps.
robots and monitors (RIGHT | LEFT):
(put right sock:put right shoe:ok right: )∨
(put right shoe:oblige remove right shoe:
removed right shoe:RIGHT)
(put left sock:put left shoe:ok left: )∨
(put left shoe:oblige remove left shoe:
removed left shoe:LEFT)
RIGHT|LEFT.
(msg MM )∧(msg ack (
The trace expression defined by MM corresponds to the first constraint informally stated above, while MA1, MA2, and MA3 formalize the second constraint. The main trace expression ABP3 can be easily read as follows: if an event has type msg1 or msg2 or msg3 , then it must verify MM , and if an event has type msg1 or ack1 , then it must verify MA1, and if an event has type msg2 or ack2 , then it must extract(ID, AlreadyMetTrExp, Str, Level, τ ) is defined by cases: 1) if TrExpr belongs to AlreadyMetTrExp, then return; 2) if TrExpr is , then return; 3) if τ is α uop τ1, where uop is an operator in {:, }, then a) NewStr = Str • (uop, Level+1) b) extract all the possible pairs of senders and receivers (S, R) such that S and R are involved in α c) for each of such pairs, generate and assert edge(ID,
d) NewAlreadyMetTrExp = {τ } S AlreadyMetTrExp
Level+1, τ1) 4) if τ is τ1∧τ2, then a) NewStr = Str • (∧, Level+1) b) NewAlreadyMetTrExp = {τ } S AlreadyMetTrExp
Level+1, τ1)
Level+1, τ2) 5) if τ is τ1 bop τ2, where bop is an operator in {·, ∨, |}, then a) NewStr1 = Str • (bop, Level+1) b) NewStr2 = Str • (bop, 2*Level+1) c) NewAlreadyMetTrExp = {τ } S AlreadyMetTrExp
Level+1, τ1)
2*Level+1, τ2)
Given a protocol identified by ID and represented by the trace expression τ , extract(ID, {}, Λ, 1, τ ) generates and asserts all the edges in IGext. The generation of IGext nodes is straightforward. The idea behind this function is that edges whose labels share the same prefix have a strong dependency as they belong to the same intersection. In fact, the only case where labels of edges share the same prefix is that of ∧ (case 4), where the same string and level are passed to the recursive calls. If the operator is not an intersection (case 5), the strings and levels passed to the recursive calls are different, meaning that the two operands are independent from one another and so will be the edges generated during their exploration.
For example, the edges in the auxiliary IGext graph
extracted from the ABP3 protocol are:
(bob, alice, ((∧, 2) (
∧ ∧
(bob, carol, ((∧, 2) (
∧ ∧
(bob, dave, ((∧, 2) (
∧ ∧
(bob, alice, ((∧, 2) (
∧ ∧
(bob, carol, ((∧, 2) (∧, 3) (∧, 4) (
∧
(bob, carol, ((∧, 2) (
∧
(carol, bob, ((∧, 2) (
∧
(bob, dave, ((∧, 2) (
can be monitored independently from one another, as some interaction patterns that must be respected by a set of agents seen as a whole, could be lost when looking at subsets of the agents.
As an example, alice, bob, carol and dave in the ABP3 represent an unsplittable set of agents. In fact, if we monitored interactions involving alice and bob only, we could find that they respect the second constraint of the protocol, but we could never ensure that the first constraint – which also depends on the interactions of bob with carol and dave – is respected as well. The notions of dependence and independence are related to the protocol but also to the formalism used for modeling it, so no general rule for this step can be devised. When the interaction formalism F is that of trace expressions, however, dependencies among interactions are naturally modeled using the intersection operator. Thus, although it may be an overcautious approach, when using trace expressions we define “unsplittable” the agents involved in interactions connected by an intersection operator.
The algorithm for performing the identification of
unsplittable agents looks at the labels in IGext and creates
sets of agents involved in interactions whose label has the
same prefix before the first∧ operator in the label, if any.
For example, in SaS no label contains ∧ and hence the set
of unsplittable agents is empty, whereas in ABP3 all the
edge labels share the (
Considering the running examples above, the weighted nodes in the SaS CIG are ({right robot},1) ({right node monitor},1) ({plan monitor},1) ({left robot},1) ({left node monitor},1) namely, no collapse took place, while the only weighted node in the ABP3 CIG is ({alice,bob,carol,dave},4) labeled with the set of unsplittable agents.
The edges in the SaS CIG are the same as those in the SaS IG, while there are no edges in the ABP3 CIG due to the presence of only one node. 4) Graph partitioning. This stage of the algorithm consists in partitioning the CIG graph obtained by the collapse stage. The number of expected partitions is given as an input by the user and must be grater than one. Any suitable partitioning algorithm could be used during this stage. We will discuss our implementative choice in Section V.
The partition of the original, not collapsed graph IG, is trivially derived by that of CIG by making the union of the agents in the labels of the nodes in each CIG partition. the node weights in each partition is about the same and the number of edges connecting nodes in two different partitions is minimized (by associating the unit weight with each edge), we can obtain the following partition for the agents {plan monitor, right node monitor, right robot} } . involved in the SaS protocol: {{left node monitor, left robot},
The agents involved in the ABP3 protocol cannot be partitioned because the collapsed graph consists of only one node. 5) Projection. Once the agents belonging to the same partition have been devised, the projection algorithm presented in Section III-B can be used to project the global interaction protocol onto each of them.
The MAS-DRiVe algorithm is fully implemented in SWIProlog (http://www.swi-prolog.org/, accessed on June 2016), apart from the graph partitioning stage which exploits the METIS tool described in Section III. The extraction of the IG from the protocol, the identification of the unsplittable agents sets, and the generation of the collapsed graph CIG are performed by Prolog predicates. After them, a predicate for encoding CIG into a format suitable for METIS and saving it into a file is called. The command line for running METIS on that file is launched from inside Prolog, and the result is read and decoded.
In order to run the algorithm, the user must call the partition/3 predicate with three arguments: the identifier of the agent interaction protocol to distribute, the number of partitions to be obtained, and the name of the file where Prolog will write the result of the partition. For example, given that abp3 identifies the ABP3 protocol, and that the trace expression associated with this identifier has been read into the Prolog knowledge base, the user should call partition(abp3, 2, ’./abp3Out.txt’) obtaining the following content for the abp3Out.txt file:
node(abp3,bob) node(abp3,alice) node(abp3,carol) node(abp3,dave)
edge(abp3,bob,alice,[ ((/\),2), ((/\),3), ((/\),4), ((>>),5)]) edge(abp3,bob,carol,[ ((/\),2), ((/\),3), ((/\),4), ((>>),5)]) ....
@((S_1|S_2), [S_1= (put_right_sock:put_right_shoe:ok_right:lambda)\/ (put_right_shoe:oblige_remove_right_shoe: removed_right_shoe:S_1), S_2= (put_left_sock:put_left_shoe:ok_left:lambda)\/ (put_left_shoe:oblige_remove_left_shoe:
removed_left_shoe:S_2)]) can be partitioned into {[left_node_monitor],[left_robot]} {[plan_monitor],[right_node_monitor],[right_robot]}
node(socks,right_robot) node(socks,right_node_monitor) node(socks,plan_monitor) node(socks,left_robot) node(socks,left_node_monitor)
edge(socks,right_robot,right_node_monitor, [((|),2), ((\/),3), ((:),4)]) edge(socks,right_robot,right_node_monitor, [((|),2), ((\/),3), ((:),4), ((:),5)]) ........
cnode(socks,[right_robot],1) cnode(socks,[right_node_monitor],1) cnode(socks,[plan_monitor],1) cnode(socks,[left_robot],1) cnode(socks,[left_node_monitor],1)
cedge(socks,[right_robot],[right_node_monitor]) cedge(socks,[right_node_monitor],[plan_monitor]) cedge(socks,[left_robot],[left_node_monitor]) cedge(socks,[left_node_monitor],[plan_monitor])
We run experiments with protocols that involve distinct groups of agents each following the ABP3 protocol. For example, in the DoubleABP3, alice, bob, carol and dave follow the ABP3 protocol, alice2, bob2, carol2 and dave2 follow the ABP3 protocol as well, and both bob and bob2 interact with boss. Since alice, bob, carol and dave have no interactions with alice2, bob2, carol2 and dave2, the two groups are independent from each other and can be safely partitioned for the purpose of decentralized runtime verification. In such a situation, the partition computed by MAS-DRiVe is the following:
[ ((*),3), ((\/),7), ((:),8), ((:),9), ((/\),10)], [alice2,bob2,carol2,dave2] [ ((*),3), ((\/),4), ((:),5), ((:),6), ((/\),7)], [alice,bob,carol,dave]
@((bobasks:lambda|bob2asks:lambda)*
((okbob:nobob2:msg3>>S_1/\msg_ack(
The code of the MAS-DRiVe algorithm can be downloaded monitors to deploy, or at least guidelines may be provided in from http://www.disi.unige.it/person/MascardiV/Software/ the future. masdrive.html. It requires SWI Prolog and the METIS Finally, as part of our future work, we plan to make an exsoftware installed and accessible via the command line from haustive experimentation of MAS-DRiVe on existing complex everywhere. We tested it on Mageia Linux. protocols. METIS can easily partition graphs with hundreds of nodes so we will model protocols involving hundreds of
VI. CONCLUSIONS AND FUTURE WORK agents and test the scalability of the approach. Studying its This paper addresses the problem of how to partition a computational properties from a theoretical viewpoint is on MAS into agents’ subsets that can be verified at runtime, our agenda as well. independently from one another, in such a way that the results obtained by the decentralized runtime verification are the ACKNOWLEDGMENTS same as those obtained by monitoring the whole MAS in a We are grateful to the anonymous reviewers for their useful centralized way. remarks and constructive comments.
We designed and implemented the MAS-DRiVe algorithm, whose results are consistent with those discussed in [2]. In that REFERENCES paper, the feasibility of distributing the runtime monitoring over user-defined sets of agents was empirically validated by checking the traces of events compliant with the decentralized subprotocols up of a given length, and verifying whether they were compliant with the original global protocol as well. That approach gave a semi-decidable information: if all traces up to a given length l were found to be compliant with the protocol, this did not ensure that problems could not arise with traces of length l + 1. With MAS-DRiVe we propose a constructive way to partition agents in the MAS, rather than letting the user decide how to partition them, and we overcome the problems due to the empirical validation approach by proposing partitions that are “safe” w.r.t. the trace expression operators. In particular, we assume that agents involved in an intersection can never be partitioned. This is an overcautious approach, but since intersection is the construct used to state constraints across different independent branches of the protocol, we assume that those branches cannot be monitored independently.
In its current version, then, the MAS can not get split if no semi-independent parts of the system can get identified.
Although this is a limitation of our approach, this could have an interesting side effect that we aim to explore in the close future, namely the possibility to come up with suggestions for MAS designers in terms of good practices for better subsystems encapsulation based on interaction protocol analysis.
Such suggestions could be applied to distributed systems in general, and not only to MASs, and could prove useful in those approaches where there is an embedded notion of some sort of encapsulation.
As far as graph partitioning is concerned, we point out that the obtained partitions do not correspond to partitions of