×

Nested semantics over finite trees are equationally hard. (English) Zbl 1101.68690

Summary: This paper studies nested simulation and nested trace semantics over the language BCCSP, a basic formalism to express finite process behaviour. It is shown that none of these semantics affords finite (in)equational axiomatizations over BCCSP. In particular, for each of the nested semantics studied in this paper, the collection of sound, closed (in)equations over a singleton action set is not finitely based.

MSC:

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

References:

[1] L. Aceto, Z. Ésik, A. Ingólfsdóttir, On the two-variable fragment of the equational theory of the max-sum algebra of the natural numbers, in: H. Reichel, S. Tison (Eds.), Proceedings of the 17th International Symposium on Theoretical Aspects of Computer Science, STACS 2000 (Lille), vol. 1770 of Lecture Notes in Computer Science, Springer-Verlag, 2000, pp. 267-278; L. Aceto, Z. Ésik, A. Ingólfsdóttir, On the two-variable fragment of the equational theory of the max-sum algebra of the natural numbers, in: H. Reichel, S. Tison (Eds.), Proceedings of the 17th International Symposium on Theoretical Aspects of Computer Science, STACS 2000 (Lille), vol. 1770 of Lecture Notes in Computer Science, Springer-Verlag, 2000, pp. 267-278 · Zbl 0955.08004
[2] Aceto, L.; Ésik, Z.; Ingólfsdóttir, A., The max-plus algebra of the natural numbers has no finite equational basis, Theor. Comput. Sci., 293, 1, 169-188 (2003) · Zbl 1021.08001
[3] Aceto, L.; Fokkink, W.; Ingólfsdóttir, A., A menagerie of non-finitely based process semantics over BPA*—from ready simulation to completed traces, Math. Struct. Comput. Sci., 8, 3, 193-230 (1998) · Zbl 0917.68138
[4] L. Aceto, W. Fokkink, A. Ingólfsdóttir, 2-nested simulation is not finitely equationally axiomatizable, in: Proceedings of the 18th International Symposium on Theoretical Aspects of Computer Science, STACS 2001 (Dresden), vol. 2010 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, 2001, pp. 39-50; L. Aceto, W. Fokkink, A. Ingólfsdóttir, 2-nested simulation is not finitely equationally axiomatizable, in: Proceedings of the 18th International Symposium on Theoretical Aspects of Computer Science, STACS 2001 (Dresden), vol. 2010 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, 2001, pp. 39-50 · Zbl 0976.68111
[5] Baeten, J. C.; Bergstra, J.; Klop, J. W., Decidability of bisimulation equivalence for processes generating context-free languages, J. ACM, 40, 3, 653-682 (1993) · Zbl 0801.68102
[6] J. Bergstra, J.W. Klop, Fixed point semantics in process algebras, Report IW 206, Mathematisch Centrum, Amsterdam, 1982; J. Bergstra, J.W. Klop, Fixed point semantics in process algebras, Report IW 206, Mathematisch Centrum, Amsterdam, 1982 · Zbl 0489.68016
[7] Bergstra, J.; Klop, J. W., Process algebra for synchronous communication, Inf. Comput., 60, 1/3, 109-137 (1984) · Zbl 0597.68027
[8] S. Blom, W. Fokkink, S. Nain, On the axiomatizability of ready traces, ready simulation and failure traces, in: J.C.M. Baeten, J.K. Lenstra, J. Parrow, G.J. Woeginger (Eds.), Proceedings 30th Colloquium on Automata, Languages and Programming—ICALP’03, Eindhoven, vol. 2719 of Lecture Notes in Computer Science, Springer-Verlag, 2003, pp. 109-118; S. Blom, W. Fokkink, S. Nain, On the axiomatizability of ready traces, ready simulation and failure traces, in: J.C.M. Baeten, J.K. Lenstra, J. Parrow, G.J. Woeginger (Eds.), Proceedings 30th Colloquium on Automata, Languages and Programming—ICALP’03, Eindhoven, vol. 2719 of Lecture Notes in Computer Science, Springer-Verlag, 2003, pp. 109-118 · Zbl 1039.68081
[9] S. Christensen, Y. Hirshfeld, F. Moller, Bisimulation equivalence is decidable for basic parallel processes, in: E. Best (Ed.), Proceedings CONCUR 93, Hildesheim, Germany, vol. 715 of Lecture Notes in Computer Science, Springer-Verlag, 1993, pp. 143-157; S. Christensen, Y. Hirshfeld, F. Moller, Bisimulation equivalence is decidable for basic parallel processes, in: E. Best (Ed.), Proceedings CONCUR 93, Hildesheim, Germany, vol. 715 of Lecture Notes in Computer Science, Springer-Verlag, 1993, pp. 143-157
[10] Christensen, S.; Hüttel, H.; Stirling, C., Bisimulation equivalence is decidable for all context-free processes, Inf. Comput., 121, 2, 143-148 (1995) · Zbl 0833.68074
[11] Conway, J. H., Regular algebra and finite machines, (Brown, R.; De Wet, J., Mathematics Series (1971), Chapman and Hall: Chapman and Hall London, UK) · Zbl 0231.94041
[12] W. Fokkink, B. Luttik, An omega-complete equational specification of interleaving, in: U. Montanari, J. Rolinn, E. Welzl (Eds.), Proceedings 27th Colloquium on Automata, Languages and Programming—ICALP’00, Geneva, vol. 1853 of Lecture Notes in Computer Science, Springer-Verlag, 2000, pp. 729-743; W. Fokkink, B. Luttik, An omega-complete equational specification of interleaving, in: U. Montanari, J. Rolinn, E. Welzl (Eds.), Proceedings 27th Colloquium on Automata, Languages and Programming—ICALP’00, Geneva, vol. 1853 of Lecture Notes in Computer Science, Springer-Verlag, 2000, pp. 729-743 · Zbl 0973.68533
[13] Gischer, J. L., The equational theory of pomsets, Theor. Comput. Sci., 61, 199-224 (1988) · Zbl 0669.68015
[14] R.J. van Glabbeek, The linear time-branching time spectrum I. The semantics of concrete, sequential processes, in: Handbook of Process Algebra, North-Holland, Amsterdam, 2001, pp. 3-99; R.J. van Glabbeek, The linear time-branching time spectrum I. The semantics of concrete, sequential processes, in: Handbook of Process Algebra, North-Holland, Amsterdam, 2001, pp. 3-99 · Zbl 1035.68073
[15] J.F. Groote, A new strategy for proving \(ω\)-completeness with applications in process algebra, in: J. Baeten, J. Klop (Eds.), Proceedings CONCUR 90, Amsterdam, vol. 458 of Lecture Notes in Computer Science, Springer-Verlag, 1990, pp. 314-331; J.F. Groote, A new strategy for proving \(ω\)-completeness with applications in process algebra, in: J. Baeten, J. Klop (Eds.), Proceedings CONCUR 90, Amsterdam, vol. 458 of Lecture Notes in Computer Science, Springer-Verlag, 1990, pp. 314-331
[16] Groote, J. F.; Hüttel, H., Undecidable equivalences for basic process algebra, Inf. Comput., 115, 2, 354-371 (1994) · Zbl 0834.68069
[17] Groote, J. F.; Vaandrager, F. W., Structured operational semantics and bisimulation as a congruence, Inf. Comput., 100, 2, 202-260 (1992) · Zbl 0752.68053
[18] Hennessy, M.; Milner, R., Algebraic laws for nondeterminism and concurrency, J. ACM, 32, 1, 137-161 (1985) · Zbl 0629.68021
[19] Hoare, C., Communicating sequential processes, (McKeag, R.; Macnaghten, A., On The Construction of Programs—An Advanced Course (1980), Cambridge University Press: Cambridge University Press Cambridge), 229-254 · Zbl 0841.68042
[20] Hoare, C., Communicating Sequential Processes (1985), Prentice-Hall International: Prentice-Hall International Englewood Cliffs · Zbl 0637.68007
[21] H. Hüttel, Undecidable equivalences for basic parallel processes, in: M. Hagiya, J.C. Mitchell (Eds.), Proceedings of the International Conference on Theoretical Aspects of Computer Software (TACS’94), Sendai, Japan, April 19-22, 1994, vol. 789 of Lecture Notes in Computer Science, Springer-Verlag, 1994, pp. 454-464; H. Hüttel, Undecidable equivalences for basic parallel processes, in: M. Hagiya, J.C. Mitchell (Eds.), Proceedings of the International Conference on Theoretical Aspects of Computer Software (TACS’94), Sendai, Japan, April 19-22, 1994, vol. 789 of Lecture Notes in Computer Science, Springer-Verlag, 1994, pp. 454-464 · Zbl 0942.68635
[22] Kannellakis, P. C.; Smolka, S. A., CCS expressions, finite state processes, and three problems of equivalence, Inf. Comput., 86, 1, 43-68 (1990) · Zbl 0705.68063
[23] Keller, R., Formal verification of parallel programs, Commun. ACM, 19, 7, 371-384 (1976) · Zbl 0329.68016
[24] H. Lin, An interactive proof tool for process algebras, in: 9th Annual Symposium on Theoretical Aspects of Computer Science, vol. 577 of Lecture Notes in Computer Science, Springer, Cachan, France, 1992, pp. 617-618; H. Lin, An interactive proof tool for process algebras, in: 9th Annual Symposium on Theoretical Aspects of Computer Science, vol. 577 of Lecture Notes in Computer Science, Springer, Cachan, France, 1992, pp. 617-618
[25] Milner, R., Communication and Concurrency (1989), Prentice-Hall International: Prentice-Hall International Englewood Cliffs · Zbl 0683.68008
[26] W. Mitchell, D. Carlisle, Modal observation equivalence of processes, Technical Report UMCS-96-1-1, Manchester University, Computer Science Department, 1996; W. Mitchell, D. Carlisle, Modal observation equivalence of processes, Technical Report UMCS-96-1-1, Manchester University, Computer Science Department, 1996
[27] F. Moller, The importance of the left merge operator in process algebras, in: M. Paterson (Ed.), Proceedings 17th ICALP, Warwick, vol. 443 of Lecture Notes in Computer Science, Springer-Verlag, 1990, pp. 752-764; F. Moller, The importance of the left merge operator in process algebras, in: M. Paterson (Ed.), Proceedings 17th ICALP, Warwick, vol. 443 of Lecture Notes in Computer Science, Springer-Verlag, 1990, pp. 752-764 · Zbl 0774.68039
[28] F. Moller, The nonexistence of finite axiomatisations for CCS congruences, in: Proceedings 5th Annual Symposium on Logic in Computer Science, Philadelphia, USA, IEEE Computer Society Press, 1990, pp. 142-153; F. Moller, The nonexistence of finite axiomatisations for CCS congruences, in: Proceedings 5th Annual Symposium on Logic in Computer Science, Philadelphia, USA, IEEE Computer Society Press, 1990, pp. 142-153
[29] D. Park, Concurrency and automata on infinite sequences, in: P. Deussen (Ed.), 5th GI Conference, Karlsruhe, Germany, vol. 104 of Lecture Notes in Computer Science, Springer-Verlag, 1981, pp. 167-183; D. Park, Concurrency and automata on infinite sequences, in: P. Deussen (Ed.), 5th GI Conference, Karlsruhe, Germany, vol. 104 of Lecture Notes in Computer Science, Springer-Verlag, 1981, pp. 167-183
[30] G. Plotkin, A structural approach to operational semantics, Report DAIMI FN-19, Computer Science Department, Aarhus University, 1981; G. Plotkin, A structural approach to operational semantics, Report DAIMI FN-19, Computer Science Department, Aarhus University, 1981
[31] Redko, V., On defining relations for the algebra of regular events, Ukr. Mat. Z., 16, 120-126 (1964), (in Russian)
[32] W. Rounds, S. Brookes, Possible futures, acceptances, refusals and communicating processes, in: 22nd Annual Symposium on Foundations of Computer Science, Nashville, Tennessee, IEEE, New York, 1981, pp. 140-149; W. Rounds, S. Brookes, Possible futures, acceptances, refusals and communicating processes, in: 22nd Annual Symposium on Foundations of Computer Science, Nashville, Tennessee, IEEE, New York, 1981, pp. 140-149
[33] Sewell, P., Nonaxiomatisability of equivalences over finite state processes, Ann. Pure Appl. Logic, 90, 1-3, 163-191 (1997) · Zbl 0898.03012
[34] S.K. Shukla, D.J. Rosenkrantz, H.B. Hunt, III, R.E. Stearns, The polynomial time decidability of simulation relations for finite state processes: a HORNSAT based approach, in: Satisfiability Problem: Theory and Applications (Piscataway, NJ, 1996), vol. 35 of DIMACS Ser. Discrete Math. Theor. Comput. Sci., Am. Math. Soc., Providence, RI, 1997, pp. 603-641; S.K. Shukla, D.J. Rosenkrantz, H.B. Hunt, III, R.E. Stearns, The polynomial time decidability of simulation relations for finite state processes: a HORNSAT based approach, in: Satisfiability Problem: Theory and Applications (Piscataway, NJ, 1996), vol. 35 of DIMACS Ser. Discrete Math. Theor. Comput. Sci., Am. Math. Soc., Providence, RI, 1997, pp. 603-641 · Zbl 0891.68059
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.