The behavior of agents in multi-agent systems is hard to control without restricting the agents' autonomy. Normative organizations have been deployed successfully to deal with this. A core requirement of a normative organization is that norm violations can be observed and dealt with. Due to the distributed nature of multi-agent systems it is often tting that this is done decentrally. In this paper we discuss a decentralized method to monitor whether norms are violated in a multi-agent system. The setting we consider is one where the organization depends on a network of monitors that share observations among each other.
The behavior of multi-agent systems (MAS) is hard to predict. This makes
it challenging to guarantee that agents behave according to preset guidelines.
Norms are a popular candidate to deal with this [
Formal methods for decentralized monitoring help to better analyze and design decentralized monitors. There are di erent models in related work (section 2) which are proposed under di erent assumptions. Our aim in this paper is to provide complementary work to analyze generic scenarios with assumptions that are not covered in other works. The basis of our method is a network of monitors of which each has its own local view on the environment. Each monitor is assigned a set of norms which concern the MAS that is being monitored. Because of the local view of monitors, it might be necessary that they communicate in order to detect violations. In our method this is done through the propagation of observations. Propagation causes delays in violation detection. The proposed method is aimed at detecting a violation in the number of computation steps that it maximally takes for an observation to be propagated across the network. We shall specify a formal framework for analyzing decentralized monitors that are based on our method.
As an example scenario we use a smarts roads use-case. We utilized the same
use-case in earlier work to highlight di erent concepts in distributed
organizations [
In our scenario, a highway segment has a special priority lane for situations where the tra c density is high (e.g. tra c jams due to accidents or rush hours). This is a lane to increase the throughput of high priority vehicles such as public transport or cars with special permits like taxis. One norm concerning the use of this priority lane is as follows: if an agent is on the priority lane, then it is obliged to get o it or have a permit, before the tra c density becomes high.
We use three di erent kinds of monitors in our scenario. Lane monitors observe whether a speci c car is on a priority lane. Tra c density monitors observe whether the tra c density is high. And a permit monitor can observe whether a speci c car has a permit to use the priority lane. The tra c density monitors can communicate with the lane monitors and the permit monitor. The norm violation in this scenario cannot be locally observed by any of the monitors. Data has to be transferred between monitors in order to detect the violation.
In section 2 we discuss related research on (decentralized) monitoring. In section 3 we explain the formal setting of our method. In particular we de ne the notions of norms, monitors and violation detection for (decentralized) monitors. We discuss the example scenario in section 4. In section 5 we provide the algorithms for how norm violations can be detected distributively by a set of monitors that observe the environment properties with delay. 2
In earlier work [
Linear temporal logic (LTL) and computational tree logic (CTL) are
commonly used to describe whether possible system traces are violating a norm
(cf. [
There are two main avors of monitors. One option is to create a nite state
machine (FSM) given a norm. As a system evolves over time, observed events
are processed in the monitor. If the monitor reaches a forbidden state, then it
detects a violation. Such an approach can be found in for instance the proposed
monitors for RV-LTL [
The other avor for monitoring LTL properties is the use of progression
functions. The progression function proposed in [
Our method neither builds a FSM, nor does it use a progression function,
but it resembles most the progression method. The reason why progression is
not needed, is that our method, in contrast to [
We will explain decentralized monitoring in various steps. Our framework builds on LTL which we shall discuss rst. Second we de ne norms and norm violations. Third we explain the notion of a monitor and norm violation detection. Fourth we discuss di erent types of monitors, that depend on their violation detection capability. Finally we discuss decentralized monitors. 3.1
Preliminaries To determine whether a norm violation has occurred in a system we start with standard LTL with a weak until operator. We assume there is a nite set of atoms A and environment states S. An in nite trace = s0s1 : : : is a trace of environment states s.t. si 2 S. The valuation function V : S ! 2A returns, given a state s, the set of atoms that hold in s. We use ! to notate the set of all in nite traces, and for the set of all nite traces. The syntax we use is as follows: ' = pj:'j' _ j
Given a trace ltl is as follows:
'j'U = s0s1 2 where p 2 A.
!, and an environment state si in , entailment ; si ltl p ; si ltl :' ; si ltl ' _ ; si ltl ' ; si ltl 'U , p 2 V (si) , ; si 6 ltl ' , ; si ltl ' or ; si ltl , ; si+1 ltl ' , 8j 2 [i; 1] : ; sj ltl ', or: 9j 2 [i; 1] : ( ; sj ltl and 8k 2 [i; j 1] : ; sk ltl ')
Runtime monitoring concerns nite traces only. For formulas such as 'U it might be the case that ' is always true in a nite trace and is always false. In such cases it is not possible to evaluate the formula as it is unclear whether the formula is true in the future of the trace. Therefore we will use common nite trace semantics for LTL that evaluates formulas as being true, false or inconclusive.
We notate a nite trace of length k + 1 as k and k ! is the set of in nite traces s.t. k is a pre x. Given a nite trace k 2 , and a state si, i 2 [0; k], nite trace LTL entailment f is de ned as follows: k; si f ' = <8 >? iiff 88 22 kk : ? otherwise ! : ; si ltl ' ! : ; si 6 ltl '
For a trace k if ' is true/false in state si, i 2 [0; k], then it is true/false in si for any nite extension of k.
Proposition 1. Let k 2 be a pre x of j 2 , ' a formula, and i 2 [0; k]: If k; si f ' = v then j ; si f ' = v, for v 2 f?; >g.
Proof sketch: This follows from the de nition of f , as future states cannot change a conclusive valuation. 3.2
Norms
Norms can have di erent forms. For instance some norms are state-based whereas
others are event-based. Also, norms can have temporal aspects in the form of
conditions and deadlines. In this paper, we use conditional norms with deadlines
that are state-based [
De nition 1. Norm. A norm is speci ed by a tuple of propositional formulas h'c; 'o; 'di s.t. 'c; 'o and 'd are the norm's condition, obligation and deadline, respectively.
We use N for the set of possible norms and AN for the set of all atoms that
occur in norms from a set N . Conditional norms with deadlines are related to
temporal logic (cf. [
If a norm is violated in a trace k, then it is violated in any nite extension of k.
Proposition 2. If a norm h'c; 'o; 'di is violated in a trace k, then it is violated in all j 2 s.t. k is a pre x of j .
Proof sketch: The violation is a conclusive formula evaluation on k and a state si. Following proposition 1, the evaluation is the same for j and si. 3.3
Monitors A monitor has a set of norms that it monitors. Monitors can observe some atoms with a delay and therefore have a delay function. This function returns, given an atom, the time that it takes to observe whether that atom holds. The delay of an observation is measured in abstract time units that correspond with the time between two states in a trace. For the following de nition, recall that A is the global set of atoms.
De nition 3. Monitor speci cation. A monitor is speci ed by a tuple hN; i, where N N is a set of norms and : A ! N1 is a delay function.
As we shall see in section 3.5 the delays in this paper are caused by communication. However delays can also originate from for instance sensors that make observations some time after they happen. Extending the framework with additional causes of delay (e.g. delayed sensors) will impact some of the results regarding the delays of when norm violations are detected. The main limitation for extending the model's delay speci cation is that the delay must be measured in equal time units.
We use M to notate the set of possible monitor speci cations. A monitor is a function that given a trace returns a set of traces that it cannot distinguish according to its speci cation. Consider a scenario with a set of atoms A = fc; o; dg and a monitor m that is speci ed by hfhc; o; dig; i, where (c) = (d) = 0, and (o) = 2. Furthermore S = fsa; sb; scg, s.t. V (sa) = fc; og; V (sb) = fcg and V (sc) = f g
d . 1 Note that given a nite trace k and a norm n = h'c; 'o; 'di, k is compliant with n i for each i 2 [0; k] : k; si f 'c ! (:'dU 'o) 6= ?
Because (o) = 2, m's view on the environment trace at moment k does not inform m whether o is true at moment k and k 1. Consider the environment trace
= sascsc. At the initial time step m does not observe o to be true or false. Instead, m observed that c is true and that d is not true. So all possible initial states are sa and sb. At the second time step m determines that the second state can only be sc, because it observed d and not c. At the third time step m observes o and d. Because of the delay, this means that o was true in the initial state. Therefore m observes that indeed in the initial time step the state was sa. Hence the possible environment traces per time step are:
2. Possible traces given 3. The possible trace given 0 = sa are sa or sb. 1 = sasc are sasc or sbsc.
2 = sascsc is sascsc.
We de ne in de nition 4 when a monitor m cannot distinguish between two traces w.r.t. the atoms that occur in norms that m monitors. These are the traces where for every state the valuation of atoms for which the delay has passed coincides. Because those are the atoms for which m has certainty. i for all i 2 [0; k]; p 2 AN ; (p) k
i: p 2 V (si) i p 2 V (s0i). cannot distinguish between s0 : : : sk and s00 : : : s0k, notated as s0 : : : sk De nition 4. Trace indistinguishability. A monitor m speci ed by hN; i m s00 : : : s0k,
Given a monitor m and a trace k, m( k) is the set of indistinguishable/equivalent traces given m's view on the environment.
De nition 5. Monitor. Let m : and k be a trace. The set of equivalent traces for m given k is notated by ! 2 be a monitor speci ed by hN; i m( k) = f 2 j k m g .
A monitor m speci ed by hN; i has uncertainty of atoms in AN as far in the past as the delay of the atoms. If the delay of an atom has passed for a state s0i in a trace 2 m( k), then its valuation equals that of the state si in k .
Proof sketch: This follows from de nitions 4 and 5.
For all s00 : : : s0k 2 m( k); p 2 AN ; i 2 [0; k (p)]:p 2 V (si) i p 2 V (s0i).
Proposition 3. Let m be a monitor speci ed by hN; i and k be a trace s0 : : : sk. m(σ k )= σk = s s , s , k-x nucertaiy s s k, k s k, m( k) share a pre x of length k
x in which there is certainty for a set of atoms.
For a monitor m speci ed by hN; i let x be the maximum delay for atoms in AN . If a trace k is longer than x, then all possible traces in m( k) have a pre x of length k x where formulas concerning atoms in AN all evaluate equally in those pre xes. This is also illustrated in Figure 1.
Proposition 4. Let m be a monitor speci ed by hN; i, k be a trace, ' be a formula of which all atoms occur in AN , q = arg maxp2AN (p) and x = k (q). For all ; 0 2 m( k), their pre xes x = s0 : : : sx and 0x = s0 : : : s0x, i 2 [0; x]: x; si f ' , 0x; s0i f '.
Proof sketch: Because all atoms evaluate equally up until k (q) (prop. 3), any verdict of a formula in the pre x up until k (q) with those atoms is the same.
Continuing with our earlier scenario, the monitor can reason about the violation of the norm as follows: 1. If 0 = sa then the violation is inconclusive.
If 0 = sb then the norm is satis ed.
So there is no violation of the norm. 2. If 1 = sasc then the norm is violated.
If 1 = sbsc then the norm is satis ed.
So there is no certain violation of the norm. 3. 2 = sascsc so the norm is satis ed so far.
Any trace is per de nition indistinguishable from itself, so k 2 m( k). A violation is detected by a monitor if a norm is violated in all possible environment traces, because then the norm is also violated in k.
De nition 6. Violation detection. Monitor m speci ed by hN; i detects a violation of n 2 N in a trace k at state sk i n is violated in all 0 2 m( k).
A property of violation detection is that there is a maximum delay x for each monitor s.t. if a norm is violated, and a monitor m can detect that violation, that then this violation is always detected within x steps. This delay x depends on the delay function of m.
Proposition 5. Let m be a monitor speci ed by hN; i, q = arg maxp2AN (p) s.t. (p) 6= 1, and k be a trace s.t. a norm n 2 N is violated in k. If m can detect the violation, then it does so within (q) steps.
Proof sketch: Because the violation will be detected, it means that the monitor gains enough information of the environment trace up until k to determine the violation. After (q) time steps, no more certainty can be gained for atoms (prop. 3 & 4). Hence the violation must be detected within (q) steps. 2 j at sj .
We distinguish between di erent types of monitors. These types indicate how well a monitor can detect norm violations. A perfect monitor detects violations whenever they occur.
De nition 7. Perfect monitor. A monitor m speci ed by hN; i is perfect i for all k 2 if there is a violation of a norm n 2 N in k, then m detects the violation in k at sk.
A delayed monitor detects violations with some delay. This means that if a norm is violated, then the monitor may not immediately detect this. But it is guaranteed that the monitor will detect the violation in the future. De nition 8. Delayed monitor. A monitor m speci ed by hN; i is delayed i fork all !,k t2here isifathperree xis aj ovifola,tijon okf, as.tn.omrmdente2ctsNthien viokl,attihoenn offorn ailnl
There is a connection between the delay function of a monitor and its type. If the delays of all atoms which are relevant for a monitor's norms are not in nite, then m is perfect and/or delayed. Also, a perfect monitor is a special case of a delayed monitor, as a perfect monitor is a delayed monitor where the delay of detecting violations is 0.
Proposition 6. Let m be a monitor speci ed by hN; i. If 8p 2 AN : (p) = 0 then m is perfect, if 8p 2 AN : 0 (p) < 1 then m is delayed.
Proof sketch: Following propositions 4 and 5: if a norm is violated in k and 8p 2 AN : (p) < 1, then the valuation of all atoms in AN becomes equal in pre xes of indistinguishable traces for m. If 8p 2 AN : (p) = 0 then the maximum delay for detecting a violation is 0, thus a violation would immediately be detected, hence m would be perfect. If 8p 2 AN : 0 (p) < 1 then the maximum delay x is nite and m will always detect the violation after x steps , hence m would be delayed.
De nition 9. Flawed monitor. A monitor m speci ed by hN; i is awed i m is not delayed.
For a awed monitor there is a trace k where a norm is violated and there
is an in nite trace 2 k ! s.t. there is no pre x of longer than k in which
the monitor detects the violation. This has as a consequence that the delay
function cannot determine whether a monitor m speci ed by hN; i is awed. To
illustrate this, consider the extreme case where for an environment there is no
trace k 2 s.t. a norm n 2 N is violated in k. If no norm can be violated,
then there is no violation that m can miss, and hence m cannot be awed. Even
if for each atom p 2 AN the delay is in nite ( (p) = 1). This extreme case is
unlikely to occur in practice, because if the norms in N cannot be violated, then
there is also no use for a monitor to monitor them.
A decentralized monitor is a network of monitors that can propagate observations
among themselves. The setting we assume is that like in [
Delays arise because it takes time to propagate observations. The delay functions of monitors therefore depend on the topology of the network. We assume that if a monitor m observes an atom p to hold in the environment, that it then sends this information to each connected monitor m0 in the network. If m receives an observation, then it also sends this information to each connected monitor m0. The propagation delay between two directly connected monitors is one. Each monitor has a visibility of the set of atoms A which it can observe directly in the environment, without delay. The delay of an atom p is therefore either zero if p is visible for m, or the length of the shortest path to a monitor for which p is visible, or in nite if there is no path to a monitor m0 s.t. p is visible for m0.
De nition 10. Decentralized monitor. A decentralized monitor is speci ed by a tuple hG; i, where G = (M; C) is a graph of monitors M M with communication lines C M M , and : M ! 2A is a visibility function. For all m speci ed by hN; i 2 M; p 2 A : (p) = >8>>>< 0x iisffhoppr6 22test ((pmmat))habnedtwxeeins tmhealnedngstohmoef the >>> m0 2 M given G s.t. p 2 (m0): > : 1 otherwise
A decentralized monitor detects violations of norms if any of its monitors in the network detects a violation.
De nition 11. Decentralized violation detection. Let h(M; C); i be the speci cation of a decentralized monitor. The violation of a norm n 2 N in a trace k is decentrally detected in k at sk i there is a monitor m 2 M speci ed by hN; i s.t. n 2 N and m detects a violation of n given k at sk.
For a decentralized monitor D speci ed by h(M; C); i, C and determine whether a monitor m 2 M is perfect, delayed or possibly awed. For instance if for a monitor m speci ed by hN; i 2 M it holds that AN (m), then (p) = 0 for any p 2 AN , which by proposition 6 makes the monitor perfect. Also if C = ;, i.e. if monitors cannot communicate, then there are no shortest paths among monitors. Therefore (p) is either 0 or 1 for any p 2 AN . Thus all monitors would be either perfect or awed.
If all monitors in the network are perfect, then any decentrally detected norm violation will occur instantaneously as the violation occurs. But the detection can 0(a) = 1, then m0 is norm instantaneously. also be instantaneous if for instance all monitors are awed. To illustrate this, consider two monitors m and m0 that are speci ed by hfng; i and hfng; 0i, where n = h
a _ b; o; di. Let the environment states S be the set fsa; sbg s.t. V (sa) = fa; dg and V (sb) = fb; dg. In both sa or sb the norm will be violated, because in those states the condition and the deadline occur at the same time, but not the obligation. If (a) = (o) = (d) = 0 and (b) = 1, then m is awed, because in the event that the trace always is a repetition of sb, then m will never detect the violation. Equally for m0 if 0(b) = 0(o) = 0(d) = 0 and awed because of the possible repetition of sa. However, in whatever trace occurs, one of the awed monitors detects the violation of the the detection was within jM j steps.
If a violation of a norm n is decentrally detected, then the maximum time that it took to detect the violation depends on the maximum time of a local monitor m speci ed by hN; i with n 2 N to detect the violation. Following proposition 5 this maximum is the maximum delay of atoms. In a decentralized monitor, the delay of an atom is the time it takes to propagate an observation, which corresponds to the shortest distance of one monitor to another monitor. Given the set of monitor speci cations M , this maximum delay is thus jM j. N , and Proposition 7. Let h(M; C); k be a trace. If n is violated in i be a decentralized monitor speci cation, n 2
k and it is decentrally detected, then
Proof sketch: For all monitors the maximum delay for an atom aside from 1 is jM j, which is the case if the network has the form of a linear list. Therefore any local monitor that detects the violation does this within jM j steps (proposition 5). 4
Example Formalized alne monitr boserv l m ednsity omnitr boserv d eprmit omnitr
boserv p m
m
We continue with the earlier mentioned smart roads scenario. To simplify the following we only consider one lane, density and permit monitor as depicted in which we model our example are as follows: { l stands for the vehicle is on a priority lane. { d stands for tra
c density is high.
{ p stands for the vehicle has a permit.
For each possible combination of l, d and p there is a state in the set of possible environment states S s.t. that combination holds. The complete setup is as follows:
Monitor m2 is a delayed monitor. The environment trace indicates that the car drove on the priority lane and obtained a permit too late when the tra c density became high. The norm is violated at the state s1, because the car is on the priority lane during high tra c density, without having a permit. We rst determine m2's observations about the environment trace per time step as depicted below. 1. d 62 V (s0) 2. d 62 V (s0), l 62 V (s0), p 62 V (s0),d 2 V (s1). 3. d 62 V (s0), l 62 V (s0), p 62 V (s0),d 2 V (s1), l 2 V (s1), p 62 V (s1),d 2 V (s2).
For any of the traces = s00s01s02 2 m2( 2) the observations of time step 3 must hold. This means that for all those traces it holds that: ; s01 f l = >, because l 2 V (s1) ; s01 f d = >, because d 2 V (s1) ; s01 f :(p _ :l) = >, because l 2 V (s1) and p 62 V (s1).
Therefore: for all = s00s01s02 2 m2( 2) there is a i (i.e. i = 1) s.t.
; s0i f l ^ :(:dU (p _ :l)) = >
So m2 detects the violation given 2 at s2. Therefore the violation is also decentrally detected. The norm was already violated when the trace was 1 = s0s1 , but at that moment m2 did not have certainty about whether l or p were in s1 or not. Had the norm been assigned to m1, then it would have taken another time step for the decentralized monitor to detect the violation. 5
A monitor that is part of a decentralized monitor may have no perfect view on the environment. We shall show it can construct a set of possible environment traces, with which it can check whether a norm is violated. For the shown algorithms we assume that monitors execute in a synchronous manner and execute the algorithms instantaneously. For space reasons, we do not provide details on communication protocols. A monitor's input is a set of observations O A, which includes communicated observations. Observations for an atom p from monitors which are not the closest connected monitor that can observe p are not part of O.
Recall that the environment is always in a state from S. A monitor m maintains a set of possible environment states per time step which is updated given the observations of the next time step. In particular m maintains a vector of sets of environment states S = S0; : : : ; Sk, s.t. all states si 2 Si are the possible environment states at time i. Given a set of observations O A, this vector is expanded with S and then all impossible states given the observations are ltered out. For every atom p 2 A if p is or is not in O then the monitor knows whether the atom was or was not true in the environment state at moment k (p). If for instance p 2 O then all si 2 Si, k (p) = i, where p 62 si have to be removed from Si. This algorithm is given below.
Algorithm 5.1: ProcessObservations(O) global S local ; S = S0; S1; : : : ; Sk 1 Sk S S S0; S1; : : : Sk 1; Sk for each Si; 0 i k 8for each si 2 Si > do <>>> do ><8>if t9hpen2 OSi^ p S62i Vn (fssii)g^ k >>>>: >:>if t9hpen62 OSi^ p S2i Vn (fssii)g^ k (p) = i (p) = i
The following algorithm is for detecting norm violations. For each possible environment trace up until now a norm is checked based on f entailment. If there is a time step where in all possible traces the norm is violated, then it must be true that in the actual environment trace the norm is violated. If a violation is detected then ViolationProcedure() could be used to for instance execute a sanction.
Algorithm 5.2: CheckViolation(h'c; 'o; 'di) local S = S0; : : : ; Sk violAll > for each k = s0 : : : sk; s:t:si 2 Si 8>violatedInT race ? >>>for each j 2 [0; k] do < if ( k; sj f 'c ^ :(:'dU 'o) = >) then violatedInT race >
violAll ^ violInT race do > > > >:violAll if violAll then ViolationProcedure()
Algorithm 5.1 mirrors for the monitor the construction of the set m( k) at moment k. Algorithm 5.2 relates to the de nition of violation detection, because the monitor checks whether in all indistinguishable traces up until now the norm is violated at some time point given nite LTL semantics. Note that in theory following proposition 7 a monitor needs to store a maximum the last jM j states of the trace, where jM j is the amount of monitors in the network. 6
We considered norms with obligations. The counterpart of obligations, prohibitions, can straightforwardly be used as well. Instead of checking for 'c ^ :(:'dU 'o), one would check for 'c ^ :(:'f U 'd), where 'f is a propositional formula denoting a forbidden state, and 'd is the deadline.
The presented algorithms for local monitors are prototypical and are designed to correspond with the de nition of delayed monitoring. Working with the set of possible states is often exponential in the number of atoms. For a better performance, the monitors could use a progression function as it is used in related work. Also the algorithms are made under the assumption that monitors are fully synchronized. In a MAS there is a high level of distribution so this assumption may not always be realizable in practice. However, many critical real life monitoring systems work with synchronization in order to be more predictable, and hence safer. It remains an important topic to see what happens if various assumptions are changed or dropped.
We will further develop our monitoring method by optimizing the algorithms for local monitors. This includes an analysis of which communication needs to take place given a speci cation of a decentralized monitor. Aside from runtime concerns, we also want to investigate how we can design e cient decentralized monitors. We saw in our example scenario that the delay with which violations are detected depends on which monitors monitor what norms. But a faster detection may require more communication.
The presented decentralized monitoring method is a step in a longer research endeavor where we aim to investigate di erent aspects of distributed organizations. For the near future we aim to connect this work to decentralized control of a multi-agent system, so that we have a complete picture of how norms can be enforced in distributed organizations.
With this we can continue to develop a practical framework for the design and development of distributed organizations. This in turn can be used to construct complex norm enforcement systems. Example target domains are service oriented architectures and large scale simulations based on autonomic computing and/or multi-agent systems. 7
We have presented a decentralized norm monitoring method. The proposal is to deploy a decentralized monitor that consists of a network of local monitors. Each of the local monitors has its own view on the environment state. Observations can be propagated among monitors in the network. We provided the formal tools to analyze a decentralized monitor and a prototype algorithm for how a local monitor can detect a norm violation.
Local monitors in our method maintain a set of possible environment traces based on their (possibly delayed) observations. If in all those traces a norm is violated, then it is guaranteed that the norm was also violated in the environment trace.The proposed method guarantees that the violation of a norm is detected within the time that is equal to the maximum propagation delay of observations between two monitors. With this decentralized monitoring method we continue our investigations in distributed organizations.