Automatic Synthesis of New Behaviors from a Library of Available Behaviors

1 Introduction

Imagine an intelligent system built from a variety of different components or devices operating (that is, performing actions) on the same shared environment. For example, consider the case of a blocks world scenario in which different kind or versions of robotic arms can move, paint, clean, dispose blocks, and so on. Next, imagine that the central system possesses some information about the logic of these components or devices-e.g., a particular arm type can paint or clean a block after picking it up, but another type of arm is only capable of painting blocks. However, the knowledge about these devices is partial in that their internal logic may potentially expose nondeterministic features. For instance, the systemmay have no information regarding the use of paint in a painting arm, and thus, it is always unable to predict whether the arm will run out of paint after a painting action. If it does, then the arm cannot be used to paint again until it is recharged. Nonetheless, the central system has full observability on the state of

Sebastian Sardina

Department of Computer Science RMIT University Melbourne, Australia

ssardina@cs.rmit.edu.au

the devices in question: after the arm is used to paint a block, the central system will come to know whether such arm ran out of paint or not (maybe via a sensor light). Finally, the central system is also (partially) knowledgeable about the shared environment, in which all the components ought to execute. As with the devices, the system possesses a nondeterministic model of the real environment and has full observability on it too. The question then is: can the central system (always) guarantee a specific deterministic overall behavior by (partially) controlling the available devices or components in a step-by-step manner, that is, by instructing them on which action to execute next and observing, afterwards, the outcome in the device used as well as in the environment?

It is not hard to see that the above setting can be recast in a variety of forms. In the context of agent-oriented programming [6; 4], an intelligent agent may control the execution of a set of predefined nondeterministic agent plans in order to realize a desired deterministic plan-intention, which in turn, may have been obtained via planning [13; 8]. Similarly, when it comes to plan coordination [9], one can think of coordinating or merging approximate models of multiple agents' plans into a global fully deterministic multi-agent plan. Also, in the context of web-service composition [12; 1; 3], 1 existing web services may be composed on the Internet so as to implement a new complex web service. In all these cases, the challenge is to automatically synthesize a fully controllable module from a set of partially controllable existing modules executing in a partially predictable environment.

Under this setting, the technical contributions of this paper are threefold. First, we formally define the problem within an abstract framework. Second, we devise a formal technique to perform automatic synthesis of the fully controllable module. We show that the technique proposed is sound, complete, and terminating. Lastly, we characterize the computational complexity of the problem and show that the proposed technique is optimal with respect to computational complexity.

2 The setting

Let us start by defining the synthesis problem [15] that is the subject of our research. To that end, we develop an abstract framework based on (sort of) finite state transition systems.

1 In particular, [3] can be seen as a simpler variant of the setting studied here, with no environment and deterministic behaviors.

Environment We assume to have a shared observable environment, which provides an abstract account of the observable effect and preconditions of actions. In giving such an account, we take into consideration that, in general, we have incomplete information about the actual effects and preconditions of actions. Thus, we allow the observable environment to be nondeterministic in general. In that way, the incomplete information on the actual world shows up as nondeterminism in our formalization.

Formally, an environment E = (A, E, e0, δE) is characterized by the following five entities:

• A is a finite set of shared actions;
• E is a finite set of possible environment states;
• e0 ∈ E is the initial state of the environment;
• δE ⊆ E ×A×E is the transition relation among states: δE (e, a, e′) holds when action a performed in state e may lead the environment to a successor state e′ .

Note that our notion of the environment shares a lot of similarities with the so-called "transition system" in action languages [5]. Indeed, one can think of using that kind of formalism to compactly represent the environment in our setting.

Behavior A behavior is essentially a program for an agent or the logic of some available device or component. Such a program however leaves the selection of the action to perform next to the agent itself. More precisely, at each step the program presents to the agent a choice of available actions; the agent selects one of them; the action is executed; and so on.

Obviously, behaviors are not intended to be executed on their own, but they are executed in the environment (cf. above). Hence, we equip them with the ability of testing conditions (i.e., guards) on the environment when needed.

Formally, a behavior B = (S, s0,G, δB, F) over an environment E, is a characterized by the following entities:

• S is a finite set of behavior states;
• s0 ∈ S is the single initial state of the behavior;
• G is a set of guards, which are boolean functions g : E → {true, false}, where E is the set of the environment states of E;
• δB ⊆ S ×G×A×S is the behavior transition relation, where A is the set of actions of E-we call the G×A components of such tuples, the label of the transition;
• finally, F ⊆ S is the set of final states of the behavior, that is, the states in which the behavior may stop executing, but does not necessarily have to.

