Predicate transformers for extended probability and non-determinism

DOI10.1017/S0960129509007555MaRDI QIDQ3636909zbMATH OpenFDO

Authors Klaus Keimel, Gordon D. Plotkin

Publication date 30 June 2009

Published in Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1017/S0960129509007555

zbMATH Keywords

nondeterminismpowerdomainspredicate transformersstate transformers

Mathematics Subject Classification ID

Continuous lattices and posets, applications (06B35) Eilenberg-Moore and Kleisli constructions for monads (18C20) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Towards a calculus of predicate transformers
• Non-deterministic expressions and predicate transformers
• An expectation-transformer model for probabilistic temporal logic
• An expectation transformer approach to predicate abstraction and data independence for probabilistic programs
• Predicate Transformer Semantics
• Predicate transformers and higher-order programs
• Relating direct and predicate transformer partial correctness semantics for an imperative probabilistic-nondeterministic language
• Mathematics of Program Construction
• Probabilistic Interpretations of Predicates
• Probabilistic models for intuitionistic predicate logic

Cites work

• A domain-theoretic Banach–Alaoglu theorem
• Abstraction, Refinement and Proof for Probabilistic Systems
• Continuous Lattices and Domains
• Demonic, angelic and unbounded probabilistic choices in sequential programs
• Exact functionals and their core
• Generalized metric spaces: Completion, topology, and powerdomains via the Yoneda embedding
• MINKOWSKI DUALITY AND ITS APPLICATIONS
• Partial correctness for probabilistic demonic programs
• Power domains and second-order predicates
• Reasoning about probabilistic sequential programs in a probabilistic logic
• Robust Statistics
• Sublinear Functionals and Ideals in Partially Ordered Vector Spaces
• Sur la fonction d'appui des ensembles convexes dans un espace localement convexe

Cited in

(13)

• A Minkowski type duality mediating between state and predicate transformer semantics for a probabilistic nondeterministic language
• A predicate transformer for the progress property `to-always'
• Weak topologies and compactness in asymmetric functional analysis
• Large Scale Inference of Deterministic Transductions: Tenjinno Problem 1
• De Groot duality and models of choice: angels, demons and nature
• Underapproximating Predicate Transformers
• Semantic domains for combining probability and non-determinism
• Isomorphism theorems between models of mixed choice
• Relating direct and predicate transformer partial correctness semantics for an imperative probabilistic-nondeterministic language
• Demonic, angelic and unbounded probabilistic choices in sequential programs
• Healthiness conditions for predicate transformers
• Probabilistic predicate transformers. II: Partially observable probability
• Generic weakest precondition semantics from monads enriched with order

This page was built for publication: Predicate transformers for extended probability and non-determinism

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