Bisimulation-invariant PTIME and higher-dimensional \(\mu\)-calculus

DOI10.1016/S0304-3975(98)00314-4zbMath0930.03030OpenAlexW1981996395MaRDI QIDQ1960425

Martin Otto

Publication date: 12 January 2000

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/s0304-3975(98)00314-4

zbMATH Keywords

polynomial timebisimulation equivalenceModel checkingFinite model theoryDescriptive complexityModal logicLogic in computer sciencehigher-dimensional \(\mu\)-calculusProcess logicsstates in finite transition systemsworlds in finite Kripke structures

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Model theory of finite structures (03C13) Descriptive complexity and finite models (68Q19)

Related Items

Generalising automaticity to modal properties of finite structures ⋮ Unnamed Item ⋮ Unnamed Item ⋮ The Descriptive Complexity of Parity Games ⋮ Model-checking process equivalences ⋮ Fixed-Point Definability and Polynomial Time on Chordal Graphs and Line Graphs ⋮ Fixed-Point Definability and Polynomial Time ⋮ The Complexity of Model-Checking Tail-Recursive Higher-Order Fixpoint Logic

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Results on the propositional \(\mu\)-calculus
• Fixed-point extensions of first-order logic
• A finite model theorem for the propositional \(\mu\)-calculus
• An automata theoretic decision procedure for the propositional mu- calculus
• A calculus of communicating systems
• Deciding bisimilarity is P-complete
• Modal correspondence for models
• Bounded variable logics: Two, three, and more
• Canonization for two variables and puzzles on the square
• Structure and complexity of relational queries
• Infinitary logic and inductive definability over finite structures
• Remarks on Berger's paper on the domino problem
• Recurring Dominoes: Making the Highly Undecidable Highly Understandable
• Relational queries computable in polynomial time
• Interpolation, preservation, and pebble games
• The expressive power of fixed-point logic with counting
• Undecidability results on two-variable logics
• The undecidability of the domino problem
• On the expressive completeness of the propositional mu-calculus with respect to monadic second order logic