Online Agent Supervision in the Situation Calculus

1 Introduction

In many settings, we want to restrict an agent's behavior to conform to a set of specifications. For instance, the activities of agents in an organization have to adhere to some business rules and privacy/security protocols. Similarly, a mobile robot has to conform to safety specifications and avoid causing injuries to others. One form of this is customization, where a generic process for performing a task or achieving a goal is refined to satisfy a client's constraints or preferences. Process customization includes personalization [Fritz and McIlraith, 2006] and configuration [Liaskos et al., 2012] and finds applications in number of areas.

A key challenge in such settings is ensuring conformance to specifications while preserving the agent's autonomy. Motivated by this and inspired by supervisory control of discrete event systems [Wonham and Ramadge, 1987; Wonham, 2014; Cassandras and Lafortune, 2008], De Giacomo, Lesp´erance and Muise [De Giacomo et al., 2012] (DLM) proposed agent supervision as a form of control/customization of an agent's behavior. The DLM framework is based on the situation calculus [McCarthy and Hayes, 1969; Reiter, 2001] and a variant of the ConGolog [De Giacomo et al., 2000]

Yves Lesp´erance York University Toronto, Canada lesperan@cse.yorku.ca

programming language. DLM represent the agent's possible behaviors as a nondeterministic ConGolog process. Another ConGolog process represents the supervision specification, i.e., which behaviors are acceptable/desirable.

If it is possible to control all of the agent's actions, then it is easy to obtain the behaviors of the supervised agent through a kind of synchronous concurrent execution of the agent process and the supervision specification process. However, some of the agent's actions may be uncontrollable. DLM formalize a notion of maximally permissive supervisor that minimally constrains the behavior of the agent in the presence of uncontrollable actions so as to enforce the desired behavioral specifications. The original DLM account of agent supervision assumes that the agent does not acquire new knowledge about her environment while executing. This means that all reasoning is done using the same knowledge base. The resulting executions are said to be offline executions.

In this paper we study how we can apply the DLM framework in the case where the agent may acquire new knowledge while executing, for example through sensing. This means that the knowledge base that the agent uses in her reasoning needs to be updated during the execution. For instance, consider a travel planner agent that needs to book a seat on a certain flight. Only after querying the airline web service offering that flight will the agent know if there are seats available on the flight.

Technically, this requires switching from offline executions to online executions [De Giacomo and Levesque, 1999; Sardi˜na et al., 2004], which, differently from offline executions, can only be defined meta-theoretically (unless one adds a knowledge operator/fluent) since at every time point the knowledge base used by the agent to deliberate about the next action is different.

Based on online executions, we formalize the notion of online maximally permissive supervisor and show its existence and uniqueness, as in the simpler case of DLM. Moreover, we meta-theoretically define a program construct (i.e., supervision operator) for online supervised execution that given the agent and specification, executes them to obtain only runs allowed by the maximally permissive supervisor, showing its soundness and completeness. We also define a new lookahead search construct that ensures the agent can successfully complete the execution (i.e., ensures nonblockingness).

2 Preliminaries

The situation calculus (SC) is a well known predicate logic language for representing and reasoning about dynamically changing worlds. Within the language, one can formulate action theories that describe how the world changes as the result of actions [Reiter, 2001]. We assume that there is a finite number of action types A. Moreover, we assume that the terms of object sort are in fact a countably infinite set N of standard names for which we have the unique name assumption and domain closure. As a result a basic action theory (BAT) D is the union of the following disjoint sets: the foundational, domain independent, (second-order, or SO) axioms of the situation calculus (⌃), (first-order, or FO) precondition axioms stating when actions can be legally performed (Dposs), (FO) successor state axioms describing how fluents change between situations (Dssa), (FO) unique name axioms for actions and domain closure on action types (Dca); (SO) unique name axioms and domain closure for object constants (Dcoa); and (FO) axioms describing the initial configuration of the world (DS0 ). A special predicate Poss(a↪ s) is used to state that action a is executable in situation s; precondition axioms in Dposs characterize this predicate. The abbreviation Executable(s) means that every action performed in reaching situation s was possible in the situation in which it occurred. In turn, successor state axioms encode the causal laws of the world being modeled; they replace the so-called effect axioms and provide a solution to the frame problem. We write do([a1↪ a2↪ ▷ ▷ ▷ ↪ an-1↪ an]↪ s) as an abbreviation for the situation term do(an↪ do(an-1↪ ▷ ▷ ▷ ↪ do(a2↪ do(a1↪ s)) ▷ ▷ ▷)); for an action sequence ~a, we often write do(~a↪ s) for do([~a]↪ s).

