=Paper=
{{Paper
|id=Vol-3311/paper5
|storemode=property
|title=Dynamic Controllability of Temporal Networks via Supervisory Control
|pdfUrl=https://ceur-ws.org/Vol-3311/paper5.pdf
|volume=Vol-3311
|authors=Matteo Zavatteri,Davide Bresolin,Romeo Rizzi,Tiziano Villa
|dblpUrl=https://dblp.org/rec/conf/aiia/ZavatteriBRV22
}}
==Dynamic Controllability of Temporal Networks via Supervisory Control==
https://ceur-ws.org/Vol-3311/paper5.pdf
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.