2.1 BotTeam example

We will use a simple, yet nontrivial running example, called BotTeam, to illustrate the $\textsf{SA}$ machinery throughout the paper. The BotTeam case study was designed to explore simple coordination in the presence of faults. Here we describe the protocol that the agents should follow informally and introduce the model specific components for the BotTeam. Experiments applying fault models and diagnostics will be summarized in Section 9.

The BotTeam consists of two bots with different roles, an initializer, called $\textsf{BotI}$ , and a finisher, called $\textsf{BotF}$ . The high-level specification of the BotTeam case study involving two bots is depicted in Figure 1. Both bots are given a set of locations that requires treatment, e.g., some maintenance work. A treatment consists of a sequence of 4 treatment stages/steps, the first two done by $\textsf{BotI}$ , and the last two stages by $\textsf{BotF}$ .

Figure 1.

The mode automaton for the two bot classes: $\textsf{BotI}$ , the initializer, an $\textsf{BotF}$ , the finisher. In both cases, the starting state is the $\textsf{ready}$ state.

More precisely, $\textsf{BotI}$ starts in the $\textsf{ready}$ mode. It moves to mode $\textsf{enroute(tgt)}$ by selecting one location target, $\textsf{tgt}$ , that needs treatment. Once the target location is reached, $\textsf{BotI}$ moves to $\textsf{treat}$ mode and carries out the first two stages of the treatment. When all target locations are treated, $\textsf{BotI}$ enters the mode $\textsf{enroute(home)}$ , heads back to the home station, and once reached enters mode $\textsf{done}$ . $\textsf{BotF}$ follows the same modes of operation as $\textsf{BotI}$ . A difference is that $\textsf{BotF}$ requires supplies in order to carry out its treatments. Therefore, whenever the supply is low, then $\textsf{BotF}$ returns to the depot to re-supply. We also assume, not explicitly shown in the mode automation, that the bots also divert to the charging station whenever their battery level reaches dangerously low level.

Examples of protocol deviations that can be formalized using our machinery include

• — Wrong Order Treatment Deviation: $\textsf{BotF}$ carries out a treatment on a target that was not previously treated by $\textsf{BotI}$ ;

• — Delay Between Treatment Deviation: $\textsf{BotI}$ and $\textsf{BotF}$ treat a target at times $t_I$ and $t_F$ , respectively, such that $t_F > t_I + \Delta$ , for some $\Delta > 0$ , i.e., $\textsf{BotF}$ treated a target too late.

• — Treatment without Supply Deviation: $\textsf{BotF}$ attempts a treatment without actually having the necessary supplies.

• — Low Energy Deviation: $\textsf{BotI}$ or $\textsf{BotF}$ have energy too low to enable them to return to the charging station to re-charge.

Notice that deviations may involve timing aspects, as in Delay Between Treatment Deviation, or quantitative values, as in Low Energy Deviation and Treatment without Supply Deviation. In the following, we will focus on delay and energy deviations.

To carry out the assigned task of treating target and avoid deviations, the bots make use of their sensors. We assume that each bot has the following sensors: Location Sensor: This sensor reports the location of the bot. Energy Sensor: This sensor reports the current energy level of the bot. Supply Sensor: This sensor reports the current level of supplies available. (This is only used by $\textsf{BotF}$ .) Treatment Sensor: This sensor reports whether a target has been treated and up to which stage. Obstacle Sensor: This sensor reports locations of obstacles if any, e.g., a bot at an adjacent/close location. These sensors may be faulty. For example, the location sensor may provide a location reading that does not correspond to the actual location of a bot. This means that the information used by bot to decide how to act may be incorrect, and therefore, the bot does not act as specified by the expected behavior, resulting in a deviation.

4.1 Basic sorts and functions

Soft agents uses the following basic sorts:

Id is the sort of identifiers, used to identify agents, and other objects. Each model is responsible for defining its own Id constructors. The BotTeam Id constructors are b(i:Nat) (bots), st(i:Nat) (stations), dp(i:Nat) (depots), and ob(i:Nat) (obstacles). A constant eI of sort Id is declared to name the unique environment object in a system configuration.

Time is the sort used to represent time. The soft agents framework provides a variety of time modules to choose from, including discrete (natural numbers) or dense (rationals or reals) time representations. In the current soft agents framework instances, we use discrete time represented using the sort Nat of natural numbers.

The sort Loc is an interface sort at the framework level. There is a constant noLoc indicating an unknown location. In the Bot example, locations are points on a two-dimensional grid using the following sorts and constructors: sort Pt2 . subsort Pt2 < Loc . op pt : Nat Nat -> Pt2 [ctor] .

For example, pt(2,1) specifies the location (2,1) on a two-dimensional grid.

Class is the sort of object classes.

