Abstract
Prefix iteration is a variation on the original binary version of the Kleene star operation P * Q, obtained by restricting the first argument to be an atomic action, and yields simple iterative behaviours that can be equationally characterized by means of finite collections of axioms. In this paper, we present axiomatic characterizations for a significant fragment of the notions of equivalence and preorder in van Glabbeek's linear-time/branching-time spectrum over Milner's basic CCS extended with prefix iteration. More precisely, we consider ready simulation, simulation, readiness, trace and language semantics, and provide complete (in)equational axiomatizations for each of these notions over BCCS with prefix iteration. All of the axiom systems we present are finite, if so is the set of atomic actions under consideration.
Partially supported by the Human Capital and Mobility project Express.
Supported by a grant from the Danish National Research Foundation.
Chapter PDF
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
L. Aceto, W. J. Fokkink, R. J. van Glabbeek, and A. Ingólfsdóttir, Axiomatizing prefix iteration with silent steps, Information and Computation, 127 (1996), pp. 26–40.
J. Bergstra, J. W. Klop, and E.-R. Olderog, Readies and failures in the algebra of communicating processes, SIAM J. Comput., 17 (1988), pp. 1134–1177.
B. Bloom, S. Istrail, and A. R. Meyer, Bisimulation can't be traced, J. Assoc. Comput. Mach., 42 (1995), pp. 232–268.
S. Brookes, C. Hoare, and A. Roscoe, A theory of communicating sequential processes, J. Assoc. Comput. Mach., 31 (1984), pp. 560–599.
J. H. Conway, Regular Algebra and Finite Machines, Mathematics Series (R. Brown and J. De Wet eds.), Chapman and Hall, London, United Kingdom, 1971.
W. J. Fokkink, A complete equational axiomatization for prefix iteration, Inf. Process. Lett., 52 (1994), pp. 333–337.
R. J. v. Glabbeek, The linear time — branching time spectrum, in Proceedings CONCUR 90, Amsterdam, J. Baeten and J. Klop, eds., vol. 458 of Lecture Notes in Computer Science, Springer-Verlag, 1990, pp. 278–297.
-, A complete axiomatization for branching bisimulation congruence of finite-state behaviours, in Mathematical Foundations of Computer Science 1993, Gdansk, Poland, A. Borzyszkowski and S. Sokołowski, eds., vol. 711 of Lecture Notes in Computer Science, Springer-Verlag, 1993, pp. 473–484. Available by anonymous ftp from Boole.stanford.edu.
S. Kleene, Representation of events in nerve nets and finite automata, in Automata Studies, C. Shannon and J. McCarthy, eds., Princeton University Press, 1956, pp. 3–41.
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, Cachan, France, 13–15 Feb. 1992, Springer, pp. 617–618.
R. Milner, A complete inference system for a class of regular behaviours, J. Comput. System Sci., 28 (1984), pp. 439–466.
-, Communication and Concurrency, Prentice-Hall International, Englewood Cliffs, 1989.
-, The polyadic π-calculus: a tutorial, in Proceedings Marktoberdorf Summer School '91, Logic and Algebra of Specification, NATO ASI Series F94, Springer-Verlag, 1993, pp. 203–246.
D. Park, Concurrency and automata on infinite sequences, in 5 th GI Conference, Karlsruhe, Germany, P. Deussen, ed., vol. 104 of Lecture Notes in Computer Science, Springer-Verlag, 1981, pp. 167–183.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Aceto, L., Fokkink, W., Ingólfsdóttir, A. (1998). A cook's tour of equational axiomatizations for prefix iteration. In: Nivat, M. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 1998. Lecture Notes in Computer Science, vol 1378. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0053539
Download citation
DOI: https://doi.org/10.1007/BFb0053539
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-64300-5
Online ISBN: 978-3-540-69720-6
eBook Packages: Springer Book Archive