Trace semantics via determinization for probabilistic transition systems
Logic in Computer Science
2018-02-27 v1
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.
Cite
@article{arxiv.1802.09084,
title = {Trace semantics via determinization for probabilistic transition systems},
author = {Alexandre Goy},
journal= {arXiv preprint arXiv:1802.09084},
year = {2018}
}