Several real world applications require planners that deal with non-deterministic domains and with temporally extended goals. Recent research is addressing this planning problem. However, the ability of dealing in practice with large state spaces is still an open problem. In this paper we describe a planning algorithm for extended goals that makes use of BDD-based symbolic model checking techniques. We implement the algorithm in the MBP planner, evaluate its applicability experimentally, and compare it with existing tools and algorithms. The results show that, in spite of the difficulty of the problem, MBP deals in practice with domains of large size and with goals of a certain complexity.

In this paper we realize the synthesis of continuous coordinations By envisaging standards to publish and access services over based on the conceptual framework of (Pistore, the Web, the Service-Oriented Computing (SOC) paradigm Traverso, and Bertoli 2005), which recasts the composition promises a novel degree of interoperability between distributed problem in terms of planning; namely, we act at its core applications that realize business processes. One by adopting a very simple, yet expressive requirements language, cornerstone of SOC stands in the provision of novel and and devising a novel planning algorithm. In particular, more complex business logics by the coordination of existing the requirement language expresses coordination constraints services. Due to the complexity of manually realizing that are transformed into preference-ordered maintenability such coordinations, automatedly supporting the synthesis goals, and the algorithm deals with such goals in of service orchestrations is crucial to the actual enactment the presence of exogenous events (which encode independent of SOC. This problem is extremely hard since, asynchronous evolutions of services).