A KB (sort KB) is a set of knowledge items (sort KItem). There are two (sub)sorts of knowledge items, persistent (sort PKItem), and transient (sort TKItem). Transient knowledge items are time stamped information items of the form info:Info @ t:Time where terms info:Info are expected to have parameters that change over time. Persistent knowledge items model properties that do not vary over time and thus are not time stamped. There is a distinguished knowledge item clock(t:Time) that represents the current time. For example, clock(10) represents that 10 time units have passed since the starting time 0. There are two additional built in knowledge item terms. class(id:Id,cl:Class) says that the class of the entity (agent or other object) with identifier id:Id is cl:Class. It has sort PKItem as the class is not expected to change. For example, class(b(0),BotI) says that the entity with identifier b(0) is an initializer bot, BotI. The term atloc(id:Id,l:Loc) @ t:Time denotes that the entity with identifier id:Id is at location l:Loc at time t:Time. It has sort TKItem since in the case of a mobile entity l:Loc changes as the agent moves.

The local knowledge base (lkb) of a particular agent and the environment knowledge base (ekb) are of the sort KB. The former specifies the agent’s view of the world, obtained from its possibly faulty sensors, while the latter is the actual specification of the world.

We classify as background knowledge the items in a knowledge base that specify the general conditions of the scenario. Typically, the background knowledge contains data that does not change, e.g., the types of agents, the locations of stations.

lkbI = clock(0) class(b(0),BotI) class(st(0),Station) (atloc(b(0),pt(0,1)) @ 0)   (atloc(st(0),pt(3,2)) @ 0)(mode(b(0),ready) @ 0) (energy(b(0), 100) @ 0)   (ereserve(b(0),35) @ 0) home(b(0),pt(0,1)) (targets(pt(4, 0) ; pt(5, 4)) @ 0)    (fence (b(0),pt(0,0),pt(6,5)) @ 0)

The KItem (mode(b(0),ready) @ 0) specifies that the bot is ready for carrying out the tasks assigned, namely, visit the points in (targets(pt(4, 0) ; pt(5, 4)) @ 0). The background knowledge of b(0) is class(st(0),Station) (atloc(st(0),pt(3,2)) @ 0)class(b(0),BotI) home(b(0),pt(0,1)) (fence (b(0),pt(0,0),pt(6,5)) @ 0) (ereserve(b(0),35) @ 0)

The KItem (ereserve(b(0),35) @ 0) is a parameter used by the soft constraint solving mechanism to cause a Bot to pass by the charging station before its energy level gets too low. It is part of the scenario specification rather than representing state that evolves over time, and thus background knowledge. The (targets(pt(4,0) ; pt(5,4)) @ 0) KItem is the list of locations to be visited. When a target is selected it is removed from the list and made the current target. When there are no more targets and the current target has been treated, the Bot goes home using the home(b(0),pt(0,1)) KItem to remember where that is.

Elements of the sort Sensor name sensors available to an agent. The Bot sensors described in Section 2 are associated to the constants locS, energyS, obstacleS, and treatS, respectively. The finisher Bot also has a supply-level sensor with associated constant supplyS.

The sort Task represents tasks to be carried out by agents. Task events are executed by the doTask rule. In our case studies, only one task is used, namely tick. It is used to schedule the next time the agent reads its sensors and proposes actions.

Events are used to determine what happens during rule application. The sort Event has two subsorts: DEvents that are actions (sort Action) or tasks (sort Task) with delays, and IEvents that are events to be processed immediately (implicit delay of 0).

The sort Action is used to describe actions proposed by agents. Each action has an identifier parameter that identifies the agent carrying out the action and possibly other parameters. Each action consumes resources, such as energy, which are specified by the operational semantics of the scenario described in Section 4.2.

• — charge(id:Id) increases energy level provided the bot is at the supply depot.

• — mv(id:Id,dir:Pt2) moves one unit in the direction specified by the vector dir:Pt2.

• — treat(id:Id) increments treatment stage by 1. For BotF, the execution of this action uses some of the supply.

• — load(id:Id) available to BotF at the supply depot to replenish its supply.

To decide its next action, an agent ranks each applicable action in its current local knowledge base according to the agent’s preference specified using soft constraints (Bistarelli et al. Reference Bistarelli, Montanari and Rossi1997). The result is a set of ranked actions, ract, which are pairs of the form {rval,act}, where act is the action and rval is the action’s valuation, typically a value in the interval [0,1], where 1 is more preferred.

4.2 Soft agents semantics: Configuration and rules

A soft agents configuration (sort Conf) is a multiset of configuration elements (sort ConfElt). Agent objects (sort Agent) and environment objects (sort Env) are configuration elements. Formally Agent and Env are subsorts of ConfElt. A well-formed configuration needs a unique environment object and at least one agent object. Other configuration elements can be defined to control execution and to track properties of interest. Logs and bounds on the time or number of applications of selected rewrite rules are examples of other configuration elements as we will see later. Configurations are open ended as you can add or remove an element and still have a configuration. A soft agents system conf:Conf (sort ASystem) specifies exactly which configuration elements are present by enclosing them in s. The use of ASystem is required when a rewrite rule needs to know it has all elements of a configuration under consideration, in contrast to rules that operate on one or a pair of configuration elements.

