=Paper=
{{Paper
|id=Vol-1382/paper10
|storemode=property
|title=Protocols with Exceptions, Timeouts, and Handlers: A Uniform Framework for Monitoring Fail-Uncontrolled and
Ambient Intelligence Systems
|pdfUrl=https://ceur-ws.org/Vol-1382/paper10.pdf
|volume=Vol-1382
|dblpUrl=https://dblp.org/rec/conf/woa/AnconaBM15
}}
==Protocols with Exceptions, Timeouts, and Handlers: A Uniform Framework for Monitoring Fail-Uncontrolled and
Ambient Intelligence Systems==
https://ceur-ws.org/Vol-1382/paper10.pdf
Proc. of the 16th Workshop “From Object to Agents” (WOA15) June 17-19, Naples, Italy
Protocols with Exceptions, Timeouts, and Handlers:
A Uniform Framework for Monitoring
Fail-Uncontrolled and Ambient Intelligence Systems
Davide Ancona, Daniela Briola and Viviana Mascardi
Department of Informatics, Bioengineering, Robotics and System Engineering
University of Genova, Via Dodecaneso 35, 16146, Genova, ITALY
Email: {davide.ancona,daniela.briola,viviana.mascardi}@unige.it
Abstract—This paper describes an approach for designing, The basic mechanism for runtime verification that an event
formalizing and implementing sentinels that detect errors in which took place in the environment is compliant with the
fail-uncontrolled multiagent systems, and controllers that identify protocol has already been described in our previous works
particular situations in ambient intelligence (AmI) systems. The [9], [6], [12], where we presented a working framework for
formalism we use for representing the expected patterns of actions Jason [13], chosen as a paradigmatic example of logic-based
along with exceptions, timeouts, and their handlers, is that of
MAS language and framework, and for JADE [14], chosen
constrained global types extended with features for dealing with
these new constructs. We provide the syntax and semantics of because of its wide adoption both in academic and industrial
the extended constrained global types and examples of their use, environments.
in the different contexts of fail-uncontrolled and AmI systems. In this paper we describe the extensions to constrained
global types to cope with the newly introduced concepts such
I. I NTRODUCTION as events, timeouts etc, as described in Section III. Although
Multiagent protocols are usually intended as a means the updating of the existing and working prototypes for Jason
to regulate communicative interactions among agents. The [9] and JADE [6] to include these new features is still under
literature on agent interaction protocols is huge and despite way, we are confident on the positive outcomes of our efforts.
its long tradition dating back to the dawn of the research on In fact, we already implemented an SWI Prolog extended
agents and multiagent systems [1], [2], it is still a hot research interpreter that properly deals with these new features and
topic [3], [4], [5], [6], [7]. which is presented in Section III, and we tested it as a
standalone application (Section IV). The missing final step
In this paper we adhere to a general definition of protocols is to substitute the interpreter for monitoring MASs that is
as a means to define legal sequences or concurrent combina- already integrated on top of Jason (resp. JADE) with this
tions of actions without regard to the meanings of those actions new, enhanced interpreter. This requires to take care of minor
[8]: our protocols define patterns of actions in the environment, syntactic issues so it does not come completely for free, but
rather then just conversations. is should not even raise relevant technical problems.
The purpose of our research is to provide the multiagent We consider two different types of systems, fail-
system developer with a framework for designing, formalizing uncontrolled MASs and AmI systems, to prove the usability
and implementing the following monitoring agents on top of of constrained global types for representing patterns of events
existing agent environments: (that we also name situations when referred to AmI systems,
or protocols, coherently with the terminology used in the liter-
1) sentinels that detect errors in fail-uncontrolled multi- ature about security) that should drive the runtime monitoring
agent systems and activity of sentinels and controllers.
2) controllers that identify particular situations in ambi-
ent intelligence (AmI) systems. In fail-uncontrolled multiagent systems, the protocol mod-
eling the normal expected behavior of the MAS is explicitly
Despite the different contexts where sentinels and con- represented and involves events of any type (not limited
trollers are expected to operate, both must be able to monitor to communicative ones); sentinels observe the system under
the system’s behavior and to properly deal with failures and monitoring and execute user-defined, domain-dependent code
exceptional situations that may arise during the multiagent when a deviation from the expected behavior takes place.
system (MAS for short) functioning. Deviations are modeled as exceptions to the normal flow of
actions that the protocol models, and the user code must
The language we propose for formalizing the expected implement the exception handlers.
patterns of actions in the environment is that of constrained
global types [9], [10], [11] extended with features for dealing In AmI systems, where usually there is no explicit protocol
with exceptions, timeouts, and their handlers. These extensions driving the agents’ behavior, but rather agents are free to act as
are used to describe specific situations that must be managed they wish in any ambient, we only model particular situations
before they lead to an error or to a dangerous or unwanted that must be identified as soon as they arise: in this way we
situation. can respect the autonomy of agents and deal with unforeseen
65
Proc. of the 16th Workshop “From Object to Agents” (WOA15) June 17-19, Naples, Italy
events, but we are still able to check that specific situations are • fail-uncontrolled, where any type of failure
identified as “wrong” ones and their consequences are avoided. may occur.
By exploiting the abstraction of “event type” supported In such a context,
by constrained global types, we can model events which are
observed in the monitored system and that are relevant for a sentinel is an agent, and its mission is to guard
the monitored application, but also events which are not inter- specific functions or to guard against specific states
esting and hence should be discarded (uninteresting events). in the society of agents. The sentinel does not partake
Unexpected exceptions can be captured and managed as well. in domain problem solving, but it can intervene
if necessary, choosing alternative problem solving
Since sentinels and controllers are agents like any other
methods for agents, excluding faulty agents, alter-
one, they can be “part of the protocol” as well, hence being
ing parameters for agents, and reporting to human
both promoters and targets of the monitoring activities1 . For
operators. Being an agent, the sentinel interacts with
example, if the protocol states that – when an exception has
other agents using semantic addressing. Thereby it
been detected – the controller must always send a message to
can, by monitoring agent communication and by
the agent that caused it, and this does not happen, the controller
interaction (asking), build models of other agents.
can realize that it is violating the protocol and should repair
It can also use timers to detect crashed agents (or a
its own code.
faulty communication link) [18].
In order to avoid bottlenecks, the monitoring activities may
be distributed among many different and independent sentinels Exceptions can be informally defined as:
(resp. controllers), each observing a subset of the events based
[...] abnormal conditions that arise during the ex-
on their type, the location where they take place, or other
ecution of a process. The importance of exceptions
criteria. An approach for distributing the monitoring activity
stems from the simple fact that they are an essen-
by projecting the protocol onto subsets of agents involved in
tial feature of real-life processes. Businesses, for
it has been explored in [15].
example, entertain exceptional requests from cus-
The proposed approach is general enough to be imple- tomers in the interest of better customer service.
mented on top of any MAS or AmI framework where events Conversely, exceptions that occur in a process may
can be observed and translated into a suitable representation, lead to poor user satisfaction. Therefore, businesses
amenable for formal reasoning. must accommodate exceptions in their underlying
systems and their interactions with other businesses.
The paper is structured in the following way: Section II For concreteness, let us review a classification of
provides the background to this work. Section III describes exceptions proposed by Eder and Liebhart [19]:
the extension of constrained global types with exceptions,
timeouts, and their handlers. Section IV provides examples 1) Basic failures, which are system-level fail-
in different contexts. Section V concludes. ures such as network failures.
2) Application failures, such as database trans-
action failures.
II. BACKGROUND AND RELATED WORK 3) Expected exceptions, which are deviations
The classification of system failures and the definition of from the normal flow that occur infrequently
fail-uncontrolled system we refer to, is that provided in [16], but often enough to be incorporated into the
which in turn refers to [17]: process model.
4) Unexpected exceptions, which are not mod-
The most generally accepted failure classification eled and hence require a change in the de-
can be found in [17]: sign of the process when they are discovered.
1) A crash failure means a component stops An alternate classification of exceptions distin-
producing output; it is the simplest failure guishes among system level exceptions, program-
to contend with. ming language exceptions, and pragmatic excep-
2) An omission failure is a transient crash tions. Among these, pragmatic exceptions are the
failure: the faulty component will eventually most acute and the most difficult to handle [20].
resume its output production.
3) A timing failure occurs when output is pro- According to our analysis of the state of the art in fault
duced outside its specified time frame. tolerant multi-agent systems, we can distinguish two broad
4) An arbitrary (or byzantine) failure equates classes of approaches:
to the production of arbitrary output values
at arbitrary times. 1) approaches where the multiagent protocol is repre-
Given this classification, two types of failure models sented in an explicit way, and fault tolerance amounts
are usually considered in distributed environments: to handling exceptions due to a non-compliant behav-
ior w.r.t. the protocol [8], [20]; in such approaches,
• fail-silent, where the considered system al- multiagent protocols are usually limited to express
lows only crash failures, and constraints on communicative actions;
1 This “introspective” model can work only if sentinels and controllers 2) approaches where no protocol exists, and fault toler-
perform the very same monitoring activity whatever the agent being monitored, ance amounts to detecting crashed agents and repli-
including themselves. cate them in a transparent way [21], [16].
66
Proc. of the 16th Workshop “From Object to Agents” (WOA15) June 17-19, Naples, Italy
Our approach falls in the first category. III. M ULTIAGENT P ROTOCOLS WITH T IMEOUTS ,
E XCEPTIONS , AND H ANDLERS
With respect to AmI systems, the idea of implementing
them using an agent-based approach dates back to the late Our proposal is general enough to be applied to many
nineties. Among the very first projects in this area we may languages and environments for MASs. The only needed
mention the Intelligent Room project at MIT [22] that con- requirement is that some agents (the sentinels or controllers)
centrated on making the room responsive to the occupant by can be given the power and the capability to observe (some
adding intelligent sensors to the user interface, the ACHE of) the actions taking place in the environment.
system [23] which also aimed at energy saving and increased As far as sentinels are concerned, the four types of failure
personal comfort by learning the user preferences automati- identified in [17] are all resorted to a behavior that does not
cally by observing the behavior of the persons in the building, comply with the multiagent protocol:
and the work by Paul Davidsson and Magnus Boman [24]
who used multiagent principles to control building services, • a timing failure can be detected thanks to implicit
with agents that decompose systems by function rather than and explicit timeouts on the actions: if an expected
behavior. The synergy between ambient intelligence and intel- action does not take place within the given timeout,
ligent software agents has become stronger and stronger, and then a time failure takes place. More successive timing
nowadays there are tens of papers and projects in this area. failures may mean either an omission or a crash
Among the most relevant ones, we may mention [25], [26], failure;
[27]. The impressive growth in the last years [28], [29], [30], • a byzantine failure can be detected by verifying that
[31], [32] is also witnessed by the Multi-Agent Systems and the occurred action was (or was not) expected by the
Ambient Intelligence (MASAI) special track at the Practical protocol in the current state and time.
Applications of Agents and Multi-Agent Systems (PAAMS)
2014 and 2015 conferences. Sentinels implementation verifies at run-time that perceived
events are compliant with the protocol. This verification activ-
Among the most recent works in the MAS & AmI area, ity is necessary when the multiagent protocol is designed and
the closer to our proposal is [33]. That paper presents a the MAS is tested, but cannot guarantee any fault tolerance,
concrete software architecture dedicated to AmI features and as the output of the verification in any given time instant is
requirements. The proposed behavioral model, called Higher- just “yes” or “no”. In order to capture deviations from the
order Agent (HoA) captures the evolution of the mental repre- expected flow and manage them, so to possibly recover to some
sentation of the agent and the one of its plan simultaneously. acceptable state when the verification fails, the sentinel must
Plan expressions are written and composed using a formal pro-actively intervene by executing some recovery plan. We
algebraic language named AgLOTOS which is very similar to have designed the mechanism that allows a sentinel to capture
our formalism based on constrained global types although less the expected failures of the protocol by means of exceptions,
expressive because of the lack of concatenation and recursion. and the recovery intervention by means of exception handlers.
In [33], the planning process is improved with two new
services which provide a guidance for the mental process In this section we present the formalism of constrained
and a model checking approach to analyze some temporal global types introduced by Ancona, Mascardi et al. [9], [10],
properties over the agent plan. Both services are based on [11], extended to cope with any kind of observable event
a transition system called Contextual Planning Systems that, instead of only communicative actions and to model exceptions
similarly to the traces of our constrained global types, can and timeouts. Although never exploited, dealing with uninter-
represent the different execution traces the agent could perform esting events was already possible with the original versions
from a given HoA configuration, assuming the information of the formalism and hence does not represent a real extension
context of the HoA configuration holds. With AgLOTOS it is to it.
possible to handle actions and plans failures, as we do. The In the sequel, we will take the perspective of constrained
main differences between the approaches, besides the lower global types as a powerful means to specify multiagent pro-
expressive power of AgLOTOS w.r.t. the formalism that we tocols, but they can be used to specify AmI situations as
adopt, are that our approach is more general than the one well, and for the same reasons. For readability, we will avoid
discussed in [33] and it can be implemented on top of any repeating “or AmI situations”, but we emphasize that our
existing MAS framework, as the only requirement is that the assertions hold for them as well.
sentinels and controllers can observe events taking place in
the environment, but the approach based on AgLOTOS is in Intuitively, a constrained global type represents the state
a more mature development stage and has been experimented of an multiagent protocol from which several transition steps
on the field in a Smart-Campus Project. to other states (that is, to other constrained global types) are
possible, with a resulting event.
Finally, we may observe that our approach of supervising Exceptions are the mechanism we have introduced in order
the ongoing activities of the MAS, being it an AmI sys- to cope with byzantine failures, whereas timeouts are used to
tem or a more generic distributed open system, is similar detect and cope with omission, timing and crash failures.
to the “Monitoring by overhearing” approach presented in
[34], where an overhearing agent monitors the exchanged A. Syntax
communications between the system’s agents and uses the
observed communications to independently assemble and infer Event. An event e is any observable event taking place
the needed monitoring information. in the MAS environment, including communicative actions,
67
Proc. of the 16th Workshop “From Object to Agents” (WOA15) June 17-19, Naples, Italy
actions performed by agents, agent location and move, and place in the state of the protocol where the exception
actions performed by artifacts. We do not face the transduction type may be reached) whose type is illegal_move_exc,
problem and assume that events are translated into symbols and that must be handled by the code pointed to by
that agents can manipulate by some mediator between the entering_treasure_room_without_permission, with
agents and the environment. For the purposes of our work, argument A.
events are symbolic expressions.
Set timeout type. From a logical point of view, a set
Example 1: timeout type ST is a couple .
Example 2:
A timeout is set on occurrence of one event whose type
collect_parcel(agent2, parcel3, parcelweight(4, kg)). is specified as first element of the couple and causes two
alarms to be set and, later on, raised in an automatic way
The event “transport” is characterized by the involved by the system. The first alarm will be automatically raised
entities (the policeman and the prisoner, identified by their by the system after the delay timeout, unless an event tagged
names), the departure and arrival places and the means of with label l took place before, and will be handled using
transport. the associated “omission handler”. The second alarm will be
Event type. A “normal” event type η is a predicate on automatically raised by the system after the crash timeout,
events. Its interpretation is the set of events that verify η; we unless an event tagged with label l took place before. The
write e ∈ η to mean that η is true on e, and we also say that crash timeout must be greater than the delay timeout and will
e has type η. be handled using the associated “crash handler”.
The link between the two alarms set and the condition
Example 1: under which they should have no consequences on the system
behavior is given by the label l. In fact, if – after having set the
transport(policeman(marcus), prisoner(alice), from(jail),
to(room1), by(car)) ∈ move(alice, jail, room1).
alarms – an event is perceived and it matches a check timeout
(explained in the sequel) identified by the same label l, then it
means that the condition associated with the alarms has been
Example 2:
satisfied and they can be switched off.
collect_parcel(agent2, parcel3, parcelweight(4, kg))
∈ collect_parcel. From an implementation viewpoint, a set_timeout event
should save the information in the associated list for succes-
With respect to the actual event that took place in the sive retrieval using the label as a key. In our SWI-Prolog
environment and that was transduced into a symbolic form, prototype described in Section III-B, this is done by calling
the event type may abstract some details which are not the set_alarm predicate which, for each element in the list,
relevant for the sentinel monitoring activities (like in Example asserts it, computes the time when the two alarms should be
2), and can be identified by a different predicate with different raised based on the current time and the delay and crash
arguments (like in Example 1, where “move(...)” is the event timeouts, and generates the two awake events which will
type of “transport(...)” event). actually take place in the system at due time.
Example:
Exception type. An exception type E is – from a logical set_timeout( (first_move(A, _SomeRoom, key_room),0),
point of view – a quadruple . We represent
exceptions in a more compact way, as a couple whose second
element has the type of the exception as functor, and the When one event whose type is first_move(A,
pointer to the exception handler along with its arguments as _SomeRoom, key_room) takes place2 , two timeouts labeled
argument. with t1(A) together with their handlers are set:
An exception type is a way for stating that perceiving a • one whose expiration may be due to omission failures
specific event in the current state of the protocol represents an d(1000, handlerOmission(A)), meaning that if
exceptional situation and must be handled as such, calling an some check timeout event labeled with t1(A) will
ad-hoc piece of code. not take place within 1000 time units from the current
time, then the agent or component that should make
Example:
the condition associated with label t1(A) become true
(exception(move(A, key_room, treasure_room), will be considered delayed;
illegal_move_exc(
entering_treasure_room_without_permission(A)))).
2 The fact that the event type is represented as a couple
(first_move(A, _SomeRoom, key_room),0) with a 0
The events whose type is move(A, key_room, as second element means that the type is a “producer event type”. This notion
treasure_room) may raise an exception (if they take is introduced in the sequel.
68
Proc. of the 16th Workshop “From Object to Agents” (WOA15) June 17-19, Naples, Italy
• and one whose expiration may be due to crashes When one event typed with these awake types takes place,
c(2000, handlerCrash(A)), meaning that if the then the delay (resp. crash) handler defined when the timeout
check timeout events labeled with t1(A) will not take for t1(A) was set will be called in order to cope with the
place within 2000 time units from the current time, omission (resp. crash) failure.
then the agent or component that should make the
condition associated with label t1(A) become true
Uninteresting events. Events which are not interesting for
will be considered crashed.
the monitoring purposes can be tagged as uninteresting ones
just by exploiting the event type. For example, the following
When the timeout will expire, the corresponding event of type
definition of the has_type predicate states that all the actual
“awake” (explained later) will be generated by the sentinel,
events observed in the system which do not unify either with
and the handler will be used to manage the failure.
truck_at_dock(_, _, _), or with drop_parcel(_, _),
In this specific example, since the agent identity is part etc, have type uninteresting_event.
of the label itself, the agent whose delay or crash is under has_type(Event, uninteresting_event) :-
monitoring is A. As soon as A makes its first_move into /* must list explicitly all the interesting events, as
different (\=) from the current one */
the key_room, two countdowns start. If A does not ask the Event \= truck_at_dock(_, _, _),
key to the key_keeper (see example below) within 1000 Event \= drop_parcel(_, _),
Event \= move_to_free_shelf(_, _, _, _),
time units, he will be considered delayed. If he does not ask Event \= collect_parcel(_, _),
the key in 2000 time units, he will be considered crashed. Event \= move_to_truck(_, _, _, _).
Any multiagent protocol can be defined as the interesting
Check timeout type. A check timeout type CT is, from part of the protocol, interleaved with the uninteresting one.
an abstract point of view, a quadruple . As for the exception type, we
use a more compact representation as a term with its functor DISCARD = (uninteresting_event, 0): DISCARD
and arguments. meaning that a DISCARD constrained global type is defined
as an infinite sequence (sequence operator “:”) of uninteresting
events.
Example:
check_timeout((ask(A, key_keeper, key),0),timeout_exc(t1(A),
Producers and consumers. In order to model constraints
handlerEventWithDelay(ask(A, key_keeper, key))). across different branches of a constrained fork (explained
later in this section), we introduce two different kinds of event
types, called producers and consumers, respectively. Each
When one event of type ask(A, key_keeper, key)
occurrence of a producer event type must correspond to the
takes place, a check if it is on time or not is performed,
occurrence of a new event; in contrast, consumer event types
by retrieving the information associated with the label
correspond to the same event specified by a certain producer
t1(A). In our implementation, this means looking for a fact
event type. The purpose of consumer event types is to impose
previously asserted by set_alarm whose label unifies with
constraints on event sequences, without introducing new
t1(A). If the event is on time, the protocol is respected
events. A consumer is an event type η, whereas a producer is
and alarms associated with label t1(A) are switched off
an event type η equipped with a natural superscript n. In the
(namely, it is tagged as “done” and the awake events that
Prolog concrete syntax that we use, η n is represented by the
have been already generated by set alarm will have no
couple (η, n).
effect). If the event is not on time, then one or both alarms
associated with t1(A) have expired and the corresponding
handlers have been executed. Note that the crash handler Constrained global types. A constrained global type τ
is supposed to be executed when there is a high degree represents a set of possibly infinite sequences of events, and
of confidence that the expected event will not take place is defined on top of the following type constructors:
anymore. Since handlers could be generic ones, we leave
• λ (empty sequence): the singleton set {} containing
the developer the possibility to specify some further code,
the empty sequence .
handlerEventWithDelay(ask(A, key_keeper, key))
in this case, to be executed when the delayed event takes place. • η n :τ (seq-prod): the set of all sequences whose first
element is an event e matching type η (e ∈ η), and
the remaining part is a sequence in the set represented
Awake type. An awake event type AW is a couple . corresponding consumers that coincide with the same
It is automatically generated when the countdown event type η; hence, n is the required number of times
associated with a delay or crash alarm reaches 0. e ∈ η has to be “consumed” to allow a transition
labeled by e.
• η:τ (seq-cons): a consumer of event e matching type
Example: η (e ∈ η), and followed by any sequence in the set
awake_delay(t1(A)) (resp. awake_crash(t1(A))). represented by τ .
69
Proc. of the 16th Workshop “From Object to Agents” (WOA15) June 17-19, Naples, Italy
• τ1 + τ2 (choice): the union of the sequences of τ1 and infinite sequence of events e0 e1 . . . en . . . contained in ρ. The
τ2 . interpretation Jτ0 K of τ0 is the set {A(ρ) | ρ is a run for τ0 }.
A contractive constrained global type τ is deterministic if for
• τ1 |τ2 (fork): the set obtained by shuffling the se- e
any possible run ρ of τ and any possible τ 0 in ρ, if τ 0 → τ 00 ,
quences in τ1 with those in τ2 . e
and τ 0 → τ 000 , then Jτ 00 K = Jτ 000 K.
• τ1 · τ2 (concat): the concatenation of the sequences of
τ1 and τ2 . The next and empty predicates.
• The “meta-construct” fc (for finite composition) takes The next predicate implements the δ function defining the
τ , the constructor cn, and the positive natural number semantics of constrained global types extended with constructs
n as inputs and generates the “normal” constrained to deal with exceptions, timeouts and their handlers. Besides
global type (τ cn τ cn ... cn τ ) (n times, hence the definition of transition rules for “normal” constrained
fc(τ, cn, 1)=τ ). global types, in the sequel we describe the additional transition
rules for the new constructs introduced in this paper.
Constrained global types are regular terms, that is, can be
cyclic (recursive), and hence they can be represented by a Basic cases for “normal” constrained global types.
finite set of syntactic equations. To make the treatment simpler, If the constrained global type is a sequence (“:” operator)
we limit our investigation to contractive (a.k.a. guarded) and consisting of a producer event type EvType with associated
deterministic constrained global types. A constrained global number N, followed by the constrained global type T (second
type τ is contractive if all infinite paths3 in τ contain an argument), and the actual event perceived in the environment
occurrence of the “:” constructor. Determinism ensures that is Ev (third argument), and Ev has type EvType, then (Ev-
dynamic checking can be performed efficiently without back- Type,N):T can move to T (fourth argument). If there were no
tracking. Intuitively, a constrained global type is deterministic events of type EvType to be consumed (first argument of next
if, in case more transition rules can be applied when event e is zero), now N events of EvType are generated and must be
takes place, they lead to equivalent constrained global types. consumed (fifth argument of next is N, which is the number
The formal definition is given in the next section. associated with EvType in the second argument)
B. Semantics next(0,(EvType,N):T,Ev,T,N) :- has_type(Ev, EvType).
The state of a constrained global type τ can be represented
This rule is similar to the previous one, but the event type
by τ itself. In this section, when talking about constrained
EvType is a consumer (in fact, it has no number associated)
global types we will refer to their current state. Also, we will
and, if the actual event Ev perceived from the environment has
use “constrained global type” and “protocol” interchangeably.
type EvType, then EvType:T1 moves to T1 and the events of
The interpretation of a constrained global type is based on type EvType still to be consumed are decreased by one.
the notion of transition, a total function δ:N × CT × A →
Pfin (CT × N), where CT and A denote the set of contractive next(M,EvType:T1,Ev,T1,N) :-
EvType \= (_,_), has_type(Ev, EvType),
and constrained global type and of events, respectively. The M > 0, N is M - 1.
next/5 Prolog predicate discussed below implements the δ
transition function that we do not show in this paper for space If T1 can move to T2, then the choice between T1 and any
constraints. If τ1 represents the current state of the protocol other constrained global type, T1+ , can move to T2 (and the
and the event e takes place, then the protocol can move to τ2 converse for the second rule)
e
iff δ(0, τ1 , e) = (τ2 , 0), that we write as τ1 τ2 . next(M,T1+_,Ev,T2,N) :- next(M,T1,Ev,T2,N).
next(M,_+T1,Ev,T2,N) :- !, next(M,T1,Ev,T2,N).
Moving from the definition of δ to its Prolog implementa-
tion, the following relationship holds: If T1 can move to T3, then the interleaving between T1
δ(N, T 1, Ev) = (T 2, M ) iff next(N,T1,Ev,T2,M). and T2, T1|T2, can move to T3|T2 (and the converse for the
second rule)
The auxiliary function ( ), implemented by the empty/1
next(N,T1|T2,Ev,T3|T2,M) :- next(N,T1,Ev,T3,M).
Prolog predicate, specifies the constrained global types whose next(N,T1|T2,Ev,T1|T3,M) :- next(N,T2,Ev,T3,M).
interpretation contains the empty sequence . Intuitively, a
constrained global type τ s.t. (τ ) holds specifies a protocol If T1 can move to T3 and T2 can move to T4, and T1
that is allowed to successfully terminate. produces event types which can be consumed by T2, then T1
Let τ0 be a contractive and constrained global type. A run ρ and T2 can synchronize and T1|T2 can move to T3|T4 (and
e0 e1 en−1 en en+1 the converse for the second rule)
for τ0 is a sequence τ0 τ1 . . . τn τn+1 . . .
next(N,T1|T2,Ev,T3|T4,P) :-
such that (1) either the sequence is infinite, or it has finite next(N,T1,Ev,T3,M), M > 0, next(M,T2,Ev,T4,P).
length k ≥ 0 and the last constrained global type τk verifies next(N,T1|T2,Ev,T4|T3,P) :-
(τk ); and (2) for all τi , ei , and τi+1 in the sequence, !,next(N,T2,Ev,T3,M), M > 0, next(M,T1,Ev,T4,P).
ei
τi τi+1 holds. We denote by A(ρ) the possibly empty or If T1 can move to T3, then the concatenation T1*T2 can
3 By “path of a constrained global type” we mean “path in the possibly move to the concatenation T3*T2; if T1 contains , that is,
infinite tree corresponding to the term that represents the constrained global empty(T1) holds (second rule), then T1*T2 can move to T3 if
type”. T2 can move to T3
70
Proc. of the 16th Workshop “From Object to Agents” (WOA15) June 17-19, Naples, Italy
next(M,T1*T2,Ev,T3*T2,N) :- retract(timeout_setting(L, d(Delay, HandlDTimeExp), C)),
next(M,T1,Ev,T3,N). assert(timeout_setting(L, d(Delay, done), C)), !.
next(M,T1*T2,Ev,T3,N) :-
!,empty(T1), next(M,T2,Ev,T3,N). next(N,awake_crash(L):T,awake_crash(L),T,N) :-
timeout_setting(L, D, c(Crash, HandCTimeExp)),
HandCTimeExp \== done,
Rule for finite composition of constrained global types. call(HandCTimeExp),
retract(timeout_setting(L, D, c(Crash, HandCTimeExp))),
fc(T, T1, C, N) :- N>1, copy_term(T1, Fresh1), assert(timeout_setting(L, D, c(Crash, done))), !.
N1 is N-1, fc(T2, T1, C, N1), T =.. [C, Fresh1, T2].
fc(Fresh1, T1, _C, 1) :- copy_term(T1, Fresh1).
Code for setting the alarms.
Additional rule for dealing with exceptions.
set_alarm([]).
If the constrained global type is a sequence consisting of an
event of type EvType, which raises an exception to be handled set_alarm(
[timeout_setting(L, d(D, HandlDTimeExp),
with the Handler code, followed by T, and the actual event c(C, HandCTimeExp))|T]) :-
perceived in the environment is Ev, and Ev has type EvType, asserta(timeout_setting(L, d(D, HandlDTimeExp),
c(C, HandCTimeExp))),
then the Handler is executed and exception(EvType,Code):T get_time(CurrentTime), !,
moves to T. DT is CurrentTime + D,
CT is CurrentTime + C,
next(0, exception(EvType,Handler):T, Ev,T,0) :- generate_event(DT, awake_delay(L)),
has_type(Ev, EvType), call(Handler). generate_event(CT, awake_crash(L)),
set_alarm(T).
Additional rules for dealing with timeouts.
The empty predicate is true on the empty constrained
If the constrained global type is a sequence consisting of a global type lambda. If T 1 or T 2 contains , then T 1 + T 2
set timeout event with its parameters, followed by T, and the contains . If both T 1 and T 2 contain , then T 1|T 2 and
perceived event Ev has type EvType, then the alarm is set by T 1 ∗ T 2 contains .
calling the set alarm code. We do not show the rule dealing
empty(lambda) :- !.
with the case where EvType is a consumer event type rather empty(T1+T2) :- (empty(T1),!;empty(T2)).
than a producer. empty(T1|T2) :- !,empty(T1),empty(T2).
empty(T1*T2) :- !,empty(T1),empty(T2).
next(0,set_timeout((EvType,N), List):T, Ev,T,N) :-
has_type(Ev,EvType), set_alarm(List).
IV. E XAMPLES
If the constrained global type is a sequence consisting
of a check timeout event with its parameters, including the In all the examples of this paper, event types have the
label of the timeout handler to check and the Code to execute same syntax of the events they refer to, apart from the
if the timeout is expired, followed by T, and the perceived “uninteresting event” type which must be explicitly defined
event Ev has type EvType, then the actual time is retrieved as all the events which do not unify with an interesting event.
together with the timeout settings associated with label L. If This means that, apart from uninteresting ones, event e has
the timeout is expired, then Handler is executed, otherwise the event type e.
two alarms are switched off by setting their handlers to “done”.
The constrained global time moves to T. We do not show the A. Example 1: illegal moves
rule dealing with the case where EvType is a consumer event
type rather than a producer. This protocol states that, in order to enter the treasure room,
next(0,check_timeout((EvType,N), timeout_exc(L, Handler)):T,
an agent first moves to the key room, asks for the key of the
Ev,T,N) :- treasure room to the key keeper within 1000 secs, waits for
has_type(Ev, EvType), get_time(CurrentTime), an acceptance, enters the treasure room and then exits it. If
timeout_setting(L, d(Delay, _HandlDTimeExp), _C),
(CurrentTime > Delay ->
the key keeper refuses to give the key, the agent must exit the
call(Handler); key room. One exception to this normal flow is that from an
(retract(timeout_setting(L, d(Delay, _), c(Crash, _))), external room (we do not care which one) the agent enters the
assert(timeout_setting(L, d(Delay, done), c(Crash,
done)))) treasure room with some trick without asking the permission
). to the key keeper and without waiting for the key. In this case,
an exception is raised and the exception handler associated
If the constrained global type is a sequence consisting of with this “illegal move” exception must be executed. Among
an awake delay event with a label L as argument, followed the actions implemented by the handler, some will be executed
by T, and the perceived event is awake delay(L) which is (and consequently monitored too) by the sentinel. In particular,
automatically generated when a timeout expires, then the code the sentinel will sanction the agent, which will be transported
associated with that awake event is executed and this fact out of the treasure room, and in jail. After some time, the agent
is recorded by setting the handler to “done” for avoiding will be set free again. Note that here, the sentinel monitors
successive re-executions. The constrained global time moves one of its actions, sanction(sentinel, A), implementing
to T. a form of introspection.
next(N,awake_delay(L):T,awake_delay(L),T,N) :- The last line of the protocol models the case when the event
timeout_setting(L, d(Delay, HandlDTimeExp), C),
HandlDTimeExp \== done, that has been sensed is unknown. If the unknown_event(A)
call(HandlDTimeExp), event type holds on all the events that the sentinel is not able
71
Proc. of the 16th Workshop “From Object to Agents” (WOA15) June 17-19, Naples, Italy
to manage, then this exception will be thrown whenever the move(alice, key_room, treasure_room),
sentinel is facing an unexpected exception. The handler can be sanction(sentinel, alice),
transport(alice, treasure_room, key_room),
some general code trying to ensure the vital functions of the transport(alice, key_room, jail),
system even if the normal flow has some fail. transport(alice, jail, room1)
T = ((set_timeout((move(A, _SomeRoom, key_room),0), move(alice, room1, treasure_room),
[timeout_setting( sanction(sentinel, alice),
t1(A), transport(alice, treasure_room, key_room),
d(1000, handlerDTimeoutExpiration(A)), transport(alice, key_room, jail),
c(2000, handlerCTimeoutExpiration(A)))]): transport(alice, jail, room1),
((check_timeout((ask(A, key_keeper, key),0), move(alice, room1, key_room)
timeout_exc(
t1(A),
handlerEventWithDelay(ask(A, key_keeper, key)))):
( B. Example 2: dock loading and unloading
((accept(key_keeper, A, key),0):(give(key_keeper, A,
key),0): This example is a simplified version of the scenario de-
(move(A, key_room, treasure_room),0):(move(A, scribed in [35]:
treasure_room, key_room),0):
+
(give(A, key_keeper:key),0):lambda) In the loader dock several workers wander around
((refuse(key_keeper, A, key),0): or carry parcels between incoming trucks and the
(move(A, key_room, _AnotherRoom),0):lambda) shelves. Their job is to unload parcels from a
)*T)
+
full truck, or to deliver parcels to an empty one,
((exception(move(A, _SomeRoom, treasure_room), whenever trucks arrive at the store. The dock itself
illegal_move_exc( contains shelves where parcels can be placed tem-
entering_treasure_room_without_permission(A)))):
(sanction(sentinel, A),0):(transport(A, treasure_room, porally. The shelves are separated by corridor ways,
key_room),0): which are used by workers to transport the parcels.
(transport(A, key_room, jail),0):(transport(A, jail,
_AnyRoom),0):lambda)
... When a worker makes an intention to move
) somewhere, it communicates this intention to other
) ones for the purpose of coordination. A trajectory of
+
((exception(unknown_event(A), unknown_event_exc(A))):lambda
the movement, described by points and exact time-
)). values, is sent to each worker, so it can update its
beliefs about future changes in the environment. This
Now we show some events traces compliant with the information is stored in a domain time model repre-
protocol, generated using SWI Prolog implementing the next senting the beliefs concerning prospective workers’
predicate defined in Section III and the accept predicate that positions. This information guides the planning pro-
accepts (or generates, if the free variables can be grounded cess of each worker, so none of them intersects a
when has_type is called) sequences of events with a given path of another.
length N, which respect the constrained global type T. By using
In this example we assume that workers and trucks are
the findall builtin predicate on accept, we were able to
represented as agents, which are free to execute many actions
generate all the accepted traces of a given length.
including those related to the work in the dock loader. The
accept(N,T,[*]) :- empty(T), N==0,!. next code manages a simplification of the described example,
accept(0,_,[]) :- !.
accept(N,T1,[Ev|L]) :- without monitoring for example that agents will not crash
next(0,T1,Ev,T2,0), M is N-1, accept(M,T2,L). while moving: its aim is to give a flavor of how we can use the
uninteresting events to specify only the subset of the actions
Correct traces with length 6 include: that are relevant for the controller.
move(alice, room1, key_room), The protocol starts when a Truck arrives at the dock
ask(alice, key_keeper, key),
accept(key_keeper, alice, key), (UNLOAD_TRUCK), carrying NumberOfParcels parcels, which
give(key_keeper, alice, key), must be unloaded (so, after this event, the protocol moves on
move(alice, key_room, treasure_room), with UNLOAD_ALL_PARCELS, that is created repeating the trace
move(alice, treasure_room, key_room)
UNLOAD_PARCEL for each parcel in a parallel way using the |
move(alice, room1, key_room), constructor). The protocol part identified by UNLOAD_PARCEL
ask(alice, key_keeper, key),
refuse(key_keeper, alice, key),
states that the correct sequence is that firstly an agent comes
move(alice, key_room, room1), to the Truck position, then it collects a parcel, moves to a
move(alice, room1, key_room), free shelf and leaves there the parcel.
ask(alice, key_keeper, key)
We model the positions inside the dock as couples of
move(alice, room1, key_room),
ask(alice, key_keeper, key), points, and the time slots as couples of minutes.
refuse(key_keeper, alice, key),
move(alice, key_room, room2), To model the fact that we are only interested in monitoring
move(alice, room2, key_room), the events specified in the previous traces, but not the others
ask(alice, key_keeper, key)
(that is, if one event that is not related to this protocol takes
place during the protocol, it is not a violation of it!), we
Some traces with length 6 where an exception is found and add in the trace UNLOAD_TRUCK a fork (| operator) with
the sentinel sanctions alice are: DISCARD, so that any event of type uninteresting_event,
move(alice, room1, key_room), at any time, is caught by the trace DISCARD (that simply
72
Proc. of the 16th Workshop “From Object to Agents” (WOA15) June 17-19, Naples, Italy
skips that event and waits for the next one). The type SAFETY_CHECK =
uninteresting_event is defined differently from all the (
(
other events: an uninteresting_event is whatever event ((counted_more_than_1000_visitors,0):
that is not move_to_truck, collect_up_parcel, and so lambda)
|
on. ((temperature_higher_than_30_celsius,0):
UNLOAD_PARCEL = lambda)
(move_to_truck(Agent, _FromPosition, TruckPosition, )
_TimeSlot),0): *
(collect_parcel(Agent, P),0): (
(move_to_free_shelf(Agent, TruckPosition, _FreeShelfPosition ((air_conditioning_off,0):
, _SuccTimeSlot),0): (switch_air_conditioning_on,0):
(drop_parcel(Agent, P),0): lambda
lambda, )
fc(UNLOAD_ALL_PARCELS, UNLOAD_PARCEL, |, NumberOfParcels), +
UNLOAD_TRUCK = ((air_conditioning_on,0):
(((truck_at_dock(_TruckId,TruckPosition,NumberOfParcels) (do_not_admit_other_visitors,0):
,0): lambda
UNLOAD_ALL_PARCELS)| )
DISCARD), )
DISCARD = (uninteresting_event, 0): DISCARD. )
*
SAFETY_CHECK,
An example of a trace (including events not interesting AC = (SAFETY_CHECK | DISCARD),
for the protocol) which is recognized as compliant with the DISCARD = (uninteresting_event, 0): DISCARD.
protocol is:
snoring(a1), Some examples of traces which are recognized as compliant
truck_at_dock(truck1, (0, 0), NumberOfParcels), with the protocol are:
move_to_truck(a1, (6, 21), (0, 0), (10, 15)),
collect_parcel(a1, p1), counted_more_than_1000_visitors,
move_to_truck(a2, (12, 3), (0, 0), (15, 18)), temperature_higher_than_30_celsius,
snoring(a1), air_conditioning_on,
smiling(a1), do_not_admit_other_visitors.
move_to_free_shelf(a1, (0, 0), (54, 3), (15, 22)),
drop_parcel(a1, p1), counted_more_than_1000_visitors,
move_to_truck(a1, (54, 3), (0, 0), (10, 15)), temperature_higher_than_30_celsius,
collect_parcel(a2, p2), air_conditioning_off,
snoring(a2), switch_air_conditioning_on
dancing_tiptap(a1),
move_to_free_shelf(a2, (0, 0), (43, 78), (18, 21)), temperature_higher_than_30_celsius,
drop_parcel(a2, p2), concert_begins,
move_to_truck(a1, (4, 9), (0, 0), (30, 35)), counted_more_than_1000_visitors,
collect_parcel(a1, p3), air_conditioning_off,
move_to_truck(a3, (44, 9), (0, 0), (31, 37)), switch_air_conditioning_on
collect_parcel(a3, p4),
move_to_free_shelf(a3, (0, 0), (6, 24), (37, 49)),
drop_parcel(a3, p4),
move_to_free_shelf(a1, (0, 0), (1, 24), (35, 43)), In this case the constrained global type is used to con-
drop_parcel(a1, p3), trol that if a specific situation happens (visitors > 1000
snoring(truck), and temperature > 30, with events perceived in any order),
smiling(truck),
drinking_a_beer(truck) some specific action (do_not_admit_other_visitors or
switch_air_conditioning_on) is taken.
whereas the following trace is not compliant because parcel
p1, collected up by agent a1 (third event), is dropped by agent
a4 (fourth event) instead of being dropped by a1. V. C ONCLUSIONS
truck_at_dock(truck1, (0, 0), NumberOfParcels), In this paper we described an approach for designing,
move_to_truck(a1, (6, 21), (0, 0), (10, 15)),
collect_parcel(a1, p1),
formalizing and implementing sentinels that detect errors
drop_parcel(a4, p1). in fail-uncontrolled multiagent systems, and controllers that
identify particular situations in AmI systems. Our approach
– like all the approaches aimed at runtime verification of
C. Example 3: air conditioning system properties – requires that a formal representation of
The last example relates to the AmI context, where we the system property (a MAS protocol in our case) is available.
assume to manage a building for social events (concerts, We used constrained global types extended with constructs for
workshops and so on): in this building there are many rooms, modeling exceptions, timeouts, and handlers as representation
and we would add some intelligence to the system itself, formalism. We implemented the SWI Prolog interpreter for this
specifying some rules that should be respected in the building. formalism and we run different tests in different application
In particular, if there are more then 1000 visitors and the tem- domains.
perature inside the building is >30, then if the air conditioning
Representing a protocol using our formalism may not be
is closed, it must be switched on, otherwise, no more visitors
trivial, but the more expressive is the formalism, the more
can enter the building.
difficult is using it. When used for runtime verification, our
This situation is (partially) described by the constrained formalism is more expressive than linear time temporal logic
global type AC: (LTL [36]) because it can represent a protocol like an bn which
73
Proc. of the 16th Workshop “From Object to Agents” (WOA15) June 17-19, Naples, Italy
cannot be expressed using LTL4 . For this reason it should not different controllers the supervision of those parts of the MAS,
be surprising that our formalism is more complex than, for we have not solved the problem of how to identify the best
example, LTL. protocol distribution, which is not even always possible. In a
similar way, the decision of what to do in case of a failure is
There are however many benefits in using such a formal-
demanded to the protocol formalization or to the actual agent
ism:
code, and is out of the scope of our work.
• having a protocol formalization can help testing the As part of our future work, we are investigating how
MAS itself, since our Prolog translation can be ex- expressing more complex behaviors when specifying timeout,
ploited to generate and test correct, an not correct, and how managing timeouts related to the same agent. From a
simulations of the system, and constrained global more theoretical point of view, the relationships between our
types have already been proven a powerful language, formalism and timed linear time temporal logic [37] should be
able to model complex protocols (as shown in [12]); deeply analyzed.
• in AmI systems, controllers can be added on top of
the already existing agents, as an independent layer, ACKNOWLEDGMENT
improving the modularity of the overall system and
simplifying the design, development and maintenance This work has been partially supported by the MIUR PRIN
phases while, in fail-uncontrolled MASs, sentinels may Project CINA: Compositionality, Interaction, Negotiation, Au-
help to identify and recover from error situations by tonomicity for the future ICT society, prot. 2010LHT4KM.
separating the errors management from the normal
protocol flow; R EFERENCES
• the basic version of our approach, without the ex- [1] Y. Demazeau, “From interactions to collective behaviour in agent-
based systems,” in In Proceedings of the 1st European Conference on
tensions discussed in this paper, works for JADE Cognitive Science. Saint-Malo, 1995, pp. 117–132.
and Jason, two among the most used platforms for [2] M. Barbuceanu and M. S. Fox, “COOL: A language for describing
MAS development; the transition rules providing the coordination in multi agent systems,” in Proceedings of the First
semantics of the improved formalism presented in this International Conference on Multiagent Systems, June 12-14, 1995, San
paper have been already translated into Prolog, the Francisco, California, USA, V. R. Lesser and L. Gasser, Eds. The MIT
language we used for implementing our approach on Press, 1995, pp. 17–24.
top of JADE and Jason, so we claim that extending the [3] Y. Abushark, J. Thangarajah, T. Miller, and J. Harland, “Checking con-
sistency of agent designs against interaction protocols for early-phase
JADE and Jason prototypes with exceptions, timeouts, defect location,” in Proceedings of the 2014 international conference on
and handlers should raise no technical problems; Autonomous agents and multi-agent systems. International Foundation
for Autonomous Agents and Multiagent Systems, 2014, pp. 933–940.
• the extensions presented in this paper enhance the
[4] M. Baldoni, C. Baroglio, and F. Capuzzimati, “Typing multi-agent sys-
“MAS control layer” with the possibility to manage tems via commitments,” in Engineering Multi-Agent Systems. Springer,
both MASs where a predefined global protocol does 2014, pp. 388–405.
not exist (AmI systems) and MASs where errors may [5] F. Al-Saqqar, J. Bentahar, K. Sultan, and M. El Menshawy, “On the
arise and must be formalized and managed in a interaction between knowledge and social commitments in multi-agent
controlled way. systems,” Applied intelligence, vol. 41, no. 1, pp. 235–259, 2014.
[6] D. Briola, V. Mascardi, and D. Ancona, “Distributed runtime verification
The formalism that we have discussed in this paper seems of JADE multiagent systems,” in Intelligent Distributed Computing
suitable for being integrated into a sensor network in order VIII - Proceedings of the 8th International Symposium on Intelligent
to capture what happens in the environment, as we did in Distributed Computing, IDC 2014, Madrid, Spain, September 3-5, 2014,
ser. Studies in Computational Intelligence, D. Camacho, L. Braubach,
[12]. Thanks to its modularity it could be used to monitor S. Venticinque, and C. Badica, Eds., vol. 570. Springer, 2014, pp. 81–
and supervise environments where physical agents (robots) 91. [Online]. Available: http://dx.doi.org/10.1007/978-3-319-10422-5
can fail leading to exceptional situations and need to be either 10
reconfigured or replaced at runtime. [7] D. Ancona, D. Briola, A. Ferrando, and V. Mascardi, “Global protocols
as first class entities for self-adaptive agents,” in Proceedings of the
The feasibility of the approach is limited to situations 14th International Conference on Autonomous Agents and Multiagent
where a formal representation of entities, messages and in Systems (AAMAS 2015), May 4–8, 2015, Istanbul, Turkey, R. Bordini,
general events, exists: so, when considering dynamic and E. Elkind, G. Weiss, and P. Yolum, Eds. IFAAMAS/ACM, 2015.
open large-scale MASs as those in AmI and wireless sensor [8] P. Yolum and M. P. Singh, “Reasoning about commitments in the event
calculus: An approach for specifying and executing protocols,” Ann.
networks, we assume that all the agents that can join the Math. Artif. Intell., vol. 42, no. 1-3, pp. 227–253, 2004.
MAS (maybe developed by third parties), are foreseen in the [9] D. Ancona, S. Drossopoulou, and V. Mascardi, “Automatic Generation
formalization. Our work is meant to provide a set of tools and of Self-Monitoring MASs from Multiparty Global Session Types in
languages for monitoring distributed systems, without claiming Jason,” in DALT X. Revised, Selected and Invited Papers, ser. LNAI,
to be able to solve all the related problems. vol. 7784. Springer, 2012.
[10] D. Ancona, M. Barbieri, and V. Mascardi, “Constrained global types
For example, although we can automatically project the for dynamic checking of protocol conformance in multi-agent systems,”
protocol onto subsets of agents (it means that the protocol 2013, sAC 2013. ACM.
itself can be split into separated parts) and then allocate to [11] V. Mascardi and D. Ancona, “Attribute global types for dynamic
checking of protocols in logic-based multiagent systems (technical
4 The protocol where one agent sends n messages of type a to another communication),” 2013, to appear in Theory and Practice of Logic
agent (with n that can be any positive number) and the receiver answers with Programming, On-line Supplement, as technical communication of the
n messages of type b. ICLP 2013 conference.
74
Proc. of the 16th Workshop “From Object to Agents” (WOA15) June 17-19, Naples, Italy
[12] V. Mascardi, D. Briola, and D. Ancona, “On the expressiveness of [25] H. Hagras, V. Callaghan, M. Colley, G. Clarke, A. Pounds-Cornish,
attribute global types: The formalization of a real multiagent system and H. Duman, “Creating an ambient-intelligence environment using
protocol,” in AI*IA 2013: Advances in Artificial Intelligence - XIIIth embedded agents,” IEEE Intelligent Systems, vol. 19, no. 6, pp. 12–20,
International Conference of the Italian Association for Artificial Intel- 2004. [Online]. Available: http://doi.ieeecomputersociety.org/10.1109/
ligence, Turin, Italy, December 4-6, 2013. Proceedings, ser. Lecture MIS.2004.61
Notes in Computer Science, M. Baldoni, C. Baroglio, G. Boella, and [26] F. Doctor, H. Hagras, and V. Callaghan, “A fuzzy embedded agent-
R. Micalizio, Eds., vol. 8249. Springer, 2013, pp. 300–311. [Online]. based approach for realizing ambient intelligence in intelligent inhabited
Available: http://dx.doi.org/10.1007/978-3-319-03524-6 26 environments,” IEEE Transactions on Systems, Man, and Cybernetics,
[13] R. H. Bordini, J. F. Hübner, and M. Wooldridge, Programming Multi- Part A, vol. 35, no. 1, pp. 55–65, 2005. [Online]. Available: http://dx.
Agent Systems in AgentSpeak Using Jason. John Wiley & Sons, 2007. doi.org/10.1109/TSMCA.2004.838488
[14] F. L. Bellifemine, G. Caire, and D. Greenwood, Developing Multi-Agent [27] C. Ramos, J. C. Augusto, and D. Shapiro, “Ambient intelligence
Systems with JADE. Wiley, 2007. - the next step for artificial intelligence,” IEEE Intelligent Systems,
[15] D. Ancona, D. Briola, A. El Fallah Seghrouchni, V. Mascardi, and vol. 23, no. 2, pp. 15–18, 2008. [Online]. Available: http://doi.
P. Taillibert, “Efficient verification of MASs with projections,” in ieeecomputersociety.org/10.1109/MIS.2008.19
Engineering Multi-Agent Systems - Second International Workshop, [28] J. M. Gascueña, E. Navarro, P. Fernández-Sotos, A. Fernández-
EMAS 2014, Revised Selected Papers, ser. Lecture Notes in Computer Caballero, and J. Pavón, “Idk and icaro to develop multi-agent systems
Science, F. Dalpiaz and J. D. M. B. van Riemsdijk, Eds., vol. 8758, in support of ambient intelligence,” Journal of Intelligent and Fuzzy
2014, pp. 246–270. Systems, 2014.
[16] N. Faci, Z. Guessoum, and O. Marin, “DimaX: A fault-tolerant [29] M. Villaverde, D. Perez, and F. Moreno, “Cooperative learning model
multi-agent platform,” in EUMAS, ser. CEUR Workshop Proceedings, based on multi-agent architecture for embedded intelligent systems,” in
B. Dunin-Keplicz, A. Omicini, and J. A. Padget, Eds., vol. 223. CEUR- Industrial Electronics Society, IECON 2014-40th Annual Conference of
WS.org, 2006. the IEEE. IEEE, 2014, pp. 2724–2730.
[17] D. Powell, Ed., Delta-4: A Generic Architecture for Dependable Dis- [30] A. Olaru, “Context-awareness in multi-agent systems for ambient intel-
tributed Computing (Research Reports Espirit Project 818/2252, Delta ligence,” in Context in Computing. Springer, 2014, pp. 541–556.
4, Vol. 1), 1992. [31] M. Ruta, F. Scioscia, G. Loseto, and E. Di Sciascio, “Semantic-based
[18] S. Hägg, “A sentinel approach to fault handling in multi-agent systems,” resource discovery and orchestration in home and building automation:
Second Australian Workshop on Distributed Artificial Intelligence, a multi-agent approach,” Industrial Informatics, IEEE Transactions on,
Cairns, QLD, Australia, August 27, 1996, vol. s. 181-95, 1997. vol. 10, no. 1, pp. 730–741, 2014.
[19] J. Eder and W. Liebhart, “The workflow activity model WAMO,” in [32] A. Freitas, D. Schmidt, A. Panisson, R. H. Bordini, F. Meneguzzi,
Proc. 3rd Int. Conf. Cooperative Inf. Syst., 1995, pp. 87–98. and R. Vieira, “Applying ontologies and agent technologies to generate
[20] A. U. Mallya and M. P. Singh, “Modeling exceptions via commitment ambient intelligence applications,” in Agent Technology for Intelligent
protocols,” in AAMAS, F. Dignum, V. Dignum, S. Koenig, S. Kraus, Mobile Services and Smart Societies. Springer, 2015, pp. 22–33.
M. P. Singh, and M. Wooldridge, Eds. ACM, 2005, pp. 122–129. [33] A. Chaouche, A. E. Fallah-Seghrouchni, J. Ilié, and D. Saı̈douni,
[21] Z. Guessoum, M. Ziane, and N. Faci, “Monitoring and organizational- “A higher-order agent model with contextual planning management
level adaptation of multi-agent systems,” in AAMAS. IEEE Computer for ambient systems,” T. Computational Collective Intelligence, vol.
Society, 2004, pp. 514–521. 8780, pp. 146–169, 2014. [Online]. Available: http://dx.doi.org/10.1007/
978-3-662-44871-7 6
[22] M. H. Coen, “Design principles for intelligent environments,” in Pro-
ceedings of the Fifteenth National Conference on Artificial Intelligence [34] G. Gutnik, “Monitoring large-scale multi-agent systems using overhear-
and Tenth Innovative Applications of Artificial Intelligence Conference, ing,” in Proceedings of the Fourth International Joint Conference on
AAAI 98, IAAI 98, July 26-30, 1998, Madison, Wisconsin, USA., Autonomous Agents and Multiagent Systems, ser. AAMAS ’05. New
J. Mostow and C. Rich, Eds. AAAI Press / The MIT Press, 1998, pp. York, NY, USA: ACM, 2005, pp. 1377–1377. [Online]. Available:
547–554. [Online]. Available: http://www.aaai.org/Library/AAAI/1998/ http://doi.acm.org/10.1145/1082473.1082785
aaai98-077.php [35] A. Walczak, L. Braubach, A. Pokahr, and W. Lamersdorf, “Augmenting
[23] M. C. Mozer, “The neural network house: An environment that adapts bdi agents with deliberative planning techniques,” in Proceedings of the
to its inhabitants,” in Proc. Am. Assoc. Artificial Intelligence Spring 4th International Conference on Programming Multi-agent Systems, ser.
Symp. Intelligent Environments. AAAI Press, 1998, pp. 110–114. ProMAS’06. Berlin, Heidelberg: Springer-Verlag, 2007, pp. 113–127.
[Online]. Available: http://dl.acm.org/citation.cfm?id=1759324.1759334
[24] P. Davidsson and M. Boman, “Saving energy and providing value added
services in intelligent buildings: A MAS approach,” in Agent Systems, [36] A. Pnueli, “The temporal logic of programs,” in FOCS, IEEE, Ed.,
Mobile Agents, and Applications, Second International Symposium on 1977, pp. 46–57.
Agent Systems and Applications and Fourth International Symposium [37] J.-F. Raskin, “Logics, automata and classical theories for deciding real-
on Mobile Agents, ASA/MA 2000, Zürich, Switzerland, September 13- time,” Ph.D. dissertation, Namur, Belgium, 1999.
15, 2000, Proceedings, ser. Lecture Notes in Computer Science, D. Kotz
and F. Mattern, Eds., vol. 1882. Springer, 2000, pp. 166–177. [Online].
Available: http://dx.doi.org/10.1007/978-3-540-45347-5 14
75