×

Linearization in parallel pCRL. (English) Zbl 0988.68121

Summary: We describe a linearization algorithm for parallel pCRL processes similar to the one implemented in the linearizer of the \(\mu\)CRL toolset. This algorithm finds its roots in formal language theory: the ‘grammar’ defining a process is transformed into a variant of Greibach normal form. Next, any such form is further reduced to linear form, i.e., to an equation that resembles a right-linear, data-parametric grammar. We aim at proving the correctness of this linearization algorithm. To this end we define an equivalence relation on recursive specifications in \(\mu\)CRL that is model independent and does not involve an explicit notion of solution.

MSC:

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)

Software:

UNITY
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Baeten, J. C.M.; Bergstra, J. A.; Klop, J. W., Decidability of bisimulation equivalence for processes generating context-free languages, Journal of the ACM, 40, 3, 653-682 (1993) · Zbl 0801.68102
[2] 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
[3] Benson, D. B.; Guessarian, I., Algebraic solutions to recursion schemes, Journal of Computer and System Sciences, 35, 365-400 (1987) · Zbl 0637.68018
[4] Bergstra, J. A.; Klop, J. W., Process algebra for synchronous communication, Information and Computation, 60, 1/3, 109-137 (1984) · Zbl 0597.68027
[5] J.A.Bergstra,J.W.Klop,Acompleteinferencesystemforregularprocesseswithsilentmoves,in:F.R.Drake,J.K.Truss(Eds.),ProceedingsLogicColloquiumHull1986,North-Holland,Amsterdam1988,pp. 21-81. First appeared as: Report CS-R8420, CWI, Amsterdam, 1984; J.A.Bergstra,J.W.Klop,Acompleteinferencesystemforregularprocesseswithsilentmoves,in:F.R.Drake,J.K.Truss(Eds.),ProceedingsLogicColloquiumHull1986,North-Holland,Amsterdam1988,pp. 21-81. First appeared as: Report CS-R8420, CWI, Amsterdam, 1984
[6] J.A. Bergstra, A. Ponse, Translation of a muCRL-fragment to I-CRL, in: Methods for the Transformation and Analysis of CRL. Deliverable 46/SPE/WP5/DS/A/007/b1, SPECS RACE Project no. 1046, pp. 125-148, Available through GSI Tecsi, May 1991; J.A. Bergstra, A. Ponse, Translation of a muCRL-fragment to I-CRL, in: Methods for the Transformation and Analysis of CRL. Deliverable 46/SPE/WP5/DS/A/007/b1, SPECS RACE Project no. 1046, pp. 125-148, Available through GSI Tecsi, May 1991
[7] M.A. Bezem, J.F. Groote, Invariants in process algebra with data, in: B. Jonsson, J. Parrow, (Eds.), CONCUR’94, Lecture Notes in Computer Science, vol. 836, Springer, Berlin, 1994, pp. 401-416; M.A. Bezem, J.F. Groote, Invariants in process algebra with data, in: B. Jonsson, J. Parrow, (Eds.), CONCUR’94, Lecture Notes in Computer Science, vol. 836, Springer, Berlin, 1994, pp. 401-416
[8] D.J.B. Bosscher, A. Ponse, Translating a process algebra with symbolic data values to linear format, in: U.H. Engberg, K.G. Larsen,, A. Skou (Eds.), Proceedings of the Workshop on Tools and Algorithms for the Construction and Analysis of Systems, Aarhus, Denmark, volume NS-95-2 of BRICS Notes Series, Department of Computer Science, University of Aarhus, May 1995, pp. 119-130; D.J.B. Bosscher, A. Ponse, Translating a process algebra with symbolic data values to linear format, in: U.H. Engberg, K.G. Larsen,, A. Skou (Eds.), Proceedings of the Workshop on Tools and Algorithms for the Construction and Analysis of Systems, Aarhus, Denmark, volume NS-95-2 of BRICS Notes Series, Department of Computer Science, University of Aarhus, May 1995, pp. 119-130
[9] J.J. Brunekreef, Process specification in a UNITY format, in: A. Ponse, C. Verhoef, S.F.M. van Vlijmen (Eds.), Algebra of Communicating Processes, Utrecht 1994, Workshops in Computing, Springer, Berlin, 1995, pp. 319-337; J.J. Brunekreef, Process specification in a UNITY format, in: A. Ponse, C. Verhoef, S.F.M. van Vlijmen (Eds.), Algebra of Communicating Processes, Utrecht 1994, Workshops in Computing, Springer, Berlin, 1995, pp. 319-337
[10] Burris, S.; Sankappanavar, H. P., A Course in Universal Algebra, Graduate Texts in Mathematics, vol. 78 (1981), Springer: Springer Berlin · Zbl 0478.08001
[11] Chandy, K. M.; Misra, J., Parallel Program Design. A Foundation (1988), Addison-Wesley: Addison-Wesley New York · Zbl 0717.68034
[12] Courcelle, B., Equivalences and transformations of regular systems-applications to recursive program schemes and grammars, Theoretical Computer Science, 42, 1-122 (1986) · Zbl 0636.68104
[13] B. Courcelle, Recursive applicative program schemes, in: J. van Leeuwen (Ed.), Handbook of Theoretical Computer Science, vol. B, chapter 9, Elsevier, Amsterdam, 1990, pp. 459-492; B. Courcelle, Recursive applicative program schemes, in: J. van Leeuwen (Ed.), Handbook of Theoretical Computer Science, vol. B, chapter 9, Elsevier, Amsterdam, 1990, pp. 459-492 · Zbl 0900.68095
[14] Fokkink, W. J., Introduction to Process Algebra, Texts in Theoretical Computer Science. An EATCS Series (2000), Springer: Springer Berlin · Zbl 0941.68087
[15] R.J. van Glabbeek, The linear time-branching time spectrum II; the semantics of sequential systems with silent moves, Manuscript. Preliminary version available by ftp at ftp://boole.stanford.edu/pub/spectrum.ps.gz, 1993. Extended abstract, in: E. Best (Ed.), Proceedings CONCUR’93, 4th International Conference on Concurrency Theory, Hildesheim, Germany, August 1993, Lecture Notes in Computer Science, vol. 715, Springer, Berlin, pp. 66-81; R.J. van Glabbeek, The linear time-branching time spectrum II; the semantics of sequential systems with silent moves, Manuscript. Preliminary version available by ftp at ftp://boole.stanford.edu/pub/spectrum.ps.gz, 1993. Extended abstract, in: E. Best (Ed.), Proceedings CONCUR’93, 4th International Conference on Concurrency Theory, Hildesheim, Germany, August 1993, Lecture Notes in Computer Science, vol. 715, Springer, Berlin, pp. 66-81
[16] J.F. Groote, The syntax and semantics of timed μCRL, Report SEN-R9709, CWI, The Netherlands, 1997; J.F. Groote, The syntax and semantics of timed μCRL, Report SEN-R9709, CWI, The Netherlands, 1997
[17] J.F. Groote, B. Lisser, Tutorial and Reference Guide for the μCRL toolset version 1.0, CWI, 1999. Available from http://www.cwi.nl/∼mcrl/mutool.html; J.F. Groote, B. Lisser, Tutorial and Reference Guide for the μCRL toolset version 1.0, CWI, 1999. Available from http://www.cwi.nl/∼mcrl/mutool.html
[18] J.F. Groote, S.P. Luttik, Undecidability and completeness results for process algebras with alternative quantification over data, Report SEN-R9806, CWI, The Netherlands, July 1998. Available from http://www.cwi.nl/∼luttik/; submitted for publication; J.F. Groote, S.P. Luttik, Undecidability and completeness results for process algebras with alternative quantification over data, Report SEN-R9806, CWI, The Netherlands, July 1998. Available from http://www.cwi.nl/∼luttik/; submitted for publication
[19] J.F. Groote, A. Ponse, Proof theory for μCRL: a language for processes with data, in: D.J. Andrews, J.F. Groote, C.A. Middelburg (Eds.), Semantics of Specification Languages, Workshop in Computing Series, Springer, Berlin, 1994, pp. 232-251; J.F. Groote, A. Ponse, Proof theory for μCRL: a language for processes with data, in: D.J. Andrews, J.F. Groote, C.A. Middelburg (Eds.), Semantics of Specification Languages, Workshop in Computing Series, Springer, Berlin, 1994, pp. 232-251 · Zbl 0813.68135
[20] J.F. Groote, A. Ponse, The syntax and semantics of μCRL, in: A. Ponse, C. Verhoef, S.F.M. van Vlijmen (Eds.), Algebra of Communicating Processes1994, Workshop in Computing Series, Springer, Berlin, 1995, pp. 26-62; J.F. Groote, A. Ponse, The syntax and semantics of μCRL, in: A. Ponse, C. Verhoef, S.F.M. van Vlijmen (Eds.), Algebra of Communicating Processes1994, Workshop in Computing Series, Springer, Berlin, 1995, pp. 26-62
[21] J.F. Groote, J. Springintveld, Focus points and convergent process operators. A proof strategy for protocol verification, Technical Report 142, Department of Philosophy, Utrecht University, 1995. Available from ftp://ftp.phil.uu.nl/pub/logic/PREPRINTS/preprint142.ps.Z; J.F. Groote, J. Springintveld, Focus points and convergent process operators. A proof strategy for protocol verification, Technical Report 142, Department of Philosophy, Utrecht University, 1995. Available from ftp://ftp.phil.uu.nl/pub/logic/PREPRINTS/preprint142.ps.Z · Zbl 1015.68175
[22] J.F. Groote, J.J. van Wamel, Algebraic data types and induction in μCRL, Technical Report P9409, University of Amsterdam, Programming Research Group, 1994; J.F. Groote, J.J. van Wamel, Algebraic data types and induction in μCRL, Technical Report P9409, University of Amsterdam, Programming Research Group, 1994
[23] Y. Hirshfeld, F. Moller. Decidability results in automata and process theory, in: F. Moller, G. Birtwistle (Eds.), Logics for Concurrency: Structure versus Automata, Lecture Notes in Computer Science, vol. 1043, Springer, Berlin, 1996, pp. 102-148; Y. Hirshfeld, F. Moller. Decidability results in automata and process theory, in: F. Moller, G. Birtwistle (Eds.), Logics for Concurrency: Structure versus Automata, Lecture Notes in Computer Science, vol. 1043, Springer, Berlin, 1996, pp. 102-148
[24] 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 Interconection, Genève, September 1988; 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 Interconection, Genève, September 1988
[25] S. Mauw, J.C. Mulder, Regularity of BPA-systems is decidable, in: B. Jonsson, J. Parrow (Eds.), Proc. CONCUR ’94, Lecture Notes in Computer Science, vol. 836, Springer, Berlin, 1994, pp. 34-47; S. Mauw, J.C. Mulder, Regularity of BPA-systems is decidable, in: B. Jonsson, J. Parrow (Eds.), Proc. CONCUR ’94, Lecture Notes in Computer Science, vol. 836, Springer, Berlin, 1994, pp. 34-47
[26] Mauw, S.; Veltink, G. J., A process specification formalism, Fundamenta Informaticae, 13, 85-139 (1990) · Zbl 0705.68075
[27] S. Mauw, G.J. Veltink (Eds.), Algebraic Specification of Communication Protocols, Cambridge Tracts in Theoretical Computer Science, vol. 36, Cambridge University Press, Cambridge, 1993; S. Mauw, G.J. Veltink (Eds.), Algebraic Specification of Communication Protocols, Cambridge Tracts in Theoretical Computer Science, vol. 36, Cambridge University Press, Cambridge, 1993 · Zbl 0820.68078
[28] Milner, R., A complete inference system for a class of regular behaviours, Journal of Computer and System Sciences, 28, 439-466 (1984) · Zbl 0562.68065
[29] V. van Oostrom, Personal communications, 2000; V. van Oostrom, Personal communications, 2000
[30] Ponse, A., Computable processes and bisimulation equivalence, Formal Aspects of Computing, 8, 6, 648-678 (1996) · Zbl 0862.68052
[31] A. Ponse, Y.S. Usenko, Equivalence of recursive specifications in process algebra, Information Processing Letters, to appear; A. Ponse, Y.S. Usenko, Equivalence of recursive specifications in process algebra, Information Processing Letters, to appear · Zbl 1003.68088
[32] SPECS-Semantics and Analysis, Definition of MR and CRL Version 2.1. Deliverable 46/SPE/WP5/DS/A/017/b1, SPECS RACE Project no. 1046. Available through GSI Tecsi, 1990; SPECS-Semantics and Analysis, Definition of MR and CRL Version 2.1. Deliverable 46/SPE/WP5/DS/A/017/b1, SPECS RACE Project no. 1046. Available through GSI Tecsi, 1990
[33] Specification and description language (SDL). ITU-T Recommendation Z. 100, 1994; Specification and description language (SDL). ITU-T Recommendation Z. 100, 1994
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.