On the expressive completeness of the propositional mu-calculus with respect to monadic second order logic

DOI10.1007/3-540-61604-7_60zbMath1514.68171OpenAlexW2113800199MaRDI QIDQ6104378

Publication date: 28 June 2023

Published in: CONCUR '96: Concurrency Theory (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-61604-7_60

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Temporal logic (03B44)

Related Items (47)

Satisfiability of $\operatorname{ECTL}^\ast$ with constraints ⋮ Unifying models ⋮ Generalising automaticity to modal properties of finite structures ⋮ The mu-calculus and Model Checking ⋮ A focus system for the alternation-free $\mu $-calculus ⋮ $\aleph_1$ and the modal $\mu$-calculus ⋮ Model theory of monadic predicate logic with the infinity quantifier ⋮ The monadic theory of finite representations of infinite words ⋮ The $\mu$-calculus alternation depth hierarchy is infinite over finite planar graphs ⋮ Bisimulation equivalence and regularity for real-time one-counter automata ⋮ Unnamed Item ⋮ Measure properties of regular sets of trees ⋮ Deciding the unguarded modal -calculus ⋮ Bisimulation invariant monadic-second order logic in the finite ⋮ Relating Paths in Transition Systems: The Fall of the Modal Mu-Calculus ⋮ Separation logics and modalities: a survey ⋮ Knowledge forgetting in propositional $\mu$-calculus ⋮ Counting on CTL$^*$: On the expressive power of monadic path logic ⋮ Sahlqvist theorem for modal fixed point logic ⋮ The finite model property for logics with the tangle modality ⋮ Bisimulation-invariant PTIME and higher-dimensional $\mu$-calculus ⋮ Model checking the full modal mu-calculus for infinite sequential processes ⋮ Refinement modal logic ⋮ Characterization, definability and separation via saturated models ⋮ The $\mu$-calculus alternation hierarchy collapses over structures with restricted connectivity ⋮ Second-order propositional modal logic: expressiveness and completeness results ⋮ Bisimulation Invariant Monadic-Second Order Logic in the Finite ⋮ Temporal Logic with Recursion. ⋮ Completeness for the modal $\mu$-calculus: separating the combinatorics from the dynamics ⋮ Spatial logic of tangled closure operators and modal mu-calculus ⋮ On expressive power of basic modal intuitionistic logic as a fragment of classical FOL ⋮ Monadic Second Order Logic And Its Fragments ⋮ Unnamed Item ⋮ Automata and fixed point logic: a coalgebraic perspective ⋮ Temporal logics with language parameters ⋮ On modal $\mu$-calculus with explicit interpolants ⋮ Modal characterisation theorems over special classes of frames ⋮ Determinizing monitors for HML with recursion ⋮ Temporal logic with recursion ⋮ Unnamed Item ⋮ The Complexity of Model-Checking Tail-Recursive Higher-Order Fixpoint Logic ⋮ Alternating Context-Free Languages and Linear Time μ-Calculus with Sequential Composition ⋮ Modality, bisimulation and interpolation in infinitary logic ⋮ Guarded fixed point logics and the monadic theory of countable trees. ⋮ An infinite hierarchy of temporal logics over branching time ⋮ Monadic second-order logic on tree-like structures ⋮ Expressiveness of concept expressions in first-order description logics

Cites Work

This page was built for publication: On the expressive completeness of the propositional mu-calculus with respect to monadic second order logic