Predicate transformers for extended probability and non-determinism

DOI10.1017/S0960129509007555zbMath1175.68253MaRDI QIDQ3636909

Klaus Keimel, Gordon D. Plotkin

Publication date: 30 June 2009

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

zbMATH Keywords

powerdomainsnondeterminismpredicate transformersstate transformers

Mathematics Subject Classification ID

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

Related Items

Generic weakest precondition semantics from monads enriched with order ⋮ Isomorphism theorems between models of mixed choice ⋮ Healthiness conditions for predicate transformers ⋮ De Groot duality and models of choice: angels, demons and nature ⋮ Relating direct and predicate transformer partial correctness semantics for an imperative probabilistic-nondeterministic language ⋮ Weak topologies and compactness in asymmetric functional analysis ⋮ A Minkowski type duality mediating between state and predicate transformer semantics for a probabilistic nondeterministic language

Cites Work

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