Observe that, in general, behaviors are nondeterministic in the sense that they may allow more than one transition with the same action a and compatible guards evaluating to the same truth value. 2 As a result, the central system, when making its choice of which action to execute next, cannot be certain of which choices it will have later on, since that depends on what transition is actually executed. In other words, nondeterministic behaviors are only partially controllable.

2 Note that this kind of nondeterminism is of a devilish nature, so as to capture the idea that through the choice of actions alone one cannot fully control the behavior.

We say that a behavior B = (S, s0, G, δB, F), over the environment E, is deterministic if there is no environment state e of E for which there exist two distinct transitions (s, g1, a, s1) and (s, g2, a, s2) in δB such that g1(e) = g2(e). Notice that given a state in a deterministic behavior and a legal action in that state, we always know exactly which is the next state of the behavior. In other words, deterministic behaviors are fully controllable through the selection of the action to perform next, while this is not the case for nondeterministic ones.

Runs and traces Given a behavior B = (S, s0,G, δ, F) and an environment E = (A,E, e0, δE), we define the runs of B on E as, possibly infinite, alternating sequences of the following form: (s0 , e0)a1 (s1 , e1 )a2 · · · , where s0 = s0 and e0 = e0, and for every i we have that (si , ei )ai+1 (si+1 , ei+1 ) is such that:

• there exists a transition (ei , ai+1 , ei+1 ) ∈ δE; and
• there exists a transition (si , gi+1 , ai+1 , si+1 ) ∈ δB, such that gi+1 (ei) = true.

Moreover if the run is finite, that is, it is of the form (s0 , e0 )a1 · · · aℓ (sℓ , eℓ ), then sℓ ∈ F.

Apart from runs, we are also interested in traces generated by the behavior. A trace is a sequence of pairs (g, a), where g ∈ G is a guard of B and a ∈ A is an action, of the form t = (g1 , a1 ) · (g2 , a2 ) · · · such that there exists a run (s0 , e0 )a1 (s1 , e1 )a2 · · · , as above, where gi (ei-1) = true for all i. If the trace t = (g1 , a1 ) · · · (gℓ , aℓ) is finite, then there exists a finite run (s0 , e0 )a1 · · · aℓ (sℓ , eℓ) with sℓ ∈ F .

The traces of the deterministic behaviors are of particular interest: any initial fragment of a trace leads to a single state in the behavior. In a sense, the deterministic behavior itself can be seen as a specification of a set of traces.

The system A system S = (B1, . . . , Bn, E) is formed by an observable environment E and n predefined nondeterministic behaviors Bi, called the available behaviors. A system configuration is a tuple (s1, . . . , sn, e) denoting a snapshot of the system: behavior Bi is in state si and the environment E is in state e. We assume that the system has a specific component, called the scheduler, that is able to activate, stop, and resume the behaviors at each point in time.

The problem The problem we are interested in is the following: given a system S = (B1, . . . , Bn, E) and a deterministic behavior, called the target behavior B0 over E, synthesize a program for the scheduler such that the target behavior is realized by suitably scheduling the available behaviors.

In order to make this precise, we need to clarify which are the basic capabilities of the scheduler. The scheduler has the ability of activating-resuming one 3 of the many available behaviors by instructing it to execute an action among those that are possible in its current state (taking into account the environment). Also, the scheduler has the ability of keeping track (at runtime) of the current state of each available behavior.

3 For simplicity, we assume that the scheduler activates/resumes only one behavior at each step, though our approach can be extended to the case where more available services are activated at each step.

Technically, such a capability is called full observability on the states of the available behaviors. Although other choices are possible [1], full observability is the natural choice in this context, since the available behaviors are already suitable abstractions for the actual behaviors, and hence there is no reason to make its states partially unobservable: if details have to be hidden, this can be done directly within the abstract behavior exposed, possibly making use of nondeterminism.

We are now ready to formally define our synthesis problem. Let the system be S = (B1, . . . , Bn, E), where E = (A,E, e0, δE) is the environment and Bi = (Si, si0,Gi, δi, Fi) are the available behaviors. Let the target behavior be B0 = (S0, s00, δ0, F0).

