A proof rule for fair termination of guarded commands

DOI10.1016/S0019-9958(85)80014-0zbMath0577.68022MaRDI QIDQ3698284

Orna Grumberg, Nissim Francez, Johann A. Makowsky

Publication date: 1985

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

zbMATH Keywords

completenessLPS-ruleoperational semantics of computation treesproof rule for fairly terminating guarded commands

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) General topics in the theory of software (68N01)

Related Items (17)

A complete rule for equifair termination ⋮ Infinite trees, markings, and well-foundedness ⋮ Appraising fairness in languages for distributed programming ⋮ A methodology for designing proof rules for fair parallel programs ⋮ The \(\mu\)-calculus as an assertion-language for fairness arguments ⋮ Liminf progress measures ⋮ Completing the temporal picture ⋮ Complete proof rules for strong fairness and strong extreme fairness ⋮ Verification of distributed programs using representative interleaving sequences ⋮ A Bibliography of Willem-Paul de Roever ⋮ Explicit Fair Scheduling for Dynamic Control ⋮ Verification of concurrent programs: The automata-theoretic framework ⋮ Fifty years of Hoare's logic ⋮ Probabilistic termination versus fair termination ⋮ Convergence of iteration systems ⋮ Fair derivations in E0L systems ⋮ Proving partial order properties

This page was built for publication: A proof rule for fair termination of guarded commands