To represent and reason about complex actions or processes obtained by suitably executing atomic actions, various so-called high-level programming languages have been defined. Here, we concentrate on (a fragment of) ConGolog that includes the following constructs:

In the above, ↵ is an action term, possibly with parameters, and ' is situation-suppressed formula, i.e., a SC formula with all situation arguments in fluents suppressed. As usual, we denote by '[s] the formula obtained from ' by restoring the situation argument s into all fluents in '. Program δ1♣δ2 allows for the nondeterministic choice between programs δ1 and δ2, while ⇡x▷δ executes program δ for some nondeterministic choice of a legal binding for variable x (observe that such a choice is, in general, unbounded). δ⇤ performs δ zero or more times. Program δ1kδ2 represents the interleaved concurrent execution of programs δ1 and δ2. The intersection/synchronous concurrent execution of programs δ1 and δ2 (introduced by DLM) is denoted by δ1& δ2.

Formally, the semantics of ConGolog is specified in terms of single-step transitions, using two predicates [De Giacomo et al., 2000]: (i) Trans(δ↪ s↪ δ0 ↪ s0 ), which holds if one step of program δ in situation s may lead to situation s0 with δ0 remaining to be executed; and (ii) Final(δ↪ s), which holds if program δ may legally terminate in situation s. The definitions of Trans and Final we use are as in [De Giacomo et al., 2010]; differently from [De Giacomo et al., 2000], the test construct '? does not yield any transition, but is final when satisfied. Thus, it is a synchronous version of the original test construct (it does not allow interleaving). As a result, in our version of ConGolog, every transition involves the execution of an action. Predicate Do(δ↪ s↪ s0 ) means that program δ, when executed starting in situation s, has as a legal terminating situation s0 , and is defined as Do(δ↪ s↪ s0 ) ▷= 9δ0 ▷Trans⇤ (δ↪ s↪ δ0 ↪ s0 ) ^Final(δ0 ↪ s0 ) where Trans⇤ denotes the reflexive transitive closure of Trans.

A ConGolog program δ is situation-determined (SD) in a situation s [De Giacomo et al., 2012] if for every sequence of actions, the remaining program is determined by the resulting situation, i.e.,

For example, program (a; b) ♣ (a; c) is not SD, while a; (b ♣ c) is (assuming the actions involved are always executable). Thus, a (partial) execution of a SD program is uniquely determined by the sequence of actions it has produced. Hence a program in a starting situation generates a set/language of action sequences, its executions, and operations like intersection and union become natural. In the rest, we use C to denote the axioms defining the ConGolog programming language.

3 Agents Executing Online

In our account of agent supervision, we want to accommodate agents that can acquire new knowledge about their environment during execution, for example by sensing, and where their knowledge base is updated with this new knowledge. Thus we consider an agent's online executions, where, as she executes the program, at each time point, she makes decisions on what to do next based on what her current knowledge is.

Sensing. A crucial aspect of online executions is that the agent can take advantage of sensing. Similarly to [Lesp´erance et al., 2008], we model sensing as an ordinary action which queries a sensor, followed by the reporting of a sensor result, in the form of an exogenous action.

Specifically, to sense whether fluent P holds within a program, we use a macro:

where QryIfP is an ordinary action that is always executable and is used to query (i.e., sense) if P holds and repV alP(x) is an exogenous action with no effect that informs the agent if P holds through its precondition axiom, which is of the form:

Thus, we can understand that SenseP reports value 1 through the execution of repV alP(1) if P holds, and 0 through the execution of repV alP(0) otherwise.

For example, consider the following agent program:

