A Specification Format for Rooted Branching Bisimulation

• Autorzy: Castiglioni V. , Lanotte R. , Tini S.

Identyfikatory

DOI

10.3233/FI-2014-1128

• Języki publikacji: EN

Abstrakty

EN

Rule formats are sets of syntactical constraints over SOS rules ensuring semantical properties of the derived LTS. Given a rule format, our proposal is to relax the constraints imposed on each single rule and to introduce some constraints on the form of the whole set of rules, thus obtaining a new format ensuring the same semantical property and being less demanding than the original one. We apply our idea to a well known rule format for rooted branching bisimulation equivalence.

Słowa kluczowe

EN

weak equivalence; rooted branching bisimulation; specification format

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2014
• Tom: Vol. 135, nr 4
• Strony: 355--369
• Opis fizyczny: Bibliogr. 23 poz.

Twórcy

autor

Castiglioni V.

• Department of Scienza e Alta Tecnologia, University of Insubria, Como, Italy

autor

Lanotte R.

• Department of Scienza e Alta Tecnologia, University of Insubria, Como, Italy

autor

Tini S.

• Department of Scienza e Alta Tecnologia, University of Insubria, Como, Italy

Bibliografia

• [1] Aceto, L., Fokkink, W. J., Verhoef, C.: Structural operational semantics, in: Handbook of Process Algebra, Elsevier, 2001, 197–292.
• [2] Baeten, J., Basten, T., Reiners, M.: Process algebra: equational theories of communicating processes, Cambridge University Press, 2009.
• [3] Basten, T.: Branching bisimilarity is an equivalence indeed!, Inform. Proc. Lett., 58(3), 1996, 141–147.
• [4] Bloom, B.: Structural operational semantics for weak bisimulations, Theoret. Comput. Sci., 146, 1995, 25-68.
• [5] Fokkink,W. J.: Rooted branching bisimulation as a congruence, J. Comput. Syst. Sci., 60(1), 2000, 13–37.
• [6] Fokkink, W. J., van Glabbeek, R. J., deWind, P.W.: Divide and Congruence: From Decomposition of Modal Formulas to Preservation of Branching and η-Bisimilarity, Inf. Comput, 214, 2012, 59–85.
• [7] Fokkink, W. J., Verhoef, C.: A conservative look at operational semantics with variable binding, Inform. Comput., 146(1), 1998, 24–54.
• [8] van Glabbeek, R. J.: The Linear Time - Branching Time Spectrum, CONCUR ’90, number 458 in LNCS, Springer, 1990.
• [9] van Glabbeek, R. J.: The Linear Time - Branching Time Spectrum II, CONCUR ’93, number 715 in LNCS, Springer, 1993.
• [10] van Glabbeek, R. J.: The Meaning of Negative Premises in Transition System Specifications II, ICALP’96, number 1099 in LNCS, Springer, 1996.
• [11] van Glabbeek, R. J.: On Cool Congruence Formats for Weak Bisimulations, Theoret. Comput. Sci., 412(28), 2011, 3283–3302.
• [12] van Glabbeek, R. J., Weijland, W. P.: Branching time and abstraction in bisimulation semantics, J. Assoc. Comput. Mach., 43(3), 1996, 555–600.
• [13] Groote, J. F.: Transition system specifications with negative premises, Theoret. Comput. Sci., 118(2), 1993,
• [14] Hennessy, M., Milner, R.: Algebraic laws for nondeterminism and concurrency, J. Assoc. Comput. Mach., 32, 1985, 137–161.
• [15] Lanotte, R., Tini, S.: Probabilistic Congruence for Semistochastic Generative Processes, FOSSACS, LNCS, Springer, 2005.
• [16] Lanotte, R., Tini, S.: Probabilistic Bisimulation as a Congruence, ACM TOCL, 10, 2009, 1–48.
• [17] Plotkin, G.: A structural approach to operational semantics, Report DAIMI FN-19, Aarhus University, 1981.
• [18] Przymusinski, T. C.: The well-founded semantics coincides with the three-valued stable semantics, Fundam. Inform., 13(4), 1990, 445–463.
• [19] de Simone, R.: Higher-level synchronising devices in Meije-SCCS, Theoret. Comput. Sci., 37, 1985, 245–267.
• [20] Tini, S.: Rule Formats for Non Interference, ESOP, LNCS, Springer, 2003.
• [21] Tini, S.: Rule format for compositional non interference properties, JLAP, 60–61, 2004, 353–400.
• [22] Tini, S.: Non Expansive epsilon-Bisimulations, AMAST, LNCS, Springer, 2008.
• [23] Tini, S.: Non-expansive Є-bisimulations for Probabilistic Processes, TCS, 411, 2010, 2202–2222.