Skip to main content
SpringerLink
Log in

Task Planning with OMT: An Application to Production Logistics

  • Conference paper
  • First Online:
Integrated Formal Methods (IFM 2018)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 11023))

Included in the following conference series:

Abstract

Task planning is a well-studied problem for which interesting applications exist in production logistics. Planning for such domains requires to take into account not only feasible plans, but also optimality targets, e.g., minimize time, costs or energy consumption. Although there exist several algorithms to compute optimal solutions with formal guarantees, heuristic approaches are typically preferred in practical applications, trading certified solutions for a reduced computational cost. Reverting this trend represents a standing challenge within the domain of task planning at large. In this paper we discuss our experience using Optimization Modulo Theories to synthesize optimal plans for multi-robot teams handling production processes within the RoboCup Logistics League. Besides presenting our results, we discuss challenges and possible directions for future development of OMT planning.

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

Notes

  1. 1.

    https://www2.deloitte.com/insights/us/en/focus/industry-4-0/smart-factory-connected-manufacturing.html.

  2. 2.

    For instance, if f and \(\varphi _S\) are expressed in QF_LRA, this can be done with Simplex.

  3. 3.

    http://www.robocup-logistics.org/sim-comp.

References

  1. EXplainable AI Planning (2018). http://icaps18.icaps-conference.org/xaip/

  2. Baier, C., Katoen, J.: Principles of Model Checking. MIT Press, Cambridge (2008)

    MATH  Google Scholar 

  3. Bensalem, S., Havelund, K., Orlandini, A.: Verification and validation meet planning and scheduling. STTT 16(1), 1–12 (2014)

    Article  Google Scholar 

  4. Bit-Monnot, A., Leofante, F., Pulina, L., Ábrahám, E., Tacchella, A.: SMarTplan: a task planner for smart factories. CoRR abs/1806.07135 (2018)

    Google Scholar 

  5. Bjørner, N., Phan, A.-D., Fleckenstein, L.: \(\nu \)z - An optimizing SMT solver. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 194–199. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-46681-0_14

    Chapter  Google Scholar 

  6. Cashmore, M., Fox, M., Long, D., Magazzeni, D.: A compilation of the full PDDL+ language into SMT. In: Proceedings of ICAPS 2016, pp. 79–87 (2016)

    Google Scholar 

  7. Cimatti, A., Griggio, A., Irfan, A., Roveri, M., Sebastiani, R.: Invariant checking of NRA transition systems via incremental reduction to LRA with EUF. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 58–75. Springer, Heidelberg (2017). https://doi.org/10.1007/978-3-662-54577-5_4

    Chapter  Google Scholar 

  8. Cimatti, A., Griggio, A., Irfan, A., Roveri, M., Sebastiani, R.: Satisfiability modulo transcendental functions via incremental linearization. In: de Moura, L. (ed.) CADE 2017. LNCS (LNAI), vol. 10395, pp. 95–113. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-63046-5_7

    Chapter  Google Scholar 

  9. Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The mathSAT5 SMT solver. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 93–107. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-36742-7_7

    Chapter  MATH  Google Scholar 

  10. Corzilius, F., Kremer, G., Junges, S., Schupp, S., Ábrahám, E.: SMT-RAT: an open source C++ toolbox for strategic and parallel SMT solving. In: Heule, M., Weaver, S. (eds.) SAT 2015. LNCS, vol. 9340, pp. 360–368. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-24318-4_26

    Chapter  MATH  Google Scholar 

  11. Ghallab, M., Nau, D.S., Traverso, P.: Automated Planning and Acting. Cambridge University Press, Cambridge (2016)

    MATH  Google Scholar 

  12. Gini, M.L.: Multi-robot allocation of tasks with temporal and ordering constraints. In: Proceedings of AAAI 2018, pp. 4863–4869 (2017)

    Google Scholar 

  13. Hamadi, Y., Wintersteiger, C.M.: Seven challenges in parallel SAT solving. AI Mag. 34(2), 99–106 (2013)

    Article  Google Scholar 

  14. Hofmann, T., Niemueller, T., Claßen, J., Lakemeyer, G.: Continual planning in Golog. In: Proceeding of AAAI 2016, pp. 3346–3353 (2016)

    Google Scholar 

  15. Hyvärinen, A.E.J., Wintersteiger, C.M.: Parallel satisfiability modulo theories. In: Hamadi, Y., Sais, L. (eds.) Handbook of Parallel Constraint Reasoning, pp. 141–178. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-63516-3_5

    Chapter  Google Scholar 

  16. Kautz, H.A., Selman, B.: Planning as satisfiability. In: ECAI, pp. 359–363 (1992)

    Google Scholar 

  17. Krizhevsky, A., Sutskever, I., Hinton, G.E.: Imagenet classification with deep convolutional neural networks. In: Proceedings of NIPS 2012, pp. 1097–1105 (2012)

    Google Scholar 

  18. LaValle, S.M.: Planning Algorithms. Cambridge University Press, Cambridge (2006)

    Book  Google Scholar 

  19. Leofante, F.: Guaranteed plans for multi-robot systems via optimization modulo theories. In: Proceedings of AAAI 2018 (2018)

    Google Scholar 

  20. Leofante, F.: Optimal multi-robot task planning: from synthesis to execution (and back). In: Proceeding of IJCAI 2018 (2018, to appear)

    Google Scholar 

  21. Leofante, F., Ábrahám, E., Niemueller, T., Lakemeyer, G., Tacchella, A.: On the synthesis of guaranteed-quality plans for robot fleets in logistics scenarios via optimization modulo theories. In: Proceedings of IRI 2017, pp. 403–410 (2017)

    Google Scholar 

  22. Leofante, F., Ábrahám, E., Niemueller, T., Lakemeyer, G., Tacchella, A.: Integrated Synthesis and Execution of Optimal Plans for Multi-Robot Systems in Logistics. Information Systems Frontiers, pp. 1–21. Springer, New York (2018). https://doi.org/10.1007/s10796-018-9858-3

    Book  Google Scholar 

  23. de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-3_24

    Chapter  Google Scholar 

  24. Niemueller, T., Karpas, E., Vaquero, T., Timmons, E.: Planning competition for logistics robots in simulation. In: Proceeding of PlanRob@ICAPS 2016 (2016)

    Google Scholar 

  25. Niemueller, T., Lakemeyer, G., Ferrein, A.: Incremental task-level reasoning in a competitive factory automation scenario. In: AAAI Spring Symposium - Designing Intelligent Robots: Reintegrating AI (2013)

    Google Scholar 

  26. Niemueller, T., Lakemeyer, G., Ferrein, A.: The RoboCup Logistics League as a benchmark for planning in robotics. In: Proceeding of PlanRob@ICAPS 2015 (2015)

    Google Scholar 

  27. Niemueller, T., Lakemeyer, G., Leofante, F., Ábrahám, E.: Towards CLIPS-based task execution and monitoring with SMT-based decision optimization. In: Proceedings of PlanRob@ICAPS 2017 (2017)

    Google Scholar 

  28. Nunes, E., Manner, M.D., Mitiche, H., Gini, M.L.: A taxonomy for task allocation problems with temporal and ordering constraints. Robot. Auton. Syst. 90, 55–70 (2017)

    Article  Google Scholar 

  29. Popplestone, R., Ambler, A., Bellos, I.: RAPT: a language for describing assemblies. Ind. Robot Int. J. 5(3), 131–137 (1978)

    Article  Google Scholar 

  30. RCLL Technical Committee: RoboCup Logistics League – Rules and regulations 2017 (2017)

    Google Scholar 

  31. Sebastiani, R., Tomasi, S.: Optimization modulo theories with linear rational costs. ACM Trans. Comput. Log. 16(2), 12:1–12:43 (2015)

    Article  MathSciNet  Google Scholar 

  32. Sebastiani, R., Trentin, P.: OptiMathSAT: a tool for optimization modulo theories. In: Proceedings of CAV 2015, pp. 447–454 (2015)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Genoa, Genoa, Italy

    Francesco Leofante & Armando Tacchella

  2. RWTH Aachen University, Aachen, Germany

    Francesco Leofante & Erika Ábrahám

Authors
  1. Francesco Leofante
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Erika Ábrahám
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Armando Tacchella
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Francesco Leofante .

Editor information

Editors and Affiliations

  1. Università della Svizzera Italiana, Lugano, Switzerland

    Carlo A. Furia

  2. University of Queensland, Brisbane, Queensland, Australia

    Kirsten Winter

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Leofante, F., Ábrahám, E., Tacchella, A. (2018). Task Planning with OMT: An Application to Production Logistics. In: Furia, C., Winter, K. (eds) Integrated Formal Methods. IFM 2018. Lecture Notes in Computer Science(), vol 11023. Springer, Cham. https://doi.org/10.1007/978-3-319-98938-9_18

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-98938-9_18

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-98937-2

  • Online ISBN: 978-3-319-98938-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation