Author name cluster

Marco Pistore

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

16 papers

2 author rows

AIJ Journal 2010 Journal Article

Automated composition of Web services via planning in asynchronous domains

Piergiorgio Bertoli
Marco Pistore
Paolo Traverso

The service-oriented paradigm promises a novel degree of interoperability between business processes, and is leading to a major shift in way distributed applications are designed and realized. While novel and more powerful services can be obtained, in such setting, by suitably orchestrating existing ones, manually developing such orchestrations is highly demanding, time-consuming and error-prone. Providing automated service composition tools is therefore essential to reduce the time to market of services, and ultimately to successfully enact the service-oriented approach. In this paper, we show that such tools can be realized based on the adoption and extension of powerful AI planning techniques, taking the “planning via model-checking” approach as a stepping stone. In this respect, this paper summarizes and substantially extends a research line that started early in this decade and has continued till now. Specifically, this work provides three key contributions. First, we describe a novel planning framework for the automated composition of Web services, which can handle services specified and implemented using industrial standard languages for business processes modeling and execution, like ws-bpel. Since these languages describe stateful Web services that rely on asynchronous communication primitives, a distinctive aspect of the presented framework is its ability to model and solve planning problems for asynchronous domains. Second, we formally spell out the theory underlying the framework, and provide algorithms to solve service composition in such framework, proving their correctness and completeness. The presented algorithms significantly extend state-of-the-art techniques for planning under uncertainty, by allowing the combination of asynchronous domains according to behavioral requirements. Third, we provide and discuss an implementation of the approach, and report extensive experimental results which demonstrate its ability to scale up to significant cases for which the manual development of ws-bpel composed services is far from trivial and time consuming.

Details DOI

ICAPS Conference 2009 Conference Paper

Continuous Orchestration of Web Services via Planning

Piergiorgio Bertoli
Raman Kazhamiakin
Massimo Paolucci 0001
Marco Pistore
Heorhi Raik
Matthias Wagner 0001

The service-oriented paradigm is rapidly emerging as the key approach to develop distributed business applications. Its enactment requires the ability to automatically coordinate existing services to realize novel and powerful desired functionalities, and planning-based solutions have proved to be strong candidates for this hard task. However, no current approach can satisfactorily coordinate stateful services that evolve continuously and indefinitely in an asynchronous way, such as e. g. notification services made increasingly available by business entities. This severely limits the practical applicability of current solutions. In this paper, we provide for the first time a full-fledged planning-based solution to the problem of continuously orchestrating stateful asynchronous services. To do so, we adopt a simple yet expressive requirement language, and we devise a novel planning algorithm that solves preference-ordered maintenability goals in the presence of exogenous events. Our approach is correct and complete, and our tests on a symbolic BDD-based implementation witness its ability and effectiveness in dealing with significant and realistic scenarios which no other current approach can tackle.

Details

AIJ Journal 2009 Journal Article

Task decomposition on abstract states, for planning under nondeterminism

Ugur Kuter
Dana Nau
Marco Pistore
Paolo Traverso

Although several approaches have been developed for planning in nondeterministic domains, solving large planning problems is still quite difficult. In this work, we present a new planning algorithm, called Yoyo, for solving planning problems in fully observable nondeterministic domains. Yoyo combines an HTN-based mechanism for constraining its search and a Binary Decision Diagram (BDD) representation for reasoning about sets of states and state transitions. We provide correctness theorems for Yoyo, and an experimental comparison of it with MBP and ND-SHOP2, the two previously-best algorithms for planning in nondeterministic domains. In our experiments, Yoyo could easily deal with problem sizes that neither MBP nor ND-SHOP2 could scale up to, and could solve problems about 100 to 1000 times faster than MBP and ND-SHOP2.

Details DOI

ICAPS Conference 2006 Conference Paper

Automated Web Service Composition by On-the-Fly Belief Space Search

Piergiorgio Bertoli
Marco Pistore
Paolo Traverso

Composition of stateful web services expressed in BPEL4WS can be recasted as a problem of planning in asynchronous domains. In (PTB05), this is pursued by encoding the asynchronous and partially observable behaviors of services within a domain whose states represent 'beliefs' on the state of each service. In this work, we propose a novel approach, where such belief-level domain is not built explicitly, but rather visited on-the-fly. We evaluate the relative merits of the approaches, showing the advantages of the on-the-fly approach for a significant class of composition problems.

Details

ICAPS Conference 2006 Conference Paper

Run-Time Monitoring of the Execution of Plans for Web Service Composition

Fabio Barbon
Paolo Traverso
Marco Pistore
Michele Trainotti

