On the universal and existential fragments of the -calculus

DOI10.1016/J.TCS.2005.11.015MaRDI QIDQ2368950zbMATH OpenOpenAlexFDO

Authors Thomas A. Henzinger, Orna Kupferman, Rupak Majumdar

Publication date 28 April 2006

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

Full work available at URL https://doi.org/10.1016/j.tcs.2005.11.015

zbMATH Keywords

Model checkingSatisfiability\(\mu\)-CalculusAutomata and logic

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Automata and formal grammars in connection with logical questions (03D05) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• scientific article; zbMATH DE number 1956572
• On model checking for the \(\mu\)-calculus and its fragments
• STACS 2004
• Some model theory for the modal \(\mu\)-calculus: syntactic characterisations of semantic properties
• From linear time to branching time

Cites work

• scientific article; zbMATH DE number 3870578 (Why is no real title available?)
• scientific article; zbMATH DE number 3926220 (Why is no real title available?)
• scientific article; zbMATH DE number 3960988 (Why is no real title available?)
• scientific article; zbMATH DE number 1500523 (Why is no real title available?)
• scientific article; zbMATH DE number 784042 (Why is no real title available?)
• μ-definable sets of integers
• A linear-time model-checking algorithm for the alternation-free modal mu- calculus
• Algebraic laws for nondeterminism and concurrency
• An automata-theoretic approach to branching-time model checking
• Automata for the modal \(\mu \)-calculus and related results
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• CTL\(^*\) and ECTL\(^*\) as fragments of the modal \(\mu\)-calculus
• Deciding the winner in parity games is in \(\mathrm{UP}\cap\mathrm{co-UP}\)
• Fast and simple nested fixpoints
• Fixpoint alternation: arithmetic, transition systems, and the binary tree
• Interpolants and Symbolic Model Checking
• Number of quantifiers is better than number of tape cells
• On model checking for the \(\mu\)-calculus and its fragments
• Property preserving abstractions for the verification of concurrent systems
• Propositional dynamic logic of regular programs
• Results on the propositional \(\mu\)-calculus
• Rudiments of \(\mu\)-calculus
• Symbolic model checking: \(10^{20}\) states and beyond
• Temporal logic in specification. Altrincham, UK, April 8-10, 1987. Proceedings
• The modal mu-calculus alternation hierarchy is strict
• “Sometimes” and “not never” revisited

Cited in

(14)

• Mu-depth 3 is more than 2: A game-theoretic proof
• The \(\mu\) quantification operator in explicit mathematics with universes and iterated fixed point theories with ordinals
• On temporal logics with data variable quantifications: decidability and complexity
• Polynomial approximations for model checking
• Achieving new upper bounds for the hypergraph duality problem through logic
• Satisfiability of quantitative probabilistic CTL: rise to the challenge
• On model checking for the \(\mu\)-calculus and its fragments
• FRAGMENTS OF FREGE’SGRUNDGESETZEAND GÖDEL’S CONSTRUCTIBLE UNIVERSE
• The satisfiability problem for unbounded fragments of probabilistic CTL
• Implementing fragments of ZFC within an r.e. Universe
• Effective cut-elimination for a fragment of modal mu-calculus
• Formal Techniques for Networked and Distributed Systems - FORTE 2005
• FM 2005: Formal Methods
• scientific article; zbMATH DE number 1956572 (Why is no real title available?)

This page was built for publication: On the universal and existential fragments of the \(\mu\)-calculus

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2368950)