Trace expressions are a compact and expressive formalism, initially devised for runtime veri cation of agent interactions in multiagent systems (MAS), which has been successfully employed to model real protocols, and to generate monitors for mainstream multiagent system platforms, and generalized to support runtime veri cation of di erent kinds of properties and systems. In this paper we present the trace expression formalism and its use in the runtime veri cation context focusing on future works related to the distribution aspects.
Runtime veri cation (RV) is a software veri cation technique that complements formal static veri cation (as model checking) and testing. In RV dynamic checking of the correct behavior of a system can be performed by a monitor which is generated from a formal speci cation of the properties to be veri ed. A possible way to specify the monitor behavior is through the set of all correct traces ( nite or in nite sequences of events) which can be generated during the system execution. Sets of traces may be represented in many di erent ways. In this extended abstract we present trace expressions [3, 4], a formalism inspired to session types [8, 12] which can be used to design monitors for the RV of centralized and decentralized software systems. Distributed runtime veri cation (DRV), as described by S. Rajsbaum in his keynote speech at the SSS 2015 Symposium [10], 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. Once the formal speci cation of the global pattern of events is given, however, distributing the monitoring activity can be resorted to decomposing the global speci cation into \sub-speci cations", 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 speci cation. The trace expression formalism can be used to construct protocols representing sequences on generic events. Since we focus on its distributed aspects, we limit the set of the events to the subset corresponding to the interaction events, where interactions are intended as exchange of messages among agents in a MAS. Trace expressions are already used for centralized runtime veri cation (no distribution) [4] and for the automatic generation of protocol-driven agents (total distribution) [2] through projection on each single agent involved in the protocol. This work lays the foundations to ll the gap between these two projects obtaining a middle way approach between the centralization (bottleneck) and the total distribution (ine cient) implementations. 2
A trace expression represents a set of possibly in nite event traces, and is
de ned on top of the following operators: (
Example 1. Let E = fe1; : : : ; e7g, and #i, i = 1; : : : ; 7, be the event types such that e 2 #i i e = ei (that is, J#iK = feig); then the trace expression 1 = ((#1: j#2: )_(#3: j#4: )) (#5:#6: j#7: ) denotes the following set of event traces: e1e2e5e6e7; e1e2e5e7e6; e1e2e7e5e6; e2e1e5e6e7; e2e1e5e7e6; e2e1e7e5e6; e3e4e5e6e7; e3e4e5e7e6; e3e4e7e5e6; e4e3e5e6e7; e4e3e5e7e6; e4e3e7e5e6 Example 2. Let the set of interaction types ET = f ping; pongg and E = fpingA!B; pongB!Ag, J pingK = fpingA!Bg and J pongK = fpongB!Ag; then the trace expression P ingP ong = ( ping:P ingP ong pong: )_ denotes the following set of interaction events: fpingA!BpongB!A; pingA!BpingA!BpongB!ApongB!A; :::; pingAn!BpongBn!Ag: 2.1
The projection function was rst introduced in [1]. Given the nite set AGS of all the agents that could play a role in the MAS and an interaction type (an event type containing only interaction events), 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 in interactions of type . The involves predicate holds on one interaction type and one set of agents Ags, involves( ; Ags), i (senders( ) \ Ags 6= ;) _ (receivers( ) \ Ags 6= ;).
We de ne two auxiliary functions f irst : T ! P(ET) (last : T ! P(ET)),
f irst( ) = f#1; #2; :::; #ng (last( ) = f#1; #2; :::; #ng) i 8#i :9e2#i s.t. e is
one of the rst (last) events which can be consumed by the transition
relation called on . In this way we can introduce the derived sets involved( ) =
Ags () senders( ) [ receivers( ) = Ags and involved( ) = ;; involved( ) =
involved(
As already anticipated, we consider trace expressions to model interaction protocols inside a MAS. With respect to the centralized runtime veri cation approach proposed in [4], we want to reason about the trace expression distribution in order to obtain a set of trace expressions where each one represents the protocol subset related to a xed set of agents. The main problem of this approach is to understand which agents can be monitored separately and which must be monitored together (unsplittable) in order to guarantee that the distributed monitoring gives the same results as the centralized one. This notion is strongly related to the correctness de nition in the Choreographies research eld [9] where a choreography can be projected on each single entity (agent for us) only if it satis es three conditions (for trace expressions the rst two are enough). We report these two conditions adapted for the trace expression formalism. De nition 1. The two conditions which a trace expression must satisfy in order to be correctly projected on each single agent involved in its event types are: 1. Connectedness for sequence.
For each sub-expression : 1, with f irst(
For each sub-expression 1_ 2, with f irst(
Without loss of generality we consider only trace expressions where all interaction types represent nite sets of events. Thus, we can have interaction types like = fi1A!B; i2B!A; i3A!B; :::g and not interaction types like = fi1A!B; i2C!D; :::g or = fi1A!B; i2A!D; :::g.
We can observe that the two conditions are too restrictive when we want to distribute our protocols on sets of agents. In particular, we can easily nd protocols that cannot be projected on a single agent but can be projected on a set of agents. Considering for instance the trace expression = :::( ping: pong: )::: where ::: means that contains also other terms and J pingK = fpingA!Bg, J pongK = fpongC!Dg, can immediately note that it does not satisfy the rst condition (the connectedness for sequence). Since can be a very large trace expression we would like to distribute it anyway. Even if we cannot distribute it on each single agent ffAg; fBg; fCg; fDgg, in this particular case a possible choice for the distribution could be ffAg; fB; Cg; fDgg obtaining three di erent projections of the global protocol in three separated parts where B and C are projected and monitored together.
Example 3. Given the trace expression = ( m1: )_( m2: ) where AGS = fA; B; C; Dg, J m1K = fmsg1A!Bg and J m2K = fmsg2C!Dg. ( ; fAg) = ( ; fBg) = (( m1: )_( m2: )) = ( m1: ( ))_( ( )) = ( m1: )_( ) = m1: and ( ; fCg) = ( ; fDg) = (( m1: )_( m2: )) = ( ( ))_( m2: ( )) = ( )_( m2: ) = m2: The two local versions of the protocol have lost the unique point of choice information. 3.1
An important feature in order to distribute a trace expression is the automatic
generation of the set of all possible partitions of agents that preserve the
semantics during the projection phase. Since we know that a trace expression must
satisfy the two conditions (De nition 1) to be correctly projected on each single
agents involved in the protocol, we can use this information to guide our analysis.
From an high level point of view, given a trace expression , for each subterm of
we can check if the two conditions are satis ed; if a condition is not satis ed
on a singular agent, we try to evaluate it on a set of agents containing the agent.
Considering for instance the rst condition (connectedness for sequence), if we
nd a subterm 1 : 2 : :::, with involved(
We are working on the implementation of the corresponding algorithm focusing on the correctness and completeness proofs. The intuition is that forcing the preservation of the two conditions (De nition 1) we preserve all critical points of the trace expression, where the critical points are all points of the protocol where it could be necessary monitor some agents together. 4
In this extended abstract we have presented a possible approach for the distribution of a trace expression on a set of agents. Following the conditions deriving from Choreographies (De nition 1) we can extract the partitions of agents which allow us to obtain the semantic preservation during the projection phase. Once we have the set of all possible valid partitions we can use them to generate the monitors to perform the distributed runtime veri cation of our MAS.
We can nd works on distributed runtime monitoring like [7, 6, 11] but w.r.t. DRV of MASs we were not able to nd any related work, except for the one which spun o from [1], namely [5]. Another relevant work is [13] where an interesting distributed approach to process mining is presented. Considering the conformance checking, that work is extremely related to ours and it can be useful to study the possible connections. For instance using trace expressions instead of Petri nets for the conformance checking of event logs.
Future work will be to implement the algorithm corresponding to this intuition using the programming language Prolog whereby we have already implemented the semantics of trace expressions and the projection function. Once we will have implemented the distribution algorithm we will be able to project the global protocol on each single partition in order to automatically generate distributed monitors. A possible implementation could be using a MASs framework based on logic programming, in this way we will be able to generate monitors directly by the projected trace expressions. We will try our approach rst on some well known communicative protocols (as Contract Net Protocol, Alternating Bit Protocol, and so on) and after on a real case study concerning the distributed runtime veri cation of a MAS.