CTL\(^*\) and ECTL\(^*\) as fragments of the modal \(\mu\)-calculus

DOI10.1016/0304-3975(94)90269-0zbMath0798.03018OpenAlexW2112535338MaRDI QIDQ1325848

Mads Dam

Publication date: 15 May 1994

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

Full work available at URL: https://doi.org/10.1016/0304-3975(94)90269-0

zbMATH Keywords

tableauxembeddingsconcurrencyBüchi automatamodal \(\mu\)-calculusextremal fixed pointsfull branching-time

Mathematics Subject Classification ID

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

Related Items

Satisfiability of \(\operatorname{ECTL}^\ast\) with constraints, On the universal and existential fragments of the \(\mu\)-calculus, The mu-calculus and Model Checking, Symbolic Model Checking in Non-Boolean Domains, The power of first-order quantification over states in branching and linear time temporal logics, Towards the hierarchical verification of reactive systems, Proving properties of dynamic process networks, Deciding the unguarded modal -calculus, Expressiveness and succinctness of a logic of robustness, A CTL* Model Checker for Petri Nets, On temporal logic versus Datalog, Maximal traces and path-based coalgebraic temporal logics, Mathematical modal logic: A view of its evolution, Games for the \(\mu\)-calculus, The monadic second-order logic of graphs. IX: Machines and their behaviours, Local model checking for infinite state spaces, The Modal μ-Calculus Caught Off Guard, On the expressive power of hybrid branching-time logics, Completeness for the modal \(\mu\)-calculus: separating the combinatorics from the dynamics, Compositional checking of satisfaction, A Multi-Core Solver for Parity Games, Model-checking games for fixpoint logics with partial order models, CTRL: extension of CTL with regular expressions and fairness operators to verify genetic regulatory networks, A linear translation from CTL\(^*\) to the first-order modal \(\mu \)-calculus, An Automata-Theoretic Approach to Infinite-State Systems, A Logical Approach to Hamiltonian Graphs, Branching-Time Model-Checking of Probabilistic Pushdown Automata, A Note on Negative Tagging for Least Fixed-Point Formulae, Model checking for hybrid branching-time logics, Temporal Logics with Reference Pointers and Computation Tree Logics, Towards physical hybrid systems, Decidability and Expressivity of Ockhamist Propositional Dynamic Logics, Modal Expressiveness of Graph Properties

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The temporal logic of branching time
• Results on the propositional \(\mu\)-calculus
• Automated analysis of mutual exclusion algorithms using CCS
• An automata theoretic decision procedure for the propositional mu- calculus
• Tableau-based model checking in the propositional mu-calculus
• Local model checking in the modal mu-calculus
• Local model checking for infinite state spaces
• Propositional dynamic logic of regular programs
• The formalization and analysis of a communications protocol
• Temporal logic can be more expressive
• Propositional dynamic logic of looping and converse is elementarily decidable
• Deciding full branching time logic
• Automatic Verification of Sequential Circuits Using Temporal Logic
• “Sometimes” and “not never” revisited
• Algebraic laws for nondeterminism and concurrency
• An exercise in proving parallel programs correct
• Star-free regular sets of ω-sequences
• Testing and generating infinite sequences by a finite automaton