caa a22 4500 467989796 CHVBK 20180323112541.0 cr unu---uuuuu 170328e19900301xx s 000 0 eng 10.1007/BF00264610 doi (NATIONALLICENCE)springer-10.1007/BF00264610 Morris Joseph Department of Computing Science, University of Glasgow, G128QQ, Glasgow, Scotland, UK aut Temporal predicate transformers and fair termination [Elektronische Daten] [Joseph Morris] Summary: 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 socalled weak and strong fairness in both their all-levels and top-level forms. Our formalization of the notion of fairness does not exploit the syntactic shape of programs, and allows the familiar nondeterminacy and fair nondeterminacy to be arbitrarily combined in the one program. Invariance theorems for reasoning about fairly terminating programs are proved. The semantics admits probabilistic implementations provided that unbounded fairness is excluded. Springer-Verlag, 1990 Acta Informatica Springer-Verlag 27/4(1990-03-01), 287-313 0001-5903 27:4<287 1990 27 236 https://doi.org/10.1007/BF00264610 text/html Onlinezugriff via DOI 1 research-article jats NATIONALLICENCE 856 40 https://doi.org/10.1007/BF00264610 text/html Onlinezugriff via DOI NATIONALLICENCE 100 1- Morris Joseph Department of Computing Science, University of Glasgow, G128QQ, Glasgow, Scotland, UK aut NATIONALLICENCE 773 0- Acta Informatica Springer-Verlag 27/4(1990-03-01), 287-313 0001-5903 27:4<287 1990 27 236 Metadata rights reserved Springer special CC-BY-NC licence nationallicence BK010053 XK010053 XK010000 NATIONALLICENCE NATIONALLICENCE NL-springer