Supremal Realizability of Behaviors with Uncontrollable Exogenous Events

1 Introduction

The behavior composition problem amounts to whether a set of available, though partially controllable, behavior modules (e.g., smart robotic devices such as automatic blinds and lights, audio and screen devices, video cameras) can be suitably coordinated (i.e., composed) in a way that it appears as if a desired but non-existent target behavior (e.g., a house entertainment or surveillance system) is being executed. The problem is appealing in that with computers now present in everyday devices like phones, cars and planes or places like homes, offices and factories, the trend is to build embedded complex systems from a collection of simple components. Indeed, the composition problem has been studied in various areas of computer science, including (web) services [Balbiani et al., 2008], AI reasoning about action [Sardina et al., 2008; Stroeder and Pagnucco, 2009; De Giacomo et al., 2013], verification [Lustig and Vardi, 2009], and robotics [Bordignon et al., 2007]. From an AI perspective, a behavior refers to the abstract operational model of a device or program, and is generally represented as a nondeterministic transition system.

The classical behavior composition task has been extensively investigated in the recent literature (see [De Giacomo et Giuseppe De Giacomo Sapienza Univ. di Roma Roma, Italy

∗The last author acknowledges the support of the Australian Research Council under grant DP120100332.

degiacomo@dis.uniroma1.it

Sebastian Sardina RMIT University

Melbourne, Australia

sebastian.sardina@rmit.edu.au

al., 2013] for an extensive review). However, one open issue has resisted principled solutions: if the target specification is not fully realizable, is there a way to realize it "at best"? Stroeder and Pagnucco [2009] were the first to highlight this issue and proposed a search-based method that could eventually be adapted to compute approximate solutions "close" to the perfect one. However, they did not detail what those "approximations" look like. Then, Yadav and Sardina [2012] developed an account of "approximate" composition where the task is to return an alternative target closest to the original one, but fully solvable. While their proposal, based on the formal notion of simulation, comes as a principled generalization of the classical framework, it did not provide ways to actually compute such solutions for the general case, but only for the special case of deterministic behaviors.

In this paper, we present a novel technique to effectively build the largest realizable fragment-the "supremal"-of a given target specification for the general composition case in which available behaviors may be nondeterministic. The technique relies on two simple and well-known operations over transition systems (or state models), namely, cross product and belief-level state construction. In doing so, we provide an elegant result on the uniqueness of such fragments.

Then, we investigate-inspired by work on AI reasoning about action [Reiter, 2001] and on discrete event systems [Cassandras and Lafortune, 2006]-the composition task in the presence of exogenous events. These are special events that behaviors may spontaneously generate, such as the light bulb of a projector fusing when turned on. Importantly, such events are uncontrollable and their occurrence cannot be disabled. As a result, we obtain a strictly more general composition framework. We demonstrate that the supremal realizable target can again be defined and computed. However, this time, solutions come into two variants, depending on the ability of the target's user to observe such events. If exogenous events can be observed by the user, then the supremal fragment may be conditional on such events (e.g., if the projector's light bulb fuses, the user may only request changing the bulb). Otherwise, the supremal ought to be comformant to all possible exogenous events that may ensue.

2 Preliminaries

We briefly review the classical composition framework [Sardina et al., 2008; Stroeder and Pagnucco, 2009; De Giacomo et al., 2013]. We omit wlog the environment for simplicity.

Behavior A behavior represents the operational logic of a device or a program and it is modeled using a finite transition system. Formally, a behavior is a tuple B = 〈B,A, b0, ϱ〉, where:

• B is the finite set of behavior's states;
• A is the set of actions;
• b0 ∈ B is the initial state;
• ϱ ⊆ B × A × B is the behavior's transition relation, where 〈b, a, b′ 〉 ∈ ϱ, or b a -→ b′ in B, denotes that action a executed in behavior state b may lead the behavior to successor state b′ .

Observe that since behaviors may be nondeterministic, one cannot know beforehand what actions will be available to execute after an action is performed in a state, as the next set of applicable actions would depend on the successor state in which the behavior happens to be in. Hence, we say that nondeterministic behaviors are only partially controllable. A deterministic behavior is one where the successor state is always uniquely determined-a fully controllable behavior.

Available System The system stands for a collection of behaviors that are at disposal. Technically, an available system is a tuple S = 〈B1, . . . , Bn〉, where Bi = 〈Bi,Ai, bi0, ϱi〉, for i ∈ {1, . . . , n}, is a, possibly nondeterministic, behavior, called an available behavior in the system. To refer to the behavior that emerges from the joint execution of available behaviors, the notion enacted system behavior is used in the literature [De Giacomo et al., 2013]. The enacted system behavior of a system S is a tuple ES = 〈S, AS , s0, δ〉, where:

• S = B1 × · · · ×Bn is the finite set of ES's states; when s = 〈b1, . . . , bn〉, we denote bi by behi(s), for i ≤ n;
• AS = ⋃ni=1 Ai is the set of actions of ES;
• s0 = 〈b10, . . . , bn0〉 ∈ S is ES's initial state;
• δ ⊆ S×AS ×{1, . . . , n}×S is ES's transition relation, where 〈s, a, k, s′ 〉 ∈ δ, or s a,k -→ s′ in ES, iff:

Target Specification A target behavior specification T = 〈T,AT , t0, ϱT 〉 is a behavior specification that stands for the desired, though not directly available, functionality to be obtained. Following in particular [Yadav and Sardina, 2012], the idea is that the user agent is meant to request transitions in T in a step-by-step fashion, and the action in the chosen transition is suitably delegated by a controller to one of the available behavior of the system.

So, informally, the behavior composition task can be stated as follows: Given a system S and a target behavior T , is it possible to (partially) control the available behaviors in S in a step-by-step manner-by instructing them on which action to execute next and observing, afterwards, the outcome in the behavior used-so as to "realize" the desired target behavior. In other words, by adequately controlling the system, it appears as if one was actually executing the target behavior.

Consider the presentation room scenario depicted in Figure 1, ignoring all dashed transitions. There are two available behaviors, a projector BP and a speaker system BA. The projector allows setting of the SOURCE and WARMUP of the device in any order, followed by turning it OFF. The speaker on the other hand can simply be toggled on/off. The question then is whether these two devices are enough to be able to run the desired target behavior T . The answer, in this case, is yes.

Exact Compositions via Simulation Though technically involved, one can formally define when a so-called controller, a function taking a run of the system and the next action request and outputting the index of the available behavior where the action is being delegated, realizes the target behavior; see [De Giacomo and Sardina, 2007; De Giacomo et al., 2013]. Such controllers are called exact compositions, solutions to the composition problem guaranteeing the complete realization of the target in the system. In our presentation room example, there exists an exact composition for target behavior T in available system 〈BP, BA〉.

An interesting and much used result links exact compositions to the formal notion of simulation [Milner, 1971]. A simulation relation captures the behavioral equivalence of two transition systems. Intuitively, a (transition) system S1 "simulates" another system S2, denoted S2 ⪯ S1, if S1 is able to match all of S2's moves. Thus, Sardina et al. [2008] defined a so-called ND-simulation (nondeterministic simulation) relation between (the states of) the target behavior T and (the states of) the enacted system ES , denoted ⪯ND, and prove that there exists an exact composition for a target behavior T on an available system S iff T ⪯ND ES, that is, the enacted system can ND-simulate the target behavior. While in this paper we do not really need the details of ND-simulation, the plain notion of simulation plays a key role, so let us introduce it formally. Let Ti = 〈Si,A, si0, ϱi〉, where i ∈ {1, 2}, be two transition systems. A simulation relation of T2 by T1 is a relation Sim ⊆ S2 × S1 such that 〈s2, s1〉 ∈ Sim iff: ∀a, s′2 .〈s2, a, s′2 〉 ∈ ϱ2 ⇒ ∃s′1 〈s1, a, s′1 〉∈ ϱ1∧〈s′2 , s′1 〉∈Sim. We say that a state s2 ∈ S2 is simulated by a state s1 ∈ S1 (or s1 simulates s2), denoted s2 ⪯ s1, iff there exists a simulation relation Sim of T2 by T1 such that 〈s2, s1〉 ∈ Sim. Observe that relation ⪯ is itself a simulation relation (of T2 by T1), and in fact, it is the largest simulation relation, in that all simulation relations are contained in it. We say that a transition system T1 simulates another transition system T2, denoted T2 ⪯ T1, if it is the case that s20 ⪯ s10. Two transition systems are said to be simulation equivalent, denoted T1 ∼ T2, whenever they simulate each other.

Approximated Compositions The classical composition task described above has been extensively studied in the literature and various extensions-e.g., distributed and multitarget composition, composition under uncertainty-have been developed (see [De Giacomo et al., 2013] for a comprehensive review). However, such frameworks may prove insufficient for composition instances admitting no exact solutions (i.e., unsolvable instances)-a mere "no solution" answer may be highly unsatisfactory in many settings.

The first one to concretely deal with this issue was Stroeder and Pagnucco [2009]. In their work, they claimed that their search-based method "can easily be used to calculate approximations," that is, controllers that may not qualify as exact solutions but come "close" (enough) to them. They argue approximations are useful when no exact solution exists and when one is willing to trade faster solutions at the expense of incompleteness (of target realizability). Nonetheless, the authors did not provide a semantics of what these "approximations" are and what "closeness" means, both were left as important future work.

Later, Yadav and Sardina [2012] looked closer at a composition framework that can better accommodate unsolvable instances. In doing so, however, they proposed to focus on approximating the target, rather than the controller. To that end, they defined, based on the notion of simulation, what they called target approximations, namely, alternative target behaviors that are "contained" in the original target while enjoying exact composition solutions. In turn, they defined the optimal target approximation as that one which is "closest" possible to the original target (and that is fully realized by some controller). In fact, they showed that such an optimal target is unique. They also provided a technique to compute such a solution, but only for the special case of deterministic behaviors. Here, we will provide a general technique as well as the complexity characterization of the problem.

3 Supremal Realizable Target Behavior

We adopt the approach of Yadav and Sardina [2012] to define the notion of realizable target from a target specification. We do not call it "approximation" in light of the extension with exogenous events that we study later. Indeed, once exogenous events are mentioned in the target specification, such a specification is not directly a target behavior anymore.

Formally, we say that behavior ˜ T is a realizable target behavior (RTB) of target specification T in system S iff

1. ˜ T ⪯ T (that is, ˜ T is "contained" in T );
2. ˜ T ⪯ND ES, i.e, there is an exact composition for ˜ T on S (that is, it is fully realizable).

Notice that we elected "simulation" as the measure for comparing target behaviors. In particular if T1 ⪯ T2 this means that an agent can mimic the behavior T1 by suitably choosing the transitions to traverse in T2. If T1 and T2 are simulation equivalent (i.e., T1 ⪯ T2 and T2 ⪯ T1) then the agent can mimic exactly one behavior using the other one, hence from the point of view of the agent the two behaviors are identical.

A behavior ˜ T is "the" supremal realizable target behavior (SRTB) of target T on systemS iff ˜ T is a RTB of T in S and there is no RTB ˜ T ′ such that ˜ T ≺ ˜ T ′ , that is, ˜ T is the largest realizable fragment of T . It can be shown that the SRTB is unique up to simulation equivalence.

We provide a simple and elegant characterization of SRTB as follows. Let T1 ∪ T2 = 〈T,A, t10, ϱ〉, where Ti = 〈Ti,Ai, ti0, ϱi〉 have disjoint states, be the resulting unified

(target) behavior where T2's initial state is merged with T1's: (i) T = T1 ∪ (T2 \ {t20}); (ii) A = A1 ∪ A2; and ϱ = ϱ1 ∪ ϱ2|t10 t20 (ϱ|t′ t is relation ϱ with all states t replaced with t′ ).

Theorem 1 Let ˜ T1 and ˜ T2 be two RTB for target specification T in system S. Then ˜ T1 ∪ ˜ T2 is an RTB for T in S too.

