A Cancellation Theorem for BCCSP

• Autorzy: Aceto L. , Fokkink W. , Ingolfsdottir A.
• Języki publikacji: EN

Abstrakty

EN

This paper presents a cancellation theorem for the preorders in van Glabbeek's linear time-branching time spectrum over BCCSP. Apart from having some intrinsic interest, the proven cancellation result plays a crucial role in the study of the cover equations, in the sense of Fokkink and Nain, that characterize the studied semantics. The techniques used in the proof of the cancellation theorem may also have some independent interest.

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2008
• Tom: Vol. 88, nr 1-2
• Strony: 1--21
• Opis fizyczny: bibliogr. 14 poz.

Twórcy

autor

Aceto L.

autor

Fokkink W.

autor

Ingolfsdottir A.

• Vrije Universiteit Amsterdam, Department of Computer Science, De Boelelaan 1081a, 1081 HV Amsterdam, The Netherlands,

Bibliografia

• [1] L. Aceto, W. Fokkink, R.J. van Glabbeek, and A. Ingolfsdottir. Nested semantics over finite trees are equationally hard. Information and Computation, 191(2):203-232, 2004.
• [2] L. Aceto, W. Fokkink, and A. Ingolfsdottir. A menagerie of non-finitely based process semantics over BPA*-from ready simulation to completed traces. Mathematical Structures in Computer Science, 8(3):193-230, 1998.
• [3] L. Aceto, W. Fokkink, and A. Ingolfsdottir. Ready to preorder: Get your BCCSP axiomatization for free! In Proc. CALCO'07, LNCS 4624, pp. 65-79. Springer, 2007.
• [4] L. Aceto, W. Fokkink, and A. Ingolfsdottir. A cancellation theorem for BCCSP. BRICS Report RS-07-17, Aalborg University, December 2007. http://www.ru.is/faculty/luca/PAPERS/cancellation.pdf.
• [5] S. Blom, W. Fokkink, and S. Nain. On the axiomatizability of ready traces, ready simulation and failure traces. In Proc. ICALP'03, LNCS 2719, pp. 109-118. Springer, 2003.
• [6] T. Chen, W. Fokkink, B. Luttik, and S. Nain. On finite alphabets and infinite bases. Information and Computation, 206(5):492-519, 2008.
• [7] W. Fokkink and S. Nain. On finite alphabets and infinite bases: from ready pairs to possible worlds. In Proc. FoSSaCS'04, LNCS 2987, pp. 182-194. Springer, 2004.
• [8] W. Fokkink and S. Nain. A finite basis for failure semantics. In Proc. ICALP'05, LNCS 3580, pp. 755-765. Springer, 2005.
• [9] R.J. van Glabbeek. The linear time-branching time spectrum I. The semantics of concrete, sequential processes. In J.A. Bergstra, A. Ponse, and S.A. Smolka, eds, Handbook of Process Algebra, pp. 3-99. Elsevier, 2001.
• [10] J.F. Groote. A new strategy for proving !-completeness with applications in process algebra. In Proc. CONCUR' 90, LNCS 458, pp. 314-331. Springer, 1990.
• [11] M.C.B. Hennessy and R. Milner. Algebraic laws for nondeterminism and concurrency. Journal of the ACM, 32(1):137-161, 1985.
• [12] C.A.R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985.
• [13] R. Milner. Communication and Concurrency. Prentice-Hall, 1989.
• [14] F. Moller. Axioms for Concurrency. PhD thesis, Department of Computer Science, University of Edinburgh, July 1989. Report CST-59-89. Also published as ECS-LFCS-89-84.