Proceedings of the 1st Workshop on Artificial Intelligence and Formal Verification, Logics, Automata and Synthesis (OVERLAY), Rende, Italy, November 19–20, 2019 Complexity of Weak, Strong and Dynamic Controllability of CNCUs Matteo Zavatteri1 , Romeo Rizzi1 , and Tiziano Villa1 1 University of Verona, Italy 1 {matteo.zavatteri,romeo.rizzi,tiziano.villa}@univr.it Abstract A Constraint Network Under Conditional Uncertainty (CNCU) is a formalism able to model a constraint satisfaction problem (CSP) where variables and con- straints are labeled by a conjunction of Boolean variables, or booleans, whose truth value assignments are out of control and only discovered upon the execution of their related observation points (special kind of variables). At the start of the execution of the CNCU (i.e., the online assignment of values to variables), we do not know yet which constraints and variables will be taken into consideration nor in which order. Weak controllability implies the existence of a strategy to execute a CNCU whenever the whole uncontrollable part is known before executing. Strong controllability is the opposite case and implies the existence of a strategy to execute a CNCU always the same way no matter how the uncontrollable part will behave. Dynamic controllability implies the existence of an adaptive strategy to execute the CNCU taking into account how the uncontrollable part is behaving. In this paper we classify the computational complexity of weak, strong and dynamic con- trollability of CNCUs. We prove that weak controllability is Πp2 -complete, strong controllability is NP-complete and dynamic controllability is PSPACE-complete. 1 Constraint Networks Under Conditional Uncertainty Constraint networks (CNs, [5]) are a framework to model constraint satisfaction problems (CSPs) and check the coherence of their relational constraints saying which combinations of values assigned to the variables are permitted. The main components of a constraint network are variables, domains and constraints and whenever all these components are under control we simply deal with a consistency problem asking us to find an assignment of values to all variables satisfying all constraints. Definition 1. A Constraint Network (CN) is a tuple hX , V, D, Ci, where X = {X1 , . . . , Xn } is a finite set of variables, V = {v1 , . . . , vm } is a finite set of discrete values, D ⊆ X × V is the domain relation (we write D(X) = {v | (X, v) ∈ D} to shorten the domain of X) and C = {RS1 , . . . , RSk } is a finite set of relational constraints. Each RSi is defined over a scope of variables Si ⊆ X such that if Si = {Xi1 , . . . , Xij }, then RSi ⊆ D(Xi1 ) × · · · × D(Xij ). A CN is consistent iff every variable X ∈ X can be assigned a value v ∈ D(X) such that all constraints in C are satisfied. Deciding consistency of CNs is NP-complete [5]. Copyright c 2020 for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0). 84 M. Zavatteri, R. Rizzi, T. Villa (6=, e) 6= 6= {v1 , v2 , v3 } {v1 , v2 , v3 } [ ] [e] X1 X2 E? X3 E? X3 E? X3 {v1 , v2 } E? {v1 , v2 } {v1 , v2 } {v1 , v2 } {v1 , v2 } {v1 , v2 } {v1 , v2 } 6= (R, ) 6= 6= R R [ ] [ ] R 6= X1 X2 X1 X2 X1 X2 X3 X4 X1 X2 {v1 , v2 } {v2 } {v1 , v2 } {v2 } {v1 , v2 } {v2 } {v1 , v2 , v3 } {v1 , v2 , v3 } (6=, e) (=, ¬e) 6= {v1 , v2 } = {v2 } 6= ∩ = (a) CN. (b) CNCU. (c) Proj. onto e. (d) Proj. onto ¬e. (e) Super proj. Figure 1: CN, CNCU and projections. R = {(v1 , v1 ), (v1 , v2 ), (v2 , v2 )}. Red parts are uncontrollable. Fig. 1a shows an example of consistent CN, where a possible solution is X1 = v1 , X2 = v3 , X3 = v3 and X4 = v2 . Classic CNs do not address uncontrollable components. Indeed, when some component is out of control, satisfiability is, in general, not enough, and in such a case, we deal with a controllability problem. To address uncontrollable conditional constraints, CNCUs were proposed in [14, 16] as an extension of CNs to handle resource allocation problems under uncertainty in the context of business process management (BPM). 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 booleans 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. A label `1 contains a label `2 (written `2 ⊆ `1 ) if and only if all literals in `2 appear in `1 too (i.e., if `1 is more specific than `2 ). Definition 2. A Constraint Network Under Conditional Uncertainty (CNCU) is a tuple hX , V, D, O, B, O, L, ≺, Ci, where: • X , V, D are the same as those given for CNs in Definition 1. • O ⊆ X = {A?, B?, . . . } is a set of observation points. • B = {a, b, . . . , z} is a finite set of booleans. O : B → O is a bijection assigning a unique observation point A? to each boolean a. When A? is assigned a value v ∈ D(A?), the truth value of a is set by Nature and no longer changes. • L : X → B ∗ is a mapping assigning a label ` to each variable X. • ≺ is a partial order on X . We write X1 ≺ X2 to express that X1 must be executed before X2 . • C is a finite set of conditional constraints of the form ` ⇒ RS , where ` ∈ B ∗ and RS is a classic relational constraint. Definition 3. A CNCU is well defined iff all labels are consistent and: 1. For each X ∈ X , if a literal a (or ¬a) ∈ L(X), then L(O(a)) ⊆ L(X) and O(a) ≺ X. V 2. For each constraint (RS , `) ∈ C, X∈S L(X) ⊆ ` and if a literal a (or ¬a) ∈ L(X), then L(O(a)) ⊆ `. 3. L(X1 ) ∧ L(X2 ) is consistent whenever X1 ≺ X2 . Regarding the notions of well-definedness (initially proposed for conditional temporal networks in [6] and then adapted to CNCUs in [14, 16]), (1) and the second part of (2) say that any label must contain the labels of the observation points associated to each proposition embedded in each contained literal (label honesty). The first part of (2) says that a label on a constraint must be at least as expressive as any label in the scope of the relation (label coherence). Condition (3) says that we cannot impose an order between two variables not taking part together in any execution. Complexity of Weak, Strong and Dynamic Controllability of CNCUs 85 Fig. 1b shows the graphical representation of a well-defined CNCU specifying 4 variables E?, X1 , X2 , X3 , where D(E?) = D(X1 ) = D(X3 ) = {v1 , v2 } and D(X2 ) = {v2 }. E? is an observation point whose associated boolean is e. Order edges (directed thick edges) say that E? must be executed (i.e., assigned a value) before X2 and X3 , whereas X1 must be executed before X2 . E?, X1 and X2 are always executed as L(E?) = L(X1 ) = L(X2 ) = (empty label imposes no conditions). X3 is executed if and only if e is assigned true as L(X3 ) = e, ignored otherwise. The CNCU specifies four constraints represented as labels on constraints edges (undirected thin edges). For example, (R, ) between E? and X1 (see caption) represents a relation ⇒ R saying that if E? = v1 , then X1 can be any value, whereas if E? = v2 , then X1 = v2 . The constraint holds for any execution as its label is . Instead, (6=, e) between E? and X3 says that if e is assigned true, then E? 6= X3 . Likewise, if e is assigned true, then X1 6= X2 , else X1 = X2 . A scenario s : B → {⊥, >} is a total assignment of truth values to the booleans in B. A scenario satisfies a label ` (in symbols s |= `) if ` valuates true under the interpretation given by s. Variables and constraints are relevant for a scenario s if their labels are satisfied by s. A projection of a CNCU onto a scenario s is a classic constraint network (plus the partial order between the survived variables) in which we keep only variables and constraints relevant for s. For instance, Fig. 1c and Fig. 1d show the 2 possible projections of Fig. 1b onto s(e) = > and s(e) = ⊥. Definition 4. A CNCU N is weakly controllable if every projection P of N satisfies two properties: (1) there exists a total extension ≺T of ≺, and (2) P is a consistent CN. Fig. 1b is weakly controllable. If s(e) = > (Fig. 1c), then E? = v1 , X1 = v1 , X2 = v2 and X3 = v2 (in this order). If s(e) = ⊥ (Fig. 1d), then E? = v1 , X1 = v2 and X2 = v2 (again, in this order). Definition 5. A CNCU N is strongly controllable if there exists a total extension ≺T of ≺ and an assignment α of values to the variables such that α satisfies all constraints in each scenario. An initial approach to strong controllability is that of computing a super-projection obtained by wiping out labels on variables and constraints [14, 16]. Fig. 1b is not strongly controllable. The super projection (Fig. 1e) contains (6=, e) and (=, ¬e) between X1 and X2 (of the original CNCU) whose intersection yields an empty relation. For weak and strong controllability we just make sure that a total order for X exists (that’s why we grayed it in Fig. 1c, Fig. 1d and Fig. 1e). Instead, dynamic controllability of CNCUs is a matter of order. Definition 6. A CNCU is dynamically controllable if there exists a dynamic strategy operating in real time that guarantees that we end up with all constraints in C evaluating to true. A strategy is called dynamic if the variable executed next and the value assigned to it only depend on the partial scenario revealed up to that point. Note that despite variables specify labels, assigning values to those that have become irrelevant is superfluous but not wrong (we can always ignore those assignments at the end of the execution). Fig. 1b is uncontrollable if X1 is executed before E?. Indeed, if X1 = v1 and E? = v1 and then s(e) = ⊥ (or X1 = v2 and E? = v2 and then s(e) = >), there is not valid value for X2 satisfying (=, ¬e) or (6=, e), respectively. Instead, the CNCU is dynamically controllable if E? is executed first. A possible execution strategy is: E? = v1 (always). If s(e) = >, then X1 = v1 , X2 = v2 and X3 = v2 , whereas if s(e) = ⊥ then X1 = v2 and X2 = v2 (we omit irrelevant variables). 2 Complexity of Weak, Strong and Dynamic Controllability Let α : X → V be an assignment of values to the variables. Given a CNCU N = hX , V, D, O, B, O, L, ≺, Ci and a pair (s, α), where s is a scenario and α an assignment, we say that (s, α) |= N iff (1) for each X ∈ X , α(X) ∈ D(X) and (2) for each ` ⇒ R{Xi1 ,...,Xin } ∈ C, if s |= `, then (α(Xi1 ), . . . , α(Xin )) ∈ R{Xi1 ,...,Xin } . Theorem 1. Strong controllability of CNCUs is NP-complete. Proof. Hardness: Consequence of the fact that deciding consistency of CNs is NP-hard and it is a special case of deciding strong controllability of CNCUs (when the set of observations is empty). Membership: 86 M. Zavatteri, R. Rizzi, T. Villa ({(1)}, y1 ) ({(0)}, ¬y1 ) ({(1)}, y2 ) ({(0)}, ¬y2 ) [ ] [ ] [ ] [ ] [ ] [ ] [ ] X1 By1 ? Y1 X2 By2 ? Y2 X3 {0, 1} {0, 1} {0, 1} {0, 1} {0, 1} {0, 1} {0, 1} Figure 2: Example of QBF2CNCU(∃x1 ∀y1 ∃x2 ∀y2 ∃x3 (x1 ∨ ¬y2 ∨ ¬y1 ) ∧ (x2 ∨ ¬x3 ∨ y1 )). The first clause is encoded as ⇒ R1 where R1 ≡ D(X1 ) × D(Y2 ) × D(Y1 ) \ {(0, 1, 1)} and the second one as ⇒ R2 where R2 ≡ D(X2 ) × D(X3 ) × D(Y1 ) \ {(0, 1, 0)}. Being ternary, ⇒ R1 and ⇒ R2 are not shown. as a certificate of YES consider a pair comprising a total extension ≺T of ≺ and a total assignment α to the variables that obeys all constraints regardless of the truth assignment s to the booleans. Notice that any single constraint ` ⇒ R is satisfied by α for each possible s if and only if α satisfies R, and since we have a finite number of constraints to check, the overall check is polynomial. To prove that deciding weak controllability of CNCUs is Πp2 -hard and deciding dynamic controllability of CNCUs is PSPACE-hard, we first describe a polynomial time algorithm that, given in input any quantified boolean formula (QBF) Φ with n variables and m clauses, and at most 3 literals in each clause constructs a CNCU NΦ with at most 2 × n variables with binary domain, exactly n booleans, and at most (2 × n) + m constraints each one of arity of at most 3. With this, the description length of NΦ is at most polynomial in m and n. The Πp2 -hardness and PSPACE-hardness results are then obtained in Lemma 1 and Lemma 2 where it is shown that particular instances of Φ are satisfiable iff NΦ is weakly controllable and dynamically controllable, respectively. Fig. 2 provides an example of use of QBF2CNCU (Algorithm 1). Algorithm 1: QBF2CNCU(Φ) Input: A a quantified boolean formula Φ ≡ Q1 x1 , . . . , Qn xn ϕ where Qi ∈ {∃, ∀} (1 ≤ i ≤ n) and ϕ ≡ C1 ∧ · · · ∧ Cm is a 3-CNF specifying m clauses over the variables x1 , . . . , xn Output: A CNCU NΦ = hX , V, D, O, B, O, L, ≺, Ci. 1 For each “∃x” in Φ, we add a variable X to X such that D(X) = {0, 1} and L(X) = . 2 For each “∀y” in Φ we add a boolean y to B, an observation point By ? to X and to O and a variable Y to X such that O(y) = By ?, D(By ?) = D(Y ) = {0, 1} and L(By ?) = L(Y ) = . We impose that By ? executes before Y (i.e., By ≺ Y ). We add two conditional relational constraints y ⇒ RY> and ¬y ⇒ RY⊥ to C, where RY> = {(1)} and RY⊥ = {(0)}. 3 We add n − 1 precedence constraints to connect each previous discussed “gadget” encoding a quantified variable of Φ to the next one according to the order in which these variables appear in the quantified part of Φ. 4 For each clause Ci we add a relational constraint ⇒ RSi such that the scope Si contains the three variables embedded in the literals appearing in Ci , whereas the set of tuples is the cross product of the domains of such variables minus the unique tuple falsifying the clause (each of these relations has exactly 23 − 1 tuples). Lemma 1. Weak controllability of CNCUs is Πp2 -complete. Proof. Hardness: Let Φ ≡ ∀y1 , . . . ∀yn , ∃x1 , . . . ∃xm ϕ a QBF. Solving such an instance of QBF is known to be Πp2 -complete. We claim that Φ is satisfiable if and only if QBF2CNCU(Φ) is weakly controllable. Let t a truth value assignment for Φ. Let s(yi ) = t(yi ) for each yi in Φ. Let α(Xi ) = t(xi ) for each xi in Φ, α(Yi ) = s(yi ) for each yi in Φ and α(BYi ) = {0} for each yi in Φ. Let ≺T = Y1 ≺ · · · ≺ Yn ≺ X1 ≺ · · · ≺ Xm . If t |= Φ, then (s, α) |= NΦ . We know that is is true because the constraints of NΦ translate the clauses of Φ. Let now consider the opposite direction. Consider any scenario s and any assignment α. Let ≺T as before. Let t(yi ) = s(yi ) = α(Yi ) for each Yi in NΦ and let t(xi ) = α(Xi ) for each Xi in NΦ . If (s, α) |= NΦ , then t |= Φ. Again, this is true as the clauses of Φ resemble the relational constraints of N . Membership: A CNCU is weekly controllable iff: for each scenario s there exists a total extension ≺s of ≺ and an assignment αs to the variables satisfying all pertinent constrains. Since the assignment s to the Complexity of Weak, Strong and Dynamic Controllability of CNCUs 87 booleans can be seen as a binary string of length |B|, and the total extension ≺s and the assignment αs have a compact encoding, then week controllability of CNCUs is in Πp2 by its very definition. Lemma 2. Dynamic controllability of CNCUs is PSPACE-hard. Proof. Let Φ ≡ ∃x1 , . . . ∀y1 , ∃x2 , ∀y2 . . . ∃xn ∀yn ϕ a QBF. Solving such an instance of QBF is known to be PSPACE-complete. We claim that Φ is satisfiable iff QBF2CNCU(Φ) is dynamically controllable. The construction t, α, s and ≺T are similar to that discussed in Lemma 1. Theorem 2. Dynamic controllability of CNCUs is PSPACE-complete. Proof. Hardness: Proved in Lemma 2. Membership: Algorithm 2 is a polynomial space algorithm to decide dynamic controllability of any CNCU. An AND/OR search tree whose depth size is bounded by a polynomial in the number of variables. Algorithm 2: CncuDC(N ) Input: A CNCU N = hX , V, D, O, B, O, L, ≺, Ci Output: Yes, if N is dynamically controllable. No otherwise. 1 CncuDC (N ) 2 Let s, α be an empty scenario and assignment. 3 return Explore(N , X , s, α) 4 Explore (N , X , s, α) 5 if X = ∅ then return (s, α) |= N . leaf check 6 for X ∈ X do . pick a variable 7 UP(X) ← {Y | Y ≺ X, Y ∈ X } . unexecuted predecessors 8 if UP(X) = ∅ then 9 for v ∈ D(X) do . look for a value to assign to X 10 α0 ← α ∪ {α0 (X) ← v} . extend current plan 11 if X ∈ O then . case 1 12 Let x be the boolean associated to X 13 s0 ← s ∪ {s(x) ← >} . extend scenario (positive case) 14 s00 ← s ∪ {s(x) ← ⊥} . extend scenario (negative case) 15 if Explore(N , X \ {X}, s0 , α0 ) ∧ Explore(N , X \ {X}, s00 , α0 ) then 16 return Yes 17 if X 6∈ O ∧ Explore(N , X \ {X}, s, α0 ) then return Yes . case 2 18 return No . “no strategy” from subtree 3 Conclusions and Future Work We classified the computational complexity of weak, strong and dynamic controllability of CNCUs. Weak controllability is Πp2 -complete, strong controllability is NP-complete, whereas dynamic controllability is PSPACE-complete. As future work, we plan to compare with complexity results for other classes of (temporal)-constraint networks such as those discussed (or employed) in [1, 2, 3, 4, 7, 8, 9, 10, 11, 12, 13, 15, 14, 16, 17]. References [1] M. Cairo, C. Combi, C. Comin, L. Hunsberger, R. Posenato, R. Rizzi, and M. Zavatteri. Incorporating decision nodes into conditional simple temporal networks. In 24th International Symposium on Temporal Representation and Reasoning, TIME 2017, volume 90 of LIPIcs, pages 9:1–9:17. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2017. 88 M. Zavatteri, R. Rizzi, T. Villa [2] C. Combi, R. Posenato, L. Viganò, and M. Zavatteri. Access controlled temporal networks. In 9th International Conference on Agents and Artificial Intelligence, ICAART 2017, pages 118–131. INSTICC, ScitePress, 2017. [3] 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. [4] C. Combi, L. Viganò, and M. Zavatteri. Security constraints in temporal role-based access-controlled workflows. In 6th ACM Conference on Data and Application Security and Privacy, CODASPY ’16, pages 207–218. ACM, 2016. [5] R. Dechter. Constraint processing. Elsevier, 2003. [6] 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 22nd International Symposium on Temporal Representation and Reasoning, TIME 2015, pages 4–18. IEEE CPS, 2015. [7] M. Zavatteri. Conditional simple temporal networks with uncertainty and decisions. In 24th International Symposium on Temporal Representation and Reasoning, TIME 2017, volume 90 of LIPIcs, pages 23:1–23:17. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2017. [8] M. Zavatteri. Temporal and Resource Controllability of Workflows Under Uncertainty. PhD thesis, University of Verona, Italy, 2018. [9] 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. [10] M. Zavatteri, C. Combi, R. Posenato, and L. Viganò. Weak, strong and dynamic controllability of access-controlled workflows under conditional uncertainty. In Business Process Management - 15th International Conference, BPM 2017, pages 235–251. Springer, 2017. [11] M. Zavatteri, C. Combi, R. Rizzi, and L. Viganò. Hybrid sat-based consistency checking algorithms for simple temporal networks with decisions. In 26th International Symposium on Temporal Representation and Reasoning, TIME 2019, volume 147, page 2:1–2:17. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2019. [12] M. Zavatteri, C. Combi, and L. Viganò. Resource controllability of workflows under conditional uncertainty. In Business Process Management Workshops, pages 68–80. Springer, 2019. [13] M. Zavatteri, R. Rizzi, and T. Villa. Strong controllability of temporal networks with decisions. In OVERLAY 2019 (to appear). CEUR-WS.org, 2019. [14] M. Zavatteri and L. Viganò. Constraint networks under conditional uncertainty. In 10th International Conference on Agents and Artificial Intelligence — Volume 2, ICAART 2018, pages 41–52. SciTePress, 2018. [15] M. Zavatteri and L. Viganò. Conditional simple temporal networks with uncertainty and decisions. Theoretical Computer Science, 797:77–101, 2019. [16] M. Zavatteri and L. Viganò. Conditional uncertainty in constraint networks. In Agents and Artificial Intelligence, pages 130–160. Springer, 2019. [17] 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.