On a Non-Context-Free Extension of PDL

Stefan Göller; Dirk Nowotka

Home/Archive/arXiv

arXiv · 0707.0562

On a Non-Context-Free Extension of PDL

Stefan Göller·Dirk Nowotka

View original source ↗Read source document ↗Export metadata ↓

Abstract

Over the last 25 years, a lot of work has been done on seeking for decidable non-regular extensions of Propositional Dynamic Logic (PDL). Only recently, an expressive extension of PDL, allowing visibly pushdown automata (VPAs) as a formalism to describe programs, was introduced and proven to have a satisfiability problem complete for deterministic double exponential time. Lately, the VPA formalism was extended to so called k-phase multi-stack visibly pushdown automata (k-MVPAs). Similarly to VPAs, it has been shown that the language of k-MVPAs have desirable effective closure properties and that the emptiness problem is decidable. On the occasion of introducing k-MVPAs, it has been asked whether the extension of PDL with k-MVPAs still leads to a decidable logic. This question is answered negatively here. We prove that already for the extension of PDL with 2-phase MVPAs with two stacks satisfiability becomes Σ_1^1-complete.

Explore related subjects

cs.LO

Keep this discovery

Explore connections, maps & timelines

BibTeX RIS

Stefan Göller, Dirk Nowotka. 2007-07-18. On a Non-Context-Free Extension of PDL. https://arxiv.org/abs/0707.0562

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

Terminal Coalgebras in Countably Many Steps

We present a collection of results that imply that an endofunctor on a category has a terminal coalgebra obtainable as a countable limit of its terminal-coalgebra chain. This holds for finitary endofunctors on locally finitely presentable categories under conditions on both the functor and the category. We adapt finiteness arguments that were originally advanced by Worrell concerning terminal coalgebras for finitary set functors. Examples include the categories of sets, posets, vector spaces, graphs, nominal sets, and presheaves on finite sets. Worrell also described, without proof, the terminal-coalgebra chain of the finite power-set functor. We provide a detailed proof following his ideas. We then turn to polynomial endofunctors on the categories of Hausdorff topological spaces and metric spaces. The Vietoris space of compact subsets yields an endofunctor $\mathscr{V}$ on the category of Hausdorff spaces. Vietoris polynomial endofunctors are built from $ \mathscr{V}$, the identity and constant functors by forming products, coproducts and compositions. Their terminal coalgebras are obtained in $ω$ steps. We then turn to the class of Hausdorff polynomial functors on the category of metric spaces, which is analogous but uses in lieu of $\mathscr{V}$ the Hausdorff functor $\mathcal{H}$. We prove they have terminal coalgebras obtained in $ω+ ω$ steps. Finally, we show that every finitary endofunctor on the category of vector spaces over a fixed field again has a terminal coalgebra obtained in $ω+ω$ steps.

cs.LO↗

arXiv2026

Tactix: Towards a Programmable Strategy Interface for Flexible SAT Solving

Modern SAT solvers combine a rich repertoire of proof rules with sophisticated strategies that determine when and how to apply them. Often, the internal implementations are tightly coupled to particular strategies, making it inconvenient to define new strategies without changing solver internals. We present Tactix, a proof-producing sequential CDCL solver that incorporates a wide range of techniques in state-of-the-art solvers with a clean separation of proof rules from solving strategies. This separation enables a public interface through which users can invoke particular techniques, observe their effects, and program a wide range of solving strategies. The default strategy of Tactix is programmable over this interface and outperforms state-of-the-art solvers on benchmarks from the 2024--2026 SAT Competitions. We also use the interface to develop novel strategies tailored to challenging benchmarks from two application domains, which led to performance gains over strong baselines. We intend Tactix to serve as an infrastructure for designing and evaluating novel solving strategies. Finally, we also present a self-study of the AI-assisted development process behind Tactix.

cs.LO↗

arXiv2026

The Lattice of Coalition Logics between MCL and CL: Coatoms and Compact Meets

For a fixed finite set $N$ of at least two agents, we investigate the lattice $L_N$ of coalition logics between minimal coalition logic (MCL) and classical coalition logic (CL), with extensions required to be structural. This lattice is order-dual to an interval in the subvariety lattice of Boolean coalition algebras. The eight basic extensions obtained by imposing seriality, independence of agents, and determinism form a Boolean cube under inclusion, but not a sublattice of $L_N$. Our main results concern coatoms and compact meets. First, finite critical coalition algebras, realized as complex algebras of finite general concurrent games, yield three infinite families of pairwise distinct coatoms containing seriality, distinguished by failures of independence, determinism, or both. An explicit splitting characterizes the unique coatom omitting seriality. Second, the meet of two basic extensions is compact if and only if the extensions are comparable. For incomparable pairs, no axiomatization of the meet can use formulas of uniformly bounded modal depth, even with infinitely many axioms. Consequently, $L_N$ and three natural principal intervals are non-coherent algebraic lattices. These results reveal lattice-theoretic phenomena beyond the inclusion order of the eight basic extensions.

cs.LO↗