Many Planning and Scheduling systems are designed assuming that the system under control is able to decide the duration of all the activities being executed. However, in many application scenarios this assumption is not acceptable because the actual timing of actions is not under direct control of the plan executor. Hence, new Planning and Scheduling techniques are needed to deal with this temporal uncertainty explicitly.
In this paper, we summarize and systematize a series of works in which we addressed this uncertainty problem in the realm of temporal network scheduling. We show how Satisfiability Modulo Theory (SMT) solvers can be exploited to quickly solve different kinds of query in this setting. In particular, we focus on the framework of Disjunctive Temporal Networks with Uncertainty and address the three degrees of controllability for the fully-disjunctive class of problems, solving several open problems in the literature and experimentally showing the performance of the developed techniques. Finally, we outline and discuss several foreseeable directions of research in this field.
AbdeddaïmY., AsarinE., GallienM., IngrandF., LesireC. and SighireanuM., Planning robust temporal plans: A comparison between CBTP and TGA approaches. In Proceedings of the Seventeenth International Conference on Automated Planning and Scheduling, ICAPS 2007, Providence, Rhode Island, USA, September 22-26, 2007, pp. 2–9.
2.
AlurR. and DillD.L., A theory of timed automata, Theoretical Computer Science126(2) (1994), 183–235.
3.
ArmandoA., CastelliniC. and GiunchigliaE., SAT-based procedures for temporal reasoning, In ECP, 1999, pp. 97–108.
4.
BarrettC.W., SebastianiR., SeshiaS.A. and TinelliC., Satisfiability modulo theories. In Handbook of Satisfiability, IOS Press, 2009, pp. 825–885.
5.
BehrmannG., CougnardA., DavidA., FleuryE., LarsenK.G. and LimeD., Uppaal-Tiga: Time for playing games!, In CAV, 2007, pp. 121–125.
6.
Bit-MonnotA., GhallabM. and IngrandF., Which contingent events to observe for the dynamic controllability of a plan. In Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence, IJCAI 2016, New York, NY, USA, 9-15 July 2016, 2016, pp. 3038–3044.
7.
BruttomessoR., CimattiA., FranzénA., GriggioA. and SebastianiR., The MathSAT 4 SMT solver, In CAV, 2008, pp. 299–303.
8.
BruttomessoR., PekE., SharyginaN. and TsitovichA., The OpenSMT solver, In TACAS, 2010, pp. 150–153.
9.
CassezF., DavidA., FleuryE. and GuldstrandK., Larsen and D. Lime, Efficient on-the-fly algorithms for the analysis of timed games, In CONCUR, 2005, pp. 66–80.
10.
CimattiA., GriggioA., SchaafsmaB.J. and SebastianiR., The MathSAT5 SMT solver, In TACAS, 2013.
11.
CimattiA., HunsbergerL., MicheliA., PosenatoR. and RoveriM., Sound and complete algorithms for checking the dynamic controllability of temporal networks with uncertainty, disjunction and observation, In TIME, 2014, pp. 27–36.
12.
CimattiA., HunsbergerL., MicheliA., PosenatoR. and RoveriM., Dynamic controllability via timed game automata, Acta Inf53(6-8) (2016), 681–722.
13.
CimattiA., HunsbergerL., MicheliA. and RoveriM., Using timed game automata to synthesize execution strategies for simple temporal networks with uncertainty, IN AAAI, 2014, pp. 2242–2249.
14.
CimattiA., MicheliA. and RoveriM., Solving temporal problems using SMT: Strong controllability, In CP, 2012, pp. 248–264.
15.
CimattiA., MicheliA. and RoveriM., Solving temporal problems using SMT: Weak controllability, In AAAI, 2012.
16.
CimattiA., MicheliA. and RoveriM., An SMT-based approach to weak controllability for disjunctive temporal problems with uncertainty, Artificial Intelligence224 (2015), 1–27.
17.
CimattiA., MicheliA. and RoveriM., Solving strong controllability of temporal problems with uncertainty using SMT. Constraints, 2015.
18.
CimattiA., MicheliA. and RoveriM., Strong temporal planning with uncontrollable durations: A state-space approach. In AAAI, 2015, pp. 3254–3260.
19.
CimattiA., MicheliA. and RoveriM., Dynamic controllability of disjunctive temporal networks: Validation and synthesis of executable strategies, In AAAI, page to appear, 2016.
20.
CuiJ., YuP., FangC., HaslumP. and WilliamsB.C., Optimising bounds in simple temporal networks with uncertainty under dynamic controllability constraints, In ICAPS, 2015, pp. 52–60.
21.
DavisM., LogemannG. and LovelandD.W., A machine program for theorem-proving, Communications of ACM5(7) (1962), 394–397.
22.
Thierry de la Tour. Minimizing the number of clauses by renaming. In
StickelMark, editor, volume 449 of LNCS, Springer, 1990, pp. 558–572.
23.
MouraL.M.D. and BjørnerN., Z3: An efficient SMT solver, In TACAS, 2008, pp. 337–340.
GhallabM. and LaruelleH., Representation and control in ixtet, a temporal planner, In AIPS, 1994, pp. 61–67.
27.
GhallabM., NauD.S. and TraversoP., Automated planning - theory and practice, Elsevier, 2004.
28.
GranlundT., and the GMP development team. GNU MP: The GNU Multiple Precision Arithmetic Library, 5.0.5 edition, 2012. http://gmplib.org/.
29.
HunsbergerL., Fixing the semantics for dynamic controllability and providing a more practical characterization of dynamic execution strategies. In TIME, 2009, pp. 155–162.
30.
HunsbergerL., A fast incremental algorithm for managing the execution of dynamically controllable temporal networks, In TIME, 2010, pp. 121–128.
31.
HunsbergerL., A fast incremental algorithm for managing the execution of dynamically controllable temporal networks. In TIME, pages 121–128, Los Alamitos, CA, USA, 2010. IEEE Computer Society.
32.
HunsbergerL., A faster execution algorithm for dynamically controllable stnus, In TIME, 2013, pp. 26–33.
33.
HunsbergerL., A faster algorithm for checking the dynamic controllability of simple temporal networks with uncertainty, In ICAART, 2014.
34.
KimH., SomenziF. and JinH.S., Efficient Term-ITE conversion for satisfiability modulo theories, In SAT, 2009, pp. 195–208.
35.
KleeneS.C., Mathematical Logic. J. Wiley & Sons, 1967.
36.
LaborieP., Resource temporal networks: Definition and complexity, In IJCAI-03, Proceedings of the Eighteenth International Joint Conference on Artificial Intelligence, Acapulco, Mexico, August 9-15, 2003, pp. 948–953.
37.
LombardiM. and MilanoM., Constraint based scheduling to deal with uncertain durations and self-timed execution, In Principles and Practice of Constraint Programming - CP 2010 - 16th International Conference, CP 2010, St. Andrews, Scotland, UK, September 6-10, 2010. Proceedings, 2010, pp. 383–397.
38.
LoosR. and WeispfenningV., Applying linear quantifier elimination, Computer Journal36(5) (1993), 450–462.
39.
MalerO., PnueliA. and SifakisJ., On the synthesis of discrete controllers for timed systems, In STACS, 1995, pp. 229–242.
40.
MayerM.C. and OrlandiniA., An executable semantics of flexible plans in terms of timed game automata In 22nd International Symposium on Temporal Representation and Reasoning, TIME 2015, Kassel, Germany, September 23-25, 2015, pp. 160–169.
41.
MicheliA., Planning and Scheduling in Temporally Uncertain Domains. PhD thesis, University of Trento, 1 2016. Fulltext available at http://www.mikand.net/thesis/.
42.
MicheliA., DoM. and SmithD.E., Compiling away uncertainty in strong temporal planning with uncontrollable durations. In IJCAI, 2015.
43.
MorrisP., A structural characterization of temporal dynamic controllability, In CP, pp. 375–389.
44.
MorrisP., Dynamic controllability and dispatchability relationships. In
SimonisHelmut, editor, CPAIOR, volume 8451 of Lecture Notes in Computer Science, Springer, 2014, pp. 464–479.
45.
MorrisP.H. and MuscettolaN., Temporal dynamic controllability revisited, In AAAI, 2005, pp. 1193–1198.
46.
MorrisP.H., MuscettolaN. and VidalT., Dynamic control of plans with temporal uncertainty. In IJCAI, 2001, pp. 494–502.
47.
MoskewiczM.W., MadiganC.F., ZhaoY., ZhangL. and MalikS., Chaff: Engineering an efficient sat solver. In DAC, 2001, pp. 530–535.
48.
MuscettolaN., NayakP.P., PellB. and WilliamsB.C., Remote agent: To boldly go where no ai system has gone before, Artificial Intelligence103(1-2) (1998), 5–47.
49.
OrlandiniA., FinziA., CestaA. and FratiniS., Tga-based controllers for flexible plan execution, In KI 2011: Advances in Artificial Intelligence, 34th Annual German Conference on AI, Berlin, Germany, October 4-7, 2011. Proceedings, 2011, pp. 233–245.
50.
PeintnerB., VenableK.B. and Yorke-SmithN., Strong controllability of disjunctive temporal problems with uncertainty. In CP, 2007, pp. 856–863.
51.
SchrijverA., Theory of Linear and Integer Programming, J Wiley & Sons, 1998.
52.
SebastianiR. and TomasiS., Optimization modulo theories with linear rational costs, ACM Transactions on Computational Logic16(2) (2015), 12:1–12:43.
53.
StergiouK. and KoubarakisM., Backtracking algorithms for disjunctions of temporal constraints, Artificial Intelligence120(1) (2000), 81–117.
54.
TsamardinosI., VidalT. and PollackM., Ctp: A new constraint-based formalism for conditional, temporal planning, Constraints8(4) (2003), 365–388.
55.
VenableK.B., VolpatoM., PeintnerB. and Yorke-SmithN., Weak and dynamic controllability of temporal problems with disjunctions and uncertainty. In ICAPS - COPLAS Workshop, 2010, pp. 50–59.
56.
VidalT., Controllability characterization and checking in contingent temporal constraint networks. In KR, 2000, pp. 559–570.
57.
VidalT., A unified dynamic approach for dealing with temporal uncertainty and conditional planning. In Proceedings of the Fifth International Conference on Artificial Intelligence Planning Systems, Breckenridge, CO, USA, April 14-17, 2000, pp. 395–402.
58.
VidalT. and FargierH., Handling contingency in temporal constraint networks: From consistency to controllabilities, Journal of Experimental and Theoretical Artificial Intelligence11(1) (1999), 23–45.
59.
VidalT. and FargierH., Handling contingency in temporal constraint networks: From consistency to controllabilities, Journal of Experimental and Theoretical Artificial Intelligence11(1) (1999), 23–45.