An agent object has the form [id:Id : cl:Class | attrs:AttributeSet] where an attribute is a key-value pair. Agent objects must have at least the following attributes: lkb : localkb:KB, the agent’s local KB; sensors : ss:SensorSet, the agent’s sensors evs : events:Events, events awaiting processing ckb : cachedkb:KB, cached knowledge to be shared.

[b(0) : BotI | lkb : lkbI, ckb : none,               sensors : (locS obstacleS energyS treatS), evs : (tick @ 0)]

An environment object has the form [eid:Id | ekb:KB] The environment KB (ekb:KB) contains information about the physical state of each agent such as location and energy, information about resources such as location of charging stations, information about obstacles, global parameters such as communication range, and fault models. The environment KB and each agent local KB contain a clock knowledge item.

The semantics of an soft agents configuration is defined by two rewrite rules: doTask and timestep described in the following.

4.3 Executions

Using the two rewrite rules, doTask and timeStep, executions of a soft agents system alternate steps where agents observe (read their sensors) and decide on actions, and steps where the actions are realized by the environment. Assuming a set of agents, $a_1, \ldots, a_n$ , an execution step is a sequence of transition segments of the form

\begin{equation*} \mathcal{C}_0 \longrightarrow[\texttt{doTask}(a_1)]~ \mathcal{C}_1 \longrightarrow[\texttt{doTask}(a_2)]~ \cdots \longrightarrow[\texttt{doTask}(a_n)]~ \mathcal{C}_n \longrightarrow[\texttt{timestep}]~\mathcal{C}'\end{equation*}

with a sequence of applications of doTask $(a_i)$ applied to an agent $a_i \in \{a_1,\ldots,a_n\}$ followed by an instance of the timestep rule. We will abbreviate any such sequence as

\begin{equation*} \mathcal{C}_0 \longrightarrow[\texttt{doTask}]~ \mathcal{C}_n \longrightarrow[\texttt{timestep}]~\mathcal{C}'.\end{equation*}

An execution trace is a sequence of execution steps.

The Maude implementation of the soft agents framework, case studies, sample output of executions and searches, and documentation is available at

github.com/SRI-CSL/SoftAgentsDiagnosis.git.

It is possible to use Maude rewriting and search machinery to carry out experiments and analysis.

The command to search for one example of non compliance by the finisher bot b(1) is search [1] mkInitS(pt(4, 0) ; pt(5, 4), true) =>+    {aconf:Conf [eI | ekb:KB ]} such that getEnergy(b(1),ekb:KB) < 35 .

and the result is No solution. This means that in the absence of faults, the energy of b(1) is not lower than 35.

6.1 SA protocols

A soft agents protocol is a finite partial order of observable event patterns together with constraints on the pattern variables and possibly additional invariant constraints independent of the event pattern variables. Using event patterns rather than concrete events allows for compact specification and also for specifications that can be met under many conditions. For example, there is no need to specify concrete times for events, when relative times and time intervals are what is important; one may not want to specify precise locations, but only neighborhoods; and in some cases, the order between a pair of events may not matter as long as both happen.oft agents event patterns are represented by symbolic knowledge items, i.e., time stamped information items where the time stamps are variables, and the parameters of the information part may be variables. The partial order is specified by ordering relations on the time stamp variables. We require that each event has a unique symbolic time stamp. Thus, a symbolic event can be identified by its time stamp and so multiple occurrences of the same information template can be distinguished. Invariants are typically used to represent safety envelopes, such as maintaining energy above a given minimum level or ensuring that the distance between pairs of agents is greater than a given minimum.

• — $\mathit{TL}$ is a list of timelines, where the timeline for an agent is the list of time stamp variables for events under control of that agent.

• — $\mathit{Eps}$ is the set of protocol event patterns.

• — $\mathit{LO}$ is the set of local order constraints for each agent. A local order constraint for an agent has the form s0:Time < s1:Time where s0:Time, s1:Time are time stamp variables in the timeline for that agent.

• — $\mathit{GO}$ is the set of global order constraints, s0:Time < s1:Time where s0:Time, s1:Time belong to the timelines of different agents.

• — $\mathit{CS}$ consists of additional constraints on protocol event pattern variables.

• — $\mathit{Inv}$ is the set of invariant constraints. These are implications epats => c where epats is a list of event pattern viewed as a conjunction, c is a constraint on the variables of the event patterns in epats.

timeline(b(0),s00:Time,s01:Time,s02:Time,s03:Time,s04:Time,s05:Time)

The time stamp variables are used in the event pattern: atloc(b(0),pt(4, 0)) @ s00:Time treatStage(pt(4, 0),2) @ s01:Time atloc(b(0),l0:Pt2) @ s02:Time atloc(b(0),pt(5, 4)) @ s03:Time treatStage(pt(5, 4),2) @ s04:Time atloc(b(0),l1:Pt2) @ s05:Time

This pattern specifies the events to be carried out by the bot, namely, the locations b(0) to be visited and the treatments to be applied.