A system history is an alternating sequence of system configurations and actions of the form h = (s01 , . . . , s0n, e0) · a1 · (s11 , . . . , s1n, e1 ) · · · (sℓ-1 1 , . . . , sℓ-1 n , eℓ ) · aℓ · (sℓ1 , . . . , sℓn, eℓ ) such that the following constraints hold:

• s0i = si0 for i ∈ {1, . . . , n}, that is, each behavior starts in its initial state;
• e0 = e0, that is, the environment starts in its initial state;
• at each step 0 ≤ k ≤ ℓ, there exists an i ∈ {1, . . . , n} such that (ski , gk+1 i , ak+1 , sk+1 i ) ∈ δi and for all j ̸= i, sk+1 j = skj , that is, at each step in the history, only one of the behaviors, namely Bi, has made a (legal) transition (according to its transition relation δi), while the other ones have remained still;
• at each step 0 ≤ k ≤ ℓ, we have that (ek , ak+1 , ek+1 ) ∈ δE, that is, the environment has also made a legal transition according to its transition relation.

A scheduler program is a function P : H × A → {1, . . . , n, u} that, given a history h ∈ H (where H is the set of all system histories as defined above) and an action a ∈ A to perform, returns the behavior (actually the behavior index) that is scheduled to perform the action. Observe that such a function may also return a special value u, for "undefined." This is a technical convenience to make P a total function returning values even for histories that are not of interest, or for actions that no behavior can perform after a given history.

Next, we define when a scheduler program is a composition that realizes the target behavior-a solution to the problem. First, we point out that, because the target behavior is a deterministic transition system, its behavior is completely characterized by the set of its traces, that is, by the set of infinite sequences of actions that are faithful to its transitions, and of finite sequences that in addition lead to a final state.

So, given a trace t = (g1 , a1 ) · (g2 , a2 ) · · · of the target behavior, we say that a scheduler program P realizes the trace t iff for all ℓ and for all system histories h ∈ Hℓ t,P (Hℓ t,P is defined below) such that gℓ+1(eℓh ) = true in the last environment state eℓh of h, we have that P(h, aℓ+1) ̸= u and Hℓ+1 t,P is nonempty, where the set of system histories Hℓ t,P is inductively defined as follows:

• H0 t,P = {(s10, . . . , sn0, e0)};
• Hℓ+1 t,P is the set of ℓ + 1-length system histories of the form h · aℓ+1 · (sℓ+1 1 , . . . , sℓ+1 n , eℓ+1 ) such that:
• h ∈ Hℓ t,P , where (sℓ1 , . . . , sℓn, eℓ ) is the last system configuration in h;
• aℓ+1 is an action such that P(h, aℓ+1)=i, with i̸= u, that is, the scheduler states that action aℓ+1 at system history h should be executed in behavior Bi;
• (sℓi , g, aℓ+1, s′i ) ∈ δi with g(eℓ) = true, that is, behavior Bi may evolve from its current state sℓi to state s′i w.r.t. the (current) environment state eℓ ;
• (eℓ , aℓ+1 , eℓ+1) ∈ δE, that is, the environment may evolve from its current state eℓ to state eℓ+1 ;
• sℓ+1 i = s′i and sℓ+1 j = sℓj , for j ̸= i, that is, only behavior Bi is allowed to perform a step.

Moreover, as before, if a trace is finite and ends after m actions, and all along all its guards are satisfied, we have that all histories in Hm t,P end with all behaviors in a final state. Finally, we say that a scheduler program P realizes the target behavior B0 if it realizes all its traces. 4

In order to understand the above definitions, let us observe that, intuitively, the scheduler program realizes a trace if, as long as the guards in the trace are satisfied, it can choose at every step an available behavior to perform the requested action. If at a certain point a guard in the trace is not satisfied in the current environment state, then we may consider the trace finished (even if it is not in a final state). As before, however, because the available behaviors nondeterministically choose what transition to actually performwhen executing an action, the scheduler program must be such that the scheduler will always be able to continue with the execution of the next action no matter how both the activated behavior and the environment evolve after each step. Finally, the last requirement makes sure that all available behaviors are left in a final state when a finite trace reaches its end with all guards satisfied.

Observe that, in general, a scheduler program could require infinite states. However, we will show later that if a scheduler that realizes the target behavior does exist, then there exists one with a finite number states. Note also that the scheduler has to observe the states of the available behaviors in order to decide which behavior to select next (for a given action requested by the target behavior). This makes these scheduler programs akin to an advanced form of conditional plans [16].

3 An example