In words, RTBs are closed under union. With this in mind, it is not hard to see that one can build the largest RTB-the supremal-by taking the union of all realizable targets.

Notice that any ˜ T which is simulation equivalent to T ∗ is also "the" SRTB (we focus on semantics not syntax here).

Obviously, it remains to be seen if the SRTB can actually be computed and represented finitely. This is what we do next. Our technique to synthesize the SRTB relies on two simple operations on transition systems, namely, a specific synchronous product and a conformance enforcing procedure. Roughly speaking, the technique is as follows:

1. We take the synchronous product of the enacted system ES and the target T , yielding the structure F〈S,T 〉.
2. We modify F〈S,T 〉 to enforce conformance on its states which cannot be distinguished by the user of the target.

In fact the second step is needed only when the system includes nondeterministic available behaviors.

Full enacted system The full enacted system models the behavior that emerges from joint parallel execution of the enacted system and the target. Formally, given the enacted system ES = 〈S,AS, s0, δ〉 for a system S = 〈B1, . . . , Bn〉 and a target specification T = 〈T,AT , t0, ϱT 〉, the full enacted system of T and S, denoted by T × ES, is a tuple F〈S,T 〉 = 〈F, AF , f0, γ〉, where:

• F = S × T is the finite set of F〈S,T 〉's states; when f = 〈s, t〉, we denote s by sys(f) and t by tgt(f);
• f0 = 〈s0, t0〉 ∈ F, is F〈S,T 〉's initial state;
• AF = AS ∪ AT (note that we allow for AS ̸= AT );
• γ ⊆ F × AF × {1, . . . , n} × F is F〈S,T 〉's transition relation, where 〈f, a, k, f ′ 〉∈γ, or f a,k -→f ′ in F〈S,T 〉 iff
• tgt(f) a -→ tgt(f ′ ) in T ; and
• sys(f) a,k -→ sys(f ′ ) in ES.

Observe that the transition relation of the full enacted system requires both the enacted system and the target to evolve jointly: the full enacted system is the synchronous product of the target specification and the enacted system.

As expected, the synchronous product (once we project out the indexes {1, . . . , n}) is simulated by both the enacted system and the target (i.e., T × ES ⪯ ES and T × ES ⪯ T ). If the system includes only deterministic available behavior the regular simulation T ×ES ⪯ ES suffices to conclude that the composition exists (ND-simulation is not needed in this case) [Sardina et al., 2008] . Hence, by Theorem 2, if available behaviours are deterministic T × ES is included in, and simulation by, T ∗ . The converse can be shown along the line suggested in [Yadav and Sardina, 2012]. Hence:

Theorem 3 Let S = 〈B1, . . . , Bn〉 be a deterministic available system and T = 〈T,AT , t0, ϱT 〉 a target specification behavior. Then, F〈S,T 〉 is the SRTB of T in S.

Also from the construction of F〈S,T 〉 we can conclude that building the SRTB of T in S can be done in exponential time in the number of behaviors and polynomial in the number of states in each behavior.

When we consider nondeterministic available modules, and hence resort to ND-simulation, this is not true anymore. Indeed, there are examples where T × ES ⪯ND ES does not hold due to the nondeterminism present in ES. In those cases, the full enacted system is a sort of target behavior in which agent transition requests are conditional on the nondeterministic execution of available behaviors. However, the agent using the target is not meant to have observability on such behaviors, and so it cannot decide its request upon such contingencies. Figure 2 shows one such case. Take product T ×ES as a candidate for SRTB. After fulfilling transition request q0 a -→ q2 using module B1, the next request q2 c -→ q0 can only be honored if B1 happens to evolve to state b2, but this is not guaranteed. Therefore, T × ES cannot be realized by B1 and hence it is not an RTB of T in S.