Local order constraints specify temporal conditions for the protocol. The following local ordering constraint specifies that the timestamps of the events in the pattern above shall form a total order, i.e., one event is followed by the next one. s00:Time < s01:Time s01:Time < s02:Time s02:Time < s03:Time s03:Time < s04:Time s04:Time < s05:Time

The local ordering s03:Time - s01:Time < 15 specifies that the bot shall not take too long to reach the second location once the second treatment of the first location is completed.

Global order constraints can specify timing conditions involving multiple agents. For example, treatStage(pt(4, 0),4) @ s11:Time is in the event patterns of bot b(1), and the global order constraint s11:Time - s01:Time < 10 specifies that the time between treatments shall not exceed 10 time units.

The following invariant specifies that the energy levels of the bot shall always be greater than 35 time units: energy(id:Id,e:Nat) @ s:Time => e > = 35

The design of the protocol language has been carefully crafted to enable the development of automated workflows using SMT-solvers and Maude. While we believe that it is possible to extend the language with other constructs such as finite branching and finite unfolding, unbounded recursion will likely lead to undecidability of the diagnosis problem, or to problems that current SMT implementations cannot check satisfiability.

Typically in an execution of the protocol the local order for an agent is a total order. The order need not be totally specified, meaning that multiple orders are acceptable. Some actions may cause change in more than one observable and hence the corresponding events will appear simultaneously.

6.2 Protocol satisfaction by event logs

Not all knowledge items make sense as events. The realization of a protocol event is the result of an agent action, that is it is among the knowledge items returned by doAct or envAct. In particular, for the agents to execute the protocol these events should be under the control of the agents, not environment actions. In the case of the BotTeam protocol events are location, treatment stage, and energy knowledge items. If the bots had cameras, knowledge items relevant to taking pictures could be protocol events.

We define the event language, $\mathit{EL}$ , of a protocol to be the knowledge items generated by the information constructors used in the event patterns appearing in the protocol (both the partial order and the invariants). This language is specified by a sub-signature of the Maude KB signature. For example, the event language of the BotTeam above is given by the constructors atloc : Id Loc -> Info treatStage : Loc Nat -> Info energy : Id Nat -> Info

• — $\mathit{EvL} \models \mathcal{P}$ if and only if $\mathit{EvL} \models (\mathit{Eps}, \mathit{LO}, \mathit{GO}, \mathit{CS})$ and $\mathit{EvL} \models \mathit{Inv}$ .

• — $\mathit{EvL} \models (\mathit{Eps}, \mathit{LO}, \mathit{GO}, \mathit{CS})$ if and only if there is a substitution, $\sigma$ , embedding $\mathit{Eps}$ in $\mathit{EvL}$ ( $\sigma(\mathit{Eps}) \subseteq \mathit{EvL}$ ) such that $\sigma(\mathit{LO})$ , $\sigma(\mathit{GO})$ , $\sigma(\mathit{CS})$ are all true.

• — $\mathit{EvL} \models \mathit{Inv}$ if and only if $\mathit{EvL} \models \mathtt{ep => c}$ for each invariant expression ep => c in $\mathit{Inv}$ .

• — $\mathit{EvL} \models \mathtt{ep => c}$ if and only if for each instance $\sigma_0(\mathtt{ep})$ in $\mathit{EvL}$ , $\sigma_0(\mathtt{c})$ is true.

(atloc(b(0), pt(0,0)) @ 1) ... atloc(b(0), pt(5,4)) @ 20) (treatStage(pt(4,0), 2) @ 9) ... (treatStage(pt(4,0), 4) @ 15) (treatStage(pt(5,4), 2) @ 28) ... (treatStage(pt(5,4), 4) @ 34) ((energy(b(0), 100) @ 1)) ... (energy(b(0), 60) @ 34)

The first line contains the events with positions of b(0) during the execution, while the following two lines contains the treatment events for the two treatment points. The last line contains the bot’s energy levels. This event log satisfies the local constraint s03:Time - s01:Time < 15 described in Example 6.2. Indeed, the time of completion of the second treatment of the location pt(4,0) is nine, i.e., the value s01:Time is nine. Moreover, the time b(0) reached and the second point was 20, i.e., the value of s03:Time is 20. Thus, the constraint s03:Time - s01:Time < 15 is true as $20 - 9 = 11 < 15$ .

6.3 Protocol satisfaction by execution traces

In Section 4.2.2, a generic mechanism for collecting execution logs was described. Here we consider logs appropriate for checking satisfaction and detecting deviations from a protocol and derive event logs from these execution logs.ecall that a log item has the form t, acts,lconf where t is a time stamp, acts an action set, and lconf a set of configuration elements. t is the time just before the actions are carried out. A log $\mathit{Lg}$ is a sequence of log items with time increasing. We write $len(\mathit{Lg})$ for the length of the sequence. Define $\mathit{Lg}[t]$ to be the (unique) log item of $\mathit{Lg}$ with time stamp t, i.e., the log item of the form t, acts, lconf. $\mathit{Lg}[t]$ is nil if there is no such log item. Note that the logs generated by updateLog have a log item for each time from 0 up to (not including) the length of the log.

