Coalgebraic trace semantics via forgetful logics

TL;DR

This paper develops a coalgebraic framework using modal logic to unify and analyze trace semantics across various automata types, providing conditions for logical and trace semantics alignment and a canonical determinization method.

Contribution

It introduces a flexible coalgebraic approach with conditions ensuring logical and trace semantics coincide, and proposes a canonical determinization procedure related to Brzozowski's algorithm.

Findings

Logical semantics can coincide with trace semantics under certain conditions.

A canonical determinization procedure exists and is correct with respect to logical semantics.

The approach applies to weighted, alternating, tree automata, and probabilistic systems.

Abstract

We use modal logic as a framework for coalgebraic trace semantics, and show the flexibility of the approach with concrete examples such as the language semantics of weighted, alternating and tree automata, and the trace semantics of generative probabilistic systems. We provide a sufficient condition under which a logical semantics coincides with the trace semantics obtained via a given determinization construction. Finally, we consider a condition that guarantees the existence of a canonical determinization procedure that is correct with respect to a given logical semantics. That procedure is closely related to Brzozowski's minimization algorithm.