The \(\mu\)-calculus as an assertion-language for fairness arguments

DOI10.1016/0890-5401(89)90004-7zbMath0678.68010OpenAlexW1982457550MaRDI QIDQ1124314

S. H. Smith

Publication date: 1989

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0890-5401(89)90004-7

zbMATH Keywords

fairness\(\mu\)-calculusterminationweakest preconditionassertion-language

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65) General topics in the theory of software (68N01)

Related Items (12)

Merging regular processes by means of fixed-point theory ⋮ A methodology for designing proof rules for fair parallel programs ⋮ Liminf progress measures ⋮ Some subsets of monadic first-order logic (MFO) used for the specification and synthesis of \(\Sigma\)-automata ⋮ Completing the temporal picture ⋮ Deductive verification of alternating systems ⋮ A compositional approach to CTL\(^*\) verification ⋮ Verification by augmented abstraction: The automata-theoretic view ⋮ A Bibliography of Willem-Paul de Roever ⋮ Model checking with strong fairness ⋮ Verification by augmented finitary abstraction ⋮ Proving partial order properties

Cites Work

• Fair termination revisited - with delay
• Elementary induction on abstract structures
• First-order dynamic logic
• A proof rule for fair termination of guarded commands
• Countable nondeterminism and random assignment
• Formalization of Properties of Functional Programs
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: The \(\mu\)-calculus as an assertion-language for fairness arguments