What we need, is the target to be conformant, i.e., independent of conditions on the available behaviors states. Hence inspired by the literature on planning under uncertainty we construct a sort of belief states, and in turn, the belief level full enacted system. The idea behind generating the belief states is to track the states where the enacted system could evolve. Given a full enacted system F〈S,T 〉 = 〈F,AF, f0, γ〉 for a target T = 〈T,AT , t0, ϱT 〉 and a system S = 〈B1, . . . , Bn〉 where Bi = 〈Bi,Ai, bi0, ϱi〉 for i ≤ n, the belief-level full enacted system is a tuple K〈S,T 〉 = 〈Q, AF , q0, δK〉, where:

• Q = 2(B1×···×Bn) × T is K〈S,T 〉's set of states; when q = 〈{s1, . . . , sℓ}, t〉 ∈ Q we denote {s1, . . . , sℓ} by sys(q) and t by tgt(q);
• q0=〈{s0}, t0〉 such that f0=〈s0, t0〉, is the initial state;
• δK ⊆ Q×A×Q is K〈S,T 〉's transition relation, where 〈〈S, t〉, a, 〈S′ , t′ 〉〉∈δK iff :
• there exists a set Indx = {〈s1 : k1〉, . . ., 〈sℓ : kℓ〉} such that {s1, . . . , sℓ} = S; and 〈si, t〉 a,ki -→ 〈s′ , t′ 〉 in F〈S,T 〉 for all i ≤ ℓ; that is, the action a must be executable from all enacted system states in S; and
• S′ = ⋃〈s:i〉∈Indx{s′ | 〈〈s, t〉, a, i, 〈s′ , t′ 〉〉 ∈ γ}; that is, S′ should contain all successors of enacted system states in S resulting from action a.

Observe, K〈S,T 〉 is nondeterministic with respect to target evolutions and different behavior delegations. Note also that K〈S,T 〉 can be built in time 2O(|B|n ) where |B| is the number of states of the largest behavior in S, and n is the number of available behaviors in S. Observe, however, that K〈S,T 〉 can be computed on-the-fly in a step-wise fashion: given the current belief state q we can generate the next possible states without looking at any other state in Q.

Next, we show that K〈S,T 〉 is the finite representation of SRTB T ∗ of target T in system S (see Theorem 2).

Theorem 4 Let S be an available system and T a target specification behavior. Then, K〈S,T 〉 is the SRTB of T in S.

PROOF (SKETCH). Let T ∗ be the SRTB of T in S. Suppose T ∗ is not simulated by K〈S,T 〉. Therefore, there exists a finite trace τ ′ of a RTB T ′ contained in T ∗ whose last transition cannot be simulated by any trace of K〈S,T 〉. Observe, there exists a trace τ of T such that τ simulates τ ′ . Moreover, there exists a set of traces Γ in S, induced as a result of realizing τ ′ . Using τ and Γ we construct a trace τK of K〈S,T 〉 such that, each state τK[i] comprises of τ[i] and set of states Γ[i], where x[i] denotes the i-th state of trace x, and Γ[i] is the union of ith state of each trace in Γ. Such a trace τK is a legal trace of K〈S,T 〉 and simulates τ ′ , thereby, contradicting our assumption. Since, by construction, K〈S,T 〉 is a RTB of T in S, by definition it is contained in T ∗ . Therefore, T ∗ and K〈S,T 〉 are simulation equivalent.

We note some similarities in the use of belief-level behaviors with the work in [De Giacomo et al., 2009] for composition under partial observability of the available behaviors. There the controller required to be conformant, here instead the target behavior must be so.

4 Composition with Exogenous Events

With an effective technique to synthesize the supremal realizable target at hand, we now turn to the second contribution of this paper. Inspired by discrete event systems [Cassandras and Lafortune, 2006] and reasoning about action work for dynamic systems [Reiter, 2001], we show here how to accommodate exogenous uncontrollable events into the composition framework in a parsimonious manner. In doing so, it will come clear how robust and elaboration tolerant the definition of SRTBs and the technique to compute them are.

Let us return to our presentation room example in Figure 1. Suppose that when the projector's light bulb is onafter WARMUP has been executed-it may FUSE anytime and requires the device to be repaired. Similarly, if a source is set before warming up the projector, an ERROR may occur and the projector will need to be RESET. The occurrence of both events-FUSE and ERROR-is outside the control of the client or the controller, they occur spontaneously. Hence, they are akin to exogenous events in reasoning about action literature [Reiter, 2001] and uncontrollable events in discrete event systems [Cassandras and Lafortune, 2006].

