Trace semantics via determinization for probabilistic transition systems

TL;DR

This paper develops a coalgebraic approach to trace semantics for probabilistic transition systems using determinization, enabling algorithmic equivalence checking of finite systems.

Contribution

It introduces a coalgebraic determinization method for probabilistic systems, facilitating the use of up-to techniques for equivalence checking.

Findings

Enables algorithmic equivalence checking of finite probabilistic systems

Provides a coalgebraic framework for trace semantics via determinization

Utilizes up-to techniques to exploit determinized structure

Abstract

A coalgebraic definition of finite and infinite trace semantics for probabilistic transition systems has recently been given using a certain Kleisli category. In this paper this semantics is developed using a coalgebraic method which is an instance of general determinization. Once applied to discrete systems, this point of view allows the exploitation of the determinized structure by up-to techniques. Thereby it becomes possible to algorithmically check the equivalence of two finite probabilistic transition systems.