One-counter automata (OCA) are pushdown automata which operate only on a unary stack alphabet. We study the computational complexity of model checking computation tree logic (${\mathsf{CTL}}$) on ...transition systems induced by OCA. A ${\mathsf{PSPACE}}$ upper bound is inherited from the modal $\mu$-calculus for this problem proved by Serre. First, we analyze the periodic behavior of ${\mathsf{CTL}}$ over OCA and derive a model checking algorithm whose running time is exponential only in the number of control locations and a syntactic notion of the formula that we call leftward until depth. In particular, model checking fixed OCA against ${\mathsf{CTL}}$ formulas with a fixed leftward until depth is in $\mathsf{P}$. This generalizes a corresponding recent result of Goller, Mayr, and To for the expression complexity of ${\mathsf{CTL}}$'s fragment ${\mathsf{EF}}$. Second, we prove that already over some fixed OCA, ${\mathsf{CTL}}$ model checking is ${\mathsf{PSPACE}}$-hard, i.e., expression complexity is ${\mathsf{PSPACE}}$-hard. Third, we show that there already exists a fixed ${\mathsf{CTL}}$ formula for which model checking of OCA is ${\mathsf{PSPACE}}$-hard, i.e., data complexity is ${\mathsf{PSPACE}}$-hard as well. To obtain the latter result, we employ two results from complexity theory: (i) Converting a natural number in Chinese remainder presentation into binary presentation is in logspace-uniform ${\mathsf{NC}}^1$ and (ii) ${\mathsf{PSPACE}}$ is $\mathsf{AC}^0$-serializable. We demonstrate that our approach can be used to obtain further results. We show that model checking ${\mathsf{CTL}}$'s fragment ${\mathsf{EF}}$ over OCA is hard for $\mathsf{P}^{\mathsf{NP}}$, thus establishing a matching lower bound. Moreover, we show that the following problem is hard for ${\mathsf{PSPACE}}$: Given a one-counter Markov decision process, a set of target states with counter value zero each, and an initial state, to decide whether the probability that the initial state will eventually reach one of the target states is arbitrarily close to $1$. This improves a recently proved lower bound for every level of the boolean hierarchy shown by Brazdil et al. Finally, we prove that there is a fixed ${\mathsf{CTL}}$ formula for which model checking 2-clock timed automata is ${\mathsf{PSPACE}}$-hard, generalizing a ${\mathsf{PSPACE}}$-hardness result for the combined complexity by Laroussinie, Markey, and Schnoebelen. PUBLICATION ABSTRACT
We study the satisfiability problem of the logic K
2
= K × K—the two-dimensional variant of unimodal logic, where models are restricted to asynchronous products of two Kripke frames. Gabbay and ...Shehtman proved in 1998 that this problem is decidable in a tower of exponentials. So far, the best-known lower bound is NEXP-hardness shown by Marx and Mikulás in 2001.
Our first main result closes this complexity gap. We show that satisfiability in K
2
is nonelementary. More precisely, we prove that it is
k
-NEXP-complete, where
k
is the switching depth (the minimal modal rank among the two dimensions) of the input formula, hereby solving a conjecture of Marx and Mikulás. Using our lower-bound technique also allows us to derive nonelementary lower bounds for the two-dimensional modal logics K4 × K and S5
2
× K, for which only elementary lower bounds were previously known.
Moreover, we apply our technique to prove nonelementary lower bounds for the sizes of Feferman-Vaught decompositions with respect to product for any decomposable logic that is at least as expressive as unimodal K, generalizing a recent result by the first author and Lin. For the three-variable fragment FO
3
of first-order logic, we obtain the following two immediate corollaries: the size of Feferman-Vaught decompositions with respect to disjoint sum are inherently nonelementary, and equivalent formulas in Gaifman normal form are inherently nonelementary.
Our second main result consists in providing effective elementary (more precisely, doubly exponential) upper bounds for the two-variable fragment FO
2
of first-order logic both for Feferman-Vaught decompositions and for equivalent formulas in Gaifman normal form.
We study satisfiability and infinite-state model checking in ICPDL, which extends Propositional Dynamic Logic (PDL) with intersection and converse operators on programs. The two main results of this ...paper are that (i) satisfiability is in 2EXPTIME, thus 2EXPTIME-complete by an existing lower bound, and (ii) infinite-state model checking of basic process algebras and pushdown systems is also 2EXPTIME-complete. Both upper bounds are obtained by polynomial time computable reductions to ω-regular tree satisfiability in ICPDL, a reasoning problem that we introduce specifically for this purpose. This problem is then reduced to the emptiness problem for alternating two-way automata on infinite trees. Our approach to (i) also provides a shorter and more elegant proof of Danecki's difficult result that satisfiability in IPDL is in 2EXPTIME. We prove the lower bound(s) for infinite-state model checking using an encoding of alternating Turing machines.
Hierarchical graph definitions allow a modular description of graphs using modules for the specification of repeated substructures. Beside this modularity, hierarchical graph definitions also allow ...to specify graphs of exponential size using polynomial size descriptions. In many cases, this succinctness increases the computational complexity of decision problems. In this paper, the model-checking problem for the modal
μ
-calculus and (monadic) least fixpoint logic on hierarchically defined input graphs is investigated. In order to analyze the modal
μ
-calculus, parity games on hierarchically defined input graphs are investigated. Precise upper and lower complexity bounds are derived. A restriction on hierarchical graph definitions that leads to more efficient model-checking algorithms is presented.
We show that the satisfiability problem for the two-dimensional extension KxK of unimodal K is nonelementary, hereby confirming a conjecture of Marx and Mikulas from 2001. Our lower bound technique ...allows us to derive further lower bounds for many-dimensional modal logics for which only elementary lower bounds were previously known. We also derive nonelementary lower bounds on the sizes of Feferman-Vaught decompositions w.r.t. product for any decomposable logic that is at least as expressive as unimodal K. Finally, we study the sizes of Feferman-Vaught decompositions and formulas in Gaifman normal form for fixed-variable fragments of first-order logic.
We study the complexity of satisfiability in the expressive extension ICPDL of PDL (Propositional Dynamic Logic), which admits intersection and converse as program operations. Our main result is ...containment in 2EXP, which improves the previously known non-elementary upper bound and implies 2EXP-completeness due to an existing lower bound for PDL with intersection. The proof proceeds by showing that every satisfiable ICPDL formula has a model of tree-width at most two and then giving a reduction to the (non)-emptiness problem for alternating two-way automata on infinite trees. In this way, we also reprove in an elegant way Danecki’s difficult result that satisfiability for PDL with intersection is in 2EXP.
Vorgestellt werden das Konzept und die bisherige praktische Umsetzung des Projekts "Familienpflege für psychisch kranke Jugendliche". Erstmals wurden fünf Jugendliche in Pflegefamilien vermittelt, ...die durch ein professionelles Familienpflegeteam weiterbetreut werden und durch die vorbehandelnde Abteilung für Kinder-und Jugendpsychiatrie und Psychotherapie ambulant weiterbehandelt werden. (ZPID).
PDF