We now come back to our original blocks world example in order to illustrate the abstract framework developed in the previous section. The complete scenario is depicted in Figure 1. The aim of the whole system is to paint existing blocks. Blocks can be processed by cleaning and painting them. Before processing a block, though, it is necessary to prepare it, for example, by moving it to a special processing location. Furthermore, only after a block has been disposed, can another block be prepared for processing. Finally, cleaning and painting may, sometimes, require resources, namely, water and paint, respectively: we assume there are two tanks, for water and paint, respectively, and that both are recharged simultaneously by pressing a recharging button.

4 Recall that because the target behavior is deterministic, it can be seen as a specification of a, possibly infinite, set of traces.

Now, the desired target behavior T that we want to achieve is as follows. First, a block is prepared for processing. Then, the block in question can either be painted right away or painted after being cleaned-some (dirty) blocks may need to be washed before being painted. Note that the decision of whether a block needs to be cleaned lays outside of our framework. After a block has been painted, it is disposed. Finally, the recharging button is pushed. See that this target behavior is "conservative," in that it always recharges the tanks after a block has been processed.

One can think of the above target behavior as the arm that one would like to have. However, such arm does not exist in reality. Instead, there are only two different arms available. The first arm A, a cleaning-disposing arm, is able to clean and dispose blocks. The second arm B is capable of preparing, cleaning, and painting blocks. Both arms are able to press the recharge button to refill the tanks.

So, the system is composed of the environment E and the two arms A and B shown in Figure 1. Let us now note a few interesting points. First, the environment E provides the (general) preconditions of actions in the domain (e.g., dispose can only be executed after a prepare action). The environment also includes some information about the water tank: in e1 and e2, the water tank is not empty; and in e3 and e4, the water tank is indeed empty. Notice that it is still conceivable to clean a block in state e3, by some method that does not rely on water. However, because arm A does use water to clean blocks, it can only do it when the environment is in fact in state e2. Second, we observe that whereas only the second arm can prepare a block, only the first arm can dispose a block. Lastly, the most interesting remark comes from arm B's internal logic, for which the system only has partial information. After painting a block, arm B may evolve nondeterministically to two different states: b1 or b3. Intuitively, the arm evolves to state b3 as soon as the paint tank becomes empty; otherwise the arm evolves to state b1. Once the arm runs out of paint, it can only clean blocks until the tanks are eventually recharged. Notice also that, unlike arm A, arm B does not require the environment to be in state e2 to clean a block, as its cleaning mechanism does not rely on water.

We aim to automatically synthesize a scheduler program so as to realize the target behavior (T) by making use of the available behaviors (arms A and B) and considering the environment (E). See the next section.

4 The synthesis technique

We are now ready to investigate how to check for the existence of a scheduler program that realizes the target behavior, and even more, how to actually compute it. We start with some preliminary considerations on the computational complexity that we should expect. The result by Muscholl and Walukiewicz in [14], which can be easily rephrased in our framework, gives us an EXPTIME lowerbound.

More precisely, let us call empty environment any environment of the form E = (A,E, eo, δE), where E = {eo} (i.e., the (observable) environment has a single state), and δE = {(e0, a, e0) | a ∈ A}, (i.e., there are no preconditions on actions, nor actions have any effect on the environment). Also, let us call deterministic guardless behavior any behavior of the form B = (S, s0, {gtrue}, δB, F), where gtrue is the constant function returning always true, and δB is functional, i.e., for each state s ∈ S and action a ∈ A, there is at most one state s′ such that (s, a, s′ ) ∈ δB. Then, Muscholl and Walukiewicz's result can be stated as follows.

Theorem 4.1 (Muscholl &Walukiewicz 2005) Checking the existence of a scheduler program that realizes a target deterministic guardless behavior in a system consisting of an empty environment and a set of available deterministic guardless behaviors is EXPTIME-hard. 5

Hence, checking the existence of a scheduler program in our general framework is at least exponential time. Next, we show that the problem is actually EXPTIME-complete, by resorting to a reduction to satisfiability in Propositional Dynamic Logic (PDL). Moreover, such a reduction can be exploited to generate the actual scheduler program which will be finite. In doing this, we extend the approach in [3], originally developed in the context of service composition to deal with empty environments and deterministic guardless behaviors. Dealing with a non-trivial environment, and especially dealing with the nondeterminism of the available behaviors, requires solving same subtle points that reflects the sophisticated notion of scheduler program that is needed for that.

4.1 Propositional Dynamic Logic

