Abstract
Regular expressions and Kleene Algebras have been a direct inspiration for many constructs and axiomatizations for concurrency models. These, however, put a different stress on nondeterminism. With concurrent interpretations in mind, we study the effect of removing the idempotence law X+X=X and distribution law X·(Y+Z)=X·Y +X·Z from Kleene Algebras. We propose an operational semantics that is sound and complete w.r.t. the new set of axioms and is fully abstract w.r.t. a denotational semantic based on trees. The operational semantics is based on labelled transition systems that keep track of the performed choices and on a preorder relation (we call it resource simulation) that takes also into account the number of states reachable via every action.An important property we exhibit is that resource bisimulation equivalence can be obtained as the kernel of resource simulation.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Baeten,J.C.M., Bergstra,J.A.: Process Algebra with a Zero Object. In Proc. Concur'90, Springer-Verlag LNCS 458 (1990) 83–98.
Bergstra,J.A., Klop,J.W.: Process Theory based on Bisimulation Semantics. In LNCS 354 (1989) 50–122.
Baeten,J., Weijland, P.: Process Algebras. Cambridge University Press (1990).
De Nicola,R., Labella,A.: A Functorial Assessment of Bisimulation. Internal Report, Università di Roma “La Sapienza”, SI-92-06 (1992).
De Nicola,R., Labella,A.: A Completeness Theorem for Nondeterministic Kleene Algebras. In Proc. MFCS'94, Springer-Verlag LNCS 841 (1994) 536–545.
Hennessy,M., Milner,R.: Algebraic Laws for Nondeterminism and Concurrency. Journal of ACM 32 (1985) 137–161.
Hoare, C.A.R.: Communicating Sequential Processes. Prentice Hall (1989).
Kleene,S.C.: Representation of Events in Nerve Nets and Finite Automata. Automata Studies (Shannon and McCarthy ed.) Princeton Univ. Pr. (1956) 3–41.
Kozen,D.: A Completeness Theorem for Kleene Algebras and the Algebra of Regular Events. Information and Computation 110 (1994) 366–390.
Milner,R.: Communication and Concurrency. Prentice Hall (1989).
Park,D.: Concurrency and Automata on Infinite sequences. In Proc. GI, LNCS 104 (1981) 167–183.
Salomaa,A.: Two Complete Axiom Systems for the Algebra of Regular Events. Journal of ACM 13 (1966) 158–169.
Smith,M.B., Plotkin,G.D.: The category-Theoretic Solution of Recursive Domain Equation. SIAM Journal on Computing 11 (1982) 762–783.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Corradini, F., De Nicola, R., Labella, A. (1995). Fully abstract models for nondeterministic regular expressions. In: Lee, I., Smolka, S.A. (eds) CONCUR '95: Concurrency Theory. CONCUR 1995. Lecture Notes in Computer Science, vol 962. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60218-6_10
Download citation
DOI: https://doi.org/10.1007/3-540-60218-6_10
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-60218-7
Online ISBN: 978-3-540-44738-2
eBook Packages: Springer Book Archive