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

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

Martin Otto

Publication date: 12 January 2000

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

zbMATH Keywords

polynomial time; bisimulation equivalence; Model checking; Finite model theory; Descriptive complexity; Modal logic; Logic in computer science; higher-dimensional \(\mu\)-calculus; Process logics; states in finite transition systems; worlds in finite Kripke structures

Mathematics Subject Classification ID

03B45: Modal logic (including the logic of norms)

03B70: Logic in computer science

68Q60: Specification and verification (program logics, model checking, etc.)

03C13: Model theory of finite structures

68Q19: Descriptive complexity and finite models

Related Items

Model-checking process equivalences, Generalising automaticity to modal properties of finite structures, The Descriptive Complexity of Parity Games, Fixed-Point Definability and Polynomial Time on Chordal Graphs and Line Graphs, Fixed-Point Definability and Polynomial Time

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