Propositional Dynamic Logic (PDL) is a modal logic specifically developed for reasoning about computer programs [7]. Syntactically, PDL formulas are built from a set P of atomic propositions and a set Σ of atomic actions:

where P is an atomic proposition in P, r is a regular expression over the set of actions in Σ, and a is an atomic action in Σ. That is, PDL formulas are composed from atomic propositions by applying arbitrary propositional connectives, and modal operators 〈r〉φ and [r]φ. Formula 〈r〉φ means that there exists an execution of r (i.e., a sequence of actions conforming to the regular expression r) reaching a state where φ

5 In fact, Muscholl and Walukiewicz show EXPTIME-hardness in the setting of service composition studied in [2; 3], where all available services are deterministic [14].

holds; and formula [r]φ is intended to mean that all terminating executions of r reach a state where φ holds.

A PDL formula φ is satisfiable if there exists a model for φ-an interpretation where φ is true. Checking satisfiability of a PDL formula is EXPTIME-complete [7].

PDL enjoys two properties that are of particular interest for us [7]. The first is the tree model property, which says that every model of a formula can be unwound to a, possibly infinite, tree-shaped model (considering domain elements as nodes and partial functions interpreting actions as edges). The second is the small model property, which says that every satisfiable formula admits a finite model whose size (in particular the number of domain elements) is at most exponential in the size of the formula itself.

4.2 Reduction to PDL

Let S=(B1, . . . , Bn, E) be a system, where E =(A, E, e0, δE ) is the environment and Bi = (Si, si0, Gi, δi, Fi) are the available behaviors over E, and let B0 = (S0, s00, δ0, F0) be the target behavior (over E as well). Then, we build a PDL formula Φ to check for satisfiability as follows.

As actions in Φ, we have the actions A in E. As atomic propositions, we have: 6

• one atomic proposition e for each state e of E, which intuitively denotes that E is in state e;
• one atomic proposition s for each state s of Bi, for i ∈ {0, 1, . . . , n}, denoting that Bi is in state s;
• atomic propositions Fi, for i ∈ {0, 1, . . .n}, denoting that Bi is in a final state;
• atomic propositions execia, for i ∈ {1, . . .n} and a ∈ A, denoting that a will be executed next by behavior Bi;
• one atomic proposition undef denoting that we reached a situation where the scheduler can be left undefined.

Let us now build the formula Φ. For representing the transitions of the target behavior B0, we construct a formula φ0 as the conjunction of (for each s of B0 and e of E):

• s∧e → 〈a〉true∧[a]s′ , for each transition (s, g, a, s′) ∈ δ0 such that g(e) = true, encoding that the target behavior can do an a-transition, whose guard g is satisfied, by going from state s to state s′ ;
• s ∧ e → [a]undef , for each a such that for no g and s′ we have (s, g, a, s′ ) ∈ δ0 with g(e) = true. This takes into account that the target behavior cannot perform an a-transition.

For representing the transitions of each available behavior Bi, we construct a formula φi as the conjunction of:

· the formula

where Δ = {(s′ , e′ ) | (s, g, a, s′ ) ∈ δi, g(e) = true, (e, a, e′ ) ∈ δE}, for each environment state e, each s of Bi, and each a ∈ A. These assertions encode that if the current environment state is e and the available behavior Bi is in state s and is selected for the execution of an action a (i.e., execia is true), then for each possible a-transition of Bi with its guard true in e and of E, we have a possible a-successor in the models of Φ;

6 In this paper, we are not concerned with compact representations of the states of the environment E and the behaviors Bi. However, we observe that if states are succinctly represented (e.g., in binary format) then, in general, we can exploit such a representation in Φ to get a corresponding compact formula as well.

• s ∧ e ∧ execia → [a]false, for each environment state e of E, and each state s of Bi such that for no g, s′ , and e′ , we have that (s, g, a, s′ ) ∈ δi with g(e) = true and (e, a, e′ )∈ δE . This states that if the current environment state is e and Bi, whose current state is s, is selected for the execution of a, but a cannot be executed by Bi in e, then there is no a-successor in the models of Φ;
• s ∧ ¬execia → [a]s, for each state s of Bi and each action a. This assertion encodes that if behavior Bi is in state s and is not selected for the execution of a, then if a is performed (by some other available behavior), Bi does not change state.

In addition, we have the formula φadd, of general constraints, obtained as the conjunction of:

