Dynamic Controllability of Temporal Networks via Supervisory Control Matteo Zavatteri1 , Davide Bresolin1 , Romeo Rizzi2 and Tiziano Villa2 1 Department of Mathematics, University of Padova, Italy 2 Department of Computer Science, University of Verona, Italy Abstract Temporal networks are expressive formalisms employed in AI to model, validate, and execute temporal plans. The core parts of a temporal network are a finite set of real variables called time points and a finite set of constraints bounding the minimal and/or maximal temporal distance between pairs of time points. When uncontrollable choices are considered, a problem of interest is determining whether or not a network is dynamically controllable. That is, whether there exists a strategy that, based only on the values already assigned to uncontrollable variables, progressively assigns the controllable variables with their final values in such a way that all constraints will be met in the end. Current single-strategy synthesis approaches are mainly based on constraint propagation or controller synthesis for timed game automata. In this paper we show how to model a temporal network as a Discrete Event System (DES) so as to leverage on Supervisory Control Theory to synthesize all dynamic integer strategies within a finite time horizon. Keywords AI, formal methods, temporal network, discrete event system, supervisory control 1. Temporal Networks In the Artificial Intelligence community, temporal networks are a framework to model tem- poral plans and check the consistency of temporal constraints imposing delays and deadlines between the occurrences of events in the plan [1]. Over the years the core formalism of Sim- ple Temporal Networks [1] has been extended in several ways to cope with uncontrollable durations, (un)controllable choices, disjunctive and conditional constraints, see for example [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11]. The most expressive formalisms of temporal networks are those that simultaneously handle all such features. In this paper we stick with the restriction of CDT- NUs [5] (or CTNUDs [11]) that only consider uncontrollable choices and conditional disjunctive constraints over the same pair of time points. We address the dynamic controllability problem from a maximally-permissive point of view. That is, we synthesize all strategies that correctly assign integer values to the controllable variables (within a finite time horizon) only depending on the already observed values assigned to the uncontrollable ones. OVERLAY 2022: 4th Workshop on Artificial Intelligence and Formal Verification, Logic, Automata, and Synthesis, November 28, 2022, Udine, Italy $ matteo.zavatteri@unipd.it (M. Zavatteri); davide.bresolin@unipd.it (D. Bresolin); romeo.rizzi@univr.it (R. Rizzi); tiziano.villa@univr.it (T. Villa) Β© 2022 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0). CEUR Workshop Proceedings http://ceur-ws.org ISSN 1613-0073 CEUR Workshop Proceedings (CEUR-WS.org) Β¬π‘Ÿ, [5, 5] βˆͺ [15, 15] [10, 20] π‘Ÿ, [10, 10] βˆͺ [30, 30] π‘Š 𝐿 𝐴 [βˆ’βˆž, 30] Figure 1: The commuting example. Definition 1.1. The temporal network model of this paper is a tuple (𝒯 , ℬ, ℐ, π’ž), where 𝒯 is a finite set of controllable real variables called time points; ℬ is a finite set of uncontrollable Boolean variables called booleans; ℐ : ℬ β†’ 𝒯 is an injective function associating booleans ⋃︀ π’ž is a finite set of conditional constraints. Each constraint has the form to time points; and 𝐿 β‡’ π‘Œ ⋃︀ βˆ’ 𝑋 ∈ 𝑛𝑖=1 [ℓ𝑖 , 𝑒𝑖 ], where 𝐿 is a consistent conjunction of literals over ℬ; π‘Œ, 𝑋 are time points; 𝑛𝑖=1 [ℓ𝑖 , 𝑒𝑖 ] is a finite disjoint union of intervals [ℓ𝑖 , 𝑒𝑖 ] with ℓ𝑖 , 𝑒𝑖 ∈ Z βˆͺ {±∞} and ℓ𝑖 ≀ 𝑒𝑖 for each 𝑖 = 1, . . . , 𝑛. An example of temporal network is given in Figure 1, where 𝒯 := {π‘Š, 𝐿, 𝐴}, ℬ := {π‘Ÿ}, ℐ(π‘Ÿ) := π‘Š , and π’ž := {𝐿 βˆ’ π‘Š ∈ [10, 20], Β¬π‘Ÿ β‡’ 𝐴 βˆ’ 𝐿 ∈ [5, 5] βˆͺ [15, 15], π‘Ÿ β‡’ 𝐴 βˆ’ 𝐿 ∈ [10, 10] βˆͺ [30, 30], 𝐴 βˆ’ π‘Š ∈ [βˆ’βˆž, 30]}. Such a temporal network models a daily commuting plan to get to work. Specifically, the time point π‘Š models the commuter that checks the weather to see if it is raining or not before leaving. If so, the uncontrollable boolean π‘Ÿ associated to π‘Š will be observed to be true. False, otherwise. After that, the time points 𝐿 and 𝐴 model the commuter leaving for and arriving to work, respectively. 𝐿 occurs from 10 to 20 minutes since π‘Š (unconditional constraint 𝐿 βˆ’ π‘Š ∈ [10, 20]). When leaving, the commuter might chose to go by car or by bus. It takes 5 minutes to go by car or 15 minutes to go by bus when it is not raining (constraint Β¬π‘Ÿ β‡’ 𝐴 βˆ’ 𝐿 ∈ [5, 5] βˆͺ [15, 15]). Instead, if it is raining, these times are doubled (constraint 𝑠 β‡’ 𝐴 βˆ’ 𝐿 ∈ [10, 10] βˆͺ [30, 30]). Finally, the commuter must arrive to work within 30 minutes (unconditional constraint 𝐴 βˆ’ π‘Š ∈ [βˆ’βˆž, 30]). Clearly, the exact time at which the commuter arrives to work depends on the combination of weather and means of transport. Notice that the temporal network is dynamically controllable. A possible strategy is as follows. The commuter checks the weather at time 0 and then leaves at time 10. If it is not raining (s)he takes the bus and arrives at work at 25. If it is raining (s)he takes the car and arrives at work at 20. Clearly, there is more than one possible strategy. For example, if it is not raining and the commuter leaves no later than 15, then (s)he will be able to choose any means of transport (or car only if (s)he leaves after 15). Instead, if it is raining, regardless on when the commuter leaves (from 10 to 20) (s)he will be able to only go by car. 2. Non-Blocking Supervisory Control Supervisory control provides tools and methodologies for the automatic synthesis of controllers with respect to a set of requirements [12]. The need for control arises whenever the plant admits a subset of behaviors that are undesired and must therefore be prevented by control. Concretely, this is achieved by deploying a supervisor in feedback loop with the plant that will tell which events are allowed next. A Discrete Event System (DES) is a transition system that generates and marks a pair of formal languages built on a finite alphabet of events, where each event is 0} β‰₯ 𝑏, ¬𝑏 π‘Ÿ, Β¬π‘Ÿ 𝐿0 , . . . , 𝐿30 ,𝑑 X0 Xb0 {π‘Œπ‘‘ ∈ 𝐸 | π‘Œ ΜΈ= 𝑋, 𝑑 β‰₯ 0} W0 Wr0 𝑋 𝐴 0 ., 3 𝐴0 , . . . , 𝐴30 .. .,𝐿 ΜΈ= 30 |π‘Œ .. 0 0, W0 𝑋 𝐸 𝐿 𝑏, ¬𝑏 π‘Ÿ, Β¬π‘Ÿ 0, 𝐿1 , . . . , 𝐿30 𝑑 ∈ Wr1 𝐴 𝑋1 X1 Xb1 {π‘Œπ‘‘ ∈ 𝐸 | π‘Œ ΜΈ= 𝑋, 𝑑 β‰₯ 1} W1 W1 {π‘Œ 𝐴1 , . . . , 𝐴30 start I .. .. start I .. .. . . . . 𝑋 W3 β„Ž 𝑏, ¬𝑏 0 π‘Ÿ, Β¬π‘Ÿ Xh Xbh {π‘Œπ‘‘ ∈ 𝐸 | π‘Œ ΜΈ= 𝑋, 𝑑 β‰₯ β„Ž} W30 Wr30 𝐿30 , 𝐴30 (a) Encoding a time point 𝑋 with associated boolean 𝑏. (b) Encoding π‘Š . Not(𝐿) Β¬π‘Ÿ No X0 SA t(𝐿) L0 𝐴1 Β¬π‘Ÿ, T(𝑋 , 𝑋0 0,𝐴 0) L0 3 0 {π‘Œπ‘‘ ∈ 𝐸 | 𝑑 β‰₯ 0}, 𝐿0 , . . . , 𝐿30 start I .. S {𝑋𝑑 ∈ 𝐸 | 𝑑 β‰₯ 0} .. . start I . S 𝐴0 , . . . , 𝐴30 , Not(𝐿) A3 Β¬π‘Ÿ 0 π‘Œβ„Ž ), , (π‘Œ β„Ž 𝐿 20 Yh SAT t(𝐿) A30 𝐿 0, π‘Ÿ No Β¬ ⋃︀𝑛 (c) Encoding a constraint 𝐿 β‡’ π‘Œ βˆ’π‘‹ ∈ 𝑖=1 [ℓ𝑖 , 𝑒𝑖 ]. (d) Encoding π‘Ÿ β‡’ 𝐴 βˆ’ 𝐿 ∈ [10, 10] βˆͺ [30, 30]. Figure 2: Encoding Temporal Networks into Plant and ⋃︀ 𝑛 β€² ⋃︀𝑛Requirement Automata. Let 𝐿 β‡’ π‘Œ βˆ’ 𝑋 ∈ [β„“ 𝑖=1 𝑖 , 𝑒𝑖 ]. Then, SAT(𝑋𝑑 ) := {π‘Œπ‘‘β€² ∈ 𝐸 | 𝑑 βˆ’ 𝑑 ∈ 𝑖=1 [ℓ𝑖 , 𝑒𝑖 ]}, SAT(π‘Œπ‘‘ ) is defined simmetrically, Not(𝐿) := {𝑏𝐹 | 𝑏 ∈ 𝐿} βˆͺ {𝑏𝑇 | ¬𝑏 ∈ 𝐿}. either controllable or uncontrollable. When working with regular languages, we can model DESs by means of finite state automata. The control synthesis problem takes as input a set of automata whose concurrent behavior models the plant and another set of automata modeling requirements and it tries to build a controller that is maximally-permissive and non-blocking. Roughly speaking, the former means that all executions of the plant that are legal must not be blocked, whereas the latter means that no execution of the plant gets to a point at which it cannot β€œcomplete” (i.e., reach a marked state). In the case of finite state automata, the synthesis algorithm starts from the parallel composition of the plant automata with the requirement automata and then removes states if they disable uncontrollable events or if there is no path toward a marked state. The algorithm ends when there are no more states to remove. Eventually, either all states are removed (and thus we have no supervisor) or we get a maximally, non-blocking supervisor. 3. Dynamic Controllability via Supervisory Control Let 𝑁 := (𝒯 , ℬ, ℐ, π’ž) be a temporal network and let β„Ž be a finite time horizon. That is, a number β€œbig enough” to guarantee that if 𝑁 is dynamically controllable, then there exists some strategy that always schedules all events within β„Ž. In our example, β„Ž = 30 suffices because of the constraint 𝐴 βˆ’ π‘Š ∈ [βˆ’βˆž, 30]. Also, when all numbers in the instance are integers, the network is dynamically controllable, and we assume instantaneous reaction semantics, then there exist integer strategies. We start from a set of events 𝐸 that contains β„Ž + 1 controllable events 𝑋0 , . . . , π‘‹β„Ž for each 𝑋 ∈ 𝒯 , and two uncontrollable events 𝑏, ¬𝑏 for each 𝑏 ∈ ℬ. An event 𝑋𝑑 means that time point 𝑋 is executed at time 𝑑. An event 𝑏 (resp., ¬𝑏) means that the boolean 𝑏 has been observed true (resp., false). The first thing that we need to do is to create the plant that guarantees the followings: (1) each time point is executed exactly once, (2) if a time point 𝑋 has a boolean associated, then the boolean is assigned a truth value exactly once upon the execution of 𝑋, and (3) the time assigned to a time point is monotone non-decreasing (w.r.t. the time assigned to the already executed time points). To achieve this purpose, we create a plant automaton for each time point 𝑋 ∈ 𝒯 as shown in Figure 2a. Self loops at state I (initial state) allow the execution of other time points before the execution of 𝑋. The execution of 𝑋 at time 𝑑 ∈ {0, . . . , β„Ž} happens by taking a transition 𝑋𝑑 leading to the state Xt . If 𝑋 has also a boolean 𝑏 associated (i.e., 𝐼(𝑏) = 𝑋), then the assignment of a truth value to 𝑏 occurs by executing one of the events 𝑏, ¬𝑏 leading to the marked state Xbt . If 𝑋 does not have any boolean associated, then the automaton lacks the transitions labeled by 𝑏/¬𝑏 as well as the state Xbi , but in that case it is Xt to be marked. At marked states (Xt or Xbt ), the execution of all other time points is restricted to occur at a time β‰₯ 𝑑 (self loops at marked states). The concurrent behavior of all these automata meets (1), (2), and (3) described above. To give an example, Figure 2b provides the encoding of the time point π‘Š of Figure 1. The second thing that we need to do is to create the requirement automata. To ⋃︀ achieve this purpose, we create a requirement automaton for each constraint 𝐿 β‡’ 𝑋 βˆ’ π‘Œ ∈ 𝑛𝑖=1 [ℓ𝑖 , 𝑒𝑖 ] in π’ž. Figure 2c shows such encoding. Basically, the automaton is synchronized with the execution of 𝑋𝑑 , π‘Œπ‘‘ (for 𝑑 ∈ {0, . . . , β„Ž}) and the observation of the truth values of booleans in 𝐿. The states of the automaton handle all possible valid executions of these events. At any state Xt a set of transitions leading to S are labeled by events π‘Œπ‘‘β€² resembling the executions of π‘Œ that satisfy the constraint (event set SAT(𝑋𝑑 )). Symmetrically, for any state Yt transitions to S are labeled with events from SAT(π‘Œπ‘‘ ). Also, from any state it is always possible to reach S with a boolean event that makes 𝐿 false (event set Not(L)). Finally, at S there are self loop transitions to avoid blocking the execution once the constraint is satisfied. This way, all executions not satisfying the constraint will get stuck in some state different from S. Figure 2d shows the encoding of π‘Ÿ β‡’ 𝐴 βˆ’ 𝐿 ∈ [10, 10] βˆͺ [30, 30] of Figure 1. For example, if we could leave at 0 (state L0 ), then either it does not rain and thus the constraint does not apply leading immediately to S, or we would need to arrive at work at time 10 or 30 in order to satisfy the constraint. Finally, if we run the synthesis algorithm with these plant and requirement automata we can obtain a supervisor if and only if the temporal network is dynamically controllable. 4. Conclusions and Future Work This paper places dynamic controllability of temporal networks at the intersection of Formal Methods and Artificial Intelligence, by modeling temporal networks as discrete event systems, so we leverage 40-more years of Supervisory Control to solve dynamic controllability in a maximally-permissive way. In the case of the example in Figure 1 the supervisor has 399 states and 398 transitions (52 states and 228 transitions, if minimized). As future work we plan to explore variations of classic supervisory control (e.g., [13, 14]) in order to reduce time and space complexity of the synthesis. Acknowledgments This work was partially supported by MIUR, Project Italian Outstanding Departments, 2018-2022, by INdAM, GNCS 2022, Project Elaborazione del Linguaggio Naturale e Logica Temporale per la Formalizzazione di Testi, and by the SID/BIRD project Deep Graph Memory Networks, Department of Mathematics, University of Padova. References [1] R. Dechter, I. Meiri, J. Pearl, Temporal constraint networks, Artif. Intell. 49 (1991) 61–95. [2] T. Vidal, H. Fargier, Handling contingency in temporal constraint networks: from consis- tency to controllabilities, Jour. of Exp. & Theor. Artif. Intell. 11 (1999) 23–45. [3] P. R. Conrad, B. C. Williams, Drake: An efficient executive for temporal plans with choice, JAIR 42 (2011) 607–659. [4] I. Tsamardinos, T. Vidal, M. E. Pollack, CTP: A new constraint-based formalism for conditional, temporal planning, Constraints 8 (2003) 365–388. [5] A. Cimatti, L. Hunsberger, A. Micheli, R. Posenato, M. Roveri, Dynamic controllability via timed game automata, Acta Informatica 53 (2016) 681–722. [6] E. Karpas, S. J. Levine, P. Yu, B. C. Williams, Robust execution of plans for human-robot teams, in: ICAPS ’15, AAAI Press, 2015, pp. 342–346. [7] S. J. Levine, B. C. Williams, Concurrent plan recognition and execution for human-robot teams, in: ICAPS ’14, AAAI, 2014, pp. 490–498. [8] P. Yu, C. Fang, B. C. Williams, Resolving uncontrollable conditional temporal problems using continuous relaxations, in: ICAPS ’14, AAAI, 2014, pp. 341–349. [9] M. Zavatteri, Conditional simple temporal networks with uncertainty and decisions, in: TIME 2017, Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2017, pp. 23:1–23:17. [10] M. Zavatteri, L. ViganΓ², Conditional simple temporal networks with uncertainty and decisions, Theoretical Computer Science 797 (2019) 77–101. [11] M. Zavatteri, R. Rizzi, T. Villa, Dynamic controllability of temporal networks with instan- taneous reaction, Information Sciences (2022). doi:https://doi.org/10.1016/j.ins. 2022.08.099. [12] P. J. Ramadge, W. M. Wonham, Supervisory control of a class of discrete event processes, SIAM Journal on Control and Optimization 25 (1987) 206–230. doi:10.1137/0325013. [13] C. Ma, W. M. Wonham, Nonblocking supervisory control of state tree structures, IEEE Transactions on Automatic Control 51 (2006) 782–793. [14] L. Ouedraogo, R. Kumar, R. Malik, K. Akesson, Nonblocking and safe control of discrete- event systems modeled as extended finite automata, IEEE Transactions on Automation Science and Engineering 8 (2011) 560–569. doi:10.1109/TASE.2011.2124457.