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 ifnite 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.
In the Artificial Intelligence community, temporal networks are a framework to model
temporal plans and check the consistency of temporal constraints imposing delays and deadlines
between the occurrences of events in the plan [
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 to time points; and is a finite set of conditional constraints. Each constraint has the form ⇒ − ∈ ⋃︀=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 := { − ∈ [
Supervisory control provides tools and methodologies for the automatic synthesis of controllers
with respect to a set of requirements [
X0 ...
Yh
SANTo(t(ℎ),)
S (a) Encoding a time point with associated boolean .
Not() { ∈ | ̸= , ≥ 0} { ∈ | ̸= , ≥ 1} { ∈ | ̸= , ≥ ℎ} start ... 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.
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 sufices 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 diferent from S. Figure 2d shows the encoding of
⇒ − ∈ [
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.
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., [