Enabledness and termination in refinement algebra

DOI10.1016/j.scico.2007.11.004zbMath1192.68163OpenAlexW2056368148WikidataQ114850295 ScholiaQ114850295MaRDI QIDQ923890

Kim Solin, Joakim von Wright

Publication date: 24 July 2009

Published in: Science of Computer Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.scico.2007.11.004

zbMATH Keywords

terminationaction systemsenablednessrefinement algebra

Mathematics Subject Classification ID

Theory of software (68N99)

Related Items (6)

An algebraic approach to computations with progress ⋮ Exploring an Interface Model for CKA ⋮ A sketch of a dynamic epistemic semiring ⋮ Dual choice and iteration in an abstract algebra of action ⋮ Normal forms in total correctness for while programs and action systems ⋮ Algebra of Monotonic Boolean Transformers

Uses Software

• KAT-ML

Cites Work

• Program inversion: More than fun!
• Kleene getting lazy
• Reasoning algebraically about loops
• A completeness theorem for Kleene algebras and the algebra of regular events
• Towards a refinement algebra
• Algebraic Notions of Termination
• Reactive Probabilistic Programs and Refinement Algebra
• Automated Reasoning in Kleene Algebra
• A Sketch of a Dynamic Epistemic Semiring
• Refinement Algebra with Operators for Enabledness and Termination
• KAT-ML: an interactive theorem prover for Kleene algebra with tests
• Refinement Calculus
• Kleene algebra with domain
• Omega Algebra, Demonic Refinement Algebra and Commands
• On Two Dually Nondeterministic Refinement Algebras
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Enabledness and termination in refinement algebra