Hostname: page-component-586b7cd67f-g8jcs Total loading time: 0 Render date: 2024-11-22T06:20:49.909Z Has data issue: false hasContentIssue false
  • English
  • Français

Proving the validity of equations in GSOS languages using rule-matching bisimilarity

Published online by Cambridge University Press:  28 February 2012

LUCA ACETO ,
MATTEO CIMINI  and
ANNA INGOLFSDOTTIR
LUCA ACETO
Affiliation:
School of Computer Science, Reykjavik University, Menntavegur 1, Nauthólsvík, IS-101 Reykjavík, Iceland Email: [email protected], [email protected], [email protected]
MATTEO CIMINI
Affiliation:
School of Computer Science, Reykjavik University, Menntavegur 1, Nauthólsvík, IS-101 Reykjavík, Iceland Email: [email protected], [email protected], [email protected]
ANNA INGOLFSDOTTIR
Affiliation:
School of Computer Science, Reykjavik University, Menntavegur 1, Nauthólsvík, IS-101 Reykjavík, Iceland Email: [email protected], [email protected], [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

This paper presents a bisimulation-based method for establishing the soundness of equations between terms constructed using operations whose semantics are specified by rules in the GSOS format of Bloom, Istrail and Meyer. The method is inspired by de Simone's FH-bisimilarity and uses transition rules as schematic transitions in a bisimulation-like relation between open terms. The soundness of the method is proved and examples showing its applicability are provided. The proposed bisimulation-based proof method is incomplete, but we do offer some completeness results for restricted classes of GSOS specifications. An extension of the proof method to the setting of GSOS languages with predicates is also offered.

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 22 , Special Issue 2: Express '09, Ice '09 and Sos '09 , April 2012 , pp. 291 - 331
Copyright
Copyright © Cambridge University Press 2012

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Aceto, L., Birgisson, A., Ingolfsdottir, A., Mousavi, M. and Reniers, M. (2010) Rule formats for determinism and idempotence. In: Arbab, F. and Sirjani, M. (eds.) Fundamentals of Software Engineering, Third IPM International Conference, FSEN 2009, Revised Selected Papers. Springer-Verlag Lecture Notes in Computer Science 5961 146–161.CrossRefGoogle Scholar
Aceto, L., Bloom, B. and Vaandrager, F. (1994) Turning SOS rules into equations. Information and Computation 111 (1)1–52.CrossRefGoogle Scholar
Aceto, L., Cimini, M. and Ingolfsdottir, A. (2010a) A bisimulation-based method for proving the validity of equations in GSOS languages. In: Klin, B. and Sobocinski, P. (eds.) Proceedings Sixth Workshop on Structural Operational Semantics (SOS 2009). Electronic Proceedings in Theoretical Computer Science 18 1–16.CrossRefGoogle Scholar
Aceto, L., Fokkink, W., Ingolfsdottir, A. and Luttik, B. (2005) Finite equational bases in process algebra: Results and open questions. In: Middeldorp, A., van Oostrom, V., van Raamsdonk, F. and de Vrijer, R. C. (eds.) Processes, Terms and Cycles: Steps on the Road to Infinity, Essays Dedicated to Jan Willem Klop, on the Occasion of His 60th Birthday. Springer-Verlag Lecture Notes in Computer Science 3838 338–367.CrossRefGoogle Scholar
Aceto, L., Fokkink, W., Ingolfsdottir, A. and Luttik, B. (2009) A finite equational base for CCS with left merge and communication merge. ACM Transactions on Compututational Logic 10 (1).Google Scholar
Aceto, L., Fokkink, W. and Verhoef, C. (2001) Structural operational semantics. In: Bergstra, J., Ponse, A. and Smolka, S. A. (eds.) Handbook of Process Algebra, Elsevier 197–292.CrossRefGoogle Scholar
Aceto, L., Ingolfsdottir, A., Luttik, B. and van Tilburg, P. (2008) Finite equational bases for fragments of CCS with restriction and relabelling. In: Ausiello, G., Karhumäki, J., Mauri, G. and Ong, C.-H. L. (eds.) Fifth IFIP International Conference On Theoretical Computer Science – TCS 2008. IFIP 273 317–332.Google Scholar
Aceto, L., Ingolfsdottir, A., Mousavi, M. and Reniers, M. (2010b) A rule format for unit elements. In: van Leeuwen, J., Muscholl, A., Peleg, D., Pokorný, J. and Rumpe, B. (eds.) Proceedings SOFSEM 2010: Theory and Practice of Computer Science, 36th Conference on Current Trends in Theory and Practice of Computer Science. Springer-Verlag Lecture Notes in Computer Science 5901 141–152.CrossRefGoogle Scholar
Baeten, J. and Bergstra, J. (1990) Process algebra with a zero object. In: Baeten, J. C. M. and Klop, J. W. (eds.) Proceedings CONCUR 90. Springer-Verlag Lecture Notes in Computer Science 458 83–98.CrossRefGoogle Scholar
Baeten, J. and de Vink, E. P. (2004) Axiomatizing GSOS with termination. Journal of Logic and Algebraic Programming 60–61 323–351.CrossRefGoogle Scholar
Baeten, J. and Vaandrager, F. (1992) An algebra for process creation. Acta Informatica 29 (4)303–334.CrossRefGoogle Scholar
Baeten, J. and Weijland, P. (1990) Process Algebra, Cambridge Tracts in Theoretical Computer Science 18, Cambridge University Press.CrossRefGoogle Scholar
Bloom, B., Fokkink, W. and van Glabbeek, R. (2004) Precongruence formats for decorated trace semantics. ACM Transactions on Computational Logic 5 (1)26–78.CrossRefGoogle Scholar
Bloom, B., Istrail, S. and Meyer, A. (1995) Bisimulation can't be traced. Journal of the ACM 42 (1)232–268.CrossRefGoogle Scholar
Bruni, R., de Frutos-Escrig, D., Martí-Oliet, N. and Montanari, U. (2000) Bisimilarity congruences for open terms and term graphs via tile logic. In: Palamidessi, C. (ed.) CONCUR 2000 – Concurrency Theory, 11th International Conference, Proceedings. Springer-Verlag Lecture Notes in Computer Science 1877 259–274.CrossRefGoogle Scholar
Cranen, S., Mousavi, M. and Reniers, M. (2008) A rule format for associativity. In: van Breugel, F. and Chechik, M. (eds.) Proceedings of CONCUR 2008 – Concurrency Theory, 19th International Conference. Springer-Verlag Lecture Notes in Computer Science 5201 447–461.CrossRefGoogle Scholar
Doumenc, G., Madelaine, E. and de Simone, R. (1990) Proving process calculi translations in ECRINS. Technical Report RR1192, INRIA.Google Scholar
Fokkink, W., van Glabbeek, R. and de Wind, P. (2006) Compositionality of Hennessy–Milner logic by structural operational semantics. Theoretical Computer Science 354 (3)421–440.CrossRefGoogle Scholar
Fokkink, W. and Verhoef, C. (1998) A conservative look at operational semantics with variable binding. Information and Computation 146 (1)24–54.CrossRefGoogle Scholar
van Glabbeek, R. (2001) The linear time–branching time spectrum. I. The semantics of concrete, sequential processes. In: Bergstra, J., Ponse, A. and Smolka, S. A. (eds.) Handbook of Process Algebra, Elsevier 3–99.CrossRefGoogle Scholar
Groote, J. F. and Vaandrager, F. (1992) Structured operational semantics and bisimulation as a congruence. Information and Computation 100 (2)202–260.CrossRefGoogle Scholar
Hennessy, M. (1988) Algebraic Theory of Processes, MIT Press.Google Scholar
Hennessy, M. and Milner, R. (1985) Algebraic laws for nondeterminism and concurrency. Journal of the ACM 32 (1)137–161.CrossRefGoogle Scholar
Hoare, C. A. R. (1985) Communicating Sequential Processes. Prentice-Hall International. (Available at http://www.usingcsp.com/cspbook.pdf.)Google Scholar
Hoare, C. A. R. et al. (1987) Laws of programming. Communications of the ACM 30 (8)672–686.CrossRefGoogle Scholar
Larsen, K. G. and Liu, X. (1991) Compositionality through an operational semantics of contexts. Journal of Logic and Computation 1 (6)761–795.CrossRefGoogle Scholar
Madelaine, E. and Vergamini, D. (1991) Finiteness conditions and structural construction of automata for all process algebras. DIMACS Series in Discrete Mathematics and Theoretical Computer Science 3 275–292.CrossRefGoogle Scholar
Milner, R. (1984) A complete inference system for a class of regular behaviours. Journal of Computer and System Sciences 28 439–466.CrossRefGoogle Scholar
Milner, R. (1989) Communication and Concurrency, Prentice-Hall International.Google Scholar
Mousavi, M. and Reniers, M. (2005) Orthogonal extensions in structural operational semantics. In: Proceedings of the 32nd International Colloquium on Automata, Languages and Programming (ICALP'05). Springer-Verlag Lecture Notes in Computer Science 3580 1214–1225.CrossRefGoogle Scholar
Mousavi, M., Reniers, M. and Groote, J. F. (2005) A syntactic commutativity format for SOS. Information Processing Letters 93 217–223.CrossRefGoogle Scholar
Mousavi, M., Reniers, M. and Groote, J. F. (2007) SOS formats and meta-theory: 20 years after. Theoretical Computer Science 373 (3)238–272.CrossRefGoogle Scholar
Park, D. (1981) Concurrency and automata on infinite sequences. In: Deussen, P. (ed.) 5th GI Conference, Karlsruhe, Germany. Springer-Verlag Lecture Notes in Computer Science 104 167–183.CrossRefGoogle Scholar
Plotkin, G. D. (1981) A structural approach to operational semantics. Report DAIMI FN-19, Computer Science Department, Aarhus University.Google Scholar
Plotkin, G. D. (2004) A structural approach to operational semantics. Journal of Logic and Algebraic Programming 60–61 17–139. (This is a revised version of Plotkin (1981).)Google Scholar
Rensink, A. (2000) Bisimilarity of open terms. Information and Computation 156 (1-2)345–385.CrossRefGoogle Scholar
de Simone, R. (1984) Calculabilité et Expressivité dans l'Algèbre de Processus Parallèles Meije, Thèse de 3e cycle, Univ. Paris 7.Google Scholar
de Simone, R. (1985) Higher-level synchronising devices in Meije–SCCS. Theoretical Computer Science 37 245–267.CrossRefGoogle Scholar
van Weerdenburg, M. (2008) Automating soundness proofs. In Hennessy, M. and Klin, B. (eds.) Proceedings of the Workshop on Structural Operational Semantics (SOS 2008). Electronic Notes in Theoretical Computer Science 229 (4)107–118.CrossRefGoogle Scholar