Temporal predicate transformers and fair termination

DOI10.1007/BF00264610MaRDI QIDQ1120264zbMATH OpenFDO

Authors Joseph M. Morris

Publication date 1990

Published in Acta Informatica (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/BF00264610

zbMATH Keywords

fairly- terminating programsnondeterministic programspredicate transformer semantics

Mathematics Subject Classification ID

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

Review text

It is usually assumed that implementations of nondeterministic programs may resolve the nondeterminacy arbitrarily. In some circumstances, however, we may wish to assume that the implementation is in some sense fair, by which we mean that in its long-term behaviour it does not show undue bias in forever favouring some nondeterministic choices over others. Under the assumption of fairness many otherwise failing programs become terminating. We construct various predicate transformer semantics of such fairly-terminating programs. The approach is based on formulating the familiar temporal operators always, eventually, and infinitely often as predicate transformers. We use these operators to construct a framework that accommodates many kinds of fairness, including varieties of so-called weak and strong fairness in both their all-levels and top- level forms. The semantics does not make any assumptions about the syntactic shape of programs, and allows the familiar nondeterminacy and fair nondeterminacy to be arbitrarily combined in the open program. Invariance theorems for reasoning about fairly terminating programs are proved. The semantics admits probabilistic implementations provided that unbounded fairness is excluded.

Recommendations

• scientific article; zbMATH DE number 3965428
• scientific article; zbMATH DE number 3846836
• Fair termination revisited - with delay
• Semantic models for total correctness and fairness
• Probabilistic termination versus fair termination

Cited in

(12)

• Fairness and the axioms of control predicates
• The \(\mu\)-calculus as an assertion-language for fairness arguments
• Weakest preconditions for progress
• Safety and progress of recursive procedures
• scientific article; zbMATH DE number 1612489 (Why is no real title available?)
• scientific article; zbMATH DE number 3846836 (Why is no real title available?)
• scientific article; zbMATH DE number 3890707 (Why is no real title available?)
• On the Expressiveness of MTL Variants over Dense Time
• scientific article; zbMATH DE number 3965428 (Why is no real title available?)
• An algebraic approach to refinement with fair choice
• Semantic models for total correctness and fairness
• Demonic, angelic and unbounded probabilistic choices in sequential programs

This page was built for publication: Temporal predicate transformers and fair termination

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1120264)