Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Blom, S., Orzan, S.: Distributed branching bisimulation reduction of state spaces. In: PDMC 2003, Parallel and Distributed Model Checking (Satellite workshop of CAV 2003). ENTCS, vol. 89(1), pp. 99–113. Elsevier, Amsterdam (2003)
Cormen, T., Leiserson, C., Rivest, R., Stein, C.: Introduction to Algorithms, 2nd edn. MIT Press, Cambridge (2001)
De Nicola, R., Vaandrager, F.: Three logics for branching bisimulation. Journal of the ACM 42(2), 458–487 (1995)
Eloranta, J.: Minimal Transition Systems with Respect to Divergence Preserving Behavioural Equivalences. PhD thesis, University of Helsinki (1994)
Engelfriet, J.: Determinacy \(\longrightarrow\) (observation equivalence = trace equivalence). Theoretical Computer Science 36(1), 21–25 (1985)
Groote, J.F., Vaandrager, F.: An efficient algorithm for branching bisimulation and stuttering equivalence. In: Paterson, M. (ed.) ICALP 1990. LNCS, vol. 443, pp. 626–638. Springer, Heidelberg (1990)
Roscoe, A.W.: CSP and determinism in security modelling. In: Proceedings of IEEE Symposium on Security and Privacy, pp. 114–127. IEEE, Los Alamitos (1995)
Roscoe, A.W.: The Theory and Practice of Concurrency, p. 565. Prentice-Hall, Englewood Cliffs (1998)
Ryan, P.Y.A., Schneider, S.A.: Process algebra and non-interference. In: Proceedings of Computer Security Foundations Workshop, pp. 214–227. IEEE, Los Alamitos (1999)
Van Glabbeek, R.J.: The linear time – branching time spectrum II; the semantics of sequential systems with silent moves. In: Best, E. (ed.) CONCUR 1993. LNCS, vol. 715, pp. 66–81. Springer, Heidelberg (1993)
Van Glabbeek, R.J., Weijland, W.P.: Branching time and abstraction in bisimulation semantics. Journal of the ACM 43(3), 555–600 (1996)
Voorhoeve, M., Mauw, S.: Impossible futures and determinism. Information Processing Letters 80(1), 51–58 (2001)
Zdancewic, S., Myers, A.: Observational determinism for concurrent program security. In: Proceedings of the 16th IEEE Computer Security Foundations Workshop, pp. 29–43. IEEE, Los Alamitos (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hansen, H., Valmari, A. (2006). Operational Determinism and Fast Algorithms. In: Baier, C., Hermanns, H. (eds) CONCUR 2006 – Concurrency Theory. CONCUR 2006. Lecture Notes in Computer Science, vol 4137. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11817949_13
Download citation
DOI: https://doi.org/10.1007/11817949_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-37376-6
Online ISBN: 978-3-540-37377-3
eBook Packages: Computer ScienceComputer Science (R0)