Modal Semirings and Kleene Algebras
Georg Struth, University of Sheffield

Modal semirings and Kleene algebras have been proposed as
unifying semantics for computing systems that support equational
modelling and calculational reasoning in particularly simple and
concise ways, e.g., by using automated theorem proving systems.

These formalisms are obtained by expanding semirings or Kleene
algebras with domain operations that are axiomatised equationally. The
axioms are inspired by binary relations, where the domain forms the set
of all those states which are related to some other state. Modal
diamond operators can then be obtained from domain as abstract image
or preimage operations, in accordance with the usual frame
semantics. Modal box operators are obtained by duality.

This talk surveys a range of domain axiomatisations for semigroups,
monoids, variants of semirings and Kleene algebras, and it shows how
modal operators can be defined on these in the style of Jonsson and
Tarski. Some important models are then discussed and the potential of
these structures in computing is illusrated through a number of
examples: Hoare-style program analysis, dynamic and temporal
reasoning, termination analysis.

Not enough is known about the structure theory of modal semirings
and Kleene algebras. I will therefore conclude my talk by presenting
some representability and axiomatisability results and point out some
directions for future research.