Initial Algebra Correspondence under Reachability Conditions

TL;DR

This paper presents a categorical framework that unifies conditions under which different fixed point semantics of transition systems, such as Markov chains and automata, coincide, based on reachability assumptions.

Contribution

It introduces a general categorical approach using adjunctions to establish when various semantics align, applicable to Markov chains, automata, and Markov decision processes.

Findings

Unified reachability conditions ensure semantics coincide

Framework applies to Markov chains, automata, and MDPs

Uses categorical constructs like adjunctions and Kan extensions

Abstract

Suitable reachability conditions can make two different fixed point semantics of a transition system coincide. For instance, the total and partial expected reward semantics on Markov chains (MCs) coincide whenever the MC at hand is almost surely reachable. In this paper, we present a unifying framework for such reachability conditions that ensures the correspondence of two different semantics. Our categorical framework naturally induces an abstract reachability condition via a suitable adjunction, which allows us to prove coincidences of fixed points, and more generally of initial algebras. We demonstrate the generality of our approach by instantiating several examples, including the almost surely reachability condition for MCs, and the unambiguity condition of automata. We further study a canonical construction of our instance for Markov decision processes by pointwise Kan extensions.