SMT-based Abstract Planning in PlanICS Ontology

• Autorzy: Niewiadomski A. , Penczek W. , Półrola A.

Warianty tytułu

PL

Planowanie abstrakcyjne z wykorzystaniem SMT w ontologii PlanICS

• Języki publikacji: EN

Abstrakty

EN

The paper deals with the abstract planning problem - the first stage of Web Service Composition (WSC) in the Planics framework. We present a solution based on a compact repre-sentation of abstract plans by multisets of service types and a reduction of the planning problem to a task for an SMT-solver. The paper presents theoretical aspects of the abstract planning as well as some details of our symbolic encoding and implementation, followed by preliminary experimental results.

PL

Przedmiotem niniejszej pracy jest problem planowania abstrakcyjnego - pierwszy etap kompozycji usług sieciowych w systemie Planics. Prezentujemy rozwiązanie bazujące na kompaktowej reprezentacji planów abstrakcyjnych za pomocą wielozbiorów typów usług i redukcji problemu planowania do problemu spełnialności instancji SMT (Satisfiability Modulo Theories). Przedstawiamy zarówno teoretyczne aspekty planowania, jak również szczegóły symbolicznego kodowania i implementacji oraz wstępne wyniki eksperymentalne.

Słowa kluczowe

EN

SMT; Web service composition; abstract plan

PL

SMT; kompozycja usług sieciowych; planowanie abstrakcyjne

• Wydawca: Instytut Podstaw Informatyki PAN
• Czasopismo: Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk
• Rocznik: 2012
• Tom: Nr 1027
• Strony: 1--42
• Opis fizyczny: Bibliogr. 20 poz., rys.

Twórcy

autor

Niewiadomski A.

• Instytut Informatyki UPH, ul. 3-Maja 54, 08-110 Siedlce, Polska

autor

Penczek W.

• Instytut Podstaw Informatyki PAN, ul. Jana Kazimierza 5, 01-248 Warszawa, Polska

autor

Półrola A.

• Wydział Matematyki i Informatyki UŁ, ul. Banacha 22, 90-238 Łódź, Polska

Bibliografia

• [1] S. Ambroszkiewicz. Entish: A language for describing data process-ing in open distributed systems. Fundam. Inform., 60(l-4):41-66, 2004.
• [2] C. Barrett, A. Stump, and C. Tinelli. The SMT-LIB standard - version 2.0. In Proc. of the 8th Int. Workshop on Satisfiability Modulo Theories (SMT'10), 2010.
• [3] M. Bell. Introduction to Service-Oriented Modeling. John Wiley & Sons, 2008.
• [4] L. Bentakouk, P. Poizat, and F. Zaidi. Checking the behavioral conformance of web sendces with symbolic testing and an SMT solver. In Tests and Proofs, volume 6706 of LNCS, pages 33-50. Springer, 2011. ISBN 978-3-642-21767-8.
• [5] M. M. Bersani, L. Cavallaro, A. Frigeri, M. Pradella, and M. Rossi. SMT-based verification of LTL specification with integer constraints and its application to runtime checking of service substitutability. In SEFM, pages 244-254, 2010.
• [6] D.R.Cook.The SMT-LIBv2 Language and Tools: A Tutorial. http://www.grammatech.com/resource/smt/jSMTLIBTutorial.pdf, 2012.
• [7] L. M. de Moura and N. Bjorner. Z3: An efficient SMT solver. In Proc. of TACAS'08, volume 4963 of LNCS, pages 337-340. Springer-Verlag, 2008.
• [8] D. Doliwa, W. Horzelski, M. Jarocki, A. Niewiadomski, W. Penczek, A. Półrola, M. Szreter, and A. Zbrzezny. PlanICS - a web service Compositon toolset. Fundam. Inform., 112(1):47-71, 2011.
• [9] D. Doliwa, W. Horzelski, M. Jarocki, A. Niewiadomski, W. Penczek, A. Półrola, and J. Skaruz. HarmonICS - a tool for composing med-ical sendces. In ZEUS, pages 25-33, 2012.
• [10] M. Elwakil, Z. Yang, L. Wang, and Q. Chen. Message race detection for web services by an SMT-based analysis. In Proc. of the 7th Int. Conference on Autonomic and Trusted Computing, ATC'10, pages 182-194. Springer, 2010. ISBN 3-642-16575-3, 978-3-642-16575-7.
• [11] V. Gehlot and K. Edupuganti. Use of colored petri nets to model, analyze, and evaluate service composition and orchestration. In System Sciences, 2009. HICSS '09. 42nd Hawaii International Conference on, pages 1 -8, 2009.
• [12] Z. Li, L. O'Brien, J. Keung, and X. Xu. Effort-oriented classification matrix of web service composition. In Proc. of the Fifth International Conference on Internet and Web Applications and Services, pages 357-362, 2010. ISBN 978-0-7695-4022-1.
• [13] S. Mitra, R. Kumar, and S. Basu. Automated choreographer synthesis for web services composition using I/O automata. In ICWS, pages 364-371, 2007.
• [14] G. Monakova, O. Kopp, F. Leymann, S. Moser, and K. Schafers. Verifying business rules using an SMT solver for BPEL processes. In BPSC, pages 81-94, 2009.
• [15] W. Nam, H. Kil, and D. Lee. Type-aware web service composition using boolean satisfiability solver. In Proc. of the 2008 10th IEEE Conference on E-Commerce Technology and the Fifth IEEE Conference on Enterprise Computing, E-Commerce and E-Services, pages 331-334, 2008. ISBN 978-0-7695-3340-7.
• [16] OWL. OWL 2 web ontology language document overview. http:// www.w3.org/TR/owl2-overwiew/, 2009.
• [17] S. Ranise and C. Tinelli. The SMT-LIB format: An initial proposal. In In Proc. of the lst Workshop on Pragmatics of Decision Procedures in Automated Reasoning (Miami Beach, USA), 2003.
• [18] J. Rao and X. Su. A survey of automated web service composition methods. In Proc. of the Int. Workshop on Semantic Web Ser-vices and Web Process Composition (SWSWPCOA), volume 3387 of LNCS, pages 43-54. Springer-Verlag, 2004.
• [19] J. Rao, P. Kiingas, and M. Matskin. Composition of semantic web services using linear logic theorem proving. Inf. Syst., 31(4):340-360, 2006. ISSN 0306-4379.
• [20] P. Traverso and M. Pistore. Automated composition of semantic web services into executable processes. In The Semantic Web -ISWC 2004, volume 3298 of LNCS, pages 380-394. Springer, 2004. ISBN 978-3-540-23798-3