The main contribution of this work is a fast algorithm for checking whether a labelled transition system (LTS) is operationally deterministic. Operational determinism is a condition on the LTS designed to capture the notion of "deterministic behaviour" without ruling out invisible actions and divergence, and without strictly devoting oneself to any single process-algebraic semantics. Indeed, we show that in the case of operationally deterministic LTSs, all divergence-sensitive equivalences between divergence-sensitive branching bisimilarity and trace + divergence trace equivalence collapse to the same equivalence. The running time of the algorithm is linear except a term that, roughly speaking, grows as slowly as Ackermann's function grows quickly. If the original LTS is operationally deterministic, the algorithm produces as a by-product a structurally deterministic LTS that is divergence-sensitive branching bisimilar to the original one. This LTS can be minimised like a deterministic finite automaton. The overall approach is so cheap that it makes almost always sense to first try it and revert to a semantics-specific reduction or minimisation algorithm only if the LTS proves operationally nondeterministic. © Springer-Verlag Berlin Heidelberg 2006.
CITATION STYLE
Hansen, H., & Valmari, A. (2006). Operational determinism and fast algorithms. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4137 LNCS, pp. 188–202). Springer Verlag. https://doi.org/10.1007/11817949_13
Mendeley helps you to discover research relevant for your work.