Show description

It is wellknown that such inert τ -transitions can be omitted while preserving branching bisimilarity. e Sζ ) −−→ −−−→∂i,o (Vt,e Sζ ) , and, since the second transition is the only step possible after the first atransition, the τ -transition resulting from applying τi,o ( ) is again inert. d Sζ ) −−→ −−→∂i,o (Vt,e Sdζ ) , and again the τ -transition resulting from applying τi,o ( ) is inert. − →∂i,o (Vt,e S∅ ) . Conversely, let E be a BSPτ recursive specification, let p be a BSPτ process expression, and let M = (S, A , →, ↑, ↓) be the associated labeled transition system.

Springer, Heidelberg (1993) 8. : What is Branching Time Semantics and why to use it?. Bulletin of the EATCS 53, 190–198 (1994) 9. : The Linear Time – Branching Time Spectrum I. A. ) Handbook of Process Algebra, pp. 3–99. Elsevier, Amsterdam (2001) A Process-Theoretic Look at Automata 33 10. : Branching time and abstraction in bisimulation semantics. Journal of the ACM 43(3), 555–600 (1996) 11. : Introduction to Automata Theory, Languages, and Computation. Pearson, London (2006) 12. : Communication and Concurrency.

6 Conclusion Every undergraduate curriculum in computer science contains a course on automata theory and formal languages. On the other hand, an introduction to concurrency theory is usually not given in the undergraduate program. Both theories as basic models of computation are part of the foundations of computer science. Automata theory and formal languages provide a model of computation where interaction is not taken into account, so a computer is considered as a stand-alone device executing batch processes.