(In)finite Trace Equivalence of Probabilistic Transition Systems
Abstract
We show how finite and infinite trace semantics of generative probabilistic transition systems arises through a determinisation construction. This enables the use of bisimulations (up-to) to prove equivalence. In particular, it follows that trace equivalence for finite probabilistic transition systems is decidable. Further, the determinisation construction applies to both discrete and continuous probabilistic systems.
Domains
| Origin | Files produced by the author(s) |
|---|
Loading...
