=Paper= {{Paper |id=Vol-2509/paper12 |storemode=property |title=Strong Controllability of Temporal Networks with Decisions |pdfUrl=https://ceur-ws.org/Vol-2509/paper12.pdf |volume=Vol-2509 |authors=Matteo Zavatteri,Romeo Rizzi,Tiziano Villa |dblpUrl=https://dblp.org/rec/conf/aiia/ZavatteriRV19 }} ==Strong Controllability of Temporal Networks with Decisions== https://ceur-ws.org/Vol-2509/paper12.pdf
                                                   Proceedings of the
     1st Workshop on Artificial Intelligence and Formal Verification, Logics, Automata and Synthesis (OVERLAY),
                                          Rende, Italy, November 19–20, 2019




                   Strong Controllability of Temporal
                        Networks with Decisions
                         Matteo Zavatteri1 , Romeo Rizzi1 , and Tiziano Villa1
                                       1
                                           University of Verona, Italy
                     1
                         {matteo.zavatteri,romeo.rizzi,tiziano.villa}@univr.it



                                                    Abstract

               A number of extensions of simple temporal networks have been proposed over the
           last years to face several sources of uncertainty, either in isolation or simultaneously.
           This paper focuses on a hierarchy of simple temporal networks where the top-level
           formalism is that of conditional simple temporal networks with uncertainty and
           decisions (CSTNUDs), a formalism dealing with controllable and uncontrollable du-
           rations and controllable and uncontrollable conditional constraints simultaneously.
           We propose an algorithm to check strong controllability of CSTNUDs. We prove
           that strong controllability of temporal networks in this hierarchy is NP-complete if
           controllable conditional constraints are considered.


1    Introduction: A Hierarchy of Simple Temporal Networks
Temporal networks are a framework to model temporal plans and check the coherence of their temporal
constraints imposing minimal and maximal temporal distances between the occurrences of the events in the
plan. Temporal plans mainly divide in plans having everything under control and plans having something
out of control. The main components of a temporal network are time points and constraints. Time points
are real variables modeling events. Events occur when their corresponding time points are executed (i.e.,
assigned values). Constraints are linear inequalities, and more precisely difference inequalities over pairs
of events, bounding the minimal and maximal temporal distance between the respective scheduling times.
When events and constraints are fixed in advance, we deal with a standard consistency problem (STN).
Definition 1 (STN). A simple temporal network (STN) is a pair hT , Ci, where T = {X, . . . , Z} is a finite
set of time points and C is a finite set of temporal constraints Y − X ≤ k, where Y, X ∈ T and k ∈ R.
    STNs model fully controllable temporal plans. An STN is consistent if there exists a schedule t : T → R
satisfying all constraints. We write t(X) for the time at which X was executed. Consistency of STNs is in
P [11]. However, STNs cannot deal with controllable and uncontrollable conditional constraints nor with
uncontrollable durations. To bridge such gaps simple temporal networks with uncertainty (STNUs, [18])
and conditional simple temporal networks (CSTNs, [14]) were proposed.
Definition 2 (STNU). A simple temporal network with uncertainty (STNU) is a triple hT , L, Ci extending
an STN with a finite set of contingent links L each one having the form (A, x, y, C) where A, C ∈ T
and x, y ∈ R with 0 < x < y < ∞. A is the activation time point and it is under control, C is the
contingent one and it is not. Once A is executed, the execution time of C is revealed by Nature at at t(C)
guaranteeing that t(C) ∈ [t(A) + x, t(A) + y]. Contingent links do not share contingent time points.

                Copyright c 2020 for this paper by its authors.
                Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
78                                                                               M. Zavatteri, R. Rizzi, T. Villa


     STNUs model temporal plans with uncontrollable (but bounded) durations. STNUs (and all other
formalisms specifying uncontrollable parts) bring with them three main notions of controllability: weak,
strong and dynamic. Weak controllability is when, for each combination of uncontrollable parts known
in advance, there exists a way to operate on the controllable part satisfying all constraints. Strong
controllability is the opposite case and says that there exists a way to operate on the controllable part
satisfying all constraints no matter what will happen. Dynamic controllability requires the existence of a
strategy refining how we operate on the controllable part in real time depending on what is going on.
     STNUs do not specify controllable nor uncontrollable conditional constraints. To model uncontrollable
conditional constraints in isolation, the formalism of CSTNs [13] (formerly conditional temporal problem
(CTP, [17])) was proposed and subsequently extended to the formalism of CSTNUs [12, 13] in order
to augment CSTNs with uncontrollable durations. Conditionals are expressed as labels, conjunctions of
literals over a finite set of Boolean variables saying when the components labeled by them are relevant.
Initially, labels were on both time points and constraints but later it was proved that having labels on
constraints only does not limit the expressiveness of the network [3]. Temporal networks with labels on
constraints only are called streamlined. In what follows, we will only consider streamlined networks.
     Let B = {a, b, . . . , z} be a finite set of Boolean variables, a label ` = λ1 . . . λn is any finite conjunction
of literals λi over the variables in B (we omit the ∧ connective to ease reading). The empty label is denoted
by . The label universe of B, denoted by B ∗ , is the set of all possible (consistent) labels drawn from
B. For instance, if B = {a, b}, then B ∗ = { , a, b, ¬a, ¬b, ab, a¬b, ¬ab, ¬a¬b}. Two labels `1 , `2 ∈ B ∗ are
consistent if and only if their conjunction `1 `2 is satisfiable.
Definition 3 (CSTN/CSTNU). A conditional simple temporal network (CSTN) is a tuple hT , O, B, O, Ci
extending an STN with a finite set of observation time points O ⊆ T = {A?, . . . , Z?}, a finite set of
Boolean variables B, a bijection O : B → O assigning a unique Boolean variable to each observation
point (we write O−1 : O → B for the inverse), and turning C into a finite set of conditional constraints
` → Y − X ≤ k each meaning that if ` is true, then Y − X ≤ k must hold, with ` ∈ B ∗ , Y, X ∈ T and
k ∈ R. Once we execute an observation time point A?, Nature sets instantaneously the uncontrollable
truth value of the associated Boolean variable O−1 (A?) = a. A conditional simple temporal network with
uncertainty (CSTNU) is a tuple hT , O, B, O, L, Ci extending a CSTN with a finite set of contingent links.
   CSTNUs deal with controllable and uncontrollable durations and uncontrollable conditionals simul-
taneously. However, they fail to model controllable conditionals. To bridge this gap conditional simple
temporal network with uncertainty and decisions (CSTNUDs, [19, 27]) were recently proposed.
Definition 4 (CSTNUD). A conditional simple temporal network with uncertainty and decisions (CST-
NUD) is a tuple hT , O, D, B, O, L, Ci, extending a CSTNU with a finite set of decision time points
D = {D!, . . . , Z!} and in which the set of Boolean variables B is partitioned in two disjoint subsets
BD ∪ BO , representing the set of controllable and uncontrollable Boolean variables, respectively. The
mapping O is turned into a bijection O : B → O ∪ D. Once we execute a decision time point D!, we
also set instantaneously the controllable truth value of the associated Boolean variable O−1 (D!) = d. A
CSTNUD where L = ∅ is a conditional simple temporal network with decisions (CSTND, [2, 19, 27]). A
CSTNUD where O = ∅ is a simple temporal network with uncertainty and decisions (STNUD, [19, 27]).
A CSTNUD where L = O = ∅ is a simple temporal network with decisions (STND, [2, 19, 27]).
    Fig. 1a shows such a hierarchy. We graphically represent temporal networks as directed graphs whose
sets of nodes coincide with the set of time points (decision and observation time points are suffixed with !
and ?, respectively). A double red edge A ⇒ C labeled by [x, y] models a contingent links (A, x, y, C).
An edge X → Y labeled by hk, `i models a constraint ` → Y − X ≤ k. If ` = we just use k as a label.


2     Strong Controllability of CSTNUDs: Super Projections
Strong controllability of STNUs, CSTNs and CSTNUs is in P [1, 17, 18] and boils down to check the
consistency of a reduced STN. For STNUs the algorithm in [18] computes an STN by “rewriting” all
constraints involving contingent time points as constraints involving the corresponding activation only. For
CSTNs the algorithm in [17] checks consistency of the underlying STN ignoring all labels. For CSTNUs
Strong Controllability of Temporal Networks with Decisions                                                                                                                                       79



                                                                                                                                                                                [2, 4]
                     CSTNUD                                                                                                           Cm                           A                        C
                                                                                        [2, 4]                          2
                                                                          A                      C




                                                                                                                                                        h−2, ¬di
 STNUD                CSTNU          CSTND                                                                     A            −2
                                                                                                                            4                  −5                       h−3, di                 −5
                                                                         −2                          −5
    STNU                  STND           CSTN                                                              −2       −4                                                     −1     h−2, bi
                                                                                                                                      CM −5
                                                                                                                                                                   B?                       D!
                                                                                         −1                                      −1
                          STN                                             B                      D             B                              D                             h−4, d¬bi

            (a) Hierarchy of STNs.                                             (b) STNU.                        (c) StnuSP(Fig. 1b).                               (d) CSTNUD.

                                                                                         Cm                                       Cm
                    [2, 4]                                                2                                         2
            A                   C                                                                                                                                                    Cm
                                                                                                                                                                       2
                                                           A                  −2                                        −2
                                                                              4                            A
 h−2, ¬di




                                                                                                 −5                     4                  −5                              −2
                                                h−2, ¬di

                                                               h−3, di




                h−3, di             −5                                                                                                              A                      4
                                                                         −4                                        −4                                                                            −5
                                                                                                          −3
                                                                                         CM −5                                    CM −5
                     −2                                                            −2                                        −2                         −2 −4
                                                           B                                     D!                                                                                  CM −5
            B                   D!                                                                         B                               D                                    −2
                   h−4, di                                                    h−4, di                                        −4                     B                                            D
(e) CstnudSP(Fig. 1d).                                     (f) StnudSP(Fig. 1e).                           (g) StndP(Fig. 1f, d).                   (h) StndP(Fig. 1f, ¬d).

Figure 1: A hierarchy of temporal networks (a), an STNU (b), its STN super-projection (c), a CSTNUD
(d) its super-projections (e,f) and STND projections (g,h). We highlight uncontrollable parts in red.


both methods are applied one after the other: first conditionals, then contingent links [1]. In this section
we propose an alternative (simpler reduction) to check strong controllability of STNUs and then we
extend it to CSTNUDs as an initial approach. Consider the STNU in Fig. 1b. That network is strongly
controllable. A strong schedule is t(B) = 0, t(D) = 1, t(A) = 4 because if the contingent link (A, 2, 4, C)
takes its minimal duration, then C will occur at t(C) = t(A) + 2 = 6 and the constraint requiring that
C happens at least 5 since D will be satisfied. We claim that an STNU is strongly controllable iff its
super-projection is consistent. The super-projection is an STN obtained by applying the simple local
substitution reduction illustrated in Fig. 1c. The super-projection is constructed as follows. We generate
an STN whose set of time points consists of all non-contingent time points of the original STNU plus as
many pairs of time points Cm and CM as the number of contingent time points C in the original STNU.
The set of constraints is generated as follows. All original constraints not involving contingent time points
belong to this STN. For each contingent link (A, x, y, C) in the original STNU, we add four constraints
Cm − A ≤ x, A − Cm ≤ −x, CM − A ≤ y, A − CM ≤ −y in order to enforce that the corresponding Cm
and CM are executed exactly x and y after A, respectively. Each original constraint involving a contingent
time point C is duplicated in a pair of constraints: one involving Cm and the other involving CM . To give
an example, consider Fig. 1b and note that the original (A, 2, 4, C) is modeled in Fig. 1c by a triple of
time points A, Cm and CM plus Cm − A ≤ 2, A − Cm ≤ −2, CM − A ≤ 4, A − CM ≤ −4 and that the
original constraint D − C ≤ −5 is modeled by D − Cm ≤ −5 and D − CM ≤ −5. Algorithm 3 extends this
reduction in order to deal with STNUDs. To patch it for getting StnuSP(N ) we make these modifications.
The input and output become “An STNU N = hT , L, Ci” and “The STN super-projection N ∗ = hT ∗ , C ∗ i”.
Lines 8-11 remain the same without any “` →” (note that line 7 omits “ →” on constraints rewriting
contingent links). The return statement becomes hT ∗ , C ∗ i.
Theorem 1. Any STNU is strongly controllable if and only if its super-projection is consistent.
Proof. Let N = hT , L, Ci be any STNU and N ∗ = hT ∗ , C ∗ i its super-projection. Assume that N is
strongly controllable. Let TX = T ∩ T ∗ be the set of non-contingent time points and let TC = T \ TX
be the set of contingent time points N . Let t : TX 7→ R be a feasible scheduling of N (i.e., a scheduling
satisfying all constraints no matter which durations Nature chooses for contingent links). Let t∗ be the
extension of t on the new domain T ∗ (i.e., set of time points of N ∗ ) defined by the following three rules:
Rule 1: t∗ is an extension of t, thus, for each non-contingent time point X ∈ TX , t∗ (X) = t(X).
Rule 2: if X = Cm for some contingent node C ∈ TC , then t∗ (X) = t(act(C)) + L(C).
80                                                                                  M. Zavatteri, R. Rizzi, T. Villa


Rule 3: if X = CM for some contingent node C ∈ TC , then t∗ (X) = t(act(C)) + U (C).
where act(C ) is the activation time point of C (in the original STNU) and L() and U () are the lower and
upper bound vectors on the delays of contingent time points (i.e., all minimal and all maximal durations).

Fact 1 For each constraint Y − X ≤ k ∈ C where Y and X are not contingent time points, then
     Y − X ≤ k ∈ C ∗ . t(Y ) − t(X) ≤ k holds by assumption and since by Rule 1 t(Y ) = t∗ (Y ) and
     t(X) = t∗ (X), then t∗ (Y ) − t∗ (X) ≤ k holds as well.
Fact 2 For each contingent link (A, x, y, C) ∈ L, t∗ (Cm ) ≤ t(C) ≤ t∗ (CM ) because of Rules 2 and 3.
Fact 3 For each constraint X − C ≤ −k ∈ C, with C a contingent time point, t(X) − t(C) ≤ −k holds
     by assumption and t∗ (X) − t∗ (Cm ) ≤ −k and t∗ (X) − t∗ (CM ) ≤ −k hold because of Fact 2.

Fact 4 For each constraint C − X ≤ k ∈ C, with C a contingent time point, t(C) − t(X) ≤ k holds by
     assumption and t∗ (Cm ) − t∗ (X) ≤ k and t∗ (CM ) − t∗ (X) ≤ k hold because of Fact 2.

    Therefore, if t is a feasible schedule for N , then t∗ is a feasible schedule for N ∗ (Facts 1,2,3 and 4).
    Likewise, if t∗ is a feasible schedule for N ∗ , then t∗ |X is a feasible schedule for N , where t∗ |X is the
projection of t∗ over the non-contingent time points of N . Indeed, let d : TC → R be a delay vector
assigning a duration to each contingent time point C ∈ TC . For every possible delay vector d and for every
possible contingent time point C of N , it holds that t(Cm ) = t(act(C)) + L(C) ≤ t(act(C)) + d(C) ≤
t(act(C )) + L(C) = t(CM ) since L ≤ d ≤ U . That is, we only need to cope with delay vectors which are
sandwiched in-between the lower bound vector and the upper bound vector. Without loss of generality
consider a binary constraint Y − C ≤ k involving C in the original STNU N . Since t∗ (Y ) − t∗ (Cm ) ≤ k
and t∗ (Y ) − t∗ (CM ) ≤ k hold, then the original t(Y ) − t(C) ≤ k holds as well.
    Likewise, a CSTNUD is strongly controllable if and only if its STND super projection is consistent
(the proof extends that of Theorem 1 to accommodate uncontrollable conditionals as well).
    Algorithm 1 provides an approach to solve strong controllability of CSTNUDs. Algorithm 1 first
applies Algorithm 2 to get rid of uncontrollable conditional constraints, then applies Algorithm 3 to
rewrite contingent links maintaining controllable conditional constraints and finally calls a StndSolver
(see [23] for some possible algorithms) to check consistency of the STND super-projection (i.e., to find a
truth value assignment to the controllable Boolean variables such that the STN-projection according to
that assignment is consistent). Due to lack of space we only show a graphical execution of Algorithm 1
that starting on the input Fig. 1d, first removes uncontrollable conditionals getting Fig. 1e, then rewrites
contingent links getting Fig. 1f and finally returns a solution for Fig. 1h which is the only consistent
STND-projection (note the negative loop between B and D in Fig. 1g, the STND-projection according to
d). Thus, we fix ¬d as a decision and get the strong schedule t(B) = 0, t(D) = 2, t(A) = 5 for Fig. 1d.
 Algorithm 1: CstnudStrongSchedule(N )                      Algorithm 3: StnudSP(N )
     Input: A CSTNUD N = hT , O, D, B, O, L, Ci               Input: An STNUD N = hT , D, B, O, L, Ci
     Output: A strong temporal plan                           Output: The STND super-projection N ∗
                                                                ∗
 1   return StndSolver(StnudSP(CstnudSP(N )))               1 T   ← ∅, C ∗ ← ∅
                                                            2 for X ∈ T do
                                                            3     if X is non-contingent then ∆(X) = {X} ;
                                                            4     else ∆(X) = {Xm , XM } ;
 Algorithm 2: CstnudSP(N )                                  5     T ∗ ← T ∗ ∪ ∆(X)
   Input: A CSTNUD N = hT , O, D, B, O, L, Ci               6   for (A, x, y, C) ∈ L do
   Output: The STNUD super-projection N ∗                   7        C ∗ ← C ∗ ∪ {Cm − Ai ≤ x, Ai − Cm ≤ −x,
 1 for a ∈ BD do                                                       CM − Ai ≤ y, Ai − CM ≤ −y}
 2     O ∗ (a) = O(a)
                                                            8 for ` → Y − X ≤ k ∈ C do
 3 C∗ ← ∅                                                   9     for Yi ∈ ∆(Y ) do
 4 for ` → Y − X ≤ k ∈ C do                                10         for Xi ∈ ∆(X) do
 5     Let `D be ` without literals over vars in BO        11              C ∗ ← C ∗ ∪ {` → Yi − Xi ≤ k}
 6     C ∗ = C ∗ ∪ {`D → Yi − Xi ≤ k}
 7   return hT , D, BD , O ∗ , L, C ∗ i                    12   return hT ∗ , D, B, O, C ∗ i


Theorem 2. Strong controllability of STNUDs, CSTNDs and CSTNUDs is NP-complete.
Strong Controllability of Temporal Networks with Decisions                                                81


Proof. Hardness: Consequence of the fact that deciding consistency of STNDs is NP-hard and it is a
special case of deciding strong controllability of STNUDs, CSTNDs and CSTNUDs (when L = ∅, O = ∅
and L = O = ∅, respectively). Membership: Regardless of the formalism, a certificate of YES consists
of a truth value assignment s for BD and a schedule t for TX (set of non-contingent time points). To verify
it we use the reductions in Algorithm 2 to get rid of BO (if 6= ∅) and Algorithm 3 to rewrite L (if 6= ∅). If
L= 6 ∅, then for each (A, x, y, C) ∈ L, t(Cm ) = t(A) + x and t(CM ) = t(A) + y. Finally, we verify that
(s, t) is a YES certificate for the resulting STNDs. We know that this check is polynomial [2].



3     Conclusions and Future Work
We provided a simple approach to check strong controllability of CSTNUDs based on an elementary local
reduction. The resulting algorithm’s running time is upper bounded by (i) the product of a low-degree
polynomial where the magnitude of the numbers does not occur and (ii) a singly exponential term of the
form 2|D| , where D is the set of binary decisions. With small modifications the algorithm we gave can be
adapted to all formalisms in Fig. 1a. The idea is to reduce a strong controllability problem to a consistency
problem by computing super-projections. All formalisms in Fig. 1a are reducible to their super-projections
in polynomial time. Strong controllability of STNUDs, CSTNDs, CSTNUDs is NP-complete.
    As future work, we plan to deepen research on complexity of strong controllability for these and
for other classes of (temporal)-constraint networks such as those discussed (or employed) in [8, 9, 10,
20, 21, 22, 24, 25, 26, 28, 29] other than comparing with strong controllability of disjunctive formalisms
[4, 5, 6, 7, 15]. Also, a line of research started in [16] provided an approach for the optimal design of
consistent STNs. Considering the new way to compute a super-projection of an STNU, this line of research
can be extended to provide an approach for the optimal design of strongly controllable STNUs.


References
 [1] N. Bhargava and B. C. Williams. Complexity bounds for the controllability of temporal networks
     with conditions, disjunctions, and uncertainty. Artificial Intelligence, 271:1 – 17, 2019.
 [2] M. Cairo, C. Combi, C. Comin, L. Hunsberger, R. Posenato, R. Rizzi, and M. Zavatteri. Incorporating
     decision nodes into conditional simple temporal networks. In TIME 2017, volume 90 of LIPIcs, pages
     9:1–9:17. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2017.
 [3] M. Cairo, L. Hunsberger, R. Posenato, and R. Rizzi. A streamlined model of conditional simple
     temporal networks - semantics and equivalence results. In TIME 2017, volume 90 of LIPIcs, pages
     10:1–10:19. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2017.
 [4] A. Cimatti, M. Do, A. Micheli, M. Roveri, and D. E. Smith. Strong temporal planning with
     uncontrollable durations. Artificial Intelligence, 256:1–34, 2018.
 [5] A. Cimatti, L. Hunsberger, A. Micheli, R. Posenato, and M. Roveri. Sound and complete algorithms
     for checking the dynamic controllability of temporal networks with uncertainty, disjunction and
     observation. In TIME 2014, pages 27–36. IEEE CPS, 2014.
 [6] A. Cimatti, L. Hunsberger, A. Micheli, R. Posenato, and M. Roveri. Dynamic controllability via
     timed game automata. Acta Informatica, 53(6-8):681–722, 2016.
 [7] A. Cimatti, A. Micheli, and M. Roveri. Dynamic controllability of disjunctive temporal networks:
     Validation and synthesis of executable strategies. In AAAI 2013, pages 3116–3122. AAAI Press, 2016.
 [8] C. Combi, R. Posenato, L. Viganò, and M. Zavatteri. Access controlled temporal networks. In
     ICAART 2017, pages 118–131. INSTICC, ScitePress, 2017.
 [9] C. Combi, R. Posenato, L. Viganò, and M. Zavatteri. Conditional simple temporal networks with
     uncertainty and resources. Journal of Artificial Intelligence Research, 64:931–985, 2019.
82                                                                       M. Zavatteri, R. Rizzi, T. Villa


[10] C. Combi, L. Viganò, and M. Zavatteri. Security constraints in temporal role-based access-controlled
     workflows. In CODASPY 2016, pages 207–218. ACM, 2016.
[11] R. Dechter, I. Meiri, and J. Pearl. Temporal constraint networks. Artif. Intell., 49(1-3):61–95, 1991.
[12] L. Hunsberger and R. Posenato. Sound-and-complete algorithms for checking the dynamic control-
     lability of conditional simple temporal networks with uncertainty. In TIME 2018, volume 120 of
     LIPIcs, pages 14:1–14:17. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2018.
[13] L. Hunsberger, R. Posenato, and C. Combi. The Dynamic Controllability of Conditional STNs with
     Uncertainty. In PlanEx at ICAPS-2012, pages 1–8, 2012.
[14] L. Hunsberger, R. Posenato, and C. Combi. A sound-and-complete propagation-based algorithm for
     checking the dynamic consistency of conditional simple temporal networks. In TIME 2015, pages
     4–18. IEEE CPS, 2015.
[15] A. Micheli. Disjunctive temporal networks with uncertainty via SMT: recent results and directions.
     Intelligenza Artificiale, 11(2):155–178, 2017.
[16] R. Rizzi and R. Posenato. Optimal design of consistent simple temporal networks. In TIME 2013,
     pages 19–25. IEEE CPS, 2013.
[17] I. Tsamardinos, T. Vidal, and M. E. Pollack. CTP: A new constraint-based formalism for conditional,
     temporal planning. Constraints, 8(4):365–388, 2003.
[18] T. Vidal and H. Fargier. Handling contingency in temporal constraint networks: from consistency to
     controllabilities. Journal of Experimental & Theoretical Artificial Intelligence, 11(1):23–45, 1999.
[19] M. Zavatteri. Conditional simple temporal networks with uncertainty and decisions. In TIME 2017,
     volume 90 of LIPIcs, pages 23:1–23:17. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2017.
[20] M. Zavatteri. Temporal and Resource Controllability of Workflows Under Uncertainty. PhD thesis,
     University of Verona, Italy, 2018.
[21] M. Zavatteri. Temporal and resource controllability of workflows under uncertainty. In Proceedings
     of the Dissertation Award, Doctoral Consortium, and Demonstration Track at BPM 2019, volume
     2420 of CEUR Workshop Proceedings, pages 9–14. CEUR-WS.org, 2019.
[22] M. Zavatteri, C. Combi, R. Posenato, and L. Viganò. Weak, strong and dynamic controllability of
     access-controlled workflows under conditional uncertainty. In BPM 2017, pages 235–251. Springer,
     2017.
[23] M. Zavatteri, C. Combi, R. Rizzi, and L. Viganò. Hybrid sat-based consistency checking algorithms
     for simple temporal networks with decisions. In TIME 2019, volume 147, page 2:1–2:17. Schloss
     Dagstuhl-Leibniz-Zentrum fuer Informatik, 2019.
[24] M. Zavatteri, C. Combi, and L. Viganò. Resource controllability of workflows under conditional
     uncertainty. In Business Process Management Workshops, pages 68–80. Springer, 2019.
[25] M. Zavatteri, R. Rizzi, and T. Villa. Complexity of weak, strong and dynamic controllability of cncus.
     In OVERLAY 2019 (to appear). CEUR-WS.org, 2019.
[26] M. Zavatteri and L. Viganò. Constraint networks under conditional uncertainty. In ICAART 2018,
     pages 41–52. SciTePress, 2018.
[27] M. Zavatteri and L. Viganò. Conditional simple temporal networks with uncertainty and decisions.
     Theoretical Computer Science, 797:77–101, 2019.
[28] M. Zavatteri and L. Viganò. Conditional uncertainty in constraint networks. In Agents and Artificial
     Intelligence, pages 130–160. Springer, 2019.
[29] M. Zavatteri and L. Viganò. Last man standing: Static, decremental and dynamic resiliency via
     controller synthesis. Journal of Computer Security, 27(3):343–373, 2019.