Next, we extend the classical composition framework from Section 2 with exogenous events. To that end, we assume that the set of actions A in a behavior is partitioned into domain (AC ) and exogenous (AU ) events, that is, A = AC ∪AU and AC ∩ AU = ∅. Furthermore, as standard in discrete event systems, we assume exogenous events to be deterministic. 1

We note that exogenous events play an inherently different role in available behaviors than nondeterminism. Exogenous (uncontrollable) events may happen anytime from a relevant state (e.g., p1 in BP), which allows modeling of concepts such as delayed uncertainty. Moreover, whereas nondeterminism is not observable to the target's user (in fact, the user agent is not even aware of the internal logic of available behaviors), exogenous events may be. Hence, the user of the projector room may be able to observe the light bulb fusing.

When it comes to the target specification, exogenous event transitions represent those transitions that are accountedaccepted-by the target but outside the controller of the user of the target. Thus, when the target is in state t2, it only allows one exogenous event, namely, event FUSE, whose occurrence will cause the target to evolve to state t6 where its user is only allowed to request repairing the projector.

Since the user may be able to observe exogenous events, we can now consider-unlike standard composition-two types of composition solutions. Following planning terminology, a conditional SRTB is one that assumes the user is able to observe exogenous events, whereas a conformant SRTB is one where such events are non-observable to the user.

In this section, we formally define conditional and conformant solution concepts and explain how to generalize the technique developed in Section 3 to compute such solutions.

Enacted and full enacted system The formal definitions of the enacted system and the full enacted system remain same, except we assume the action set to be partitioned into controllable actions and uncontrollable exogenous events. In addition, given a full enacted system F〈S,T 〉 = 〈F,ACF ∪ AUF , f0, γ〉 for an enacted system ES = 〈S, ACS ∪ AUS , s0, δ〉

1 Should this not be the case, we can model the various outcomes with different uncontrollable exogenous events.

and a target specification T = 〈T, ACT ∪ AUT , t0, ϱT 〉, we define set ∆〈S,T 〉 as those states in F〈S,T 〉 from where prohibited exogenous events may fire. Formally,

4.1 Conditional SRTBs

When it comes to formally defining conditional SRTBs, interestingly, the definition of SRTBs from the classical framework (see Section 3) fits as is. However, we need to define exact solutions in the context of exogenous events. We do this by extending the ND-simulation relation in the light of exogenous events.

A transition system ˜ T = 〈 ˜ T, ˜ ACT ∪ ˜ AUT , ˜ t0, ˜ ϱT 〉 is a conditional-RTB for a target T = 〈T, ACT ∪AUT , t0, ϱT 〉 in system S with enacted system ES = 〈S, ACS ∪AUS , s0, δ〉 iff ˜ T ⪯ T and 〈 ˜ t0, s0〉 ∈ C where C ⊆ ˜ T × S is the conditional simulation relation of ˜ T by ES such that 〈˜ t, s〉 ∈ C iff:

1. ∀˜ t′ ∀a ∈ ˜ ACT ∃k ∀s′ (〈˜ t, a, ˜ t′ 〉 ∈ ˜ ϱT ⇒ 〈s, a, k, s′ 〉 ∈ δ) such that 〈˜ t′ , s′ 〉 ∈ C; and
2. ∀α ∈ AUS , ∀k(〈s, α, k, s′ 〉 ∈ δ ⇒ 〈˜ t, α, ˜ t′ 〉 ∈ ˜ ϱT ) such that 〈˜ t′ , s′ 〉 ∈ C.

The first condition (analogous to ND-simulation) requires all controllable actions of the RTB to be feasible. The second defines how uncontrollable exogenous events should be treated: since they are uncontrollable, their occurrences must be allowed in the target. If we want to prevent the occurrence of some exogenous event this can only be done by cutting some controllable action ahead of exogenous event's possible occurrence. This is related to the notion of controllability in discrete event systems [Wonham and Ramadge, 1987].