While a lot of work has been done on the problem of the automated generation of plans that compose web services, the problem of monitoring their execution has still to be investigated. However, the run-time monitoring of web service executions is a compelling requirement, since it makes it possible to detect misbehaviors of external component services that are provided by third parties, and thus not fully under control. In this paper we propose a technique for the automatic generation of monitors as Java programs that check at run-time the execution of plans composing web services and detect violations to interaction protocols and service level agreements. The former correspond to unexpected changes in the planning domain, while the latter represent violations of assumptions that have been used to generate the composition plan.

Details

ECAI Conference 2006 Conference Paper

Stong Cyclic Planning Under Partial Observability

Piergiorgio Bertoli
Alessandro Cimatti
Marco Pistore

Strong Cycling Planning aims at generating iterative plans that implement trial-and-error strategies, where loops are allowed only so far as there is a chance to reach the goal. In this paper, we tackle the problem of Strong Cyclic Planning under Partial Observability, making three main contributions. First, we provide a formal definition of the problem. We point out that several degrees of solution are possible and equally interesting, depending on the admissible delay between achieving the goal and detecting that it has been achieved. Second, we present a family of planning algorithms that tackle the different versions of the problem. Third, we implement the algorithms using efficient symbolic representation techniques, and experimentally compare their performances.

Details

ICAPS Conference 2006 Conference Paper

Towards Strong Cyclic Planning under Partial Observability

Piergiorgio Bertoli
Alessandro Cimatti
Marco Pistore

Strong Cyclic Planning aims at generating iterative plans that only allow loops so far as there is a chance to reach the goal. The problem is already significantly complex for fully observable domains; when considering partially observable domains, even providing a formal definition is far from straightforward. In this work, we provide a formal definition of Strong Cyclic Planning under Partial Observability, which makes clear how several degrees of solution are possible and equally interesting, depending on the admissible delay between achieving the goal and detecting that it has been achieved.

Details

ICAPS Conference 2005 Conference Paper

A Hierarchical Task-Network Planner based on Symbolic Model Checking

Ugur Kuter
Dana S. Nau
Marco Pistore
Paolo Traverso

Although several approaches have been developed for planning in nondeterministic domains, solving large planning problems is still quite difficult. In this work, we present a novel algorithm, called YoYo, for planning in nondeterministic domains under the assumption of full observability. This algorithm enables us to combine the power of search-control strategies as in Planning with Hierarchical Task Networks (HTNs) with techniques from the Planning via Symbolic Model-Checking (SMC). Our experimental evaluation confirms the potentialities of our approach, demonstrating that it combines the advantages of these paradigms.

Details

ICAPS Conference 2005 Conference Paper

Automated Composition of Web Services by Planning in Asynchronous Domains

Marco Pistore
Paolo Traverso
Piergiorgio Bertoli

Although several approaches have been developed for planning in nondeterministic domains, solving large planning problems is still quite difficult. In this work, we present a novel algorithm, called YoYo, for planning in nondeterministic domains under the assumption of full observability. This algorithm enables us to combine the power of search-control strategies as in Planning with Hierarchical Task Networks (HTNs) with techniques from the Planning via Symbolic Model-Checking (SMC). Our experimental evaluation confirms the potentialities of our approach, demonstrating that it combines the advantages of these paradigms.

Details

TCS Journal 2005 Journal Article

Structured coalgebras and minimal HD-automata for the π -calculus

Ugo Montanari
Marco Pistore

The coalgebraic framework developed for the classical process algebras, and in particular its advantages concerning minimal realizations, does not fully apply to the π -calculus, due to the constraints on the freshly generated names that appear in the bisimulation. In this paper we propose to model the transition system of the π -calculus as a coalgebra on a category of name permutation algebras and to define its abstract semantics as the final coalgebra of such a category. We show that permutations are sufficient to represent in an explicit way fresh name generation, thus allowing for the definition of minimal realizations. We also link the coalgebraic semantics with a slightly improved version of history dependent (HD) automata, a model developed for verification purposes, where states have local names and transitions are decorated with names and name relations. HD-automata associated with agents with a bounded number of threads in their derivatives are finite and can be actually minimized. We show that the bisimulation relation in the coalgebraic context corresponds to the minimal HD-automaton.

Details DOI

ICAPS Conference 2004 Conference Paper

Planning with Extended Goals and Partial Observability

Piergiorgio Bertoli
Marco Pistore

