Controller synthesis for timeline-based games. (English) Zbl 07906379
Summary: In the timeline-based approach to planning, the evolution over time of a set of state variables (the timelines) is governed by a set of temporal constraints. Traditional timeline-based planning systems excel at the integration of planning with execution by handling temporal uncertainty. In order to handle general nondeterminism as well, the concept of timeline-based games has been recently introduced. It has been proved that finding whether a winning strategy exists for such games is 2EXPTIME-complete. However, a concrete approach to synthesize controllers implementing such strategies is missing. This paper fills this gap, by providing an effective and computationally optimal approach to controller synthesis for timeline-based games.
Software:
PDDLReferences:
| [1] | Renato Acampora, Luca Geatti, Nicola Gigante, Angelo Montanari, and Valentino Picotti. Controller synthesis for timeline-based games. Electronic Proceedings in Theoretical Computer Science, 370:131-146, sep 2022. T doi:10.4204/eptcs.370.9. · Zbl 1530.68238 · doi:10.4204/eptcs.370.9 |
| [2] | Rajeev Alur, Thomas A. Henzinger, and Orna Kupferman. Alternating-time temporal logic. J. ACM, 49(5):672-713, 2002. T doi:10.1145/585265.585270. · Zbl 1326.68181 · doi:10.1145/585265.585270 |
| [3] | J Richard Buchi and Lawrence H Landweber. Solving sequential conditions by finite-state strategies. In The Collected Works of J. Richard Büchi, pages 525-541. Springer, 1990. |
| [4] | BMM + 20] Laura Bozzelli, Alberto Molinari, Angelo Montanari, Adriano Peron, and Gerhard J. Woeginger. Timeline-based planning over dense temporal domains. Theor. Comput. Sci., 813:305-326, 2020. T doi:10.1016/j.tcs.2019.12.030. · Zbl 1433.68406 · doi:10.1016/j.tcs.2019.12.030 |
| [5] | Sara Bernardini and David E. Smith. Developing domain-independent search control for Europa2. In Proceedings of the ICAPS 2007 Workshop on Heuristics for Domain-Independent Planning, 2007. |
| [6] | BWMB + 05] Tania Bedrax-Weiss, Conor McGann, Andrew Bachmann, Will Edgington, and Michael Iatauro. Europa2: User and contributor guide. Technical report, NASA Ames Research Center, 2005. |
| [7] | Tom Bylander. The computational complexity of propositional STRIPS planning. Artificial Intelligence, 69(1-2):165-204, 1994. T doi:10.1016/0004-3702(94)90081-7. [CCD + 07] Amedeo Cesta, Gabriella Cortellessa, Michel Denis, Alessandro Donati, Simone Fratini, Angelo Oddi, Nicola Policella, Erhard Rabenau, and Jonathan Schulster. MEXAR2: AI solves mission planner problems. IEEE Intelligent Systems, 22(4):12-19, 2007. T doi:10.1109/MIS.2007.75. [CCF + 06] Amedeo Cesta, Gabriella Cortellessa, Simone Fratini, Angelo Oddi, and Nicola Policella. Software companion: The MEXAR2 support to space mission planners. In Gerhard Brewka, Silvia Coradeschi, Anna Perini, and Paolo Traverso, editors, Proceedings of the 17th European Conference on Artificial Intelligence, volume 141 of Frontiers in Artificial Intelligence and Applications, pages 622-626. IOS Press, 2006. · doi:10.1109/MIS.2007.75 |
| [8] | Alonzo Church. Logic, arithmetic, and automata. In Proceedings of the international congress of mathematicians, volume 1962, pages 23-35, 1962. · Zbl 0116.33604 |
| [9] | Amedeo Cesta and Angelo Oddi. Ddl.1: A formal description of a constraint representation language for physical domains. In Malik Ghallab and Alfredo Milani, editors, New directions in AI planning. IOS Press, 1996. |
| [10] | Marta Cialdea Mayer, Andrea Orlandini, and Alessandro Umbrico. Planning and execu-tion with flexible timelines: a formal account. Acta Informatica, 53(6-8):649-680, 2016. T doi:10.1007/s00236-015-0252-z. · Zbl 1351.90092 · doi:10.1007/s00236-015-0252-z |
| [11] | S. Chien, G. Rabideau, R. Knight, R. Sherwood, B. Engelhardt, D. Mutz, T. Estlin, B. Smith, F. Fisher, T. Barrett, G. Stebbins, and D. Tran. Aspen -automating space mission operations using automated planning and scheduling. In Proceedings of the International Conference on Space Operations, 2000. |
| [12] | Steve A. Chien, Gregg Rabideau, Daniel Tran, Martina Troesch, Joshua Doubleday, Federico Nespoli, Miguel Perez Ayucar, Marc Costa Sitja, Claire Vallat, Bernhard Geiger, Nico Alto-belli, Manuel Fernandez, Fran Vallejo, Rafael Andres, and Michael Kueppers. Activity-based scheduling of science campaigns for the rosetta orbiter. In Qiang Yang and Michael Wooldridge, editors, Proceedings of the 24th International Joint Conference on Artificial Intelligence, pages 4416-4422. AAAI Press, 2015. URL: http://ijcai.org/Abstract/15/655. |
| [13] | DGM + 17] Dario Della Monica, Nicola Gigante, Angelo Montanari, Pietro Sala, and Guido Sciavicco. Bounded timed propositional temporal logic with past captures timeline-based planning with bounded constraints. In Carles Sierra, editor, Proceedings of the 26th International Joint Conference on Artificial Intelligence, pages 1008-1014, 2017. T doi:10.24963/ijcai.2017/140. 17:24 R. Acampora, L. Geatti, N. Gigante, A. Montanari, and V. Picotti Vol. 20:3 · doi:10.24963/ijcai.2017/140 |
| [14] | Dario Della Monica, Nicola Gigante, Angelo Montanari, and Pietro Sala. A novel automata-theoretic approach to timeline-based planning. In Michael Thielscher, Francesca Toni, and Frank Wolter, editors, Proceedings of the 16th International Conference on Principles of Knowledge Representation and Reasoning, pages 541-550. AAAI Press, 2018. URL: https: //aaai.org/ocs/index.php/KR/KR18/paper/view/18024. |
| [15] | Dario Della Monica, Nicola Gigante, Salvatore La Torre, and Angelo Montanari. Complexity of qualitative timeline-based planning. In Proceedings of the 27th International Symposium on Temporal Representation and Reasoning, volume 178 of LIPIcs, pages 16:1-16:13, 2020. T doi:10.4230/LIPIcs.TIME.2020.16. · Zbl 07760486 · doi:10.4230/LIPIcs.TIME.2020.16 |
| [16] | David L. Dill. Timing assumptions and verification of finite-state concurrent systems. In Joseph Sifakis, editor, Proceedings of the International Workshop on Automatic Verification Methods for Finite State Systems, volume 407 of Lecture Notes in Computer Science, pages 197-212. |
| [17] | Springer, 1989. T doi:10.1007/3-540-52148-8 17. [DPC + 08] Alessandro Donati, Nicola Policella, Amedeo Cesta, Simone Fratini, Angelo Oddi, Gabriella Cortellessa, Federico Pecora, Jonathan Schulster, Erhard Rabenau, Marc Niezette, and Robin Steel. Science operations pre-planning & optimization using ai constraint-resolution -the apsi case study 1. In Proceedings of the 8th International Conference on Space Operations, 2008. T doi:10.2514/6.2008-3268. · doi:10.2514/6.2008-3268 |
| [18] | FCO + 11] Simone Fratini, Amedeo Cesta, Andrea Orlandini, Riccardo Rasconi, and Riccardo De Benedic-tis. Apsi-based deliberation in goal oriented autonomous controllers. In ASTRA 2011, volume 11. ESA, 2011. |
| [19] | Jeremy Frank and Ari K. Jónsson. Constraint-based attribute and interval planning. Constraints, 8(4):339-364, 2003. T doi:10.1023/A:1025842019552. · Zbl 1074.68609 · doi:10.1023/A:1025842019552 |
| [20] | Maria Fox and Derek Long. PDDL2.1: An extension to PDDL for expressing temporal planning domains. Journal of Artificial Intelligence Research, 20:61-124, 2003. · Zbl 1036.68093 |
| [21] | Richard Fikes and Nils J. Nilsson. STRIPS: A new approach to the application of theorem proving to problem solving. Artificial Intelligence, 2(3/4):189-208, 1971. T doi:10.1016/0004-3702(71)90010-5. · Zbl 0234.68036 · doi:10.1016/0004-3702(71)90010-5 |
| [22] | Nicola Gigante. Timeline-based Planning: Expressiveness and Complexity. PhD thesis, Univer-sity of Udine, Italy, 2019. Available on arXiv at: https://arxiv.org/abs/1902.06123. |
| [23] | Nicola Gigante, Angelo Montanari, Marta Cialdea Mayer, and Andrea Orlandini. Timelines are expressive enough to capture action-based temporal planning. In Curtis E. Dyreson, Michael R. Hansen, and Luke Hunsberger, editors, Proceedings of the 23rd International Symposium on Temporal Representation and Reasoning, pages 100-109. IEEE Computer Society, 2016. T doi:10.1109/TIME.2016.18. · doi:10.1109/TIME.2016.18 |
| [24] | Nicola Gigante, Angelo Montanari, Marta Cialdea Mayer, and Andrea Orlandini. Complexity of timeline-based planning. In Laura Barbulescu, Jeremy Frank, Mausam, and Stephen F. Smith, editors, Proceedings of the 27th International Conference on Automated Planning and Scheduling, pages 116-124. AAAI Press, 2017. URL: https://aaai.org/ocs/index.php/ ICAPS/ICAPS17/paper/view/15758. |
| [25] | GMO + 20] Nicola Gigante, Angelo Montanari, Andrea Orlandini, Marta Cialdea Mayer, and Mark Reynolds. On timeline-based games and their complexity. Theor. Comput. Sci., 815:247-269, 2020. T doi:10.1016/j.tcs.2020.02.011. · Zbl 1433.68409 · doi:10.1016/j.tcs.2020.02.011 |
| [26] | John McCarthy and Patrick J. Hayes. Some philosophical problems from the standpoint of artificial intelligence. In B. Meltzer and D. Michie, editors, Machine Intelligence 4, pages 463-502. Edinburgh University Press, 1969. · Zbl 0226.68044 |
| [27] | Nicola Muscettola. HSTS: Integrating Planning and Scheduling. In Monte Zweben and Mark S. Fox, editors, Intelligent Scheduling, chapter 6, pages 169-212. Morgan Kaufmann, 1994. |
| [28] | Andrea Orlandini, Alberto Finzi, Amedeo Cesta, and Simone Fratini. Tga-based controllers for flexible plan execution. In Joscha Bach and Stefan Edelkamp, editors, Proceedings of the 34th Annual German Conference on Artificial Intelligence, volume 7006 of Lecture Notes in Computer Science, pages 233-245. Springer, 2011. T doi:10.1007/978-3-642-24455-1 22. · doi:10.1007/978-3-642-24455-1_22 |
| [29] | Mathias Péron and Nicolas Halbwachs. An abstract domain extending difference-bound matrices with disequality constraints. In International Workshop on Verification, Model Checking, and Abstract Interpretation, pages 268-282. Springer, 2007. T doi:10.1007/978-3-540-69738-1 20. · Zbl 1132.68464 · doi:10.1007/978-3-540-69738-1_20 |
| [30] | Vol. 20:3 CONTROLLER SYNTHESIS FOR TIMELINE-BASED GAMES 17:25 · Zbl 07906379 |
| [31] | A. Pnueli and R. Rosner. On the synthesis of a reactive module. In Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’89, page 179-190, New York, NY, USA, 1989. Association for Computing Machinery. T doi:10.1145/75277.75293. · doi:10.1145/75277.75293 |
| [32] | Amir Pnueli and Roni Rosner. On the synthesis of an asynchronous reactive module. In International Colloquium on Automata, Languages, and Programming, pages 652-671. Springer, 1989. · Zbl 0686.68015 |
| [33] | Roni Rosner. Modular synthesis of reactive systems. PhD thesis, Weizmann Institute of Science, 1992. |
| [34] | David E. Smith, Jeremy Frank, and William Cushing. The ANML language. In Proceedinsgs of the ICAPS 2008 Workshop on Knowledge Engineering for Planning and Scheduling, 2008. |
| [35] | Wolfgang Thomas. Solution of Church’s problem: A tutorial. New Perspectives on Games and Interaction. Texts on Logic and Games, 5, 2008. 17:26 R. Acampora, L. Geatti, N. Gigante, A. Montanari, and V. Picotti Vol. 20:3 (Step: Item 1a of Definition 4.5). Let a[x = v] be a quantified token of E. If start(a) ∈ I n , then γ(start(a)) = n and by definition of matching function start(x, v) ∈ A n . (Step: Item 1b of Definition 4.5).(←-). Let end(a) ̸ ∈ M n-1 be a possible candidate for inclusion in I n . If start(a) ∈ M n-1 and end(x, v) ∈ A n , then end(x, v) ends the token started at µ γ| <n (start(a)) ; otherwise, there would exist µ i = (A i , δ i ) prior to µ n such that end(x, v) ∈ A i , contradicting that γ| <n is undefined on end(a). By definition of matching function, since end(x, v) ∈ A n ends the token started at µ γ(start(a)) , we have γ(end(a)) = n and end(a) ∈ I n . (Step: Item 1b of Definition 4.5).(-→). If end(a) ∈ I n , then by definition of matching function end(x, v) ∈ A n . Furthermore, since end(a) ∈ M n , Item (I) gives γ(start(a)) ≤ γ(end(a)) for the atom start(a) ≤ [l,u] end(a) in C. By definition of event sequence, start(x, v) and end(x, v) cannot appear in the same event; hence, γ(start(a)) < γ(end(a)) = n and start(a) ∈ M n-1 . (Step: Item 2a of Definition 4.5). Let T be a term in I n , and let T ′ ∈ V be any other term such that D n-1 [T ′ , T ] ≤ 0. Then, D n-1 [T ′ , T ] can either be the lower bound of an atom T ′ ≤ [l,u] T , or the upper bound of an atom T ≤ [l,u] T ′ in C. In the first case, we can directly conclude that T ′ ∈ M n-1 ∪ I n , because T ′ ∈ M n by Item (I) of γ and M n = M n-1 ∪ I n by definition of M n-1 and I n . In the second case, note that D n-1 [T ′ , T ] = u, i.e., it has never been decremented because T ̸ ∈ M n-1 , and that upper bounds u can never be negative. Thus, u is equal to 0 and γ satisfies 0 ≤ δ(µ [γ(T )...γ(T ′ )] ) ≤ 0 (Item (I)), meaning that γ(T ′ ) = γ(T ) and T ′ ∈ I n . (Step: Item 2b of Definition 4.5). Let T ∈ I n and T ′ ∈ M n-1 . D n-1 [T ′ , T ] cannot be the upper bound of an atom T ≤ [l,u] T ′ ; otherwise, Item (I) would imply T ∈ M n-1 , contradicting T ∈ I n . Thus, D n-1 [T ′ , T ] must either represent the lower bound of an atom T ′ ≤ [l,u] T in C, or be equal to +∞. In the latter case, δ n ≥ -D n-1 [T ′ , T ] trivially holds. In the former case, D n-1 [T ′ , T ] = -l + δ(µ [γ| <n (T ′ )...n-1] ). Since γ(T ) = n, we have δ(µ [γ(T ′ )...γ(T )] ) |
| [36] | + δ n ≥ l. Hence, δ n ≥ l -δ(µ [γ(T ′ )...n- |
| [37] | = -D n-1 [T ′ , T ]. (Step: Item 2c of Definition 4.5). Let T, T ′ ∈ I n be two distinct terms. Then, γ(T ′ ) = γ(T ) and δ(µ [γ(T ′ )... |
| [38] | = 0. If T ≤ [l,u] T ′ (resp., T ′ ≤ [l,u] T ) belongs to C, then D n-1 [T, T ′ ] (resp., D n-1 [T ′ , T ]) is the lower bound l and equals 0 by Item (I). Otherwise, D n-1 [T, T ′ ] = D n-1 [T ′ , T ] = +∞. Hence, M n-1 µn,In —→ M n is well defined and ⟨I 1 , . . . , I n ⟩ is a run of M E on µ yielding M n . |
| [39] | We proceed by induction on the length of the event sequence µ = ⟨µ 1 , . . . , µ n ⟩. Base case. An empty run I yields M E = (V, D, ∅, 0) itself. Then the function γ 0 : ∅ → ∅ vacuously satisfies the definition of matching function and Items (I) and (II). Inductive step. Let I = ⟨I 1 , . . . , I n ⟩ be a run of M E on µ, yielding a matching structure M n = (V, D n , M n , t n ). Note that I [1...n-1] is a run of M E on µ [1...n-1] yielding a matching structure M n-1 = (V, D n-1 , M n-1 , t n-1 ). By the inductive hypothesis, there exists a match-ing function γ <n : M n-1 → [1, . . . , n-1] satisfying Items (I) and (II). Let γ : M n → [1, . . . , n] be the extension of γ <n to M n , such that γ(T ) = n, for all T ∈ I n . (Step: γ is a matching function). Items 1 and 2 hold for all the terms already present in the domain of γ <n . For every term in I n , Item 1 for γ follows from Item 1 of I n -match event. Let start(a), end(a) ∈ M n be two terms not both already present in M n-1 , meaning that start(a) ∈ M n-1 and end(a) ∈ I n , for some quantified token a[x = v] in E. By definition of I n -match event, µ n = (A n , δ n ) is such that end(x, v) ∈ A n and no other event in |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