Here we restrict our attention to logged configurations lconf that have the form [eid | ekbl] … [id : Cl | lkb : lkbl] … In particular, only the lkb attribute of agents is kept. How much of the execution configuration KBs to keep in the log depends on the intended use. If one is only checking protocol satisfaction, then only the knowledge items in the protocol event language are needed. For detecting deviations or diagnosis more information is usually needed. For checking properties other than protocol satisfaction, log items might collect metadata rather than environment and agent knowledge.

We introduce some auxiliary notation used to define the notion of “log for a trace” and satisfaction relations between protocols and traces or logs. In the following, $\mathit{Tr}$ is an execution trace as defined in Section 4.3 and $\mathit{Lg}$ is a log. For j from 0 up to (not including) $len(\mathit{Tr})$ , $\mathit{Tr}[j]$ is the $j^{th}$ execution step of $\mathit{Tr}$ : $\mathcal{C}_j \longrightarrow[\mathtt{doTask}]~\mathcal{C}_{j}' \longrightarrow[\mathtt{timestep}]~\mathcal{C}_{j+1}.$ Moreover, let acts.j be the actions carried out in the above timestep rule. Notice that j is the time t in $\mathcal{C}_j$ , and $j + 1$ is the time in $\mathcal{C}_{j+1}$ and we also write $\mathit{Tr}[t]$ for this trace element. For t a timestamp of $\mathit{Lg}$ , $\mathit{Lg}[t]$ is t,acts,lconf where lconf has the form [eid | ekbl] ... [id : Cl | lkb : lkbl.id] ...

We define the following notation: $\mathit{Lg}[t][eid] = \mathtt{ekbl}$ , $\mathit{Lg}[t][id] = \mathtt{lkbl.id}$ , $\mathit{Lg}[t][a] = \mathtt{acts}$ and letting [eid | ekb] … [id : cl | lkb: lkb.id …] … be the final configuration C.j+1 of $\mathit{Tr}[j]$ where $j = t$ above, then $\mathit{Tr}[t][eid] = \mathtt{ekb}$ , $\mathit{Tr}[t][id] = \mathtt{lkb.id}$ , $\mathit{Tr}[t][a] = \mathtt{acts.j}$ .

• A log $\mathit{Lg}$ is a log for $\mathit{Tr}$ if $\mathit{Lg}[j]$ is a log item for $\mathit{Tr}[j]$ for j a time stamp of $\mathit{Lg}$ .

• $\mathit{Lg}[t]$ is a log item for $\mathit{Tr}[t]$ if and only if the following conditions are satisfied

  • — $\mathit{Lg}[t][eid]$ is a subset of $\mathit{Tr}[t][eid]$

  • — $\mathit{Lg}[t][id]$ is a subset of $\mathit{Tr}[t][id]$ for id in AgentIds

  • — $\mathit{Lg}[t][a] = Tr[t][a]$

Satisfaction of a protocol from the environment and agent perspective for traces and logs is defined by reducing it to associated event logs.

• — $\mathit{Tr} \models_E \mathcal{P}$ if $\mathit{EvsE}(\mathit{Tr}) \models \mathcal{P}$ – the environment view of trace satisfaction

• — $\mathit{Tr} \models_A \mathcal{P}$ if $\mathit{EvsA}(\mathit{Tr}) \models \mathcal{P}$ – the agent view of trace satisfaction

• — $\mathit{Lg} \models_E \mathcal{P}$ if $\mathit{EvsE}(\mathit{Lg}) \models \mathcal{P}$ – the environment view of log satisfaction

• — $\mathit{Lg} \models_A \mathcal{P}$ if $\mathit{EvsA}(\mathit{Lg}) \models \mathcal{P}$ – the agent view of log satisfaction

where

A useful log should collect enough information such that if $\mathit{Lg}$ is a log for $\mathit{Tr}$ then

\begin{equation*}\mathit{Tr} \models_E \mathcal{P} \Leftrightarrow \mathit{Lg} \models_E \mathcal{P} ~\hbox{and}~ \mathit{Tr} \models_A \mathcal{P} \Leftrightarrow \mathit{Lg} \models_A \mathcal{P}\end{equation*}

In particular, the following event pattern in Example 6.2 atloc(b(0),pt(4, 0)) @ s00:Time treatStage(pt(4, 0),2) @ s01:Time atloc(b(0),l0:Pt2) @ s02:Time atloc(b(0),pt(5, 4)) @ s03:Time treatStage(pt(5, 4),2) @ s04:Time atloc(b(0),l1:Pt2) @ s05:Time

can be matched by the log in Example 6.5: (atloc(b(0), pt(0,0)) @ 1) ... atloc(b(0), pt(5,4)) @ 20) (treatStage(pt(4,0), 2) @ 9) ... (treatStage(pt(4,0), 4) @ 15) (treatStage(pt(5,4), 2) @ 28) ... (treatStage(pt(5,4), 4) @ 34) ((energy(b(0), 100) @ 1)) ... (energy(b(0), 60) @ 34)

For example, s01:Time is matched to 9. Moreover, one can check that the constraints in Example 6.2 are satisfied or not by simply checking their validity. For example, the constraint s03:Time - s01:Time < 15 is satisfied as the drone reached the location pt(5,4) at time 28 and treated location pt(4,0) at time 9.

8.1 Generating execution and event logs

Generating an execution log has two realizations. The first is instrumenting the execution so that the final state contains not only the final system configuration but also a log of the execution. The second is generating a log as a term that can be used as input for other functions, such as checking for deviations. These are different because the result of rewriting is just text that is printed as part of the Maude read-eval-print loop. However, due the Maude’s support for reflection, going from the first to the second is easy as we will see below.

To instrument the execution, recall from Section 4.2.2 that the timeStep rule provides a hook and data structures for log generation, as well as the function updateLog which invokes the model specific function kbLog to compute the configuration component of a log item.

In the BotTeam case study, kbLog collects the agent sensor readings from the environment for the environment part of the log item and collects, for each agent log component, the knowledge items used in deciding actions to propose. This includes location and energy knowledge items and information about targets for treatment and treatment status.

To check satisfaction of a soft agents protocol, we extract an event log from an execution log. Given a log lg, the function flatLog(lg,none,none) returns a pair ekbAll,lkbAll where ekbAll is the union of the environment KBs in the log items of lg and lkbAll is the union of the lkb attributes of each agent in the log items of lg. That is ekbAll is $\mathit{EvsA}(\mathtt{lg})$ and lkbAll is $\mathit{EvsE}(\mathtt{lg})$ as defined in Section 6.3.

8.2 Protocol deviations

We developed a tool called deviate to detect deviations from a protocol by transforming a protocol plus event log into a logical theory and using the Yices SMT solver to find models of the event partial order component.

To do this deviate first translates the event log into a complete set of atomic and negated atomic formula (clauses), with no free variables, in a finite language over a finite domain. It does this by assuming that if an event does not occur in the log, then the event is in fact false. The protocol is then translated into a simple set of quantifier-free constraints over the theory constructed from the log. The satisfiability of the constraints is then checked by using, the python interface to, the Yices SMT solver. If there is no solution, then we can further investigate the cause by looking at various sub problems. Either by limiting the events in the log to an initial segment or by restricting the form of the constraints generated from the protocol. In this manner, we can further clarify why the initial constraint set has no solution.

We illustrate the information provided by deviate using the following scenario: The initiator bot, b(0), starts at pt(0,1) and the finisher bot, b(1), starts at pt(0,4). The fault model adds location faults for b(1) and the initiator bot waits until b(0) is within 3 moves of the target location to start treatment. Giving deviate the BotTeam protocol and the Environment view of the events from the log for the above scenario we can ask several questions. First, simply, does the event set satisfy the the protocol. deviate reports UNSAT. Next we ask about satisfaction at different levels:

• — Level 0: Does a mapping $\sigma$ exist giving times for the specified event patterns? The answer is yes (and a witness is returned).

• — Level 1: Is there a level 0 $\sigma$ that satisfies the local order constraints (LO)? Yes. ( $\sigma$ may be different.).

• — Level 2: Is there a level 1 $\sigma$ that also satisfies the global order constraints (GO)? Yes. ( $\sigma$ may again be different.)

• — Level 3: Is there a level 2 $\sigma$ that also satisfies the event constraints (CS)? NO! (UNSAT)

• — Level 4: Is there a $\sigma$ that also satisfies the protocol invariants (INV)? NO! (UNSAT)

Finally, the frontier often provides useful information. Intuitively, the frontier specifies a possible minimal stage of concurrent execution where things go wrong, i.e., all earlier stages are consistent with the protocol.

Given a protocol with timelines $[tl_0, ... tl_N]$ where each $tl_j$ is a sequence of time stamp variables $s_{j,k}$ for $0 \le k \le N_j$ ; and an event log, the problem associated with $(i_0, ... i_N)$ is whether there is a mapping of the timeline variables $s_{j,k}$ for $0 \le k \le i_j)$ that satisfies the protocol restricted to these variables. The frontier is the set of tuples $(i_0, ... i_N)$ such that

• — $i_j \le N_j$

• — the problem associated with $(i_0, ... i_N)$ is UNSAT,

• — the problem associated with any (pointwise) smaller tuple is SAT.

In the case of our example, the frontier has a single element (1,1) and deviate tells us that the unsat core includes [(treatStage (pt 4 0) 4 s11), (treatStage (pt 4 0) 2 s01)]. That is, the finisher bot is late at the first target point.

8.3 Execution deviations

An execution deviation is a result of an agent action that differs from what is predicted by the agent’s model, or a broken sensor reading. In soft agents, an execution deviation can be determined by comparing the local knowledge base of agents and the environment knowledge base. If they differ, it means that there is an execution deviation.