Planning in nondeterministic domains with temporally extended goals under partial observability is one of the most challenging problems in planning. Simpler subsets of this problem have been already addressed in the literature, but the general combination of extended goals and partial observability is, to the best of our knowledge, still an open problem. In this paper we present a first attempt to solve the problem, namely, we define an algorithm that builds plans in the general setting of planning with extended goals and partial observability. The algorithm builds on the top of the techniques developed in the planning with model checking framework for the restricted problems of extended goals and of partial observability.

Details

ICAPS Conference 2003 Conference Paper

A Framework for Planning with Extended Goals under Partial Observability

Piergiorgio Bertoli
Alessandro Cimatti
Marco Pistore
Paolo Traverso

Planning in nondeterministic domains with temporally extended goals under partial observability is one of the most challenging problems in planning. Subsets of this problem have been already addressed in the literature. For instance, planning for extended goals has been developed under the simplifying hypothesis of full observability. And the problem of a partial observability has been tackled in the case of simple reachability goals. The general combination of extended goals and partial observability is, to the best of our knowledge, still an open problem, whose solution turns out to be by no means trivial. In this paper we do not solve the problem in its generality, but we perform a significant step in this direction by providing a solid basis for tackling it. Our first contribution is the definition of a general framework that encompasses both partial observability and temporally extended goals, and that allows for describing complex, realistic domains and significant goals over them. A second contribution is the definition of the K-CTL goal language, that extends CTL (a classical language for expressing temporal requirements) with a knowledge operator that allows to reason about the information that can be acquired at run-time. This is necessary to deal with partially observable domains, where only limited run-time "knowledge" about the domain state is available. A general mechanism for plan validation with K-CTL goals is also defined. This mechanism is based on a monitor, that plays the role of evaluating the truth of knowledge predicates.

Details

I&C Journal 2001 Journal Article

A Partition Refinement Algorithm for the π-Calculus

Marco Pistore
Davide Sangiorgi

The partition refinement algorithm is the basis for most of the tools for checking bisimulation equivalences and for computing minimal realisations of CCS-like finite state processes. In this paper, we present a partition refinement algorithm for the π-calculus, a development of CCS where channel names can be communicated. It can be used to check bisimilarity and to compute minimal realisations of finite control processes—the π-calculus counterpart of CCS finite state processes. The algorithm is developed for strong open bisimulation and can be adapted to late and early bisimulations, as well as to weak bisimulations. To arrive at the algorithm, a few laws, proof techniques, and four characterizations of open bisimulation are proved.

Details DOI

TCS Journal 2001 Journal Article

On the semantics of durational actions

Flavio Corradini
GianLuigi Ferrari
Marco Pistore

This paper develops a mathematical framework to describe and reason about semantic theories of processes where actions have a non-zero duration. The framework relies on the notions of reduction and observability and allows one to naturally explain the possible choices to incorporate timing information in terms of process interaction mechanisms. The framework provides a parameterized context where well-known and new theories can be formally compared and classified by a suitable instantiation of the parameters. A proof-technique to derive from the reduction semantics an equivalent SOS-based characterization is also provided.

Details DOI

MFCS Conference 2000 Conference Paper

pi-Calculus, Structured Coalgebras, and Minimal HD-Automata

Ugo Montanari
Marco Pistore

Abstract The coalgebraic framework developed for the classical process algebras, and in particular its advantages concerning minimal realizations, does not fully apply to the π-calculus, due to the constraints on the freshly generated names that appear in the bisimulation. In this paper we propose to model the transition system of the π-calculus as a coalgebra on a category of name permutation algebras and to define its abstract semantics as the final coalgebra of such a category. We show that permutations are sufficient to represent in an explicit way fresh name generation, thus allowing for the definition of minimal realizations. We also link the coalgebraic semantics with a slightly improved version of history dependent (HD) automata, a model developed for verification purposes, where states have local names and transitions are decorated with names and name relations. HD-automata associated with agents with a bounded number of threads in their derivatives are finite and can be actually minimized. We show that the bisimulation relation in the coalgebraic context corresponds to the minimal HD-automaton.

Details

MFCS Conference 1996 Conference Paper

Specification and Verification of Timed Lazy Systems

Flavio Corradini
Marco Pistore

Abstract In this paper CCS is equipped with a simple operational semantics that allows us to describe and reason about the performance of systems which proceed by reacting to external stimuli. Based on the new operational semantics, lazy performance equivalence is introduced as a natural extension of the standard interleaving bisimulation. It turns out to be preserved by all CCS contexts. The problem of automatically checking lazy performance equivalence is also tackled. Because of the lazy character of our calculus, an infinite transition graph is associated with every non-trivial CCS term. Nevertheless, lazy performance equivalence can be provided with an alternative finite characterization and existing algorithms for checking bisimulation based semantics can be applied to the latter.

Details