×

GSOS and finite labelled transition systems. (English) Zbl 0822.68060

Summary: Recently there has been considerable interest in studying formats of Plotkin style inference rules which ensures that the induced labelled transition system semantics have certain properties. In this note, I give a contribution to this line of research by giving a restricted version of Bloom, Istrail and Meyer’s GSOS format which induces finite labelled transition systems.

MSC:

68Q55 Semantics in the theory of computing
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Abramsky, S.; Hankin, C., Abstract Interpretation of Declarative Languages (1987), Ellis Horwood: Ellis Horwood Chichester
[2] Aceto, L.; Bloom, B.; Vaandrager, F. W., Turning SOS rules into equations, (Report CS-R9218 (June 1992), CWI: CWI Amsterdam), Inform. and Comput., submitted · Zbl 0822.68059
[3] Austry, D.; Boudol, G., Algèbre de processus et synchronisations, Theoret. Comput. Sci., 30, 1, 91-131 (1984) · Zbl 0533.68026
[4] Badouel, E.; Darondeau, P., On guarded recursion, Theoret. Comput. Sci., 82, 2, 403-408 (1991) · Zbl 0728.68079
[5] Badouel, E.; Darondeau, P., Structural operational specifications and trace automata, (Publication interne 629 (1992), IRISA: IRISA Rennes), extended abstract appeared in Proc. CONCUR ’92
[6] Baeten, J. C.M.; Bergstra, J. A.; Klop, J. W., Syntax and defining equations for an interupt mechanism in process algebra, Fund. Inform., IX, 2, 127-168 (1986) · Zbl 0617.68027
[7] Baeten, J. C.M.; Weijland, W. P., Process Algebra, Cambridge Tracts in Theoretical Computer Science, Vol. 18 (1990), Cambridge University Press: Cambridge University Press Cambridge · Zbl 0716.68002
[8] Bloom, B., Ready simulation, bisimulation, and the semantics of CCS-like languages, (Ph.D. Thesis (1989), Department of Electrical Engineering and Computer Science, MIT)
[9] Bloom, B.; Istrail, S.; Meyer, A. R., Bisimulation can’t be traced: preliminary report, (Conference Record of 15th Ann. Acm Symp. on Principles of Programming Laguages (1988)), 229-239, Acm, to appear.
[10] Bol, R. N.; Groote, J. F., The meaning of negative premises in transition system specifications (extended abstract), (Leach Albert, J.; Monien, B.; Rodríguez, M., Proc. 18th ICALP. Proc. 18th ICALP, Lecture Notes in Computer Science, Vol. 510 (1991), Springer: Springer Berlin). (Leach Albert, J.; Monien, B.; Rodríguez, M., Proc. 18th ICALP. Proc. 18th ICALP, Lecture Notes in Computer Science, Vol. 510 (1991), Springer: Springer Berlin), Report CS-R9054, 481-494 (1990), CWI: CWI Amsterdam, full version available as · Zbl 0796.68142
[11] Cleaveland, R.; Parrow, J.; Steffen, B., The concurrency workbench: a semantics-based verification tool for finite-state systems, (Report ECS-LFCS-89-83 (1989), University of Edinburgh)
[12] Darondeau, P., Concurrency and computability, (Guessarian, I., Semantics of Systems of Concurrent Processes, Proceedings LITP Spring School on Theoretical Computer Science. Semantics of Systems of Concurrent Processes, Proceedings LITP Spring School on Theoretical Computer Science, Lecture Notes in Computer Science, Vol. 469 (1990), Springer: Springer Berlin), 223-238, La Roche Posay, France
[13] De Francesco, N.; Inverardi, P., Proving finiteness of CCS processes by non-standard semantics, Acta Inform. (1992), to appear. · Zbl 0790.68066
[14] Fernandez, J.-C., Aldébaran: a tool for verification of communicating processes, (Technical report SPECTRE c14 (1989), LGI-IMAG: LGI-IMAG Grenoble)
[15] Godskesen, J. C.; Larsen, K. G.; Zeeberg, M., TAV (Tools for Automatic Verification): users manual (1988)
[16] Groote, J. F.; Vaandrager, F. W., Structured operational semantics and bisimulation as a congruence, Inform. and Comput., 100, 2, 202-260 (1992) · Zbl 0752.68053
[17] Hennessy, M., A term model for synchronous processes, Inform. and Comput., 51, 1, 58-75 (1981) · Zbl 0503.68022
[18] Hennessy, M., Algebraic Theory of Processes (1988), MIT Press: MIT Press Cambridge, MA · Zbl 0744.68047
[19] Hennessy, M.; Milner, R., Algebraic laws for nondeterminism and concurrency, J. Acm, 32, 1, 137-161 (1985) · Zbl 0629.68021
[20] Hoare, C. A.R., Communicating Sequential Processes (1985), Prentice-Hall: Prentice-Hall Englewood Cliffs, NJ · Zbl 0637.68007
[21] Keller, R. M., Formal verification of parallel programs, Comm. Acm, 19, 7, 371-384 (1976) · Zbl 0329.68016
[22] Madelaine, E.; Vergamini, D., Finiteness conditions and structural construction of automata for all process algebras, DIMACS Series in Discrete Mathematics and Theoretical Computer Science, 3, 275-292 (1991) · Zbl 0786.68065
[23] Milner, R., On relating synchrony and asynchrony, (Technical Report CSR-75-80 (1981), Department of Computer Science, University of Edinburgh)
[24] Milner, R., Calculi for synchrony and asynchrony, Theoret. Comput. Sci., 25, 267-310 (1983) · Zbl 0512.68026
[25] Milner, R., Communication and Concurrency (1989), Prentice-Hall: Prentice-Hall Englewood Cliffs, NJ · Zbl 0683.68008
[26] Milner, R.; Parrow, J.; Walker, D., A calculus of mobile processes, Inform. and Control, 100, 1, 1-77 (1992), Parts I + II · Zbl 0752.68037
[27] Parrow, J., The expressive power of parallelism, Future Generations Computer Systems, 6, 271-285 (1990)
[28] Plotkin, G. D., A structural approach to operational semantics, (Report DAIMI FN-19 (1981), Computer Science Department, Aarhus University) · Zbl 0512.68012
[29] de Simone, R., Higher-level synchronising devices in MEIJE-SCCS, Theoret. Comput. Sci., 37, 245-267 (1985) · Zbl 0598.68027
[30] de Simone, R.; Vergamini, D., Aborad AUTO, (Technical Report 111 (1989), INRIA, Centre Sophia-Antipolis: INRIA, Centre Sophia-Antipolis Valbonne)
[31] Vaandrager, F. W., On the relationship between process algebra and input/output automata (extended abstract), (Proc. 6th Ann. Symp. on Logic in Computer Science (1991), IEEE Computer Society Press: IEEE Computer Society Press Amsterdam), 387-398
[32] Vaandrager, F. W., Expressiveness results for process algebras, Proc. REX ’92 (1992), to appear
[33] Walker, D., Analysing natural exclusion algorithms using CCS, (Technical Report ECS-LFCS-88-45 (1988), Department of Computer Science, University of Edinburgh)
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.