More precisely, an execution deviation (sort EDev) has one of the forms {ract,lkb,lkb0,ekb0} {ract,lkb,lkb0,{lkb1,ekb0}}

where ract is the (ranked) action executed, lkb is the executing agent’s local KB, lkb0 is the knowledge items updated by the action carried out in lkb0 according to the agent’s model of the world, and ekb0 is the knowledge items in the environment KB, after the action, that disagree with lkb0. In the second case, lkb1 are items in lkb0 that have no corresponding update in the environment KB (for example, if a move action failed, lkb0 will have a location update, but the environment will not). ^{Footnote 7} An execution deviation element (sort EDevsElt) is a time stamped set of execution deviations [t:Time,edevs:EDevSet].

Intuitively, we compute the execution deviations from an execution log by comparing at each step of the log, the local knowledge base of an agent with the expected outcome of performing the same action (without fault models) at that step. ^{Footnote 8} If there is a disagreement, then there is an execution deviation.

[6,{{(zero).RVal,noAct}, (targets(pt(5,4)) @ 2)(target(pt(4,0)) @ 0) ... (energy(b(1),75) @ 6)(mode(b(1),enroute(pt(4, 0))) @ 6), atloc(b(1), noLoc) @ 6,atloc(b(1), pt(1, 0)) @ 6}]

At time 11 b(1) is trying to charge, since it thinks its at the charging station (pt(3,2)). Thus, it predicts that its energy increases from 55 to 75. However, from the environment perspective (ground truth), we find that the location of b(1) is pt(3,1), charging has no effect, and thus the environment does not record a new value for energy. [11,{{{cv(100),u(1)},charge(b(1))}, (targets(pt(5, 4)) @ 2) (target(pt(4,0)) @ 0) ... (atloc(b(1), pt(3,2)) @ 11) (energy(b(1), 55) @ 11) (mode(b(1), enroute(pt(4,0))) @ 11) @ 0, energy(b(1), 75) @ 12, {energy(b(1), 75) @ 12,(none).KB}}]

8.4 Checking candidate causes

We continue the scenario in Section 8.2 with protocol $\mathcal{P}$ , an event log $\mathit{EvL}$ from log $\mathit{Lg}$ for $\mathit{Tr}$ in $\mathit{Tr}(iC,\mathit{FM})$ . To check that a candidate event in the log is a possible cause for a deviation in $\mathit{Dev}(\mathit{EvL},\mathcal{P})$ we do a gedanken experiment. That is we find a trace $\mathit{Tr}'$ in $\mathit{Tr}(iC,\mathit{FM})$ that agrees with $\mathit{Tr}$ up to the event, avoids the identified event, and continues without further fault injection. ^{Footnote 9}

The idea is inspired by counterfactual reasoning. ceq gedanken(asys,asysB,n,j) = log1 if log := genLog(asys, ((s n) * 3)) --- 3 rew per time unit   /\ litem := subLog(log,n,1) --- last trace element   /\ ekb := getLIEnvKB(litem) --- current environment KB   /\ aconf := getLIAgents(litem) --- current agent state   /\ asys1 := updateSys(asysB,s n,ekb,aconf)   /\ log1 := genLog(asys1,j) . --- hoping for no deviation

asys is the system (with faults) generating $\mathit{Tr}$ and asysB contains the base configuration information needed to continue, avoiding the candidate execution deviation. The n is the time just before the candidate execution deviation, and j is how long to continue to check that the protocol deviation is gone. The factor 3 is due to the fact that for every application of the timeStep rule there are two applications of the doTask rule, one for each agent. The 3 is scenario dependent. asys1 augments the logged environment and agent state with knowledge that is constant, such as fence boundary or resource location knowledge, that are not logged, but needed to execute the rules. This information is contained in asysB. The logged environment KB does not contain fault models that are the mechanisms for generating faulty executions, but it may contain obstacles as they are among the entities in the configuration. They must be removed for the gedanken experiment, as they are the other source of perturbations. Note that for the purpose of gedanken the log needs to collect all of the agent state that changes and that is used to decide actions. It also needs to collect all environment knowledge of changing information that is needed for sensor readings or to compute the effects of actions. This may extend what is collected just for determining protocol satisfaction.

The result of this function is a new event log log1 which is then used to check for protocol deviations following the workflow shown in Figure 2. If there are no protocol deviations, then the candidate execution is deemed a possible cause.

red gedanken(addFaultsR(mkInitS(pt(4, 0) ; pt(5, 4), true),  locsf(1), 500),mkInitS(pt(4, 0) ; pt(5, 4), true), 7,90) .

shows that the execution now satisfies the protocol. In particular, we have events (treatStage(pt(4, 0), 2) @ 11) (treatStage(pt(4, 0), 4) @ 17) (treatStage(pt(5, 4), 4) @ 35) (treatStage(pt(5, 4), 2) @ 29)

Repeating the gedanken experiment by allowing the fault at 11 but no more we find that the finishing treatment at pt(4,0) is late, but the finishing treatment at pt(5,4) is on time. (treatStage(pt(4, 0), 2) @ 11) (treatStage(pt(4, 0), 4) @ 28) (treatStage(pt(5, 4), 2) @ 34) (treatStage(pt(5, 4), 4) @ 43)

