Algebras of modal operators and partial correctness |
| |
Authors: | Bernhard Möller Georg Struth |
| |
Affiliation: | 1. Institut für Informatik, Universität Augsburg, Universitätsstr. 14, D-86135 Augsburg, Germany;2. Fakultät für Informatik, Universität der Bundeswehr München, D-85577 Neubiberg, Germany |
| |
Abstract: | Modal Kleene algebras are Kleene algebras enriched by forward and backward box and diamond operators. We formalise the symmetries of these operators as Galois connections, complementarities and dualities. We study their properties in the associated operator algebras and show that the axioms of relation algebra are theorems at the operator level. Modal Kleene algebras provide a unifying semantics for various program calculi and enhance efficient cross-theory reasoning in this class, often in a very concise pointfree style. This claim is supported by novel algebraic soundness and completeness proofs for Hoare logic and by connecting this formalism with an algebraic decision procedure. |
| |
Keywords: | Semirings Kleene algebra Modal operators Partial correctness Hoare logic |
本文献已被 ScienceDirect 等数据库收录! |
|