• s → ¬s′ , for all pairs of states s, s′ of Bi, and for i ∈ {0, 1, , . . . , n}, stating that propositions representing different states of Bi are disjoint;
• Fi ↔ ∨s∈Fi s, for i ∈ {0, 1, , . . . , n}, highlighting the final states of Bi;
• undef → [a]undef , for each action a ∈ Σ, stating that once a situation is reached where undef holds, then undef holds also in all successor situations;
• ¬undef ∧ 〈a〉true → ∨i∈{1,...,n} execia, for each a ∈ A, denoting that, unless undef is true, if a is performed, then at least one of the available behaviors must be selected for the execution of a;
• execia → ¬execja for each i, j ∈ {1, . . . , n}, i ̸= j, and each a ∈ A, stating that only one available behavior is selected for the execution of a;
• F0 → ∧i∈{1,...,n} Fi, stating that when the target behavior is in a final state, so are all the available behaviors.

Finally, we define Φ as

where Init stands for e0∧s00∧s01∧· · ·∧s0n, and represents the initial state of the environment E and of all behaviors Bi (including the target), and u = (⋃a∈Σ a)∗ , which acts as the master modality [7], is used to force φ0∧∧i∈{1,...,n} φi∧φadd to be true in every point of the model. Note that u is the only complex program that appears in the PDL formula Φ. We can now state our main result.

Theorem 4.2 The PDL formula Φ, constructed as above, is satisfiable iff there exists a scheduler program for the system S = (B1, . . . , Bn, E) that realizes the target behavior B0.

Proof (sketch). "If ": PDL has the tree-model property. Hence, if Φ is satisfiable then it has a model that is tree shaped. Each node in this tree can be put in correspondence with a history, and from the truth value assignment of the propositions execia in the node one can reconstruct the scheduler program. "Only if ": if a scheduler program that realizes B0 exists, one can use it to build a tree model of Φ.

Observe that the size of Φ is polynomially with respect to E, B1, . . . , Bn and B0. Hence, from the EXPTIMEcompleteness of satisfiability in PDL and Theorem 4.1, we get the following result:

Theorem 4.3 Checking the existence of a scheduler program that realizes a target behavior B0 relative to a system S = (B1, . . . , Bn, E) is EXPTIME-complete.

Finally, by the finite-model property of PDL (i.e., if a formula is satisfiable, it is satisfiable in a model that is at most exponential in the size of the formula), we get a systematic procedure for synthesizing the composition:

Theorem 4.4 If there exists a scheduler program that realizes a target behavior B0 relative to a system (B1, . . . , Bn, E), then there exists one that requires a finite number of states. Moreover such a finite state program can be extracted from a finite model of Φ.

To end, let us return to our example of Section 3. The corresponding PDDL formula Φblocks , obtained as explained above, has a a finite model from which we can extract the scheduler program depicted in Figure 2 (after having projected out irrelevant propositions and applied minimization techniques to reduce the number of states). Such scheduler realizes the target behavior T by appealing to the two available arms A and B. As one can observe, even in this simplistic scenario, the existence of a scheduler and its corresponding program is far from trivial. For instance, it is critical to make the correct decision on which machine must recharge the tanks at every step-such a choice would depend on how arm B evolves after painting a block. Also, the scheduler must be able to terminate both arms in their corresponding final states whenever the target behavior is its final state t1.

5 Conclusion

In this paper, we have looked at automatic synthesis of a fully controllable module from a set of partially controllable existing modules that execute in a partially predictable environment. The kind of problem that we dealt with is clearly a form of reactive process synthesis [15; 10]. Standard techniques for such problems are based on automata on infinite trees, which however relay on critical steps, such as Safra's construction for complementation, that have resisted efficient implementation for a long time [11]. Instead, we based our synthesis on a reduction to satisfiability in PDL [7] with a limited use of the reflexive-transitive-closure operator. Such kind of PDL satisfiability shares the same algorithms that are behind the success of the description logic-based reasoning systems used for OWL, 7 such as FaCT, Racer, and Pellet. 8 Hence, its applicability in our context appears to be quite promising from a practical point of view.

Acknowledgments The authors would like to thankDaniela Berardi, Diego Calvanese, Rick Hull, Massimo Mecella, and Maurizio Lenzerini for discussion and insights on the issues treated in this paper. The first author was partially supported by the the European FET basic research project FP6-7603 Thinking Ontologies (TONES). The second author was supported by the Australian Research Council and Agent Oriented Software (grant LP0560702).