arXiv Science⌕ Search
Home/Archive/arXiv

arXiv · 0706.4044

PSPACE Bounds for Rank-1 Modal Logics

Lutz Schröder·Dirk Pattinson
View original source ↗Read source document ↗Export metadata ↓

Abstract

For lack of general algorithmic methods that apply to wide classes of logics, establishing a complexity bound for a given modal logic is often a laborious task. The present work is a step towards a general theory of the complexity of modal logics. Our main result is that all rank-1 logics enjoy a shallow model property and thus are, under mild assumptions on the format of their axiomatisation, in PSPACE. This leads to a unified derivation of tight PSPACE-bounds for a number of logics including K, KD, coalition logic, graded modal logic, majority logic, and probabilistic modal logic. Our generic algorithm moreover finds tableau proofs that witness pleasant proof-theoretic properties including a weak subformula property. This generality is made possible by a coalgebraic semantics, which conveniently abstracts from the details of a given model class and thus allows covering a broad range of logics in a uniform way.

Explore related subjects

cs.LOcs.CC

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Lutz Schröder, Dirk Pattinson. 2007-06-27. PSPACE Bounds for Rank-1 Modal Logics. https://doi.org/10.1145/1462179.1462185

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

KEEP EXPLORING

Related papers

arXiv2026

Decisiveness for countable MDPs and insights for NPLCSs and POMDPs

Markov chains and Markov decision processes (MDPs) are well-established probabilistic models. While finite Markov models are well-understood, analysing their infinite counterparts remains a significant challenge. Decisiveness has proved to be an elegant property for countable Markov chains: it is general enough to be satisfied by several natural classes of countable Markov chains, and it guarantees the termination of simple qualitative and approximate quantitative model-checking algorithms. In contrast, existing work on the formal analysis of countable MDPs usually relies on ad hoc techniques tailored to specific classes. In this paper, we provide a general framework to analyse countable MDPs (with finitely many enabled actions per state) by extending the notion of decisiveness. Compared to Markov chains, MDPs exhibit an additional nondeterministic choice that can be resolved in an adversarial or cooperative way, leading to multiple natural notions of decisiveness. We show that these notions enable the approximation of supremum reachability and infimum reachability (equivalently, supremum safety) probabilities in countable MDPs using generic approximation schemes. We then instantiate our generic approach to two concrete classes of models inducing countable MDPs: nondeterministic probabilistic lossy channel systems (NPLCSs) and partially observable MDPs (POMDPs). This leads to concrete algorithms to compute approximations to supremum safety probabilities in each of these classes.

cs.LO↗
arXiv2026

Complete Dynamic Logic of Communicating Hybrid Programs

This article presents a relatively complete proof calculus for the dynamic logic of communicating hybrid programs dLCHP. Beyond hybrid systems, communicating hybrid programs not only feature mixed discrete and continuous dynamics but also their parallel interactions in parallel hybrid systems. This not only combines the subtleties of hybrid and discrete parallel systems, but parallel hybrid dynamics necessitates that all parallel subsystems synchronize in time and evolve truly simultaneously. To enable compositional reasoning nevertheless, dLCHP combines differential dynamic logic dL with mutual abstraction of subsystems by assumption-commitment (ac) reasoning. The resulting proof calculus preserves the essence of dynamic logic axiomatizations, while revealing-and being driven by-a new modal logic view onto ac-reasoning. The dLCHP proof calculus is shown to be complete relative to $Ω$-FOD, the first-order logic of differential equation properties FOD augmented with communication traces. This confirms that the calculus covers all aspects of parallel hybrid systems, because it lacks no axioms to reduce all their dynamical effects to the assertion logic. Additional axioms for encoding communication traces enable a provably correct equitranslation between $Ω$-FOD and FOD, which reveals the possibility of representational succinctness in parallel hybrid systems proofs. Transitively, this establishes a full proof-theoretical alignment of dLCHP and dL, and shows that reasoning about parallel hybrid systems is exactly as hard as reasoning about hybrid systems, continuous systems, or discrete systems.

cs.LO↗
arXiv2026

Overview and Roadmap of Team Automata

Team Automata is a formalism for interacting component-based systems proposed in 1997, whereby multiple sending and receiving actions from concurrent automata can synchronise. During the past 25+ years, team automata have been studied and applied in many different contexts, involving 25+ researchers and resulting in 25+ publications. In this paper, we first revisit the specific notion of synchronisation and composition of team automata, relating it to other relevant coordination models, such as Reo, BIP, Contract Automata, Choreography Automata, and Multi-Party Session Types. We then identify several aspects that have recently been investigated for team automata and related models. These include communication properties (which are the properties of interest?), realisability (how to decompose a global model into local components?), tool support (what has been automatised or implemented?), and variability (can a family of concrete product (automata) models be captured concisely?). Our presentation of these aspects provides a snapshot of the most recent trends in research on team automata, and delineates a roadmap for future research, both for team automata and for related formalisms.

cs.LO↗