We introduce \CTLVPL, an extension of Computation Tree Logic in which the temporal operator Until is equipped with visibly pushdown languages that refine the possible moments on a path that can fulfill the Until property. We motivate the logic by showing how it can be used in order to specify programs which are not necessarily bound to be finite-state. We also show that \CTLVPL is deciable despite its expressive power and lack of finite model property. The proof uses L\"oding and Serre's technique that shows decidability of Propositional Dynamic Logic over Recursive Programs, which turns out to be a fragment of \CTLVPL.

Propositional Dynamic Logic (PDL) is Modal Logic over structures with accessibility relations represented by (possibly infinite) languages from a class $\mathcal{L}$ of formal languages. We consider IL, the class of indexed languages. It forms a genuine superclass of the Context-Free Languages whilst being a genuine subclass of the Context-Sensitive Languages. We present an explicit model checking procedure for PDL over IL that runs in deterministic exponential time. This matches the complexity-theoretic lower bound for this problem which is easily obtained from the exponential-time hardness of the emptiness problem for indexed languagues. This result extends the scope of language classes $\mathcal{L}$ for which model checking PDL over $\mathcal{L}$ is known to be decidable.

We consider bounded versions of undecidable problems about context-free languages which restrict the domain of words to some finite length: inclusion, intersection, universality, equivalence, and ambiguity.
These are in NP and thus solvable by a reduction to the satisfiability problem for propositional logic. We present such encodings -- fully utilizing the power of incrementat SAT solvers -- prove correctness and validate this approach with some benchmarks.

We present a model checking algorithm for HFL1, the first-order fragment of Higher-Order Fixpoint Logic. This logic is capable of expressing many interesting properties which are not regular and, hence, not expressible in the modal μ-calculus.
The algorithm avoids best-case exponential behaviour by localising the computation of functions and can be implemented symbolically using BDDs.
We show how insight into the behaviour of this procedure, when run on a fixed formula, can be used to obtain specialised algorithms for particular problems. This yields, for example, the competitive antichain algorithm for NFA universality but also a new algorithm for a string matching problem.

Higher Order Fixpoint Logic (HFL) is a hybrid of the simply typed λ-calculus and the modal μ-calculus. This makes it a highly expressive temporal logic that is capable of expressing various interesting correctness properties of programs that are not expressible in the modal μ-calculus.
This paper provides complexity results for its model checking problem. In particular we consider its fragments HFL^k,m which are formed using types of bounded order k and arity m only. We establish k-ExpTime-completeness for model checking each HFL^k,m fragment. For the upper bound we reduce the problem to the problem of solving rather large parity games of small index. As a consequence of this we obtain an ExpTime upper bound on the expression complexity of each HFL^k,m.
The lower bound is established by a reduction from the word problem for alternating (k-1)-fold exponential space bounded Turing Machines. As a corollary we obtain k-ExpTime-completeness for the data complexity of HFL^k,m already when m ≥ 4.