Non-Deterministic Kleene Coalgebras

TL;DR

This paper develops a systematic framework for deriving regular expression languages and axiomatizations for various systems, extending classical results to more general and non-deterministic models like Mealy and Moore machines.

Contribution

It generalizes Kleene and Milner's foundational work to a broader class of systems, providing methods to generate languages and axioms for non-deterministic coalgebraic systems.

Findings

Provides a systematic method for deriving regular languages for diverse systems

Establishes sound and complete axiomatizations for these systems

Extends classical automata theory to non-deterministic coalgebraic models

Abstract

In this paper, we present a systematic way of deriving (1) languages of (generalised) regular expressions, and (2) sound and complete axiomatizations thereof, for a wide variety of systems. This generalizes both the results of Kleene (on regular languages and deterministic finite automata) and Milner (on regular behaviours and finite labelled transition systems), and includes many other systems such as Mealy and Moore machines.