×

Revisiting sequential composition in process calculi. (English) Zbl 1330.68201

Summary: The article reviews the various ways sequential composition is defined in traditional process calculi, and shows that such definitions are not optimal, thus limiting the dissemination of concurrency theory ideas among computer scientists. An alternative approach is proposed, based on a symmetric binary operator and write-many variables. This approach, which generalizes traditional process calculi, has been used to define the new LNT language implemented in the CADP toolbox. Feedback gained from university lectures and real-life case studies shows a high acceptance by computer-science students and industry engineers.

MSC:

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
PDF BibTeX XML Cite
Full Text: DOI

References:

[1] Milner, R., A calculus of communicating systems, Lecture Notes in Computer Science, vol. 92, (1980), Springer · Zbl 0452.68027
[2] Milner, R., Communication and concurrency, (1989), Prentice-Hall · Zbl 0683.68008
[3] Brookes, S. D.; Hoare, C. A.R.; Roscoe, A. W., A theory of communicating sequential processes, J. ACM, 31, 3, 560-599, (1984) · Zbl 0628.68025
[4] Hoare, C. A.R., Communicating sequential processes, (1985), Prentice-Hall · Zbl 0637.68007
[5] Roscoe, A. W., Understanding concurrent systems, Texts in Computer Science, (2010), Springer · Zbl 1211.68205
[6] Austry, D.; Boudol, G., Algèbre de processus et synchronisation, Theor. Comput. Sci., 30, 91-131, (1984) · Zbl 0533.68026
[7] Bergstra, J. A.; Klop, J. W., Algebra of communicating processes with abstraction, Theor. Comput. Sci., 37, 77-121, (1985) · Zbl 0579.68016
[8] Baeten, J.; Weijland, W., Process algebra, Cambridge Tracts in Theoretical Computer Science, vol. 18, (1990), Cambridge University Press · Zbl 0716.68002
[9] Fokkink, W., Introduction to process algebra, Texts in Theoretical Computer Science, (2000), Springer · Zbl 0941.68087
[10] ISO/IEC, LOTOS — a formal description technique based on the temporal ordering of observational behaviour, (International Standard 8807, International Organization for Standardization — Information Processing Systems — Open Systems Interconnection, Geneva, (Sep. 1989))
[11] Bolognesi, T.; Brinksma, E., Introduction to the ISO specification language LOTOS, Comput. Netw. ISDN Syst., 14, 1, 25-59, (1988)
[12] Mauw, S.; Veltink, G. J., An introduction to psfd, (Díaz, J.; Orejas, F., Proceedings of the International Joint Conference on Theory and Practice of Software Development (TAPSOFT’89), Barcelona, Spain, Lecture Notes in Computer Science, vol. 352, (1989), Springer), 272-285
[13] Mauw, S.; Veltink, G. J., A process specification formalism, Fundam. Inform., XIII, 85-139, (1990) · Zbl 0705.68075
[14] Veltink, G. J., PSF - a retrospective, Fundam. Inform., 100, 1-4, 181-227, (2010) · Zbl 1211.68274
[15] Groote, J.; Ponse, A., The syntax and semantics of \(\mu \text{CRL}\), (1990), Centrum voor Wiskunde en Informatica Amsterdam, CS-R 9076
[16] Groote, J.; Ponse, A., The syntax and semantics of \(\mu \text{CRL}\), (Ponse, A.; Verhoef, C.; Vlijmen, S., Proceedings of the 1st Workshop on the Algebra of Communicating Processes (ACP’94), Utrecht, The Netherlands, Workshops in Computing Series, (1995), Springer), 26-62
[17] Groote, J.; Mousavi, M., Modeling and analysis of communicating systems, (2014), MIT Press · Zbl 1353.68006
[18] Cleaveland, R.; Parrow, J.; Steffen, B., The concurrency workbench, (Sifakis, J., Proceedings of the 1st Workshop on Automatic Verification Methods for Finite State Systems, Grenoble, France, Lecture Notes in Computer Science, vol. 407, (1989), Springer), 24-37
[19] Cleaveland, R.; Li, T.; Sims, S., The concurrency workbench of the new century (version 1.2) - User’s manual, (Jul. 2000), State University of New York at Stony Brook
[20] Formal Systems (Europe) Ltd., Oxford University Computing Laboratory, Failures-Divergence Refinement - FDR2 User Manual, 9th edition, Oct. 2010.
[21] Gibson-Robinson, T.; Armstrong, P. J.; Boulgakov, A.; Roscoe, A. W., FDR3 - a modern refinement checker for CSP, (Ábrahám, E.; Havelund, K., Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’14), Grenoble, France, Lecture Notes in Computer Science, vol. 8413, (2014), Springer), 187-201 · Zbl 1392.68300
[22] Sun, J.; Liu, Y.; Dong, J. S., Model checking CSP revisited: introducing a process analysis toolkit, (Margaria, T.; Steffen, B., Proceedings of the 3rd International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA’08), Porto Sani, Communications in Computer and Information Science, vol. 17, (2008), Springer Greece), 307-322
[23] Shi, L.; Liu, Y.; Sun, J.; Dong, J. S.; Carvalho, G., An analytical and experimental comparison of CSP extensions and tools, (Aoki, T.; Taguchi, K., Proceedings of the 14th International Conference on Formal Engineering Methods (ICFEM’12), Kyoto, Japan, Lecture Notes in Computer Science, vol. 7635, (2012), Springer), 381-397
[24] Garavel, H.; Lang, F.; Mateescu, R.; Serwe, W., CADP 2011: a toolbox for the construction and analysis of distributed processes, Int. J. Softw. Tools Technol. Transf., 15, 2, 89-107, (2013)
[25] Dams, D.; Groote, J. F., Specification and implementation of components of a \(\mu \text{CRL}\) toolbox, Technical Report Logic Group Preprint Series, vol. 152, (Dec. 1995), Utrecht University
[26] Cranen, S.; Groote, J.; Keiren, J.; Stappers, F.; de Vink, E.; Wesselink, W.; Willemse, T., An overview of the mcrl2 toolset and its recent advances, (Piterman, N.; Smolka, S. A., Proceedings of the 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’13), Rome, Italy, Lecture Notes in Computer Science, vol. 7795, (2013), Springer), 199-213 · Zbl 1381.68198
[27] Sokolsky, O., Efficient graph-based algorithms for model checking in the modal mu-calculus, (May 1996), State University of New York at Stony Brook, Ph.D. thesis
[28] Berthomieu, B.; Bodeveix, J.-P.; Farail, P.; Filali, M.; Garavel, H.; Gaufillet, P.; Lang, F.; Vernadat, F., FIACRE: an intermediate language for model verification in the TOPCASED environment, (Laprie, J.-C., Proceedings of the 4th European Congress on Embedded Real-Time Software (ERTS’08), Toulouse, France, (2008))
[29] Garavel, H.; Palamidessi, C.; Valencia, F. D., Reflections on the future of concurrency theory in general and process calculi in particular, Proceedings of the LIX Colloquium on Emerging Trends in Concurrency Theory, Ecole Polytechnique de Paris, France, November 13-15, 2006, Electron. Notes Theor. Comput. Sci., 209, 149-164, (2008), Elsevier Science Publishers; also available as INRIA Research Report RR-6368 · Zbl 1279.68258
[30] Champelovier, D.; Clerc, X.; Garavel, H.; Guerte, Y.; McKinty, C.; Powazny, V.; Lang, F.; Serwe, W.; Smeding, G., Reference manual of the LNT to LOTOS translator (version 6.2), (Mar. 2015), INRIA/VASY and INRIA/CONVECS, 130 p
[31] Milner, R., A complete inference system for a class of regular behaviours, J. Comput. Syst. Sci., 28, 3, 439-466, (1984) · Zbl 0562.68065
[32] Janssen, W.; Poel, M.; Zwiers, J., Action systems and action refinement in the development of parallel systems - an algebraic approach, (Baeten, J. C.M.; Groote, J. F., Proceedings of the 2nd International Conference on Concurrency Theory (CONCUR’91), Amsterdam, The Netherlands, Lecture Notes in Computer Science, vol. 527, (1991), Springer), 298-316
[33] Aceto, L.; Hennessy, M., Towards action-refinement in process algebras, Inf. Comput., 103, 2, 204-269, (1993) · Zbl 0779.68028
[34] Aceto, L.; Hennessy, M., Adding action refinement to a finite process algebra, Inf. Comput., 115, 2, 179-247, (1994) · Zbl 0834.68077
[35] Goltz, U.; Gorrieri, R.; Rensink, A., Comparing syntactic and semantic action refinement, Inf. Comput., 125, 2, 118-143, (1996) · Zbl 0853.68129
[36] Gehrke, T.; Rensink, A., Process creation and full sequential composition in a name-passing calculus, (Proceedings of the 4th Workshop on Expressiveness in Concurrency (EXPRESS’97), Santa Margherita Ligure, Italy, Electron. Notes Theor. Comput. Sci., vol. 7, (1997)), 141-160 · Zbl 0911.68054
[37] Gorrieri, R.; Rensink, A., Action refinement, (Bergstra, J.; Ponse, A.; Smolka, S., Handbook of Process Algebra, (2001), North-Holland), 1047-1147, Ch. 16 · Zbl 1035.68068
[38] Brinksma, E., On the design of extended LOTOS — a specification language for open distributed systems, (Nov. 1988), University of Twente, Ph.D. thesis
[39] Garavel, H., A wish List for the behaviour part of E-LOTOS, (Dec. 1995), Input Document [LG5] to the ISO/IEC, JTC1/SC21/WG7 Meeting on Enhancements to LOTOS, Liège, Belgium, available from
[40] Koymans, C.; Vrancken, J., Extending process algebra with the empty process, Logic Group Preprint Series, CIF, vol. 1, (1985), Department of Philosophy, Utrecht University
[41] Vrancken, J., The algebra of communicating processes with empty process, Theor. Comput. Sci., 177, 2, 287-328, (1997) · Zbl 0901.68112
[42] Bergstra, J.; Fokkink, W.; Ponse, A., Process algebra with recursive operations, (Bergstra, J. A.; Ponse, A.; Smolka, S. A., Handbook of Process Algebra, (2001), North-Holland), 333-389, Ch. 5 · Zbl 1027.68091
[43] Bergstra, J. A.; Klop, J. W., The algebra of recursively defined processes and the algebra of regular processes, (Paredaens, J., Proceedings of the 11th Colloquium on Automata, Languages and Programming (ICALP’84), Antwerp, Belgium, Lecture Notes in Computer Science, vol. 172, (1984), Springer), 82-94 · Zbl 0561.68019
[44] Baeten, J. C.M.; Bergstra, J. A., On sequential composition, action prefixes and process prefixes, Form. Asp. Comput., 6, 3, 250-268, (1994) · Zbl 0942.68608
[45] Garavel, H., On the introduction of gate typing in E-LOTOS, (Dembinski, P.; Sredniawa, M., Proceedings of the 15th IFIP International Workshop on Protocol Specification, Testing and Verification (PSTV’95), Warsaw, Poland, (1995), Chapman & Hall), 283-298
[46] Baeten, J. C.M.; van Glabbeek, R. J., Merge and termination in process algebra, (Nori, K. V., Proceedings of the 7th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS’87), Pune, India, Lecture Notes in Computer Science, vol. 287, (1987), Springer), 153-172 · Zbl 0636.68024
[47] Groote, J. F.; Vaandrager, F. W., Structural operational semantics and bisimulation as a congruence (extended abstract), (Ausiello, G.; Dezani-Ciancaglini, M.; Ronchi Della Rocca, S., Proceedings of the 16th International Colloquium on Automata, Languages and Programming (ICALP’89), Stresa, Italy, Lecture Notes in Computer Science, vol. 372, (1989), Springer), 423-438
[48] Bloom, B.; Fokkink, W.; van Glabbeek, R. J., Precongruence formats for decorated trace preorders, (Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science (LICS’00), (2000), IEEE Computer Society Santa Barbara, CA, USA), 107-118
[49] D’Argenio, P. R.; Verhoef, C., A general conservative extension theorem in process algebras with inequalities, Theor. Comput. Sci., 177, 2, 351-380, (1997) · Zbl 0901.68111
[50] Groote, J. F.; Ponse, A., Process algebra with guards: combining Hoare logic with process algebra (extended abstract), (Baeten, J. C.M.; Groote, J. F., Proceedings of the 2nd International Conference on Concurrency Theory (CONCUR’91), Amsterdam, The Netherlands, Lecture Notes in Computer Science, vol. 527, (1991), Springer), 235-249
[51] Groote, J. F.; Ponse, A., Process algebra with guards: combining Hoare logic with process algebra, Form. Asp. Comput., 6, 2, 115-164, (1994) · Zbl 0806.68078
[52] Ponse, A., Process algebra and dynamic logic, (van Eijck, J.; Visser, A., Logic and Information Flow, (1994), MIT Press), 125-148
[53] Baeten, J. C.M.; Bos, V., Formalizing programming variables in process algebra, (Dec. 2002), Turku Centre for Computer Science Turku, Finland, TUCS Technical Report 493
[54] Weichert, M., Algebra of broadcasting systems: value passing, sequential composition, and fork, (Engberg, U. H.; Larsen, K. G.; Mosses, P. D., Proceedings of the 6th Nordic Workshop on Programming Theory, Aarhus, Denmark, BRICS Note Series NS-94-6, (1994)), 428-443
[55] ISO/IEC, Enhancements to LOTOS (E-LOTOS), International Standard 15437:2001, International Organization for Standardization — Information Technology, Geneva, Sep. 2001.
[56] H. Garavel, M. Sighireanu, French-Romanian Integrated Proposal for the User Language of E-LOTOS, Rapport SPECTRE 96-05, VERIMAG, Grenoble, Input Document [KC3] to the ISO/IEC JTC1/SC21/WG7 Meeting on Enhancements to LOTOS (1.21.20.2.3), Kansas City, Missouri, USA, May, 12-21, 1996.
[57] Garavel, H.; Sighireanu, M., Towards a second generation of formal description techniques - rationale for the design of E-LOTOS, (Groote, J.-F.; Luttik, B.; Wamel, J., Proceedings of the 3rd International Workshop on Formal Methods for Industrial Critical Systems (FMICS’98), Amsterdam, The Netherlands, (1998), CWI Amsterdam), 187-230, invited lecture
[58] Garavel, H.; Lang, F.; Mateescu, R., Compiler construction using LOTOS NT, (Horspool, N., Proceedings of the 11th International Conference on Compiler Construction (CC’02), Grenoble, France, Lecture Notes in Computer Science, vol. 2304, (2002), Springer), 9-13 · Zbl 1051.68658
[59] Hoare, C. A.R., Communicating sequential processes, Commun. ACM, 21, 8, 666-677, (1978) · Zbl 0383.68028
[60] Hoare, C. A.R., The transputer and OCCAM: a personal story, Concurrency, 3, 4, 249-264, (1991)
[61] May, D., Occam, SIGPLAN Not., 18, 4, 69-79, (1983)
[62] INMOS Limited, OCCAM 2 reference manual, International Series in Computer Science, (1988), Prentice-Hall
[63] Jones, G.; Goldsmith, M., Programming in OCCAM2, (1988), Prentice-Hall, out of print; web edition available from
[64] INMOS Limited, OCCAM 2.1 reference manual, (May 1995), SGS-THOMSON Microelectronics Ltd
[65] G. Barrett, OCCAM 3 Reference Manual, Mar. 1992, iNMOS Limited, Draft.
[66] Roscoe, A. W., Denotational semantics for OCCAM, (Brookes, S. D.; Roscoe, A. W.; Winskel, G., Proceedings of the Seminar on Concurrency, Carnegie-Mellon University, Pittsburgh, PA, USA, Lecture Notes in Computer Science, vol. 197, (1984), Springer), 306-329 · Zbl 0565.68024
[67] Goldsmith, M. H.; Roscoe, A. W.; Scott, B. G.O., Denotational semantics for OCCAM2, (Jun. 1993), Oxford University Computing Laborator, Technical Monography PRG-108
[68] Roscoe, A. W.; Hoare, C., The laws of OCCAM programming, Theor. Comput. Sci., 60, 177-229, (1988) · Zbl 0719.68039
[69] Gurevich, Y.; Moss, L. S., Algebraic operational semantics and OCCAM, (Börger, E.; Büning, H. K.; Richter, M. M., Proceedings of the 3rd Workshop on Computer Science Logic (CSL’89), Kaiserslautern, Germany, Lecture Notes in Computer Science, vol. 440, (1989), Springer), 176-192 · Zbl 0925.68302
[70] Camilleri, J., An operational semantics for OCCAM, Int. J. Parallel Program., 18, 5, 365-400, (1989) · Zbl 0701.68072
[71] Barrett, G., The semantics of priority and fairness in OCCAM, (Main, M. G.; Melton, A.; Mislove, M. W.; Schmidt, D. A., Proceedings of 5th International Conference on the Mathematical Foundations of Programming Semantics (MFPS’89), Tulane University, New Orleans, LA, USA, Lecture Notes in Computer Science, vol. 442, (1989), Springer), 194-208
[72] Martin, A. J., Compiling communicating processes into delay-insensitive VLSI crcuits, Distrib. Comput., 1, 4, 226-234, (1986) · Zbl 0643.94039
[73] Garavel, H.; Salaün, G.; Serwe, W., On the semantics of communicating hardware processes and their translation into LOTOS for the verification of asynchronous circuits with CADP, Sci. Comput. Program., 74, 3, 100-127, (2009) · Zbl 1160.68465
[74] D’Argenio, P. R.; Hermanns, H.; Katoen, J.; Klaren, R., Modest - a modelling and description language for stochastic timed systems, (Proceedings of the Joint International Workshop on Process Algebra and Probabilistic Methods, Performance Modeling and Verification (PAPM-PROBMIV’01), Aachen, Germany, (2001)), 87-104 · Zbl 1007.68518
[75] Bohnenkamp, H.; d’Argenio, Pedro R.; Hermanns, H.; Katoen, J.-P., Modest: a compositional modeling formalism for real-time and stochastic systems, IEEE Trans. Softw. Eng., 32, 10, 812-830, (2006)
[76] Hahn, E.; Hartmanns, A.; Hermanns, H.; Katoen, J., A compositional modelling and analysis framework for stochastic hybrid systems, Form. Methods Syst. Des., 43, 2, 191-232, (2013) · Zbl 1291.68293
[77] Bos, V.; Kleijn, J. J.T., Redesign of a systems engineering language: formalisation of χ, Form. Asp. Comput., 15, 4, 370-389, (2003) · Zbl 1093.68597
[78] Schiffelers, R. R.H.; van Beek, D. A.; Man, K. L.; Reniers, M. A.; Rooda, J. E., Formal semantics of hybrid chi, (Larsen, K. G.; Niebert, P., Proceedings of the 1st International Workshop on Formal Modeling and Analysis of Timed Systems (FORMATS’03), Marseille, France, Lecture Notes in Computer Science, vol. 2791, (2003), Springer), 151-165 · Zbl 1099.68651
[79] van Beek, D. A.; Man, K. L.; Reniers, M. A.; Rooda, J. E.; Schiffelers, R. R.H., Syntax and consistent equation semantics of hybrid chi, J. Log. Algebr. Program., 68, 1-2, 129-210, (2006) · Zbl 1088.68111
[80] Fehnker, A.; Glabbeek, R.; Höfner, P.; McIver, A.; Portmann, M.; Tan, W. L., A process algebra for wireless mesh networks, (Seidl, H., Proceedings of the 21st European Symposium on Programming (ESOP’12), Tallinn, Estonia, Lecture Notes in Computer Science, vol. 7211, (2012), Springer), 295-315 · Zbl 1352.68183
[81] Parrow, J.; Victor, B., The update calculus (extended abstract), (Johnson, M., Proceedings of the 6th International Conference on Algebraic Methodology and Software Technology (AMAST’97), Sydney, Australia, Lecture Notes in Computer Science, vol. 1349, (1997), Springer), 409-423
[82] Ross, D. T., Uniform referents: an essential property for a software engineering language, (Tou, J., Software Engineering, vol. 1, (1970), Academic Press), 91-101
[83] Bos, V.; Kleijn, J. J.T., Formal specification and analysis of industrial systems, (Mar. 2002), Eindhoven University of Technology, Ph.D. thesis
[84] Garavel, H.; Sighireanu, M., On the introduction of exceptions in LOTOS, (Gotzhein, R.; Bredereke, J., Proceedings of the IFIP Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols, and Protocol Specification, Testing, and Verification (FORTE/PSTV’96), Kaiserslautern, Germany, (1996), Chapman & Hall), 469-484
[85] Strom, R. E.; Yemini, S., Typestate: a programming language concept for enhancing software reliability, IEEE Trans. Softw. Eng., 12, 1, 157-171, (1986) · Zbl 0575.68036
[86] Garavel, H.; Sifakis, J., Compilation and verification of LOTOS specifications, (Logrippo, L.; Probert, R. L.; Ural, H., Proceedings of the 10th IFIP International Symposium on Protocol Specification, Testing and Verification (PSTV’90), Ottawa, Canada, (1990), North-Holland), 379-394
[87] Groote, J. F.; Ponse, A.; Usenko, Y. S., Linearization in parallel pcrl, J. Log. Algebr. Program., 48, 1-2, 39-70, (2001) · Zbl 0988.68121
[88] Berthomieu, B.; Le Sergent, T., Programming with behaviors in an ML framework - the syntax and semantics of LCS, (Sannella, D., Proceedings of the 5th European Symposium on Programming Languages and Systems (ESOP’94), Edinburgh, UK, Lecture Notes in Computer Science, vol. 788, (1994), Springer), 89-104
[89] Roscoe, A. W.; Hoare, C.; Bird, R., The theory and practice of concurrency, (1997), Prentice-Hall
[90] Garavel, H.; Sighireanu, M., A graphical parallel composition operator for process algebras, (Wu, J.; Gao, Q.; Chanson, S. T., Proceedings of the IFIP Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols, and Protocol Specification, Testing, and Verification (FORTE/PSTV’99), Beijing, China, (1999), Kluwer Academic Publishers), 185-202 · Zbl 0952.68097
[91] Plotkin, G., A structural approach to operational semantics, (1981), Computer Science Department, Aarhus University Denmark, Technical Report DAIMI FN-19
[92] Plotkin, G. D., A structural approach to operational semantics, J. Log. Algebr. Program., 60-61, 17-139, (2004) · Zbl 1082.68062
[93] Plotkin, G., An operational semantics for CSP, (Salwicki, A., Proceedings of the 1980 Conference on Logics of Programs and Their Applications, Poznan, Poland, Lecture Notes in Computer Science, vol. 148, (1983), Springer), 250-252, extended version available from · Zbl 0512.68012
[94] Plotkin, G. D., The origins of structural operational semantics, J. Log. Algebr. Program., 60-61, 3-15, (2004) · Zbl 1072.68063
[95] B. Bloom, F. Vaandrager, SOS rule formats for parameterized and state-bearing processes, Unpublished manuscript available from http://www.cs.ru.nl/ita/publications/papers/fvaan/bardfrits.ps, Jul. 1994.
[96] Mousavi, M.; Reniers, M. A.; Groote, J., Congruence for SOS with data, (Proceedings of the 19th IEEE Symposium on Logic in Computer Science (LICS’04), Turku, Finland, (2004), IEEE Computer Society), 303-312
[97] Mousavi, M.; Reniers, M. A.; Groote, J., Notions of bisimulation and congruence formats for SOS with data, Inf. Comput., 200, 1, 107-147, (2005) · Zbl 1082.68075
[98] Gebler, D.; Goriac, E.; Mousavi, M., Algebraic meta-theory of processes with data, (Borgström, J.; Luttik, B., Proceedings of the Combined 20th International Workshop on Expressiveness in Concurrency and 10th Workshop on Structural Operational Semantics (EXPRESS/SOS’13), Buenos Aires, Argentina, Electronic Proceedings in Theoretical Computer Science, vol. 120, (2013)), 63-77
[99] De Nicola, R.; Labella, A., A completeness theorem for nondeterministic Kleene algebras, (Prívara, I.; Rovan, B.; Ruzicka, P., Proceedings of the 19th International Symposium on Mathematical Foundations of Computer Science (MFCS’94), Kosice, Slovakia, Lecture Notes in Computer Science, vol. 841, (1994), Springer), 536-545
[100] Corradini, F.; De Nicola, R.; Labella, A., Fully abstract models for nondeterministic regular expressions, (Lee, I.; Smolka, S. A., Proceedings of the 6th International Conference on Concurrency Theory (CONCUR’95), Philadelphia, PA, USA, Lecture Notes in Computer Science, vol. 962, (1995), Springer), 130-144
[101] Corradini, F.; De Nicola, R.; Labella, A., Models of nondeterministic regular expressions, J. Comput. Syst. Sci., 59, 3, 412-449, (1999) · Zbl 0958.68090
[102] Baeten, J. C.M.; Corradini, F., Regular expressions in process algebra, (Proceedings of the 20th IEEE Symposium on Logic in Computer Science (LICS’05), Chicago, IL, USA, (2005), IEEE Computer Society), 12-19
[103] Baeten, J. C.M.; Corradini, F.; Grabmayer, C., A characterization of regular expressions under bisimulation, J. ACM, 54, 2, (2007) · Zbl 1292.68102
[104] Dijkstra, E. W., Guarded commands, non-determinacy and formal derivation of programs, Commun. ACM, 18, 8, 453-457, (1975) · Zbl 0308.68017
[105] Garavel, H.; Lang, F., NTIF: a general symbolic model for communicating sequential processes with data, (Peled, D.; Vardi, M., Proceedings of the 22nd IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems (FORTE’02), Houston, TX, USA, Lecture Notes in Computer Science, vol. 2529, (2002), Springer), 276-291, full version available as INRIA Research Report RR-4666 · Zbl 1037.68556
[106] Lantreibecq, E.; Serwe, W., Model checking and co-simulation of a dynamic task dispatcher circuit using CADP, (Salaün, G.; Schätz, B., Proceedings of the 16th International Workshop on Formal Methods for Industrial Critical Systems (FMICS’11), Trento, Italy, Lecture Notes in Computer Science, vol. 6959, (2011), Springer), 180-195
[107] Hennessy, M., A proof system for communicating processes with value-passing (extended abstract), (Madhavan, C. E.V., Proceedings of the 9th Conference on the Foundations of Software Technology and Theoretical Computer Science (FSTTCS’89), Bangalore, India, Lecture Notes in Computer Science, vol. 405, (1989), Springer), 325-339 · Zbl 0729.68020
[108] Hennessy, M., A proof sustem for communicating processes with value-passing, Form. Asp. Comput., 3, 4, 346-366, (1991) · Zbl 0736.68057
[109] Hennessy, M.; Ingólfsdóttir, A., A theory of communicating processes with value-passing, (Paterson, M., Proceedings of the 17th International Colloquium on Automata, Languages and Programming (ICALP’90), Warwick University, England, Lecture Notes in Computer Science, vol. 443, (1990), Springer), 209-219 · Zbl 0765.68105
[110] Hennessy, M.; Ingólfsdóttir, A., A theory of communicating processes with value passing, Inf. Comput., 107, 2, 202-236, (1993) · Zbl 0794.68098
[111] Hennessy, M.; Lin, H., Proof systems for message-passing process algebras, Form. Asp. Comput., 8, 4, 379-407, (1996) · Zbl 0857.68040
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.