Model checking the full modal mu-calculus for infinite sequential processes

DOI10.1007/3-540-63165-8_198zbMath1401.68188OpenAlexW1590891429MaRDI QIDQ4571973

Bernhard Steffen, Olaf Burkart

Publication date: 4 July 2018

Published in: Automata, Languages and Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-63165-8_198

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (8)

Model checking LTL with regular valuations for pushdown systems ⋮ Model Checking Procedural Programs ⋮ Characteristic invariants in Hennessy-Milner logic ⋮ Efficient CTL model-checking for pushdown systems ⋮ Branching Temporal Logic of Calls and Returns for Pushdown Systems ⋮ Efficient CTL Model-Checking for Pushdown Systems ⋮ Model checking the full modal mu-calculus for infinite sequential processes ⋮ Automated formal analysis and verification: an overview

Cites Work

• Results on the propositional \(\mu\)-calculus
• The theory of ends, pushdown automata, and second-order logic
• Model checking the full modal mu-calculus for infinite sequential processes
• Decidability of Second-Order Theories and Automata on Infinite Trees
• The modal mu-calculus alternation hierarchy is strict
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Model checking the full modal mu-calculus for infinite sequential processes