=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==
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.