# A Compendium of Parameterized Problems at Higher Levels of the Polynomial Hierarchy
## 4 Knowledge Representation and Reasoning Problems
### Disjunctive Answer Set Programming
This task is of importance in the area of software and hardware verification (see, e.g., [55; 56]). We consider three different temporal logics: _linear-time temporal logic_ (LTL), _computation tree logic_ (CTL), and CTL\({}^{*}\), which is a superset of both LTL and CTL. Truth of formulas \(\varphi\) in these logics is defined over Kripke structures \(\mathcal{M}\)--we write \(\mathcal{M}\models\varphi\) if \(\varphi\) is true in \(\mathcal{M}\). We consider Kripke structures that are represented symbolically using propositional formulas. Moreover, for each of the logics \(\mathcal{L}\in\{\mathrm{LTL},\mathrm{CTL},\mathrm{CTL}^{*}\}\), we consider various restricted fragments \(\mathcal{L}\backslash\mathsf{X}\), \(\mathcal{L}\backslash\mathsf{U}\) and \(\mathcal{L}\backslash\mathsf{U}\),\(\mathsf{X}\), where certain operators are disallowed. For a full description of the syntax and semantics of these logics, how Kripke structures can be represented symbolically and the restricted fragments that we consider, we refer to Appendix A. In general, the problem of deciding whether a given temporal logic formula \(\varphi\) is true in a given symbolically represented Kripke structure \(\mathcal{M}\) is PSPACE-hard, even when restricted to formulas \(\varphi\) of constant size [7; 36]. We consider a variant of this problem where the Kripke structures have limited recurrence diameter. The _recurrence diameter_\(rd(\mathcal{M})\) of a Kripke structure \(\mathcal{M}\) is the length of the longest simple (non-repeating) path in \(\mathcal{M}\). [style=]

Symbolic-\(\mathrm{MC}^{*}[\mathcal{L}]\)

_Input:_ A symbolically represented Kripke structure \(\mathcal{M}\), \(rd(\mathcal{M})\) in unary, and an \(\mathcal{L}\) formula \(\varphi\). _Parameter:_\(|\varphi|\). _Question:_\(\mathcal{M}\models\varphi\)? **Complexity:**

\(\bullet\) para-co-NP-complete if \(\mathcal{L}=\mathrm{LTL}\backslash\mathsf{U}\),\(\mathsf{X}\)[7; 36],

\(\bullet\)\(\mathrm{PH}[\mathrm{level}]\text{-}\mathrm{complete}\) if \(\mathcal{L}\in\{\mathrm{CTL},\mathrm{CTL}\backslash\mathsf{X},\mathrm{ CTL}\backslash\mathsf{U},\mathrm{CTL}\backslash\mathsf{U},\mathsf{X},\mathrm{CTL}^{*}\backslash\mathsf{U},\mathsf{X}\}\)[7; 36], and

\(\bullet\) para-PSPACE-complete if \(\mathcal{L}\in\{\mathrm{CTL}^{*},\mathrm{CTL}^{*}\backslash\mathsf{X}, \mathrm{CTL}^{*}\backslash\mathsf{U}\}\)[7; 36]. ### Judgment Aggregation

The following problems are related to judgment aggregation, in the domain of computational social choice. Judgment aggregation studies procedures that combine individuals' opinions into a collective group opinion. An _agenda_ is a finite nonempty set \(\Phi=\{\varphi_{1},\ldots,\varphi_{n},\
eg\varphi_{1},\ldots,\
eg\varphi_{n}\}\) of formulas that is closed under complementation. A _judgment set_\(J\) for an agenda \(\Phi\) is a subset \(J\subseteq\Phi\). We call a judgment set _complete_ if \(\varphi_{i}\in J\) or \(\
eg\varphi_{i}\in J\) for all formulas \(\varphi_{i}\), and we call it _consistent_ if there exists an assignment that makes all formulas in \(J\) true. Let \(\mathcal{J}(\Phi)\) denote the set of all complete and consistent subsets of \(\Phi\). We call a sequence \(\boldsymbol{J}\in\mathcal{J}(\Phi)^{n}\) of complete and consistent subsets a _profile_. A (resolute) _judgment aggregation procedure_ for the agenda \(\Phi\) and \(n\) individuals is a function \(F:\mathcal{J}(\Phi)^{n}\to\mathcal{P}(\Phi\backslash\emptyset)\backslash\emptyset\) that returns for each profile \(\boldsymbol{J}\) a non-empty set \(F(\boldsymbol{J})\) of non-empty judgment sets. An example is the _majority rule_\(F^{\mathrm{maj}}\), where \(F^{\mathrm{maj}}(\boldsymbol{J})=\{J^{*}\}\) and where \(\varphi\in J^{*}\) if and only if \(\varphi\) occurs in the majority of judgment sets in \(\boldsymbol{J}\), for each \(\varphi\in\Phi\). We call \(F\)_complete_ and _consistent_, if each \(J^{*}\in F(\boldsymbol{J})\) is complete and consistent, respectively, for every \(\boldsymbol{J}\in\mathcal{J}(\Phi)^{n}\).