Trace Semantics for Nondeterministic Probabilistic Automata via Determinization
share
This paper studies trace-based equivalences for automata combining nondeterministic and probabilistic choices. We show how a trace semantics for such processes, derived from testing equivalences, can be recovered by instantiating a coalgebraic construction known as the generalized powerset construction. This construction defines trace semantics on a system in terms of bisimilarity on the determinized system. The definition of trace semantics recovered via this construction is characterized and compared to known definitions of trace equivalences appearing in the literature.
READ FULL TEXT