9.1 Summary of BotTeam execution results

The scenario for this case study has two bots on a $7 \times 6$ grid: b(0), the initiator (class BotI), with sensors locS energyS obstacleS treatS, initially at pt(0,1); and b(1), the finisher (class BotF), with sensors locS energyS obstacleS treatS supplyS, initially at pt(0,4). There is a charging station at pt(3,2) and a supply depot at pt(3,3). Experiments were done for two target lists with initial system configurations initS1a (2 targets) and initS2 (3 targets).

The fault models used in the experiments are described in Tables 1 and 2. The first column of the table is the name used for the fault model in the corresponding experiment summary table. The second column is the knowledge item(s) added to the environment KB specifying the fault. Finally, we also evaluated the impact of the choice of the random sequence used for deciding the occurrence of execution deviations due to the fault models. We specified fault models mvaf1 and mvaf1x with the same fault model specification, but with different subsequences of the sequence generated by Maude. This means that the occurrence of execution deviations using these faults are generally different.

Table 1.

Fault models used in for the experiments involving the 2 target scenario initS1a

Table 2.

Fault models used in for the experiments involving the 3 target scenario initS2

To evaluate the impact of faults on individual sensors, we used fault models for energy, location, movement actuator, and obstacles. We explain in the following the intuition of the fault models in Table 1. The meaning of the faults in Table 2 is similar but using different parameters.

• — ensfm1 corresponds to the fault model in Example 5.1. In particular, energy measurements may either not return a value or return a value 10 units below the agent’s actual energy. Such wrong measurement may impact the bot’s behavior making them decide to return to the station to recharge.

• — locsf1x is similar to ensfm1, but considers measurement errors in the location of the bot, instead of the energy.

• — mvaf1 is similar to the fault model in Example 5.2. In particular, a bot may move erroneously with a probability of 1/5 with an error of pt(-1,0). Moreover, the bot may fail to move altogether with probability of 1/10.

• — mvaf1x is similar to mvaf1 by using a different random seed.

• — Obs4-2 is a fault model where there is an unknown obstacle at position pt(4,2).

Tables 3 and 4 summarize, respectively, the results of experiments using the two target scenario, initS1a, and the three target scenario, initS2 with the SA protocol described in Example 6.2. The Faults column names the fault model used (as defined above). The Close column specifies how close the BotI bot requires the BotF bot to be before beginning treatment at a target location. Intuitively, on the one hand, the closer the bots have to be, the less is the risk that the interval between treatments constraints is not satisfied, but on the other hand, the greater is the risk that the overall time of treatment target is not satisfied. For the experiments, the possible values used are 1 and 3 distance units. The PDevs column lists the minimal (with respect to the protocol partial order) protocol deviation(s) if any. The EDevs column gives the number of execution deviations prior to the protocol deviation. In the Gedanken column, a +/- indicates that the gedanken experiment defined by the candidate execution deviation causes confirmed/failed to confirm that elimination of the deviation events eliminated the protocol deviation. na abbreviates “not applicable”.

Table 3.

Summary of experiment results for the 2 target scenario initS1a. If PDevs is none, then EDevs counts deviations in the full execution. Execution deviations due to obstacles are not currently collected. In this experiment, removing the obstacle at event before deviation corrects the behavior

Table 4.

Summary of experiment results for the 3 target scenario initS2

We use the following notation for protocol deviations.

• — delta(x,y) abbreviates: the log events have

(treatStage(pt(x,y),2) @ t0) (treatStage(pt(x,y),4) @ t1)

1. — with t1 - t0 > = 10 violating the constraint on delay between initial and final treatments.

2. − delta((x0,y0),(x1,y1)) abbreviates: the log events have

(treatStage(pt(x1,y1),2) @ t0) (tloc(b(0),pt(x0,y0)) @ t1)

1. — with t1 - t0 > = 15 violating the constraint on time between target locations.

2. − atloc(b(j),pt(x,y)) indicates an event that was expected by the protocol specification is missing.

From Tables 3 and 4, we see that in all but one case this process was able to identify execution deviations which, when removed, eliminated the protocol deviation. Already from these (non-comprehensive) experiments, it seems that for the scenario with two targets, faults on location and obstacle are most damaging. In contrast, for the scenario with three targets, the impact of energy and movement sensors/actuators start to have a greater impact. This is expected as adding an additional target results in bots needing to traverse greater distances thus consuming more energy and having tighter deadlines.

There is one exceptional case involved in the three target scenario with location sensor faults for BotI. The deviation is an event for which BotF is responsible. The actual problem is that BotF passes through a location adjacent to the target location on the way to the supply depot. It gets stuck there waiting for BotI to finish its treatment because the constraint system gives 0 preference to moving if it is adjacent to its target and BotI is there treating. For the diagnosis system to understand this, more information is needed about the constraints underlying the bots’ action decisions.