On the universal and existential fragments of the -calculus

DOI10.1016/J.TCS.2005.11.015zbMATH Open1088.68106OpenAlexW1491931107MaRDI QIDQ2368950FDOQ2368950

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

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

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)

Cites Work

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

Cited In (14)

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

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)