# A Compendium of Parameterized Problems at Higher Levels of the Polynomial Hierarchy
## 4 Knowledge Representation and Reasoning Problems
### Disjunctive Answer Set Programming
Given the set \(P\) of atomic propositions, the syntax of CTL\({}^{\star}\) formulas is defined by the following grammar (here \(\Phi\) denotes CTL\({}^{\star}\)_state formulas_, \(\varphi\) denotes CTL\({}^{\star}\)_path formulas_, and \(p\) ranges over \(P\)), given by:

\[\Phi\mathrel{\mathop{:}}=p\mid\
eg\Phi\mid(\Phi\wedge\Phi)\mid\exists\varphi,\]

\[\varphi\mathrel{\mathop{:}}=\Phi\mid\
eg\varphi\mid(\varphi\wedge\varphi) \mid X\varphi\mid\Gamma\varphi\mid(\varphi\mathrm{U}\varphi).\]

Path formulas have the same intended meaning as LTL formulas. State formulas, in addition, allow explicit quantification over paths, which is not possible in LTL. Formally, the semantics of CTL\({}^{\star}\) formulas are defined inductively as follows. Let \(\mathcal{M}=(S,R,V,s_{0})\) be a Kripke structure, \(s\in S\) be a state in \(\mathcal{M}\) and \(\overline{s}_{1}=s_{1}s_{2}s_{3}\dots\) be a path in \(\mathcal{M}\). Again, let \(\overline{s}_{i}=s_{i}s_{i+1}s_{i+2}\dots\) for each \(i\geq 2\). The truth of CTL\({}^{\star}\) state formulas \(\Phi\) on states \(s\in S\) (denoted \(s\models\Phi\)) is defined as follows:

\[ \begin{array}{ll}s\models p&\text{if}\quad p\in V(s),\\ s\models\Phi_{1}\wedge\varphi_{2},&\text{if}\quad s\models\Phi_{1}\text{ and }s\models\Phi_{2},\\ s\models\
eg\Phi,&\text{if}\quad s\
ot\models\Phi,\\ s\models\exists\varphi,&\text{if}\quad\text{there is some path }\overline{s}\text{ in }\mathcal{M}\text{ starting in }s\text{ such that }\overline{s}\models\varphi.\\ \end{array} \]

The truth of CTL\({}^{\star}\) path formulas \(\varphi\) on paths \(\overline{s}\) (denoted \(\overline{s}\models\varphi\)) is defined as follows:

\[ \begin{array}{ll}\overline{s}_{i}\models\Phi&\text{if}\quad s_{i}\models \Phi,\\ \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 F\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 a CTL\({}^{\star}\) formula \(\Phi\) is true in the Kripke structure \(\mathcal{M}\) (denoted \(\mathcal{M}\models\Phi\)) if \(s_{0}\models\Phi\). The syntax of the logic CTL is defined similarly to the syntax of CTL\({}^{\star}\). Only the grammar for path formulas \(\varphi\) differs, namely:

\[\varphi\mathrel{\mathop{:}}=\chi\Phi\mid\Gamma\Phi\mid(\Phi\mathrm{U}\Phi).\]

In particular, this means that every CTL state formula, (CTL formula for short) is also a CTL\({}^{\star}\) formula. The semantics for CTL formulas is defined as for their CTL\({}^{\star}\) counterparts. Moreover, we say that a CTL formula \(\Phi\) is true in the Kripke structure \(\mathcal{M}\) (denoted \(\mathcal{M}\models\Phi\)) if \(s_{0}\models\Phi\). For each of the logics \(\mathcal{L}\in\{\mathrm{LTL},\mathrm{CTL},\mathrm{CTL}^{\star}\}\), we consider the fragments \(\mathcal{L}\backslash\chi\), \(\mathcal{L}\backslash\mathrm{U}\) and \(\mathcal{L}\backslash\mathrm{U}\),\(\mathcal{L}\). In the fragment \(\mathcal{L}\backslash\chi\), the X-operator is disallowed. Similarly, in the fragment \(\mathcal{L}\backslash\mathrm{U}\), the U-operator is disallowed. In the fragment \(\mathcal{L}\backslash\mathrm{U}\), neither the X-operator nor the U-operator is allowed. Next, we define how Kripke structures can be represented symbolically using propositional formulas. Let \(P=\{p_{1},\dots,p_{m}\}\) be a finite set of propositional variables.