On the specification of operations on the rational behaviour of systems

TL;DR

This paper introduces a new specification format for algebraic operations that ensures the rational behaviour of finite systems is preserved, with applications to regular languages, processes, and weighted transition systems.

Contribution

It extends existing frameworks to specifically handle the rational fixpoint, capturing finite system behaviour in a formal, algebraic manner.

Findings

Rational behaviour is closed under the new specified operations.

The format applies to regular languages and processes.

Finite weighted transition systems are included in the framework.

Abstract

Structural operational semantics can be studied at the general level of distributive laws of syntax over behaviour. This yields specification formats for well-behaved algebraic operations on final coalgebras, which are a domain for the behaviour of all systems of a given type functor. We introduce a format for specification of algebraic operations that restrict to the rational fixpoint of a functor, which captures the behaviour of finite systems. In other words, we show that rational behaviour is closed under operations specified in our format. As applications we consider operations on regular languages, regular processes and finite weighted transition systems.