Skip to main content
SpringerLink
Log in

SMT-Based Abstract Parametric Temporal Planning

  • Chapter
  • First Online:
Book cover Transactions on Petri Nets and Other Models of Concurrency X

Part of the book series: Lecture Notes in Computer Science ((TOPNOC,volume 9410))

Abstract

Planics is a tool for solving the web service composition problem. It uses a uniform semantic description of the services and the service types as a part of the ontology which contains also the objects processed by the services. The user query is expressed in a fully declarative language defined over terms from the ontology by describing two object sets, called the initial and the expected world. The task of Planics consists in finding a sequence of services transforming the initial world into a superset of the expected one using service types available in the ontology and matching them later with real-world services. An abstract planning is the first phase of the task in which Planics composes service types. The paper extends this phase with a theory and a module for parametric temporal planning, by extending the user query with object variables and a PLTLX formula specifying temporal aspects of world transformations in a plan. Our solution comes together with an example, an implementation, and experimental results.

This work has been partially supported by the National Science Centre under the grant No. 2011/01/B/ST6/01477.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. Ambroszkiewicz, S.: Entish: A language for describing data processing in open distributed systems. Fundam. Inform. 60(1–4), 41–66 (2004)

    MATH  Google Scholar 

  2. Bell, M.: Introduction to Service-Oriented Modeling. Wiley, Hoboken (2008)

    Google Scholar 

  3. Bentahar, J., Yahyaoui, H., Kova, M., Maamar, Z.: Symbolic model checking composite web services using operational and control behaviors. Expert Syst. Appl. 40(2), 508–522 (2013)

    Article  Google Scholar 

  4. Bentakouk, L., Poizat, P., Zaïdi, F.: Checking the behavioral conformance of web services with symbolic testing and an SMT solver. In: Wolff, B., Gogolla, M. (eds.) TAP 2011. LNCS, vol. 6706, pp. 33–50. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  5. Bersani, M.M., Cavallaro, L., Frigeri, A., Pradella, M., Rossi, M.: SMT-based verification of LTL specification with integer constraints and its application to runtime checking of service substitutability. In: SEFM, pp. 244–254 (2010)

    Google Scholar 

  6. Chifu, V., Salomie, I., St. Chifu, E.: Fluent calculus-based web service composition - from OWL-S to fluent calculus. In: Proceedings of the 4th International Conference on Intelligent Computer Communication and Processing, pp. 161–168 (2008)

    Google Scholar 

  7. de Moura, L., Bjørner, N.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  8. Doliwa, D., Horzelski, W., Jarocki, M., Niewiadomski, A., Penczek, W., Półrola, A., Skaruz, J.: HarmonICS - a tool for composing medical services. In: ZEUS, pp. 25–33 (2012)

    Google Scholar 

  9. Doliwa, D., Horzelski, W., Jarocki, M., Niewiadomski, A., Penczek, W., Półrola, A., Szreter, M., Zbrzezny, A.: PlanICS - a web service compositon toolset. Fundam. Inform. 112(1), 47–71 (2011)

    MATH  Google Scholar 

  10. Elwakil, M., Yang, Z., Wang, L., Chen, Q.: Message race detection for web services by an SMT-based analysis. In: Zhang, D., Sadjadi, S.M., Xie, B., Branke, J., Zhou, X. (eds.) ATC 2010. LNCS, vol. 6407, pp. 182–194. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  11. Gehlot, V., Edupuganti, K.: Use of colored Petri nets to model, analyze, and evaluate service composition and orchestration. In: System Sciences, HICSS 2009, pp. 1–8, January 2009

    Google Scholar 

  12. Gerevini, A.E., Haslum, P., Long, D., Saetti, A., Dimopoulos, Y.: Deterministic planning in the fifth international planning competition: PDDL3 and experimental evaluation of the planners. Artif. Intel. 173(5–6), 619–668 (2009). Advances in Automated Plan Generation

    Article  MathSciNet  MATH  Google Scholar 

  13. Hao, S., Zhang, L.: Dynamic web services composition based on linear temporal logic. In: 2010 International Conference of Information Science and Management Engineering (ISME), vol. 1, pp. 362–365, August 2010

    Google Scholar 

  14. Li, Z., O’Brien, L., Keung, J., Xu, X.: Effort-oriented classification matrix of web service composition. In Proceedings of the Fifth International Conference on Internet and Web Applications and Services, pp. 357–362 (2010)

    Google Scholar 

  15. Monakova, G., Kopp, O., Leymann, F., Moser, S., Schäfers, K.: Verifying business rules using an SMT solver for BPEL processes. In: BPSC, pp. 81–94 (2009)

    Google Scholar 

  16. Nam, W., Kil, H., Lee, D.: Type-aware web service composition using boolean satisfiability solver. In: Proceedings of the CEC 2008 and EEE 2008, pp. 331–334 (2008)

    Google Scholar 

  17. Niewiadomski, A., Penczek, W.: Towards SMT-based abstract planning in PlanICS ontology. In: Proceedings of KEOD 2013 - International Conference on Knowledge Engineering and Ontology Development, pp. 123–131, September 2013

    Google Scholar 

  18. Niewiadomski, A., Penczek, W., Półrola, A.: Abstract planning in PlanICS ontology. An SMT-based approach. Technical report 1027, ICS PAS (2012)

    Google Scholar 

  19. Niewiadomski, A., Penczek, W., Skaruz, J.: Hybrid approach to abstract planning of web services. In: Service Computation 2015: The Seventh International Conferences on Advanced Service Computing, pp. 35–40 (2015)

    Google Scholar 

  20. Niewiadomski, A., Wolf, K.: LoLA as abstract planning engine of PlanICS. In: Proceedings of International Workshop on Petri Nets and Software Engineering, pp. 349–350 (2014)

    Google Scholar 

  21. OWL 2 web ontology language document overview (2009). http://www.w3.org/TR/owl2-overwiew/

  22. Rao, J., Küngas, P., Matskin, M.: Composition of semantic web services using linear logic theorem proving. Inf. Syst. 31(4), 340–360 (2006)

    Article  Google Scholar 

  23. Rao, J., Su, X.: A survey of automated web service composition methods. In: Cardoso, J., Sheth, A.P. (eds.) SWSWPC 2004. LNCS, vol. 3387, pp. 43–54. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  24. Skaruz, J., Niewiadomski, A., Penczek, W.: Automated abstract planning with use of genetic algorithms. In: GECCO (Companion), pp. 129–130 (2013)

    Google Scholar 

  25. Skaruz, J., Niewiadomski, A., Penczek, W.: Evolutionary algorithms for abstract planning. In: Wyrzykowski, R., Dongarra, J., Karczewski, K., Waśniewski, J. (eds.) PPAM 2013, Part I. LNCS, vol. 8384, pp. 392–401. Springer, Heidelberg (2014)

    Chapter  Google Scholar 

  26. Traverso, P., Pistore, M.: Automated composition of semantic web services into executable processes. In: van Harmelen, F., Plexousakis, D., McIlraith, S.A. (eds.) ISWC 2004. LNCS, vol. 3298, pp. 380–394. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. ICS, Siedlce University, 3-Maja 54, 08-110, Siedlce, Poland

    Artur Niewiadomski & Wojciech Penczek

  2. ICS, Polish Academy of Sciences, Jana Kazimierza 5, 01-248, Warsaw, Poland

    Wojciech Penczek

Authors
  1. Artur Niewiadomski
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Wojciech Penczek
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Wojciech Penczek .

Editor information

Editors and Affiliations

  1. Newcastle University, Newcastle upon Tyne, United Kingdom

    Maciej Koutny

  2. Lehrgebiet Software Engineering, FernUniversität in Hagen, Hagen, Germany

    Jörg Desel

  3. École Normale Supérieure de Cachan, Cachan, France

    Serge Haddad

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Niewiadomski, A., Penczek, W. (2015). SMT-Based Abstract Parametric Temporal Planning. In: Koutny, M., Desel, J., Haddad, S. (eds) Transactions on Petri Nets and Other Models of Concurrency X. Lecture Notes in Computer Science(), vol 9410. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-48650-4_4

Download citation

  • DOI: https://doi.org/10.1007/978-3-662-48650-4_4

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-662-48649-8

  • Online ISBN: 978-3-662-48650-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation