A complete axiomatisation for observational congruence of finite-state behaviours. (English) Zbl 0688.68050
Finite state automata, with non-determinism and silent transitions, are seen as congruence classes under the weak bisimulation or observational equivalence (Park, Miller). This paper is an extension of the case where all computations are finite. A comparison shows that CCS is more general, however, the method shown here is suitable enough to describe communicating protocols.
Reviewer: H.Fuss
MSC:
| 68Q45 | Formal languages and automata |
| 68Q65 | Abstract data types; algebraic specification |
| 93-04 | Software, source code, etc. for problems pertaining to systems and control theory |
References:
| [1] | Baeten, J. C.M.; Bergstra, J. A.; Klop, J. W., On the consistency of Koomen’s fair abstraction rule, J. Theor. Comput. Sci., 51, 129-176 (1987) · Zbl 0621.68010 |
| [2] | Brookes, S. D.; Hoare, C. A.R.; Roscoe, A. W., A theory of communicating sequential processes, (J. Assoc. Comput. Mach., 31 (1984)), 560-599 · Zbl 0628.68025 |
| [3] | Bergstra, J. A.; Klop, J. W., A complete inference system for regular processes with silent moves, (Drake, F. R.; Truss, J. K., Proceedings, Logic Colloquium ’86 (1988), North-Holland: North-Holland Amsterdam), 21-81, 1988 · Zbl 0647.68033 |
| [4] | Hennessy, M. C., Acceptance trees, J. Assoc. Comput. Mach., 32, 896-928 (1985) · Zbl 0633.68074 |
| [5] | Hennessy, M. C.; Milner, A. J.R. G., Algebraic laws for nondeterminism and concurrency, J. Assoc. Comput. Mach., 32, 137-161 (1985) · Zbl 0629.68021 |
| [6] | Hennessy, M. C.; Plotkin, C. D., A term model for CCS, (Lecture Notes in Computer Science, Vol. 88 (1980)), 261-274 · Zbl 0479.68011 |
| [7] | Keller, R., Formal verification of parallel programs, Comm. ACM, 19, No. 7, 561-572 (1976) |
| [8] | Milner, A. J.R. G., A Calculus for Communicating Systems, (Lecture Notes in Computer Science, Vol. 92 (1980), Springer-Verlag: Springer-Verlag New York/Berlin), to be reissued as a report of the Computer Science Dept. Edinburgh University · Zbl 0452.68027 |
| [9] | Milner, A. J.R. G., A complete inference system for a class of regular behaviours, J. Comput. System Sci., 28, 439-466 (1984) · Zbl 0562.68065 |
| [10] | Milner, A. J.R. G., Calculi for synchrony and asynchrony, J. Theor. Comput. Sci., 25, 267-310 (1983) · Zbl 0512.68026 |
| [11] | Milner, A. J.R. G., Lectures on a calculus for communicating systems, (Broy, M., Control Flow and Data Flow: Concepts of Distributed Programming, Proceedings, NATO International Summer School of Marktoberdorf in 1984 (1986), Springer-Verlag: Springer-Verlag New York/Berlin) · Zbl 0609.68020 |
| [12] | Park, D. M.R., Concurrency and automata on infinite sequences, (Proceedings, 5th Gl Conference. Proceedings, 5th Gl Conference, Lect. Notes in Comput. Sci., Vol. 104 (1981)), 167-183 · Zbl 0457.68049 |
| [13] | Walker, D. J., Bisimulation and divergence, (Proceedings 2nd Conference on Logics in Computer Science. Proceedings 2nd Conference on Logics in Computer Science, Edinburgh (1988)) · Zbl 0713.68036 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