and assume the agent does not know if P holds initially. So initially we have D [ C ♣= Trans(δi ↪ S0↪ δ0 ↪ S1) where S1 = do(QryIfP↪ S0) and δ0 = nil; (repV alP(1) ♣ repV alP(0))); [P?;A] ♣ [≻P?;B]. At S1, the agent knows either of the exogenous actions repV alP(0) or repV alP(1) could occur, but does not know which. After the occurrence of one of these actions, the agent learns whether P holds. For example, if repV alP(1) occurs, the agent's knowledge base is now updated to D [ C [ ¶Poss(repV alP(1)↪ S1)♦. With this updated knowledge, she knows which action to do next: D [ C [ Poss(repV alP(1)↪ S1) ♣= Trans(nil; [P?;A] ♣ [≻P?;B]↪ do(repV alP (1)↪ S1)↪ nil↪ do([repV alP (1)↪ A]↪ S1)).

Notice that with this way of doing sensing, we essentially store the sensing results in the situation (which includes all actions executed so far including the exogenous actions used for sensing). In particular the current KB after having performed the sequence of actions ~a is:

Note that this approach also handles the agent's acquiring knowledge from an arbitrary exogenous action.

Agent online configurations and transitions. We denote an agent by σ, denoting a pair hD↪ δi i, where δi is the initial program of the agent expressed in ConGolog and D is a BAT that represents the agent's initial knowledge (which may be incomplete). We assume that we have a finite set of primitive action types A, which is the disjoint union of a set of ordinary primitive action types Ao and exogenous primitive action types Ae .

The online transition relation between agent configurations is (a meta-theoretic) binary relation defined as:

An agent configuration is modeled as a pair hδ↪~ai, where δ is the remaining program and ~a is the sequence of actions performed so far starting from S0. The initial configuration ci is hδi ↪ ✏i, where ✏ is the empty sequence of actions.

