Document Open Access Logo

Hybrid SAT-Based Consistency Checking Algorithms for Simple Temporal Networks with Decisions

Authors Matteo Zavatteri , Carlo Combi , Romeo Rizzi , Luca Viganò

PDF
Thumbnail PDF

File

LIPIcs.TIME.2019.16.pdf
  • Filesize: 0.64 MB
  • 17 pages

Document Identifiers

Author Details

Matteo Zavatteri
  • Department of Computer Science, University of Verona, Italy
Carlo Combi
  • Department of Computer Science, University of Verona, Italy
Romeo Rizzi
  • Department of Computer Science, University of Verona, Italy
Luca Viganò
  • Department of Informatics, King’s College London, UK

Cite AsGet BibTex

Matteo Zavatteri, Carlo Combi, Romeo Rizzi, and Luca Viganò. Hybrid SAT-Based Consistency Checking Algorithms for Simple Temporal Networks with Decisions. In 26th International Symposium on Temporal Representation and Reasoning (TIME 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 147, pp. 16:1-16:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.TIME.2019.16

Abstract

A Simple Temporal Network (STN) consists of time points modeling temporal events and constraints modeling the minimal and maximal temporal distance between them. A Simple Temporal Network with Decisions (STND) extends an STN by adding decision time points to model temporal plans with decisions. A decision time point is a special kind of time point that once executed allows for deciding a truth value for an associated Boolean proposition. Furthermore, STNDs label time points and constraints by conjunctions of literals saying for which scenarios (i.e., complete truth value assignments to the propositions) they are relevant. Thus, an STND models a family of STNs each obtained as a projection of the initial STND onto a scenario. An STND is consistent if there exists a consistent scenario (i.e., a scenario such that the corresponding STN projection is consistent). Recently, a hybrid SAT-based consistency checking algorithm (HSCC) was proposed to check the consistency of an STND. Unfortunately, that approach lacks experimental evaluation and does not allow for the synthesis of all consistent scenarios. In this paper, we propose an incremental HSCC algorithm for STNDs that (i) is faster than the previous one and (ii) allows for the synthesis of all consistent scenarios and related early execution schedules (offline temporal planning). Then, we carry out an experimental evaluation with KAPPA, a tool that we developed for STNDs. Finally, we prove that STNDs and disjunctive temporal networks (DTNs) are equivalent.

Subject Classification

ACM Subject Classification
  • Theory of computation → Timed and hybrid models
  • Computing methodologies → Temporal reasoning
  • Computing methodologies → Planning and scheduling
  • Mathematics of computing → Graph algorithms
  • Hardware → Theorem proving and SAT solving
Keywords
  • Simple temporal network with decisions
  • HSCC algorithms
  • incremental SAT-solving
  • disjunctive temporal network
  • KAPPA

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Tomas Balyo, Armin Biere, Markus Iser, and Carsten Sinz. SAT race 2015. Artificial Intelligence, 241:45-65, 2016. Google Scholar
  2. Clark W. Barrett, Roberto Sebastiani, Sanjit A. Seshia, and Cesare Tinelli. Satisfiability Modulo Theories. In Handbook of Satisfiability, pages 825-885. IOS Press, 2009. Google Scholar
  3. Daniel Le Berre and Anne Parrain. The Sat4j library, release 2.2. JSAT, 7(2-3):59-6, 2010. URL: http://jsat.ewi.tudelft.nl/content/volume7/JSAT7_4_LeBerre.pdf.
  4. Massimo Cairo, Carlo Combi, Carlo Comin, Luke Hunsberger, Roberto Posenato, Romeo Rizzi, and Matteo Zavatteri. Incorporating Decision Nodes into Conditional Simple Temporal Networks. In 24th International Symposium on Temporal Representation and Reasoning (TIME 2017), volume 90 of LIPIcs, pages 9:1-9:17. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.TIME.2017.9.
  5. Massimo Cairo, Luke Hunsberger, Roberto Posenato, and Romeo Rizzi. A Streamlined Model of Conditional Simple Temporal Networks - Semantics and Equivalence Results. In 24th International Symposium on Temporal Representation and Reasoning, TIME 2017, volume 90 of LIPIcs, pages 10:1-10:19. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.TIME.2017.10.
  6. Carlo Combi, Roberto Posenato, Luca Viganò, and Matteo Zavatteri. Access Controlled Temporal Networks. In 9th International Conference on Agents and Artificial Intelligence (ICAART 2017), pages 118-131. INSTICC, ScitePress, 2017. URL: https://doi.org/10.5220/0006185701180131.
  7. Carlo Combi, Roberto Posenato, Luca Viganò, and Matteo Zavatteri. Conditional Simple Temporal Networks with Uncertainty and Resources. Journal of Artificial Intelligence Research, 64:931-985, 2019. URL: https://doi.org/10.1613/jair.1.11453.
  8. Carlo Combi, Luca Viganò, and Matteo Zavatteri. Security Constraints in Temporal Role-Based Access-Controlled Workflows. In 6th ACM Conference on Data and Application Security and Privacy, CODASPY '16, pages 207-218. ACM, 2016. URL: https://doi.org/10.1145/2857705.2857716.
  9. Patrick R. Conrad and Brian C. Williams. Drake: An Efficient Executive for Temporal Plans with Choice. Journal of Artificial Intelligence Research, 42(1):607-659, 2011. Google Scholar
  10. Neil T. Dantam, Zachary K. Kingston, Swarat Chaudhuri, and Lydia E. Kavraki. Incremental Task and Motion Planning: A Constraint-Based Approach. In Robotics: Science and Systems XII, 2016. URL: http://www.roboticsproceedings.org/rss12/.
  11. Rina Dechter, Itay Meiri, and Judea Pearl. Temporal Constraint Networks. Artificial Intelligence, 49(1-3):61-95, 1991. Google Scholar
  12. Niklas Eén and Niklas Sörensson. Temporal induction by incremental SAT solving. Electronic Notes in Theoretical Computer Science, 89(4):543-560, 2003. Google Scholar
  13. Stephan Gocht and Tomas Balyo. Accelerating SAT Based Planning with Incremental SAT Solving. In ICAPS 2017, pages 135-139. AAAI Press, 2017. Google Scholar
  14. Ruoyun Huang, Yixin Chen, and Weixiong Zhang. A Novel Transition Based Encoding Scheme for Planning as Satisfiability. In AAAI 2010. AAAI Press, 2010. Google Scholar
  15. Luke Hunsberger and Roberto Posenato. Sound-and-Complete Algorithms for Checking the Dynamic Controllability of Conditional Simple Temporal Networks with Uncertainty. In 25th International Symposium on Temporal Representation and Reasoning (TIME 2018), volume 120 of Leibniz International Proceedings in Informatics (LIPIcs), pages 14:1-14:17. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2018. URL: https://doi.org/10.4230/LIPIcs.TIME.2018.14.
  16. Luke Hunsberger, Roberto Posenato, and Carlo Combi. The Dynamic Controllability of Conditional STNs with Uncertainty. In Workshop on Planning and Plan Execution for Real-World Systems (PlanEx) at ICAPS-2012, pages 1-8, 2012. URL: http://arxiv.org/abs/1212.2005.
  17. Luke Hunsberger, Roberto Posenato, and Carlo Combi. A Sound-and-Complete Propagation-based Algorithm for Checking the Dynamic Consistency of Conditional Simple Temporal Networks. In 22nd International Symposium on Temporal Representation and Reasoning (TIME 2015), pages 4-18. IEEE, 2015. URL: https://doi.org/10.1109/TIME.2015.26.
  18. Erez Karpas, Steven James Levine, Peng Yu, and Brian Charles Williams. Robust Execution of Plans for Human-Robot Teams. In ICAPS 2015, pages 342-346. AAAI Press, 2015. Google Scholar
  19. Henry A. Kautz, David A. McAllester, and Bart Selman. Encoding Plans in Propositional Logic. In KR '96, pages 374-384. Morgan Kaufmann, 1996. Google Scholar
  20. Henry A. Kautz and Bart Selman. Planning As Satisfiability. In ECAI '92, pages 359-363. John Wiley & Sons, Inc., 1992. Google Scholar
  21. Phil Kim, Brian C. Williams, and Mark Abramson. Executing Reactive, Model-based Programs through Graph-based Temporal Planning. In IJCAI 2001, pages 487-493. Morgan Kaufmann, 2001. Google Scholar
  22. Steven James Levine and Brian Charles Williams. Concurrent Plan Recognition and Execution for Human-Robot Teams. In ICAPS 2014. AAAI Press, 2014. Google Scholar
  23. Hui Li and Brian Williams. Generalized Conflict Learning for Hybrid Discrete/Linear Optimization. In CP 2005, pages 415-429. Springer, 2005. Google Scholar
  24. Paul H. Morris, Nicola Muscettola, and Thierry Vidal. Dynamic Control Of Plans With Temporal Uncertainty. In 17th International Joint Conference on Artificial Intelligence, IJCAI 2001, pages 494-502. Morgan Kaufmann, 2001. Google Scholar
  25. Kostas Stergiou and Manolis Koubarakis. Backtracking algorithms for disjunctions of temporal constraints. Artificial Intelligence, 120(1):81-117, 2000. Google Scholar
  26. Ioannis Tsamardinos, Thierry Vidal, and Martha E. Pollack. CTP: A new constraint-based formalism for conditional, temporal planning. Constraints, 8(4):365-388, 2003. Google Scholar
  27. Peng Yu, Cheng Fang, and Brian Charles Williams. Resolving Uncontrollable Conditional Temporal Problems Using Continuous Relaxations. In ICAPS 2014. AAAI Press, 2014. Google Scholar
  28. Peng Yu and Brian Charles Williams. Continuously Relaxing Over-Constrained Conditional Temporal Problems through Generalized Conflict Learning and Resolution. In IJCAI 2013, pages 2429-2436. IJCAI/AAAI, 2013. Google Scholar
  29. Matteo Zavatteri. Conditional Simple Temporal Networks with Uncertainty and Decisions. In 24th International Symposium on Temporal Representation and Reasoning (TIME 2017), volume 90 of LIPIcs, pages 23:1-23:17. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.TIME.2017.23.
  30. Matteo Zavatteri. Temporal and Resource Controllability of Workflows Under Uncertainty. In Proceedings of the Dissertation Award, Demonstration, and Industrial Track at BPM 2019, volume 2420, pages 9-14. CEUR-WS.org, 2019. URL: http://ceur-ws.org/Vol-2420/paperDA3.pdf.
  31. Matteo Zavatteri, Carlo Combi, Roberto Posenato, and Luca Viganò. Weak, Strong and Dynamic Controllability of Access-Controlled Workflows Under Conditional Uncertainty. In Business Process Management - 15th International Conference, BPM 2017, pages 235-251. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-65000-5_14.
  32. Matteo Zavatteri, Carlo Combi, and Luca Viganò. Resource Controllability of Workflows Under Conditional Uncertainty. In Business Process Management Workshops (AI4BPM 2019) (to appear). Springer International Publishing, 2019. Google Scholar
  33. Matteo Zavatteri and Luca Viganò. Conditional simple temporal networks with uncertainty and decisions. Theoretical Computer Science, (In press):, 2018. URL: https://doi.org/10.1016/j.tcs.2018.09.023.
  34. Matteo Zavatteri and Luca Viganò. Constraint Networks Under Conditional Uncertainty. In 10th International Conference on Agents and Artificial Intelligence - Volume 2 (ICAART 2018), pages 41-52. SciTePress, 2018. URL: https://doi.org/10.5220/0006553400410052.
  35. Matteo Zavatteri and Luca Viganò. Conditional Uncertainty in Constraint Networks. In Agents and Artificial Intelligence, pages 130-160. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-05453-3_7.
  36. Matteo Zavatteri and Luca Viganò. Last Man Standing: Static, Decremental and Dynamic Resiliency via Controller Synthesis. Journal of Computer Security, 27(3):343-373, 2019. URL: https://doi.org/10.3233/JCS-181244.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact