# A Compendium of Parameterized Problems at Higher Levels of the Polynomial Hierarchy
## 4 Knowledge Representation and Reasoning Problems
### Disjunctive Answer Set Programming
The problems that we considered are related to propositional logic, quantified Boolean satisfiability, disjunctive answer set programming, constraint satisfaction, (propositional) abductive reasoning, cliques, graph coloring, first-order logic model checking, temporal logic model checking, judgment aggregation, planning, and (alternating) Turing machines. **Author Contributions:** Conceptualization, Methodology, Formal analysis, Investigation, Project administration, R.d.H. and S.S; Resources, Funding acquisition, S.S.; Writing--original draft preparation, R.d.H., Writing--review and editing, R.d.H. and S.S.; Supervision, S.S.

**Funding:** This research was funded by the European Research Council (ERC), project 239962 (COMPLEX REASON), and the Austrian Science Fund (FWF), project P26200 (Parameterized Compilation). **Acknowledgments:** Open Access Funding by the Austrian Science Fund (FWF). **Conflicts of Interest:** The authors declare no conflict of interest. The funders had no role in the design of the study; in the collection, analyses, or interpretation of data; in the writing of the manuscript, or in the decision to publish the results. ## Appendix A

We begin by defining the syntax of the logic LTL. LTL formulas \(\varphi\) are formed according to the following grammar (here \(p\) ranges over a fixed set \(P\) of propositional variables), given by:

\(\varphi\coloneqq p\mid\
eg\varphi\mid(\varphi\land\varphi)\mid\mathrm{X} \varphi\mid\mathrm{F}\varphi\mid(\varphi\mathrm{U}\varphi)\). (Further temporal operators that are considered in the literature can be defined in terms of the operators \(\mathrm{X}\) and \(\mathrm{U}\).) The semantics of LTL is defined along paths of Kripke structures. A _Kripke structure_ is a tuple \(\mathcal{M}=(S,R,V,s_{0})\), where \(S\) is a finite set of _states_, where \(R\subseteq S\times S\) is a binary relation on the set of states called the _transition relation_, where \(V:S\to 2^{P}\) is a _valuation function_ that assigns each state to a set of propositions, and where \(s_{0}\in S\) is the _initial state_. We say that a finite sequence \(s_{1}\dots s_{\ell}\) of states \(s_{i}\in S\) is a _finite path_ in \(\mathcal{M}\) if \((s_{i},s_{i+1})\in R\) for each \(i\in[\ell-1]\). Similarly, we say that an infinite sequence \(s_{1}s_{2}s_{3}\dots\) of states \(s_{i}\in S\) is an _infinite path_ in \(\mathcal{M}\) if \((s_{i},s_{i+1})\in R\) for each \(i\geq 1\). Let \(\mathcal{M}=(S,R,V,s_{0})\) be a Kripke structure, and \(\overline{s}_{1}=s_{1}s_{2}s_{3}\dots\) be a path in \(\mathcal{M}\). Moreover, let \(\overline{s}_{i}=s_{i}s_{i+1}s_{i+2}\dots\) for each \(i\geq 2\). Truth of LTL formulas \(\varphi\) on paths \(\overline{s}\) (denoted \(\overline{s}\models\varphi\)) is defined inductively as follows:

\[ \begin{array}{ll}\overline{s}_{i}\models p&\text{if}\quad p\in V(s_{i}),\\ \overline{s}_{i}\models\varphi_{1}\wedge\varphi_{2},&\text{if}\quad\overline{ s}_{i}\models\varphi_{1}\text{and}\ \overline{s}_{i}\models\varphi_{2},\\ \overline{s}_{i}\models\
eg\varphi,&\text{if}\quad\overline{s}_{i}\
ot\models \varphi,\\ \overline{s}_{i}\models\chi\varphi,&\text{if}\quad\overline{s}_{i+1}\models \varphi,\\ \overline{s}_{i}\models\Gamma\varphi,&\text{if}\quad\text{for some}\ j\geq 0, \overline{s}_{i+j}\models\varphi,\\ \overline{s}_{i}\models\varphi_{1}\cup\varphi_{2}&\text{if}\quad\text{there is some}\ j\geq 0\text{ such that}\ \overline{s}_{i+j}\models\varphi_{2}\text{ and}\ \overline{s}_{i+j}\models\varphi\text{ for each}\ j^{ }\in[0,j-1].\end{array} \]

Then, we say that an LTL formula \(\varphi\) is true in the Kripke structure \(\mathcal{M}\) (denoted \(\mathcal{M}\models\varphi\)) if for all infinite paths \(\overline{s}\) starting in \(s_{0}\) it holds that \(\overline{s}\models\varphi\). Next, we define the syntax of the logic CTL\({}^{\star}\), which consists of two different types of formulas: state formulas and path formulas. When we refer to CTL\({}^{\star}\) formulas without specifying the type, we refer to state formulas.