As usual, a conditional RTB is supremal iff it is not strictly simulated by any other conditional RTB. Consider our media room example (Figure 1), ˜ T2 is conditioned on FUSE and prohibits ERROR. Indeed, while realizing ˜ T2, it is guaranteed that ERROR will never occur.

Computing conditional SRTBs When it comes to computing conditional-SRTBs, we modify the belief level construction to allow for exogenous events. Notice that exogenous events are considered to be observable in this case, so we can use their occurrence to refine the belief states in the belieflevel full enacted system. This leads to the following definition: given a belief level full enacted system K〈S,T 〉 = 〈Q,ACF ∪ AUF , q0, δK〉 for full enacted system F〈S,T 〉 = 〈F,ACF ∪AUF , f0, γ〉, the conditional belief-level full enacted system is a tuple KC 〈S,T 〉 = 〈QC , ACF ∪ AUF , q0, δCK 〉, where:

• QC = Q \ {〈S, t〉 | 〈s, t〉 ∈ ∆〈S,T 〉, s ∈ S}; that is, prohibited exogenous events should never occur;
• δCK ⊆ Q×A×Q is KC 〈S,T 〉 's transition relation, where 〈〈S, t〉, a, 〈S′ , t′ 〉〉∈δCK iff :
• a ∈ ACF and 〈〈S, t〉, a, 〈S′ , t′ 〉〉∈δK; that is, action a should be executable from all enacted states; and
• a∈AUF and S′={s′ | 〈〈s, t〉, a, k, 〈s′ , t′ 〉〉∈γ, s∈S}; we revise belief state if an exogenous event occurs.

Next result shows that the conditional belief-level full enacted system is the SRTB in this context.

Theorem 5 Let S be an available system and T a target spec. Then, KC 〈S,T 〉 is the conditional-SRTB of T in S.

4.2 Conformant SRTBs

Conformant solutions guarantee realizability in absence of any observation over exogenous events. For example, the conformant solution ˜ T1 in Figure 1 contains a very restricted subset of the target as, if the bulb is fused then the projector cannot be operated again without a REPAIR. Solutions of such type are stricter, promising execution irrespective of which uncontrollable events occur. This provides robustness in modelling as one can still prevent unacceptable conditions under non-observability at runtime. We say a RTB to be conformant if it does not include any exogenous event, that is, AUT = ∅. Note, the target specification (problem input) is allowed to have exogenous events, however, a conformant RTB must have compiled them away. More precisely, a transition system ˜ T = 〈 ˜ T, ˜ ACT , ˜ t0, ˜ ϱT 〉 is a conformant-RTB for a target T = 〈T, ACT ∪ AUT , t0, ϱT 〉 in system S with enacted system ES = 〈S,ACS ∪AUS , s0, δ〉 iff ˜ T ⪯ T and 〈˜ t0, s0〉 ∈ Z where Z ⊆ ˜ T ×S is the conformant simulation relation of ˜ T by ES such that 〈˜ t, s〉 ∈ Z iff:

1. ∀˜ t ∀a ∃k∀s′ (〈˜ t, a, ˜ t′ 〉 ∈ ˜ ϱT ⇒ 〈s, a, k, s′ 〉 ∈ δ) such that 〈˜ t′ , s′ 〉 ∈ Z;
2. ∀α ∈ AUS , ∀k(〈s, α, k, s′ 〉 ∈ δ ⇒ 〈˜ t, s′ 〉 ∈ Z); and
3. ∀α ∈ AUS , ∀k(〈s, α, k, s′ 〉∈δ ∧ 〈˜ t, t〉 ∈⪯⇒〈t, α, t′ 〉 ∈ ϱT ) such that 〈˜ t, t′ 〉 ∈⪯.

The first condition is analogous to the usual ND-simulation one. The second condition requires occurring of exogenous events should retain the simulation relation. The third condition enforces only permitted exogenous events to ever occur in the system. As usual, a conformant RTB is supremal iff it is not strictly simulated by any other conformant RTB.

Computing conformant SRTBs Conformant solutions require realizability guarantee irrespective of any nondeterministic or exogenous evolution. In order to include them in the belief-level system we first define what we call as the ε-closure of a state. That is, where all could the system be as a result of an exogenous event from that state. Formally, given a full enacted system F〈S,T 〉 = 〈F,ACF ∪ AUF , f0, γ〉 and a state f ∈ F, the ε-closure of f, denoted by ε(f), is defined recursively as follows:

1. f ∈ ε(f), that is, the state itself is in the closure;
2. ∀α∈ AUF , ∀f ∈ ε(f) (f α,k -→ f ′ ∈ γ ⇒ f ′ ∈ε(f)), that is, all exogenous event reachable states are included; and
3. Nothing else except for 1 and 2 should be in ε(f).

Next, we re-define the belief level full enacted system to accommodate exogenous events. Here, we consider the ε-closure in both the initial state and the transition relation. Given a full enacted system F〈S,T 〉 = 〈F,ACF ∪

AUF , f0, γ〉 for a target T = 〈T,AT , t0, ϱT 〉 and a system S = 〈B1, . . . , Bn〉, the conformant belief-level full enacted system is a tuple KZ 〈S,T 〉 = 〈Q, ACF , q0, δK〉, where:

• Q = 2(B1×···×Bn×T) \ {S | s ∈ ∆〈S,T 〉, s ∈ S};
• q0=ε(f0) is KZ 〈S,T 〉 's initial state;
• δK ⊆ Q×A×Q, where 〈S, a, S′ 〉∈δK iff :
• there exists a set Indx = {〈s1 : k1〉, . . ., 〈sℓ : kℓ〉} such that {s1, . . . , sℓ} = S; si a,ki -→ s′i in F〈S,T 〉 for all i ≤ ℓ; and for all i, j ≤ ℓ if tgt(si) = tgt(sj), then tgt(s′i ) = tgt(s′j ); and
• S′ = ⋃〈s:i〉∈Indx{ε(s′ )|〈s, a, i, s′ 〉 ∈γ}, that is, S′ should contain the ε-closure of all successors of enacted system states in S resulting from action a.

Note, the belief level full enacted system is now exponential also on the target states. Observe, if the target specification allows all exogenous events at any point then the complexity in regards to the target will no longer be exponential.

Theorem 6 Let S be an available system and T a target spec. Then, KZ 〈S,T 〉 is the conformant-SRTB of T in S.

5 Conclusion and Future work

In this paper, we proved that every classical behavior composition problem instance has an optimal supremal solution (Theorem 2) and that such supremal can be effectively built using cross-product between transition systems and belieflevel state construction operations combined (Theorem 4). What is more, borrowing notions from discrete-event systems and reasoning about action, we showed how to accommodate exogenous uncontrollable events to obtain a more expressive composition framework (Section 4). We demonstrated that the definitions and techniques for supremal fragments can be adapted to this new framework (Theorems 5 and 6).

Many issues remain to be investigated. First, we aim to confirm the conjecture that our technique builds SRTBs that are optimal wrt worst-case complexity, thus implying that synthesis of supremals is, in general, more difficult than synthesis of exact composition controllers.

Second, our approach to realizing a target specification to the "best" possible is developed within a strict uncertainty context. This contrasts with the decision-theoretic approach of Yadav and Sardina [2011], where they proposed to optimize the expected reward of controllers. It would be interesting to adopt such a quantitative framework focusing on targets and devising a suitable decision-theoretic notion of SRTBs.

Finally, one may devise approaches that trade optimality for faster computation, such as restricting realizable target fragments to merely removing transitions from the original target specification, bounding its number of states, or computing it in anytime fashion. This paper provides principled means to assess the quality of such approximate approaches.

We close the paper by noting that there are some interesting links between behavior composition in AI and work on controllability in discrete event systems [Cassandras and Lafortune, 2006; Sun et al., 2010]. Exploring those links is indeed worth investigating as it can facilitate synergies between these two different fields.