Results on the propositional \(\mu\)-calculus
From MaRDI portal
Publication:801893
DOI10.1016/0304-3975(82)90125-6zbMath0553.03007OpenAlexW2015640848WikidataQ59448065 ScholiaQ59448065MaRDI QIDQ801893
Publication date: 1983
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/0304-3975(82)90125-6
completenesspropositional modal logicdecision procedurefixed point inductionPDLpropositional mu-calculussmall model property
Modal logic (including the logic of norms) (03B45) Abstract data types; algebraic specification (68Q65)
Related Items
Abstraction in Fixpoint Logic ⋮ Differential Game Logic ⋮ Bidirectional Runtime Enforcement of First-Order Branching-Time Properties ⋮ μ-definable sets of integers ⋮ European Summer Meeting of the Association for Symbolic Logic ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Data flow analysis as model checking ⋮ A CTL* Model Checker for Petri Nets ⋮ Partial-order reduction in the weak modal mu-calculus ⋮ The tail-recursive fragment of timed recursive CTL ⋮ On first-order runtime enforcement of branching-time properties ⋮ Revising system specifications in temporal logic ⋮ Fixed point logics and definable topological properties ⋮ On the expressive completeness of the propositional mu-calculus with respect to monadic second order logic ⋮ A survey on satisfiability checking for the \(\mu \)-calculus through tree automata ⋮ Focus-style proofs for the two-way alternation-free \(\mu \)-calculus ⋮ Symbolic control for stochastic systems via finite parity games ⋮ Fixed point logics and definable topological properties ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ A Note on the Completeness of Kozen's Axiomatisation of the Propositional μ-Calculus ⋮ Coinduction in Flow: The Later Modality in Fibrations ⋮ Axiomatising extended computation tree logic ⋮ Temporal Logic with Recursion. ⋮ The modal mu-calculus alternation hierarchy is strict ⋮ Sharp Congruences Adequate with Temporal Logics Combining Weak and Strong Modalities ⋮ Partial-Order Reduction for Parity Games with an Application on Parameterised Boolean Equation Systems ⋮ Propositional Dynamic Logic with Program Quantifiers ⋮ A Multi-Core Solver for Parity Games ⋮ A Rewriting-Based Model Checker for the Linear Temporal Logic of Rewriting ⋮ An operational domain-theoretic treatment of recursive types ⋮ A Formal Language for Electronic Contracts ⋮ On model checking for the \(\mu\)-calculus and its fragments ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Meanings of Model Checking ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Temporal logics with language parameters ⋮ Three notes on the complexity of model checking fixpoint logic with chop ⋮ Unnamed Item ⋮ Free \(\mu\)-lattices ⋮ Types and trace effects of higher order programs ⋮ From Monadic Logic to PSL ⋮ Modelling and analysing variability in product families: model checking of modal transition systems with variability constraints ⋮ More Precise Partition Abstractions ⋮ Model Checking for Action Abstraction ⋮ Solving Parity Games in Big Steps ⋮ Undirected Graphs of Entanglement 2 ⋮ Journeys in non-classical computation I: A grand challenge for computing research ⋮ Consistently-detecting monitors ⋮ Divergence and unique solution of equations ⋮ k-Bounded Petri Net Synthesis from Modal Transition Systems. ⋮ Unnamed Item ⋮ Monitoring for Silent Actions ⋮ Characteristic formulae for fixed-point semantics: a general framework ⋮ Inference Systems with Corules for Combined Safety and Liveness Properties of Binary Session Types ⋮ Property preserving abstractions under parallel composition ⋮ Specification and Verification of Multi-Agent Systems ⋮ Unifying models ⋮ Unnamed Item ⋮ A Formal Theory of Justifications ⋮ Symmetric Strategy Improvement ⋮ Introduction to Model Checking ⋮ Transfer of Model Checking to Industrial Practice ⋮ The mu-calculus and Model Checking ⋮ Symbolic Model Checking in Non-Boolean Domains ⋮ Process Algebra and Model Checking ⋮ A Decision Procedure for (Co)datatypes in SMT Solvers ⋮ Changing a Semantics: Opportunism or Courage? ⋮ $\aleph_1$ and the modal $\mu$-calculus ⋮ Compositional Reasoning for Multi-modal Logics ⋮ Program Schemata Technique to Solve Propositional Program Logics Revised ⋮ ON MODAL μ-CALCULUS OVER FINITE GRAPHS WITH SMALL COMPONENTS OR SMALL TREE WIDTH ⋮ From Parity and Payoff Games to Linear Programming ⋮ Measure Properties of Game Tree Languages ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Deciding the unguarded modal -calculus ⋮ A Mechanized Theory of Regular Trees in Dependent Type Theory ⋮ Reasoning About Strategies ⋮ Enriched μ–Calculus Pushdown Module Checking ⋮ A denotational semantics for equilibrium logic ⋮ Knowledge forgetting in propositional \(\mu\)-calculus ⋮ Efficiently Deciding μ-Calculus with Converse over Finite Trees ⋮ Model Checking Contracts – A Case Study ⋮ Latticed Simulation Relations and Games ⋮ Synthesising Strategy Improvement and Recursive Algorithms for Solving 2.5 Player Parity Games ⋮ The Birth of Model Checking ⋮ Correcting a Space-Efficient Simulation Algorithm ⋮ Unnamed Item ⋮ Negation-closure for JSON schema ⋮ A tableau proof system for a mazurkiewicz trace logic with fixpoints ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Computation Tree Regular Logic for Genetic Regulatory Networks ⋮ Temporal logic and categories of Petri nets ⋮ Local model checking for context-free processes ⋮ Inf-datalog, Modal Logic and Complexities ⋮ Characteristic Formulae for Timed Automata ⋮ LATTICED SIMULATION RELATIONS AND GAMES ⋮ The Modal μ-Calculus Caught Off Guard ⋮ Modular Markovian Logic ⋮ Model checking with probabilistic tabled logic programming ⋮ AN EXPRESSIVE EXTENSION OF TLC ⋮ Monadic Second Order Logic And Its Fragments ⋮ An Automata-Theoretic Approach to Infinite-State Systems ⋮ Fixpoint alternation: arithmetic, transition systems, and the binary tree ⋮ Topologies, Continuity and Bisimulations ⋮ A Note on Negative Tagging for Least Fixed-Point Formulae ⋮ Model-Checking Strategic Ability and Knowledge of the Past of Communicating Coalitions ⋮ From Philosophical to Industrial Logics ⋮ Beliefs supported by binary arguments ⋮ Connection between logical and algebraic approaches to concurrent systems ⋮ Suitability of mCRL2 for Concurrent-System Design: A 2 × 2 Switch Case Study ⋮ CVPP: A Tool Set for Compositional Verification of Control–Flow Safety Properties ⋮ On the Complexity of Semantic Self-minimization ⋮ Refinement Sensitive Formal Semantics of State Machines With Persistent Choice ⋮ Fixed-Point Elimination in the Intuitionistic Propositional Calculus ⋮ Predicate Abstraction for Dense Real-Time Systems1 1This research was supported by the National Science Foundation under grants CCR-00-82560 and CCR-00-86096 and by NASA Langley Research Center under contract B09060051 and Cooperative Agreement NCC-1-399 with Honeywell Minneapolis. Most of this research has been conducted while the first author was visiting SRI International, July/August 2001. ⋮ Satisfiability of Linear Time Mu-Calculus on Finite Traces ⋮ Weighted versus Probabilistic Logics ⋮ A Weighted μ-Calculus on Words ⋮ Domain mu-calculus ⋮ On global induction mechanisms in aμ-calculus with explicit approximations ⋮ ProMoVer: Modular Verification of Temporal Safety Properties ⋮ Egalitarian State-Transition Systems ⋮ Unnamed Item ⋮ Polynomial-Time Under-Approximation of Winning Regions in Parity Games ⋮ Switching Graphs ⋮ EXPTIME Tableaux for the Coalgebraic μ-Calculus ⋮ Solving Parity Games Using an Automata-Based Algorithm ⋮ SWITCHING GRAPHS ⋮ Computable CTL * for Discrete-Time and Continuous-Space Dynamic Systems ⋮ A Compositional Translation of Timed Automata with Deadlines to Uppaal Timed Automata ⋮ On Characterization, Definability and ω-Saturated Models ⋮ The Complexity of Model-Checking Tail-Recursive Higher-Order Fixpoint Logic ⋮ The modalμ-calculus hierarchy over restricted classes of transition systems ⋮ A Logic for Rewriting Strategies ⋮ Alternating Context-Free Languages and Linear Time μ-Calculus with Sequential Composition ⋮ Modal Logics for Cryptographic Processes ⋮ Model checking the full modal mu-calculus for infinite sequential processes ⋮ On the Strength of the Uniform Fixed Point Principle in Intuitionistic Explicit Mathematics ⋮ Automated formal analysis and verification: an overview ⋮ Process Algebra Having Inherent Choice: Revised Semantics for Concurrent Systems ⋮ Modular Games for Coalgebraic Fixed Point Logics ⋮ Property-oriented expansion ⋮ Model checking and boolean graphs ⋮ CTL\(^*\) and ECTL\(^*\) as fragments of the modal \(\mu\)-calculus ⋮ Assisting requirement formalization by means of natural language translation ⋮ Verification of \(\mathrm{EB}^3\) specifications using CADP ⋮ Towards a trustworthy semantics-based language framework via proof generation ⋮ \(\mu \)MV-algebras: An approach to fixed points in Łukasiewicz logic ⋮ Property preserving abstractions for the verification of concurrent systems ⋮ Axiomatizing the equational theory of regular tree languages ⋮ Propositional dynamic logic of context-free programs and fixpoint logic with chop ⋮ On modal mu-calculus and Büchi tree automata ⋮ Simple proof techniques for property preservation via simulation ⋮ Extension of synthesis algorithm of recursive processes to \(\mu\)-calculus ⋮ Fast and simple nested fixpoints ⋮ The \(\mu\)-calculus alternation depth hierarchy is infinite over finite planar graphs ⋮ Arthur Prior and hybrid logic ⋮ Uniform inevitability is tree automaton ineffable ⋮ Solving parity games in big steps ⋮ On the complexity of the two-variable guarded fragment with transitive guards ⋮ Reasoning about equilibria in game-like concurrent systems ⋮ Logical definability of fixed points ⋮ A linear algorithm to solve fixed-point equations on transition systems ⋮ Towards the hierarchical verification of reactive systems ⋮ Proving properties of dynamic process networks ⋮ On the \(\mu \)-calculus over transitive and finite transitive frames ⋮ Duality for modal \(\mu\)-logics ⋮ Reducing behavioural to structural properties of programs with procedures ⋮ Modal specifications for the control theory of discrete event systems ⋮ Axiomatising extended computation tree logic ⋮ Fixed point characterization of infinite behavior of finite-state systems ⋮ Synthesising correct concurrent runtime monitors ⋮ The equational logic of fixed points ⋮ Completeness of Park induction ⋮ Program schemata vs. automata for decidability of program logics ⋮ On the consistency, expressiveness, and precision of partial modeling formalisms ⋮ Almost-certain eventualities and abstract probabilities in the quantitative temporal logic qTL ⋮ On the equational definition of the least prefixed point. ⋮ Undecidable problems in unreliable computations. ⋮ On temporal logic versus Datalog ⋮ A survey of stochastic \(\omega \)-regular games ⋮ Product line process theory ⋮ Deciding the existence of uniform interpolants over transitive models ⋮ Sahlqvist theorem for modal fixed point logic ⋮ An algebra of behavioural types ⋮ An expansion of basic logic with fixed points ⋮ Model checking in the modal \(\mu \)-calculus and generic solutions ⋮ The variable hierarchy for the games \(\mu \)-calculus ⋮ Completeness for flat modal fixpoint logics ⋮ Automated analysis of mutual exclusion algorithms using CCS ⋮ Synthesis of Reactive(1) designs ⋮ Maximal traces and path-based coalgebraic temporal logics ⋮ The dag-width of directed graphs ⋮ SnS can be modally characterized ⋮ Mathematical modal logic: A view of its evolution ⋮ Completions of \(\mu \)-algebras ⋮ A note on model checking the modal \(\nu\)-calculus ⋮ The \(\mu\)-calculus alternation hierarchy collapses over structures with restricted connectivity ⋮ Local model checking in the modal mu-calculus ⋮ Algorithmic correspondence for intuitionistic modal mu-calculus ⋮ Compositional verification of sequential programs with procedures ⋮ Deductive verification of alternating systems ⋮ Cut-free sequent systems for temporal logic ⋮ Canonical completeness of infinitary \(\mu \) ⋮ Games for the \(\mu\)-calculus ⋮ Duality and the completeness of the modal \(\mu\)-calculus ⋮ An initial semantics for the \(\mu\)-calculus on trees and Rabin's complementation lemma ⋮ Local model checking for infinite state spaces ⋮ Enhancing unsatisfiable cores for LTL with information on temporal relevance ⋮ Symbolic model checking: \(10^{20}\) states and beyond ⋮ Synthesis of obfuscation policies to ensure privacy and utility ⋮ Ł\(\Pi\) logic with fixed points ⋮ Comparing disjunctive modal transition systems with an one-selecting variant ⋮ Spatial logic of tangled closure operators and modal mu-calculus ⋮ Solving Łukasiewicz \(\mu\)-terms ⋮ Concurrent common knowledge: Defining agreement for asynchronous systems ⋮ A CCS-based investigation of deadlock in a multi-process electronic mail system ⋮ Automatic verification of distributed systems: the process algebra approach. ⋮ Invariants for parameterised Boolean equation systems ⋮ Model-checking games for fixpoint logics with partial order models ⋮ Faster algorithms for mean-payoff games ⋮ CTRL: extension of CTL with regular expressions and fairness operators to verify genetic regulatory networks ⋮ Property specifications for workflow modelling ⋮ On the completeness and decidability of duration calculus with iteration ⋮ Strategy logic ⋮ Syntactic cut-elimination for a fragment of the modal mu-calculus ⋮ Verification of reactive systems via instantiation of parameterised Boolean equation systems ⋮ On the complexity of checking semantic equivalences between pushdown processes and finite-state processes ⋮ On the proof theory of the modal mu-calculus ⋮ Distributed semantics for the \(\pi \)-calculus based on Petri nets with inhibitor ARCS ⋮ On modal \(\mu \)-calculus and Gödel-Löb logic ⋮ The modal mu-calculus alternation hierarchy is strict ⋮ Reasoning about nondeterministic and concurrent actions: A process algebra approach ⋮ On the modal definability of simulability by finite transitive models ⋮ A compositional \(\mu\)-calculus proof system for statecharts processes ⋮ Systems of agents controlled by logical programs: complexity of verification ⋮ Symbolic model checking for \(\mu\)-calculus requires exponential time ⋮ A decidable class of problems for control under partial observation ⋮ Quantitative program logic and expected time bounds in probabilistic distributed algorithms. ⋮ The formalization and analysis of a communications protocol ⋮ Distributed symbolic model checking for \(\mu\)-calculus ⋮ Reduced models for efficient CCS verification ⋮ The finite graph problem for two-way alternating automata. ⋮ A decision procedure for (co)datatypes in SMT solvers ⋮ Sequent calculi for process verification: Hennessy-Milner logic for an arbitrary GSOS ⋮ On the universal and existential fragments of the \(\mu\)-calculus ⋮ Compositional analysis for verification of parameterized systems ⋮ Compositionality of Hennessy-Milner logic by structural operational semantics ⋮ Algebraic-coalgebraic specification in CoCASL ⋮ Taming the complexity of biochemical models through bisimulation and collapsing: theory and practice ⋮ Verifying persistent security properties ⋮ A spatial logic for concurrency. I ⋮ DP lower bounds for equivalence-checking and model-checking of one-counter automata ⋮ Quantitative solution of omega-regular games ⋮ A focus system for the alternation-free \(\mu \)-calculus ⋮ Compositional verification of concurrent systems by combining bisimulations ⋮ A compositional proof system on a category of labelled transition systems ⋮ Why there is no general solution to the problem of software verification ⋮ When not losing is better than winning: abstraction and refinement for the full \(\mu\)-calculus ⋮ The power of first-order quantification over states in branching and linear time temporal logics ⋮ On the complexity of determinizing monitors ⋮ Equivalence of probabilistic \(\mu\)-calculus and p-automata ⋮ Monitorability for the Hennessy-Milner logic with recursion ⋮ Measure properties of regular sets of trees ⋮ A tableau construction for finite linear-time temporal logic ⋮ Verification of finite-state machines: a distributed approach ⋮ Off-the-shelf automated analysis of liveness properties for just paths ⋮ Entanglement and the complexity of directed graphs ⋮ Exponential improvement of time complexity of model checking for multiagent systems with perfect recall ⋮ Generalized abstraction-refinement for game-based CTL lifted model checking ⋮ Model checking open systems with alternating projection temporal logic ⋮ Temporal-logic property preservation under Z refinement ⋮ Model-checking timed automata with deadlines with Uppaal ⋮ Cartesian difference categories ⋮ Exponential automatic amortized resource analysis ⋮ Natural projection as partial model checking ⋮ Hierarchical cost-parity games ⋮ Bisimulation-invariant PTIME and higher-dimensional \(\mu\)-calculus ⋮ Model checking the full modal mu-calculus for infinite sequential processes ⋮ Program schemata technique for propositional program logics: a 30-year history ⋮ A note on the approximation of mean-payoff games ⋮ Intuitionistic fixed point logic ⋮ Selective mu-calculus and formula-based equivalence of transition systems ⋮ Characterization, definability and separation via saturated models ⋮ Completeness for \(\mu\)-calculi: a coalgebraic approach ⋮ Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 5--11, 2017 ⋮ Team bisimilarity, and its associated modal logic, for BPP nets ⋮ Temporal refinements for guarded recursive types ⋮ Generative program analysis and beyond: the power of domain-specific languages (invited paper) ⋮ Sublogics of a branching time logic of robustness ⋮ Modular construction of complete coalgebraic logics ⋮ Strategies, model checking and branching-time properties in Maude ⋮ The complexity of identifying characteristic formulae ⋮ Completeness for the modal \(\mu\)-calculus: separating the combinatorics from the dynamics ⋮ On first-order logic and CPDA graphs ⋮ Bridging the gap between fair simulation and trace inclusion ⋮ Ambiguous classes in \(\mu\)-calculi hierarchies ⋮ Incompleteness of states w.r.t. traces in model checking ⋮ On modal \(\mu\)-calculus and non-well-founded set theory ⋮ Compositional verification and 3-valued abstractions join forces ⋮ A modular approach to defining and characterising notions of simulation ⋮ Logical characterization of branching metrics for nondeterministic probabilistic transition systems ⋮ On complexity of verification of interacting agents' behavior ⋮ Producing explanations for rich logics ⋮ On modal \(\mu\)-calculus with explicit interpolants ⋮ Deduction chains for common knowledge ⋮ The alternation hierarchy in fixpoint logic with chop is strict too ⋮ Compositionality for quantitative specifications ⋮ A novel approach to verifying context free properties of programs ⋮ Intuitionistic Podelski-Rybalchenko theorem and equivalence between inductive definitions and cyclic proofs ⋮ Predicate liftings and functor presentations in coalgebraic expression languages ⋮ Model checking for hybrid branching-time logics ⋮ Determinizing monitors for HML with recursion ⋮ A linear-time model-checking algorithm for the alternation-free modal mu- calculus ⋮ Improving parity games in practice ⋮ Quasipolynomial computation of nested fixpoints ⋮ Two AGM-style characterizations of model repair ⋮ Temporal logic with recursion ⋮ Performance heuristics for GR(1) synthesis and related algorithms ⋮ Logical vs. behavioural specifications ⋮ A study on team bisimulation and H-team bisimulation for BPP nets ⋮ An algebraic and algorithmic method for analysing transition systems ⋮ An algebraic characterization of transition system equivalences ⋮ Forgetting in multi-agent modal logics ⋮ A propositional dynamic logic for instantial neighborhood semantics ⋮ Probabilistic temporal logics via the modal mu-calculus ⋮ Parameterised Boolean equation systems ⋮ Capturing constrained constructor patterns in matching logic ⋮ Analysis of security protocols as open systems ⋮ Completeness of Kozen's axiomatisation of the propositional \(\mu\)-calculus. ⋮ Inductive synthesis of recursive processes from logical properties ⋮ On the formalization of the modal \(\mu\)-calculus in the calculus of inductive constructions ⋮ Module checking ⋮ Simulation preorder over simple process algebras ⋮ Tarskian set constraints ⋮ Is your model checker on time? On the complexity of model checking for timed modal logics ⋮ Iterated Boolean games ⋮ Bounded game-theoretic semantics for modal mu-calculus ⋮ Local higher-order fixpoint iteration ⋮ Compositional verification of asynchronous concurrent systems using CADP ⋮ A goal-directed decision procedure for hybrid PDL ⋮ On bidirectional runtime enforcement
Cites Work
