# submodel_enumeration_for_ctl_is_hard__faea79dc.pdf

Submodel Enumeration for CTL Is Hard

Nicolas Fr ohlich, Arne Meier

Leibniz Universit at Hannover, Institut f ur Theoretische Informatik, Appelstrasse 9a, 30167 Hannover, Germany nicolas.froehlich@thi.uni-hannover.de, meier@thi.uni-hannover.de

Expressing system specifications using Computation Tree Logic (CTL) formulas, formalising programs using Kripke structures, and then model checking the system is an established workflow in program verification and has wide applications in AI. In this paper, we consider the task of model enumeration, which asks for a uniform stream of output systems that satisfy the given specification. We show that, given a CTL formula and a system (potentially falsified by the formula), enumerating satisfying submodels is always hard for CTL regardless of which subset of CTL operators is considered. As a silver lining on the horizon, we present fragments via restrictions on the allowed Boolean functions that still allow for fast enumeration.

Introduction In artificial intelligence, temporal logic is used as a formal language to describe and reason about the temporal behaviour of systems and processes (Barringer et al. 2000; B erard et al. 2001). One of the key applications of temporal logic in artificial intelligence is the formal specification and verification of temporal properties of software systems, such as real-time systems (Bellini, Mattonlini, and Nesi 2000; Konur 2013; Blom 1996), reactive systems (Finger, Fisher, and Owens 1993), and hybrid systems (da Silva, Kurtz, and Lin 2021). Temporal logic can be used to specify the desired behaviour of these systems and to check that systems of that kind satisfy the specified properties. This task is known as model checking (MC) and is one of the most important reasoning tasks (Schnoebelen 2002). In this context, the search for satisfying submodels is a useful approach to debugging faulty systems. One of the central temporal logics for which the model checking problem is efficiently solvable (more precisely, the problem is complete for polynomial time) is the Computation Tree Logic CTL (Clarke et al. 2018). The logic is often used in the context of program verification and, accordingly, is well suited to our study. CTL formulas enrich classical propositional logic with a variety of modal operators (next, until, global, future, release) that combine with so-called path quantifiers (existential and universal) to form CTL operators.

Copyright 2024, Association for the Advancement of Artificial Intelligence (www.aaai.org). All rights reserved.

Start Error

Close w3 Close Heat

Start Close Error

w5 Start Close

w6 Start Close Heat

Figure 1: Kripke model of the microwave oven example. While the structure containing the dashed edge (w5, w6) does not satisfy the constraint φ = AG(Error Heat AU Start), the submodel without the edge does.

Kripke structures, which model the software system of interest, are essentially labelled directed graphs that have a total transition relation (Kripke 1963). A submodel of a Kripke structure is defined with respect to all possible subsets for the state set and transition relation. Note that the subset for the transition relation must still be total, otherwise it is not a valid submodel. More formally, the problem we are interested in is defined as follows. For a Kripke structure M and a CTL formula φ, list of all submodels M of M such that M satisfies φ. Let us illustrate the idea with an example. Example 1. Consider the Kripke model M shown in Figure 1, which models the behavior of a microwave oven, a well-known example from (Clarke et al. 2018). Next, consider the constraint φ = AG(Error Heat AU Start), which says that any path starting in a world labeled with the Error proposition must first reach a world where Start holds, before Heat becomes true. With the dashed edge from w5 to w6 this constraint obviously does not hold in M. In contrast, the submodel M of M without the dashed edge satisfies φ. Thus, as an automated repair or a suggestion in debugging one might want to consider the submodels of M. Also other areas of research benefit from this kind of approach as follows. For bounded model checking (Biere et al. 2003), the size of the state space can easily become very large for complex systems. For such systems, Biere et al. suggest combining model checking with SAT solvers, which allow faster exploration of the state space. Similarly, Gupta et al. 2000 showed that similar things have been ob-

The Thirty-Eighth AAAI Conference on Artiﬁcial Intelligence (AAAI-24)

served in the context of BDD-based symbolic algorithms for image processing. While one might think that the work of Sullivan et al. 2019 is closely related to our setting, the authors work with propositional logic in the setting of the specification language Alloy, which is based on first-order logic. This is somewhat different from us, as we work with CTL. However, there is work on CTL-live model checking for first-order logic validity checking (Vakili and Day 2014), but this would be a different direction to our approach. Lauri and Dutta 2019, following an ML perspective, devise an ML framework that attempts to shrink the search space and augment the solver with some help. Recently, this topic has been investigated in the context of plain modal logic (Fr ohlich and Meier 2022). Classically, the task of enumerating models is very different from counting the number of existing models or deciding on the existence of such models. Although enumeration algorithms are usually exponential time algorithms, this does not preclude practical applications. In addition to theoretical studies, there are a number of application scenarios (Fomin and Kratsch 2010), e.g., recommender systems (Friedrich and Zanker 2011), ASP (Alviano and Dodaro 2016), or ML (Lauri and Dutta 2019). The formal foundations were originally laid by Johnson et al. (1988). Intuitively, an enumeration algorithm is deterministic and produces a uniform stream of output solutions avoiding duplicates. This solution flow is mathematically modelled by the notion of the delay, i.e., an upper bound on the elapsed time between printing two successive solutions (or the time before the first, resp., after the last, solution is returned). In 2019, Creignou et al. introduced a framework for intrinsically hard enumeration problems. Here, the polynomial hierarchy and the concept of oracle machines have been utilised to present notions that allow for proving intractability bounds for enumeration problems. The complexity class Del P describes efficient enumeration, that is, a delay that is polynomially bounded in the input length, while the complexity class Del NP contains intractable and, accordingly, difficult enumeration problems. Solutions to instances of problems in Del NP cannot efficiently be produced unless the (classical) complexity classes P and NP coincide. While the tractability of MC for CTL formulas is known to be P-complete, the complexity of enumerating satisfying submodels is still open.

Contributions. In this paper, we fill this gap and present a thorough study of the complexity of the submodel enumeration problem in the context of CTL. We will see that in general the problem is complete for the class Del NP; so it is reasonable to consider restrictions that aim for tractable enumeration cases. However, our answer in this direction is on the negative side, showing that any restriction on the CTL operator side does not allow faster enumeration algorithms (assuming P = NP). Finally, we identify some further Boolean restrictions that still allow for Del P algorithms.

Related works. The work of Schnoebelen (2002) considers the classical model checking question for temporal logics. There is a study on the complexity of fragments of the model checking problem (Krebs, Meier, and Mundhenk

2019) for CTL, but it has no direct impact on our results as the problems are situated in P (or classes within).

Organisation. At first, we introduce the necessary preliminaries on temporal logic and enumeration complexity. Then we prove our dichotomy theorem. Finally, we conclude. Due to space constraints some proof details are omitted (marked with ) and can be found in the technical report (Fr ohlich and Meier 2023).

Preliminaries In this section, we assume basic familiarity with computational complexity (Papadimitriou 2007) and will make use of the framework for hard enumeration problems (Creignou et al. 2019). Furthermore, we will define the temporal logic CTL, introduce submodels, and enumeration complexity.

Computational Tree Logic. We follow standard notation of model checking (Clarke et al. 2018). Let PROP be an infinite, countable set of propositions. The set of well-formed CTL formulas is defined with the following BNF

φ ::= | p | φ | φ φ | φ φ | PT φ | φ PT φ,

where p PROP, P {E, A}, T {X, F, G}, T {U, R}. This results in ten CTL operators, consisting of six unary operators EX, EX, EF, AF, EG, AG and four binary operators EU, AU, ER, AR. The set ALL contains all ten CTL operators. We will call , , Boolean connectors. Now, we defined a special version of Kripke models.

Definition 2. A rooted Kripke model is a tuple M = (W, R, η, r) where

W is a non-empty set of worlds (or states), R W W is a total, binary transition relation on W η: W 2PROP is an assignment function, that maps each world w to a set η(w) of propositions, and r W is the root.

Definition 3. Let M = (W, R, η, r) be a rooted Kripke model. A path π in M is an infinite sequence of worlds w1, w2, . . . such that (wi, wi+1) R for all i 1. We write π[i] to denote the ith world on the path π. For a world w W we define Π(w) := { π | π[1] = w } as the (possibly infinite) set of all infinite paths of M starting with w.

Definition 4. Let M be a rooted Kripke model and φ, ψ be CTL formulas.

M, w |= always, M, w |= p iff p η(w) with p PROP, M, w |= φ iff M, w |= φ, M, w |= φ ψ iff M, w |= φ and M, w |= ψ, M, w |= φ ψ iff M, w |= φ or M, w |= ψ, M, w |= EX φ iff π Π(w) : M, π[2] |= φ, M, w |= AX φ iff π Π(w) : M, π[2] |= φ, M, w |= EF φ iff π Π(w) k 1 : M, π[k] |= φ, M, w |= AF φ iff π Π(w) k 1 : M, π[k] |= φ, M, w |= EG φ iff π Π(w) k 1 : M, π[k] |= φ, M, w |= AG φ iff π Π(w) k 1 : M, π[k] |= φ, M, w |= φ EU ψ iff π Π(w) k 1 : M, π[k] |= ψ and i < k : M, π[i] |= φ,

The Thirty-Eighth AAAI Conference on Artiﬁcial Intelligence (AAAI-24)

M, w |= φ AU ψ iff π Π(w) k 1 : M, π[k] |= ψ and i < k : M, π[i] |= φ, M, w |= φ ER ψ iff π Π(w) k 1 : M, π[k] |= ψ or i < k : M, π[i] |= φ, M, w |= φ AR ψ iff π Π(w) k 1 : M, π[k] |= ψ or i < k : M, π[i] |= φ.

Furthermore, := is constant false. Also omit the root in M, r |= φ and just write M |= φ instead. A formula φ is then said to be satisfied by model M, if M |= φ is true. Notice an observation regarding the semantics of CTL. Observation 5. The following equivalences are true:

EX φ AX( φ), AG φ EF( φ), EG φ AF( φ), EG φ ER φ, AG φ AR φ, EF φ EU φ, AF φ AU φ, φ ER ψ ( φ AU ψ), φ AR ψ ( φ EU ψ).

Now, we formally introduce submodels of Kripke models. Given two Kripke models M = (W, R, η, r) and M = (W , R , η, r). We call M a submodel (of M), if W W, R R, and R is total. For a function f : A B we write f C, given C A, for the restriction of f to domain C. Definition 6. Let M = (W, R, η, r) be a Kripke model. M = (W , R , η W , r) is a connected submodel of M, denoted by M M, if (1.) W = , (2.) M is a submodel of M, and (3.) for all w W there exists a path π Π(r) and i 1 with π[i] = w. Clearly, worlds that violate (3.) cannot have influence on the satisfiability of CTL formulas. Yet, an enumeration algorithm printing connected submodels could trivially be extended to include non-connected submodels. Additionally we want to introduce an alternative notation for submodels, M = M D, with D = (DW , DR) for r / DW a tuple consisting of a set of worlds and a set of tuples, and W = W \ DW and R = R \ DR, for M = (W, R, η, r) and M = (W , R , η W , r). Here, D is called the set of deletions. A submodel M is satisfying φ if M |= φ. The formula φ is often omitted, if it can be deduced from the context.

Enumeration Complexity. The Turing machine, as one of the standard machine models used in complexity theory, proves to be problematic for the setting of enumeration algorithms. Its linear nature in accessing data prevents a polynomial delay when traversing exponentially large data sets, even if the actual data read is small. As a result, random access machines (RAMs) are the common machine model of choice (Strozecki 2019). Definition 7. Let Σ be a finite alphabet. An enumeration problem (EP) is a tuple E = (I, Sol), where I Σ is the set of instances, Sol: I P(Σ ) is a function that maps each instance x I to a set of solutions (of x), and there exists a polynomial p such that x I y Sol(x) we have that |y| p(|x|).

Note that sometimes one is interested in dropping the last requirement of the previous definition (Strozecki 2019).

Definition 8. Let E = (I, Sol) be an EP. An algorithm A is called an enumeration algorithm for E, if for every instance x I: A(x) terminates after a finite sequence of steps and A(x) prints exactly Sol(x) without duplicates, where A(x) denotes the computation of A on input x.

We now define the mentioned delay of an enumeration algorithm.

Definition 9. Let E = (I, Sol) be an EP, A be an enumeration algorithm for E, x I be an instance and n = | Sol(x)| the number of solutions of x. We define the

ith delay of A(x) as the elapsed time between the output of the ith and (i + 1)st solution of Sol(x), 0th delay as the precomputation time, i.e, the elapsed time before the first output of A(x), and nth delay as the postcomputation time, i.e., the elapsed time after the last output of A(x) until it terminates.

We say that A has delay f, for f : N N, if for all x I and all 0 i n the ith delay of A(x) is in O(f(|x|)).

Hard enumeration. We will shortly introduce the framework of hard enumeration by Creignou et al. (2019). The idea is to analyse EPs beyond polynomial delay by introducing a hierarchy of complexity classes similar to the polynomial-time hierarchy and reduction notions for EPs. We begin by defining two decision problems that naturally arise in the context of enumeration. Let E = (I, Sol) be an EP over the alphabet Σ. The first decision problem EXIST E asks, given an instance x, for the existence of any solutions, that is, Sol(x) is nonempty. The second decision problem is concerned with obtaining new solutions. This is the question whether, given an instance x and a partial solution y, can we extend the partial solution by a word y Σ such that yy is a solution of E, where yy denotes the concatenation of y and y .

Problem: EXTENDSOL E

Input: Instance x, partial solution y Question: Is there some y such that yy Sol(x)?

As mentioned before, we use RAMs instead of Turing machines in the context of enumeration complexity. We now want to further extend the underlying machine model, by introducing decision oracles. Classically, when analysing runtime, or in this case delay, algorithm calls to its oracle are always charged as a single step, regardless of the time the oracle takes. Our machines can write into special registers and the oracle will consider these as well as all consecutive non-empty registers as its input. A query to the oracle then occurs when the machine enters a special question state and will transition into a positive/negative state if the oracle answers yes / no . Now, start with enumeration complexity classes with oracles.

Definition 10 (Creignou et al. 2019, Def. 2). Let E be an EP, and C a decision complexity class. Then we say that E Del C if there is a RAM M with oracle L in C and a polynomial p, such that for any instance x, the RAM M enumerates Sol(x) with delay p(|x|). Moreover, the size of every oracle call is bound by p(|x|).

The Thirty-Eighth AAAI Conference on Artiﬁcial Intelligence (AAAI-24)

In this paper, the enumeration classes of interest are when C is either P, or NP; so Del P and Del NP. The following Proposition 11 as well as Proposition 15 are both simplified versions of results presented by Creignou et al. (2019). While Creignou et al. considered the full polynomial hierarchies in their proofs, here we are only concerned with the P and NP cases. Proposition 11 (Creignou et al. 2019, Prop. 6). Let E = (I, Sol) be an EP and C {P, NP}. If EXTENDSOL E C then E Del C. Proposition 11 allows for membership results for EPs using the corresponding decision problem EXTENDSOL. This technique will prove particularly useful when showing membership in Del NP, as constructing enumeration algorithms with oracles can be quite difficult. We now give the necessary definitions to show hardness results for EPs. The first definition introduces yet another machine model, which can then be used to define a reduction from one EP to another. Definition 12 (Creignou et al. 2019, Def. 6). Let E be an EP. An Enumeration Oracle Machine with an enumeration oracle E, abbreviated as EOM E, is a RAM that has a sequence of new registers Ae, Oe(0), Oe(1), . . . and a new instruction NOO (next oracle output). An EOM E is oracle-bounded, if the size of all inputs to the oracle is at most polynomial in the size of the input to the EOM E. Note that the sequence of registers as input is only necessary for EOM E that are not oracle-bounded, to allow input sizes larger than polynomial. Definition 13 (Creignou et al. 2019, Def. 7). Let E = (I, Sol) be an EP and ρ1, ρ2, . . . be the run of an EOM E and assume that the kth instruction is NOO, that is, ρk = NOO. Denote with xi the word stored in Oe(0), Oe(1), . . . at step i. Let K = {ρj {ρ1, . . . , ρk 1} | ρj = NOO and xj = xk}. Then the oracle output yk in ρk is defined as an arbitrary yk Sol(xk) such that yk has not been the oracle output in any ρj K. If no such yk exists, then the oracle output in ρk is undefined. On executing NOO in step ρk, if the oracle output yk is undefined, then register Ae contains some special symbol in step ρk+1; otherwise it contains yk. Definition 14 (D-reductions). Let E and E be EPs. We say that E reduces to E via D-reduction, E D E , if there is an oracle-bounded EOM E that enumerates E in Del P and is independent of the order in which the E -oracle enumerates its answers. The next result shows that one can use the decision problem EXIST E to show hardness of the corresponding EP E. Proposition 15 (Creignou et al. 2019, Theorem 13). Let E = (I, Sol) be an EP. If EXIST E is NP-hard, then E is Del NP-hard via D-reductions. Any following result that states Del NP-hardness for an EP will be with respect to D-reductions.

Complexity of Submodel Enumeration In this section, we will present our results regarding the submodel EP with respect to CTL formulas.

Problem: E-SUBMODELS

Input: Kripke model M, CTL formula φ Task: Output all M M such that M |= φ?

Let O be a set of CTL operators. Then E-SUBMODELS(O) is E-SUBMODELS but only for CTL formulas using operators from O (besides any of the Boolean connectors). The same applies to the next two auxiliary decision problems.

Problem: SUBMODEL

Input: Kripke model M, CTL formula φ Question: Does M M exist such that M |= φ?

Problem: EXTSUBMODEL

Input: Kripke model M, CTL formula φ, set of deletions D Question: Does an extension D D exist such that M D |= φ?

The first result will show membership in the class Del NP for the unrestricted version and will make use of the auxiliary problem EXTSUBMODEL. Theorem 16. E-SUBMODELS Del NP.

Proof. The algorithm deciding EXTSUBMODEL works as follows. For given Kripke model M = (W, R, η, r), CTL formula φ, and set of deletions D = (DW , DR), guess W W and R R. Afterwards compute D := (W DW , R DR) and accept if and only if M D |= φ. For correctness, consider that if an extension D exists such that M D |= φ, it can be computed by nondeterministically guessing the worlds and relations of that extension. Guessing W and R , computing D and checking if M D |= φ can all clearly be done in polynomial time (MC is in P for CTL). By Proposition 11 this is sufficient to prove that E-SUBMODELS Del NP.

Fragment AG. We will show hardness by relating submodels to assignments of propositional formulas, such that a submodel is satisfying, if and only if the corresponding assignment satisfies the given propositional formulas. Formally this is a reduction from the well-known NP-complete problem SAT (Cook 1971; Levin 1973). Definition 17. Let φ be a propositional formula with propositions PROP(φ) = {x1, x2, . . . , xn}. We define the Kripke model M(φ) := (W, R, η, w0) as follows:

W := {w0} {w0 i , w1 i | 1 i n},

R := {(w0, wk 1) | k {0, 1}}

{(wk i , wl i+1) | k, l {0, 1}, 1 i < n}

{(wk n, wk n) | k {0, 1}},

η(wk i ) := {xi, xk i } for 1 i n, k {0, 1}.

Figure 2 depicts such a Kripke model together with one of its submodels. Notice that the formula φ = (x1 x2) ( x1 x2) of M is satisfied given the assignment I(x1) = 1, I(x2) = 0, which the submodel M encodes by containing the worlds w1 1, w0 2 and not w0 1, w1 2. The proof of the

The Thirty-Eighth AAAI Conference on Artiﬁcial Intelligence (AAAI-24)

Figure 2: Kripke model M((x1 x2) ( x1 x2)) and a submodel M of M in bold.

following theorem uses this connection by constructing formulas that are satisfied in a submodel if and only if the corresponding assignment evaluates to 1, giving rise to a nice reduction from SAT to SUBMODEL(AG).

Theorem 18. E-SUBMODELS(AG) is Del NP-complete.

Proof. The upper bound follows from Theorem 16. By Proposition 15, showing NP-hardness of SUBMODEL(AG) implies Del NP-hardness of E-SUBMODELS(AG). Let φ be propositional formula in negation normal form. φAG is constructed by substituting xi with AG(xi x1 i ) and xi with AG(xi x0 i ) in φ for all xi PROP(φ). Note that while we have not formally introduced implication, it can simply be taken as xi x1 i . Also recall that atomic negation can always be simulated by introducing new propositions and labeling the model accordingly. We now show that φ SAT, if and only if we have that M(φ), φAG SUBMODEL(AF). Suppose φ SAT. Then there exists an assignment I such that I(φ) = 1. Using I, we construct a submodel M = (W , R , η, w0) as follows:

W := W \ {wk i | 1 i n, k = 1 I(xi)},

R := R (W W ).

That is, we remove the worlds w1 i , if I(xi) = 0 and w0 i , if I(xi) = 1. Observe that M |= (xi x1 i ), if and only if I(xi) = 1, since all worlds of M labeled with xi are also labeled with x1 i . Analogously, M |= (xi x0 i ), if and only if I(xi) = 0. Because φAG differs from φ only in its atoms, it follows that M |= φAG must be true. In the same way, if there is a submodel M such that M |= φAG, we can construct an assignment I from a path π Π(M ) such that I(φ) evaluates to 1. To conclude the reduction, observe that the construction of M(φ) and φAG can both clearly be done in polynomial time, showing SAT P m SUBMODEL(AG) and proving Del NP-hardness of E-SUBMODELS(AG).

Notice that the reduction requires AG as operator and only the binary Boolean connectors , and atomic negations, which can be removed by a simple relabeling.

Fragment AF. We will show hardness via relating submodels to deciding the problem HAMPATH (Karp 1972).

xb wb xt wt

Figure 3: (a) G with Hamiltonian path s, a, b, t. (b) Kripke model M(H) of H = G, s, t .

Definition 19. Let H = G, s, t be a HAMPATH instance, with G = (V, E) a graph and s, t V . We define the Kripke model M(H) := (W, R, η, ws) as follows:

W := {wv | v V } { ˆw}, η(wv) := {xv}, for v V, R := {(wu, wv) | (u, v) E, u = t} {(wt, ˆw), ( ˆw, ˆw)}.

The underlying graph of this model is almost G itself, except that a new world ˆw is added, which became the only successor of wt and has only one relation to itself. Figure 3 (b) depicts such a model for the graph in Figure 3 (a).

Theorem 20. E-SUBMODELS(AF) is Del NP-complete.

Proof. The upper bound follows directly from Theorem 16. Let H = G, s, t be an instance of HAMPATH with G = (V, E), s, t V and n = |V |. Further let M(H) be the Kripke model obtained from H as described in Definition 19. Now, construct the formula φ := V v V AF xv. Notice that a submodel M M satisfies φ only if it is acyclic. That is because all paths have to contain a world labeled with t, which only holds at wt. The world wt has a single outgoing edge to ˆw, where all paths end in an infinite loop, making other cycles impossible. Next, we have that paths must contain worlds where v for v V holds. This can only be achieved if all path contain the worlds wv for v V . It follows that satisfying submodels must contain each world at least once, but because of acyclicity they can also only contain each world at most once. Thus satisfying submodels must be single path from s to t containing each world exactly once, i.e., they must be Hamiltonian. Construction of M(H) and φ is in P.

Notice that the reduction requires AF as operator and the Boolean connector .

Fragment AX. We again use HAMPATH to show hardness. By concatenating the AX operator n 1 times followed by xt, we enforce that submodels must satisfy xt on all path at position n. Considering the construction of M(H) this is only possible, if paths are acyclic and contain wt only at position n. This implies that all satisfying submodels describe Hamiltonian paths from s to t.

Theorem 21. E-SUBMODELS(AX) is Del NP-complete.

Proof. The upper bound follows from Theorem 16. Suppose H is an instance of HAMPATH and n = |V |. Then let M(H) be the Kripke model as defined in Definition 19 and let φ := AXn 1 xt be a formula, where AXn 1

denotes the n 1-times concatenation of the AX operator. Furthermore, let M M(H) be a satisfying submodel.

The Thirty-Eighth AAAI Conference on Artiﬁcial Intelligence (AAAI-24)

x1 x2 x3 x4

x1 x2 x3 x4

x1 x2 x3 x4

x1 x2 x3 x4

z, x1, x2, x3, x4

x1 x2 x3 x4

y, x1, x2, x3, x4

z, x1, x2, x3, x4

x1 x2 x3 x4

y, x1, x2, x3, x4

z, x1, x2, x3, x4

x1 x2 x3 x4

y, x1, x2, x3, x4

z, x1, x2, x3, x4

x1 x2 x3 x4

y, x1, x2, x3, x4

Figure 4: Kripke model (left) of MAU(H) and (right) of MAR(H) for the graph in Figure 3 (a). The highlighted worlds and relations form a submodel that induces a Hamiltonian path for the instance H = G, s, t and satisfy (left) φ4 = (((( AU xt) AU x1) AU x2) AU x3) AU x4 and (right) φ4 = ( ( AR z) AR y) AR x1) AR z) AR y) AR x2) AR z) AR y) AR x3) AR z) AR y) AR x4.

First, show that π[n] = wt for all paths π Π(M ).

M , ws |= AXn 1 xt π Π(ws) : M , π[2] |= AXn 2 xt (Def.)

π Π(ws) σ Π(π[2]) : M , σ[2] |= AXn 3 xt π Π(ws) : M , π[3] |= AXn 3 xt (prefix)

π Π(ws) : M , π[n 1] |= AX xt (repeat)

π Π(ws) : M , π[n] |= xt By the definition of M(H), only η(wt) = xt. Thus π Π(ws) we have π[n] = wt. Note that wt cannot be on any path before that. Otherwise the path could only continue to ˆw and end there. Also, submodels again cannot have cycles, otherwise there would be a path that never reaches wt. So we can conclude that on all paths in M the first n elements must be different. With n worlds other than ˆw, this leads to satisfying submodels that are Hamiltonian paths from ws to wt, showing correctness of the reduction. The reduction can be computed in P.

Notice that the reduction merely requires AX as operator and no Boolean connectors are used.

Fragment AU. We continue to use HAMPATH. For fragment AU, we construct a new submodel MAU(H) that expands each node into a diamond construct with a world for the incoming relations and a world for the outgoing relations, as well as a number of intermediate worlds equal to the total number of vertices in G. We then construct an AU formula such that all paths in a satisfying submodel are acyclic and contain a different intermediate world at each diamond , thereby describing a Hamiltonian path of G.

Definition 22. Let G = (V, E) be a graph, s, t V , n = |V |, and H = G, s, t be an instance of HAMPATH. We define the model MAU(H) := (W, R, η, ws) as follows: W := {wv, ˆwv, wv,i | v V, 1 i n}, R := {(wv, wv,i), (wv,i, ˆwv) | v V, 1 i n}, {( ˆwu, wv) | (u, v) E, u = t} {( ˆwt, ˆwt)}, η(wv,i) := {xi} for 1 i n, η( ˆwt) := {xt}. Figure 4 depicts the submodel MAU(H) constructed from the graph in Figure 3 (a), with H = G, s, t . Theorem 23 ( ). E-SUBMODELS(AU) is Del NP-complete.

Proof. The upper bound follows directly from Theorem 16. Let H = G, s, t be an instance of HAMPATH and φn be the formula of interest here, for

φi := φi 1 AU xi if i > 0, AU xt if i = 0.

The reduction then is H 7 MAU(H), φn .

Notice that the reduction merely requires AU as operator and no Boolean connectors are used.

Fragment AR. We use a similar diamond expansion of the nodes in G, as in the proof for AU. Here an extra world is added to the construct between the middle worlds and the world for outgoing relations. In addition, the labeling is extended to make AR behave in the indented way. That is, we want to repeatedly force the left hand side of the AR operator in our constructed formula φ to only hold in specific subsequent worlds to simulate the behavior of the AX operator. The construction of φ, also requires that worlds labeled with x1, x2, . . . , xn are on the paths, similar to the proof of the AU fragment. Definition 24. Let G = (V, E) be a graph with n = |V | and H := G, s, t an instance of HAMPATH. Define MAR(H) := (W, R, η, ws) as follows (see Figure 4 for an example): W := {wv, wv, ˆwv, wv,i | v V, 1 i n},

((wv, wv,i), (wv,i, wv), ( wv, ˆwv)

{( ˆ wu, wv) | (u, v) E and u = t} {( ˆwt, ˆwt)}, η(wv,i) := {xi} for 1 i n, η( ˆwv) := {z, y}, η(wv) := {z, x1, . . . , xn}, η( wv) := {y, x1, . . . , xn}. Theorem 25 ( ). E-SUBMODELS(AR) is Del NP-complete.

Proof. The upper bound follows from Theorem 16 again. For the lower bound reduce from HAMPATH, using the Kripke model MAR(H) defined in Definition 24 and φn with

φi := ((φi 1 AR z) AR y) AR xi if i > 0, if i = 0.

Notice that the reduction merely requires AR as operator and no Boolean connectors are used.

The Thirty-Eighth AAAI Conference on Artiﬁcial Intelligence (AAAI-24)

Fragment EX, EF, EG, EU & ER. Del NP-hardness of existentially quantified operators follows immediately, when considering negation.

Corollary 26. For = O {EX, EF, EG, EU, ER} we have that E-SUBMODELS(O) is NP-complete.

Proof. Follows directly form the duality between the existential and universal path quantifiers (see Observation 5) and our results for the universally quantified cases.

Notice that for the fragments EX, EU and ER negation suffices as the only Boolean connector to archive intractability. In contrast the fragments EF and EG require all Boolean connectors. We summarise all results in one statement.

Theorem 27. Let = O ALL be a set of CTL operators. Then E-SUBMODELS(O) is Del NP-complete.

The silver lining In this section, we strive for tractability results. For this we restrict also the allowed Boolean connectors and accordingly require to extend the problem notion a bit as follows. For instance, we will write EXTSUBMODEL(EX, ER, EU) whenever we restrict the formulas to only the operators EX, ER, EU without any Boolean connectors.

Fragment EX, ER, EU & Conjunction, Disjunction. The first tractability result we present is a restriction to formulas only containing existentially quantified CTL operators and no negation. That is, we show Del P membership of E-SUBMODELS(EX, ER, EU, , ). Recall that we have EF φ = EU φ and EG φ = φ ER . The following Lemma 28 gives a straightforward way to decide EXTSUBMODEL(EX, ER, EU, , ), by only having to consider the model and partial solution.

Lemma 28. Let M M be a submodel. If M |= φ, for any {EX, EU, ER, , }-formula φ, then M |= φ.

Proof. To prove this lemma consider its contraposition, i.e., M |= φ implies M |= φ. Note that the set of paths that satisfy φ in M also exist in M. Since φ does not contain negation, the same set of paths must satisfy φ in M.

Theorem 29. E-SUBMODELS(EX, ER, EU, , ) Del P

Proof. We describe a deterministic polynomial time algorithm for EXTSUBMODEL(EX, ER, EU, , ). By Lem. 28, if, for a partial solution, we have that M D |= φ, then it cannot be extended to an actual solution. Conversely, if M D |= φ is true, then the empty extension is sufficient. Thus, any polynomial time model checking algorithm on an instance M D, φ can be used to decide EXTSUBMODEL(EX, ER, EU, , ).

Fragment AF & AG. We adapted a result presented by Krebs et al. (Krebs, Meier, and Mundhenk 2019, Lemma 10), showing that every {AF, AG}-formula can be reduced to contain at most two temporal operators.

Lemma 30 ( ). For any formula φ we have that (1.) AF AF φ AF φ (2.) AG AG φ AG φ (3.) AG AF AG φ AF AG φ (4.) AF AG AF φ AG AF φ

Theorem 31 ( ). E-SUBMODELS(AF, AG) is in Del P.

Proof. The following deterministic polynomial time algorithm decides EXTSUBMODEL(AF, AG). The input is M, φ, D , where M = (W, R, η, r) is a Kripke model, φ is a {AF, AG}-formula, and D is a set of deletions. Let M = (W , R , η, r) := M D be current submodel and φ be the shortened formula obtained from φ using Lemma 30. Notice that φ can only have one of four forms. Now, the algorithm has the following behaviour, depending on φ , where x is in PROP:

φ = AF x: if M |= EF x accept, else reject. φ = AG x: if M |= EG x accept, else reject. φ = AF AG x: if M |= EF EG x accept, else reject.

φ = AG AF x: let ˆ M = (W , R , ˆη, r) be the submodel M but with a new labeling function ˆη defined as ˆη(w ) := {xw } for all w W with x η(w ). Accept if ˆ M |= EF(xw EX EF xw ) for some w W , else reject.

Conclusion and outlook

In this paper, we have presented a complete study of the submodel enumeration problem for the temporal logic CTL with respect to restrictions on the allowed CTL operators. We have examined all CTL operator fragments and show Del NP-completeness for every possible fragment in the presence of all Boolean connectors. This paints a completely negative picture and precludes using the debugging approach as motivated in this setting. As a silver lining on the horizon, we presented fragments obtained by constraints on Boolean functions, allowing for fast Del P algorithms that could be used for bugfix recommendations. We are currently planning to extend this approach to a complete picture for all Boolean fragments and combinations with CTL operator fragments. In particular, this leads to a very large number of possible fragments: as a rough estimate, one has to consider seven Boolean fragments, which, combined with ten CTL operators, lead to an astonishing number of 7 210 = 7168 cases. As future work, it would be worthwhile to apply the framework of parameterised complexity (Downey and Fellows 1999) aiming at more efficient subcases. Another pressing issue is to investigate the motivated debugging approach using enumeration algorithms in a feasibility study. Furthermore, submodel enumeration is just one of many possible enumeration problems for CTL. Other variants worth investigating in this context include (minimal) modifications to η instead of, or in addition to, frame modifications.

Acknowledgments

The authors thank the anonymous reviewers for their valuable feedback and appreciate funding by the German Research Foundation (DFG) under the project id ME4279/3-1.

The Thirty-Eighth AAAI Conference on Artiﬁcial Intelligence (AAAI-24)

References Alviano, M.; and Dodaro, C. 2016. Answer Set Enumeration via Assumption Literals. In AI*IA, volume 10037 of Lecture Notes in Computer Science, 149 163. Springer. Barringer, H.; Fisher, M.; Gabbay, D.; and Gough, G., eds. 2000. Advances in Temporal Logic. Applied Logic Series. Springer Dordrecht. Bellini, P.; Mattonlini, R.; and Nesi, P. 2000. Temporal logics for real-time system specification. ACM Comput. Surv., 32(1): 12 42. B erard, B.; Bidoit, M.; Finkel, A.; Laroussinie, F.; Petit, A.; Petrucci, L.; Schnoebelen, P.; and Mc Kenzie, P. 2001. Systems and Software Verification, Model-Checking Techniques and Tools. Springer. Biere, A.; Cimatti, A.; Clarke, E. M.; Strichman, O.; and Zhu, Y. 2003. Bounded model checking. Adv. Comput., 58: 117 148. Blom, J. 1996. Temporal logics and real time expert systems. Computer Methods and Programs in Biomedicine, 51(1): 35 49. Improving Control of Patient Status in Critical Care: The IMPROVE Project. Clarke, E. M.; Grumberg, O.; Kroening, D.; Peled, D. A.; and Veith, H. 2018. Model checking, 2nd Edition. MIT Press. ISBN 978-0-262-03883-6. Cook, S. A. 1971. The Complexity of Theorem-Proving Procedures. In STOC, 151 158. ACM. Creignou, N.; Kr oll, M.; Pichler, R.; Skritek, S.; and Vollmer, H. 2019. A complexity theory for hard enumeration problems. Discret. Appl. Math., 268: 191 209. da Silva, R. R.; Kurtz, V.; and Lin, H. 2021. Symbolic control of hybrid systems from signal temporal logic specifications. Guidance, Navigation and Control, 1(02): 2150008. Downey, R. G.; and Fellows, M. R. 1999. Parameterized Complexity. Monographs in Computer Science. Springer. Finger, M.; Fisher, M.; and Owens, R. 1993. Metatem at work: Modelling reactive systems using executable temporal logic. In IEA/AIE-93. Gordon and Breach Publishers Edinburgh, UK. Fomin, F. V.; and Kratsch, D. 2010. Exact Exponential Algorithms. Springer Berlin, Heidelberg. Friedrich, G.; and Zanker, M. 2011. A Taxonomy for Generating Explanations in Recommender Systems. AI Mag., 32(3): 90 98. Fr ohlich, N.; and Meier, A. 2022. Submodel Enumeration of Kripke Structures in Modal Logic. In Ai ML, 391 406. College Publications. Fr ohlich, N.; and Meier, A. 2023. Submodel Enumeration for CTL Is Hard. ar Xiv:2312.09868. Gupta, A.; Yang, Z.; Ashar, P.; and Gupta, A. 2000. SATBased Image Computation with Application in Reachability Analysis. In FMCAD, volume 1954 of Lecture Notes in Computer Science, 354 371. Springer. Johnson, D. S.; Yannakakis, M.; and Papadimitriou, C. H. 1988. On generating all maximal independent sets. Information Processing Letters, 27(3): 119 123.

Karp, R. M. 1972. Reducibility Among Combinatorial Problems. In Complexity of Computer Computations, The IBM Research Symposia Series, 85 103. Plenum Press, New York. Konur, S. 2013. A survey on temporal logics for specifying and verifying real-time systems. Frontiers Comput. Sci., 7(3): 370 403. Krebs, A.; Meier, A.; and Mundhenk, M. 2019. The model checking fingerprints of CTL operators. Acta Informatica, 56(6): 487 519. Kripke, S. 1963. Semantical Considerations on Modal Logic. Acta Philosophica Fennica, 16: 83 94. Lauri, J.; and Dutta, S. 2019. Fine-Grained Search Space Classification for Hard Enumeration Variants of Subset Problems. In AAAI, 2314 2321. AAAI Press. Levin, L. 1973. Universal sorting problems. Problems of Information Transmission, 9: 265 266. Papadimitriou, C. H. 2007. Computational complexity. Academic Internet Publ. Schnoebelen, P. 2002. The Complexity of Temporal Logic Model Checking. In Advances in Modal Logic, 393 436. King s College Publications. Strozecki, Y. 2019. Enumeration Complexity. Bull. EATCS, 129. Sullivan, A.; Marinov, D.; and Khurshid, S. 2019. Solution Enumeration Abstraction: A Modeling Idiom to Enhance a Lightweight Formal Method. In ICFEM, volume 11852 of Lecture Notes in Computer Science, 336 352. Springer. Vakili, A.; and Day, N. A. 2014. Reducing CTL-live model checking to first-order logic validity checking. In Formal Methods in Computer-Aided Design, FMCAD 2014, Lausanne, Switzerland, October 21-24, 2014, 215 218. IEEE.

The Thirty-Eighth AAAI Conference on Artiﬁcial Intelligence (AAAI-24)