hδ↪~ai !A(~n) hδ0 ↪~aA(~n)i if and only if either A 2 Ao ↪ ~n 2 N k and D [ C [ ¶Executable(do(~a↪ S0))♦ ♣= T rans(δ↪ do(~a↪ S0)↪ δ0 ↪ do(A(~n)↪ do(~a↪ S0))) or A 2 Ae ↪ ~n 2 N k and D [ C [ ¶Executable(do(~a↪ S0))↪ T rans(δ↪ do(~a↪ S0)↪ δ0 ↪ do(A(~n)↪ do(~a↪ S0)))♦ is satisfiable.

Here, hδ↪~ai !A(~n) hδ0 ↪~aA(~n)i means that configuration hδ↪~ai can make a single-step online transition to configuration hδ0 ↪~aA(~n)i by performing action A(~n). If A(~n) is an ordinary action, the agent must know that the action is executable and know what the remaining program is afterwards. If A(~n) is an exogenous action, the agent need only think that the action may be possible with δ0 being the remaining program, i.e., it must be consistent with what she knows that the action is executable and δ0 is the remaining program. As part of the transition, the theory is (implicitly) updated in that the new exogenous action A(~n) is added to the action sequence, and Executable(do([~a↪ A(~n)]↪ S0)) will be added to the theory when it is queried in later transitions, thus incorporating the fact that Poss(A(~n)↪ do(~a↪ S0)) is now known to hold.

The (meta-theoretic) relation c !⇤ ~a c0 is the reflexivetransitive closure of c !A(~n) c0 and denotes that online configuration c0 can be reached from the online configuration c by performing a sequence of online transitions involving the sequence of actions ~a.

We also define a (meta-theoretic) predicate cX meaning that the online configuration c is known to be final: hδ↪~aiX if and only if D [ C [ ¶Executable(do(~a↪ S0))♦ ♣= F inal(δ↪ do(~a↪ S0))▷

Online situation determined agents. In this paper, we are interested in programs that are SD, i.e., given a program, a situation and an action, we want the remaining program to be determined. However this is not sufficient when considering online executions. We want to ensure that the agent always knows what the remaining program is after any sequence of actions. We say that an agent is online situationdetermined (online SD) if for any sequence of actions that the agent can perform online, the resulting agent configuration is unique. Formally, an agent σ = hD↪ δi i with initial configuration ci = hδi ↪ ✏i is online SD if and only if for all sequences of action ~a, if ci !⇤ ~a c0 and ci !⇤ ~a c00 then c0 = c00 . In [Banihashemi et al., 2016b], it is shown that for an agent to be online SD, it is sufficient that the agent always knows what the remaining program is after an exogenous action. From now on, we assume that the agent is online SD.

Online Runs. For an agent σ that is online SD, online executions can be succinctly represented by runs formed by the corresponding sequence of actions. The set RR(σ) of (partial) runs of an online SD agent σ with starting configuration ci is the sequences of actions that can be produced by executing ci from S0: RR(σ) = ¶~a ♣ 9c▷ci !⇤ ~a c♦▷ A run is complete if it reaches a final configuration. Formally we define the set CR(σ) of complete runs as: CR(σ) = ¶~a ♣ 9c▷ci !⇤ ~a c^cX♦▷ Finally we say that a run is good if it can be extended to a complete run. Formally we define the set GR(σ) of good runs as: GR(σ) = ¶~a ♣ 9c↪ c0 ↪ ~ a0 ▷ci !⇤ ~a c ^ c !⇤~ a0 c0 ^ c0X♦▷

4 Online Agent Supervision

Agent supervision aims at restricting an agent's behavior to ensure that it conforms to a supervision specification while leaving it as much autonomy as possible. DLM's account of agent supervision is based on offline executions and does not accommodate agents that acquire new knowledge during a run. DLM represent the agent's possible behaviors by a (nondeterministic) SD ConGolog program δi relative to a BAT D. The supervision specification is represented by another SD ConGolog program δs . First note that if it is possible to control all the actions of the agent, then it is straightforward to specify the result of supervision as the intersection of the agent and the specification processes (δi& δs ). However in general, some of agent's actions may be uncontrollable. These are often the result of interaction of an agent with external resources, or may represent aspects of agent's behavior that must remain autonomous and cannot be controlled directly. This is modeled by the special fluent Au(a↪ s) that means action a is uncontrollable in situation s.

DLM say that a supervision specification δs is controllable wrt the agent program δi in situation s iff:

i.e., if we postfix an action sequence ~a that is good offline run for δs (i.e., such that 9~b▷Do(δs ↪ s↪ do([~a↪~b]↪ s)) holds) with an uncontrollable action au which is good for δi , then au must also be good for δs .

Then, DLM define the offline maximally permissive supervisor (offline MPS) mpso✏(δi ↪ δs ↪ s) of the agent behavior δi which fulfills the supervision specification δs as:

This says that the offline MPS is the union of all sets of action sequences that are complete offline runs of both δi and δs (i.e., such that Do(δi & δs ↪ s↪ do(~a↪ s))) that are controllable wrt δi in situation s.

The above definition uses the set(E) construct introduced by DLM, which is a sort of infinitary nondeterministic branch; it takes an arbitrary set of sequences of actions E and turns it into a program. We define its semantics as follows:

Therefore set(E) can be executed to produce any of the sequences of actions in E. 1

DLM show that their notion of offline MPS, mpso✏(δi ↪ δs ↪ s), has many nice properties: it always exists and is unique, it is controllable wrt the agent behavior δi in s, and it is the largest set of offline complete runs of δi that is controllable wrt δi in s and satisfy the supervision specification δs in s, i.e., is maximally permissive. However, the notion of offline MPS is inadequate in the context of online execution, as the following example shows.

Example 1 Suppose that we have an agent that does not know whether P holds initially, i.e., D 6♣= P(S0) and D 6♣= ≻P(S0). Suppose that the agent's initial program is:

where all actions are ordinary, always executable, and controllable except for U, which is always uncontrollable. Suppose that the supervision specification is:

i.e., any action except U can be performed. It is easy to show that the offline MPS obtained using DLM's definition is different depending on whether P holds or not:

For models of the theory where P holds, the offline MPS is set(¶B↪D♦), as the set of complete offline runs of δs 4 in S0

1 Obviously there are certain sets that can be expressed directly in ConGolog, e.g., when E is finite. However in the general case, the object domain may be infinite, and set(E) may not be representable as a finitary ConGolog program.

is ¶[B↪ D]↪ [A↪ C]♦ and set(¶[A↪ C]♦) is not controllable wrt δi4 in S0. For models where P does not hold, the offline MPS is set(¶A↪ D♦), since the set of complete offline runs of δs 4 in S0 is ¶[A↪D]↪ [B↪C]♦ and set(¶[B↪C]♦) is not controllable wrt δi4 in S0. Since it is not known if P holds, it seems that a correct supervisor should neither allow A nor B.

As the above example illustrates, we have an offline MPS for each model of the theory. Instead, we want a single online MPS that works for all models and includes sensing information when acquired. The difference between offline MPS and online MPS is analogous to the difference between classical plans and conditional plans that include sensing in the planning literature [Ghallab et al., 2004].

Online Maximally Permissive Supervisor. In our account of supervision, we consider agents that may acquire knowledge through sensing and exogenous actions as they operate and make decisions based on what they know, and we model these as online SD agents. To see how we can formalize supervision for such agents, assume that we have an online SD agent σ = hD↪ δi i whose behavior we want to supervise. Also suppose that we have a supervision specification δs of what behaviors we want to allow in the supervised system and that the system hD↪ δs i is also online SD.

We say that a specification δs is online controllable wrt online SD agent σ = hD↪ δi i iff:

i.e, if we postfix a good online run ~a for hD↪ δs i with an action au that is not known to be controllable which is good for σ (and so ~a must be good for σ as well), then au must also be good for hD↪ δs i (~aau 2 GR(σ) and ~aau 2 GR(hD↪ δs i) together imply that ~aau 2 GR(hD↪ δi& δs i)). This definition, differently from DLM's, applies to online runs. Moreover it treats actions that are not known to be controllable as uncontrollable, thus ensuring that δs is controllable in all possible models/worlds compatible with what the agent knows. As DLM, we focus on good runs of the process, assuming that the agent will not perform actions that don't lead to a final configuration of δi . The supervisor only ensures that given this, the process always conforms to the specification.

Given this, we can then define the online maximally permissive supervisor mpsonl (δs ↪ σ) of the online SD agent σ = hD↪ δi i which fulfills the supervision specification δs :

i.e., the online MPS is the union of all sets of action sequences that are complete online runs of both δi and δs that are online controllable wrt the agent σ. We can show that:

Theorem 1 For the online maximally permissive supervisor mpsonl (δs ↪ σ) of the online SD agent σ = hD↪ δi i which fulfills the supervision specification δs , where hD↪ δs i is also online SD, the following properties hold:

1. mpsonl (δs ↪ σ) always exists and is unique;

1. hD↪mpsonl (δs ↪ σ)i is online SD;
2. mpsonl (δs ↪ σ) is online controllable wrt σ;
3. for every possible online controllable supervision specification ˆ δs for σ such that CR(hD↪ δi&ˆ δs i) ✓ CR(hD↪ δi&δs i), we have that CR(hD↪ δi&ˆ δs i) ✓ CR(hD↪mpsonl (δs ↪ σ)i), i.e., mpsonl is maximally permissive;
4. RR(hD↪mpsonl (δs ↪ σ)i) = GR(hD↪mpsonl (δs ↪ σ)i), i.e., mpsonl (δs ↪ σ) is non-blocking.

Example 2 If we return to the agent of Example 1, who does not know whether P holds initially, it is easy to show that our definition of online MPS yields the correct result, i.e. mpsonl (δs 4 ↪ hD↪ δi4 i) = set(¶✏♦).

Example 3 Supervision can also depend on the information that the agent acquires as it executes. Again, suppose that we have an agent that does not know whether P holds initially. Suppose also that the agent's initial program is δi5 = SenseP ; δi4 . We can show that:

Again, we have different offline MPSs depending on whether P holds. But since the exogenous report makes the truth value of P known after the first action, we get one online MPS for this agent as follows:

Because the agent queries if P holds, the supervisor has enough information to decide the maximal set of runs from then on in each case. So if the reported value of P is true, then the online supervisor should eliminate the complete run [A↪ C] as it is not controllable, and if P does not hold, the run [B↪ C] should be eliminated for the same reason.

As well, an action's controllability or whether it satisfies the specification may depend on a condition whose truth only becomes known during the execution. Such cases cannot be handled by DLM's original offline account but our online supervision account does handle them correctly.

5 Online Supervision Operator

We also introduce a meta-theoretic version of a synchronous concurrency operator δi&onl Au δs that captures the maximally permissive execution of an agent hD↪ δi i under online supervision for specification δs . Wlog, we assume that both δi and δs start with a common controllable action (if not, it is trivial to add a dummy action in front of both). We define δi&onl Au δs by extending the online transition relation as follows:

where Au( ~ au↪ s), means that action sequence ~ au is uncontrollable in situation s, and is inductively defined on the length of ~ au as the smallest predicate such that: (i) Au(✏↪ s) ⌘ true; (ii) Au(au ~ au↪ s) ⌘ Au(au↪ s) ^Au( ~ au↪ do(au↪ s)). Thus, the online maximally permissive supervised execution of δi for the specification δs is allowed to perform action a in situation do(~a↪ S0) if a is allowed by both δi and δs and moreover, if a is known to be controllable, then for every sequence of actions ~ au not known to be controllable, if ~ au may be performed by δi right after a on one of its complete runs, then it must also be allowed by δs (on one of its complete runs). Essentially, a controllable action a by the agent must be forbidden if it can be followed by some sequence of actions not known to be controllable that violates the specification.

The final configurations are extended as follows:

We can show that firstly, if both the agent and supervision specification processes are online SD, then so is the program obtained using the online supervision operator, and moreover, this program is controllable wrt to the agent process:

Theorem 2

1. If hD↪ δs i and hD↪ δi i are online SD, then so is hD↪ δi&onl Au δs i.
2. δi &onl Au δs is online controllable wrt hD↪ δi i.

Moreover, the complete runs of the program obtained using the online supervision operator are exactly the same the complete runs generated under synchronous concurrency of the agent and mpsonl (δs ↪ σ):

Theorem 3

While δi &onl Au δs and mpsonl (δs ↪ σ) have the same complete runs, they differ in their set of partial runs. In general, RR(hD↪ δi &onl Au δs i) 6= GR(hD↪ δi &onl Au δs i), i.e., the program obtained using the online supervision operator is not necessarily non-blocking. This contrasts mpsonl (δs ↪ σ), which is guaranteed to be non-blocking (Theorem 1).

Example 4 Suppose we have the agent program:

where all actions except U1 and U2 are ordinary and controllable. Moreover, assume the supervision specification is:

i.e. any action except D can be performed. The online MPS for this agent is simply set(¶A♦), since CR(hD↪ δs 6 i) = ¶A↪ [B↪C↪U1]♦ and set(¶[B↪C↪U1]♦) is not controllable wrt δi6 . However, under online supervised execution, the agent may execute the action B. We have hδi6&oln Au δs 6 ↪ ✏i !B hδ06&onl Au δs 6 ↪Bi where δ06 is what remains from δi6 after executing B. The resulting program is not final in do(B↪ S0), yet there is no transition from this state, as the action C could be followed by the uncontrollable action U2 and it is not possible to ensure successful completion of the process, as the action D is not allowed. Thus, one must do lookahead search over online executions of δi6 &onl Au δs 6 to obtain good/complete runs. We propose such a search/lookahead construct next.

6 Search Over a Controllable Process

When we have a specification/process δs that is (online) controllable wrt an agent hD↪ δi i (e.g. δi &onl Au δs ), for any choice of uncontrollable action that is on a good run of δi , it is always possible to find a way to continue executing δs until the process successfully completes. We define a search construct 2 that makes an arbitrary choice of action that is on a good run of δi when the action is not known to be controllable, while still only performing actions that are on a good run of δs otherwise. We call this construct weak online search ⌃wonl (δs ↪ δi ) and define it (metatheoretically) as: 3

The final configurations are extended as follows:

It is easy to show that:

Theorem 4 If hD↪ δs i and hD↪ δi i are online SD, than so is hD↪ ⌃wonl (δs ↪ δi )i.

Now, we can show that the weak online search construct has many nice properties when the process is controllable:

Theorem 5 Suppose that we have an agent hD↪ δi i, and a supervision specification δs which are online SD. Suppose also that δs is online controllable with respect to hD↪ δi i, and that CR(hD↪ δs i) ✓ CR(hD↪ δi i). Then we have that:

1. CR(hD↪⌃wonl (δs ↪ δi )i) = CR(hD↪ δs i), i.e. the complete runs of ⌃wonl (δs ↪ δi ) are the complete runs of δs .
2. If CR(hD↪ δs i) 6= ;, then RR(hD↪⌃wonl (δs ↪ δi )i) = GR(hD↪ δs i), i.e., the partial runs of ⌃wonl (δs ↪ δi ) are the good runs of δs .
3. If CR(hD↪ δs i) 6= ;, then RR(hD↪⌃wonl (δs ↪ δi )i) = GR(hD↪⌃wonl (δs ↪ δi )i), i.e., partial runs must be good runs, and the resulting program is "non blocking".

It is also easy to show that none of these properties hold for arbitrary non-controllable processes.

Now we can show that if we apply this weak lookahead search to δi &onl Au δs , we obtain a program that has the same partial runs as mpsonl (δs ↪ σ) and is thus non-blocking:

2 In IndiGolog a simple type of search is provided that only allows a transition if the remaining program can be executed to reach a final state [De Giacomo and Levesque, 1999]. However, this search does not deal with sensing and online executions.

3 Since δi can include exogenous actions, in general, executions of the process could actually perform exogenous actions that are not on a good run of δi . However, in this paper we are interested in the case where the exogenous actions are mainly sensor reports and external requests (rather than the actions of an adversary) and assume that this won't occur. Handling adversarial nondeterminism in δi is left for future work.

If we apply the weak online search construct over δi6 &onl Au δs 6 in Example 4, we no longer have an online transition involving action B; the only possible online transition is h⌃wonl (δi6&onl Au δs 6 ↪ δi6 )↪ ✏i !A h⌃wonl (nil &onl Au δs 6 ↪ nil)↪ Ai where action A is performed, after which we have (h⌃wonl (nil &onl Au δs 6 ↪ nil)↪ Ai)X.

7 Discussion

A popular approach to automated service composition [McIlraith and Son, 2002; Sohrabi et al., 2006] customizes a generic ConGolog process based on the user's constraints. [Sardi˜na and De Giacomo, 2009] on the other hand, synthesizes a controller that orchestrates the concurrent execution of library of ConGolog programs to realize a target program not in the library. However, they assume complete information on the initial situation, and their controller is not maximally permissive. In related work, [De Giacomo et al., 2013b] synthesize a controller generator that represents all possible compositions of the target behavior and may adapt reactively based on runtime feedback. In [Yadav et al., 2013], optimal realization of the target behavior (in the presence of uncontrollable exogenous events) is considered when its full realization is not possible. [Alechina et al., 2015] regulates multiagent systems using regimented norms. A transition system describes the behavior of a (multi-) agent system and a guard function can enable/disable options that (could) violate norms after a system history (possibly using bounded lookahead). Finally, the approach in [Aucher, 2014] reformulates the results of supervisory control theory in terms of model checking problems in an epistemic temporal logic. While these approaches model behaviors as (nondeterministic) finite state transition systems, our approach enables users to express the system model and the specifications in a high-level expressive language. Moreover, due to its first-order logic foundations, it can handle infinite object domains and infinite states.

In this paper we have developed an account of supervision for agents that execute online and can acquire new knowledge as they operate. The framework uses a truely first-order representation of states and allows for an infinite object domain and infinite states. Proofs and examples of using online agent supervision to customize a travel planner agent are presented in [Banihashemi et al., 2016a]. If the object domain is finite, then finite-state techniques developed for discrete events systems [Wonham and Ramadge, 1987] can be adapted to synthesize a program that characterizes the online MPS. It should also be possible to effectively synthesize supervisors for agents that use bounded action theories [De Giacomo et al., 2013a; 2014]; verification of temporal properties over such agents is known to be decidable.

Acknowledgments

We acknowledge the support of Sapienza 2015 project "Immersive Cognitive Environments" and the National Science and Engineering Research Council of Canada.