Alternation-free weighted mu-calculus: decidability and completeness

DOI10.1016/j.entcs.2015.12.018zbMath1351.68164OpenAlexW2286042860WikidataQ113317723 ScholiaQ113317723MaRDI QIDQ5971405

Bingtian Xue, Radu Mardare, Kim Guldstrand Larsen

Publication date: 16 December 2016

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

Full work available at URL: https://doi.org/10.1016/j.entcs.2015.12.018

zbMATH Keywords

satisfiabilitycomplete axiomatizationnon-compact modal logicsweighted transition systemsweighted modal mu-calculus

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Related Items

Synthesis for Multi-weighted Games with Branching-Time Winning Conditions, Model checking and synthesis for branching multi-weighted logics, Weighted Linear Dynamic Logic, Unnamed Item, Unnamed Item

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Adequacy and complete axiomatization for timed modal logic
• Topological proofs of some Rasiowa-Sikorski lemmas
• Model-checking in dense real-time
• Proof systems for satisfiability in Hennessy-Milner logic with recursion
• An automata theoretic decision procedure for the propositional mu- calculus
• Symbolic model checking for real-time systems
• A linear-time model-checking algorithm for the alternation-free modal mu- calculus
• Completeness of Kozen's axiomatisation of the propositional \(\mu\)-calculus.
• Hybrid control of force transients for multi-point injection engines
• Strong Completeness for Markovian Logics
• A Decidable Recursive Logic for Weighted Transition Systems
• Decidability and Expressiveness of Recursive Weighted Logic
• Model Checking One-clock Priced Timed Automata
• Introduction to Boolean Algebras
• Infinite Runs in Weighted Timed Automata with Energy Constraints
• From timed automata to logic — and back
• On the role of the Baire Category Theorem and Dependent Choice in the foundations of logic
• Stone Duality for Markov Processes
• Reactive Systems
• Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
• A proof of the completeness theorem of Grödel