Meta-Theory of Algebraic Process Theories
Rannis Project nr. 100014021 (2010-2012)


PUBLICATIONS

The following scientific publications have resulted from the project work so far.

Books and Edited Volumes

  1. Luca Aceto and Lars Birkedal. Special Issue: Selected papers of the conference on ``Foundations of Software Science and Computation Structures'': FOSSACS 2012, Tallinn, Estonia, 2012. Logical Methods in Computer Science, 2013.
  2. Luca Aceto, Monika Henzinger and Jiri Sgall. Proceedings of the 38th International Colloquium on Automata, Languages and Programming (ICALP 2011), Lecture Notes in Computer Science 6755 and 6756, Springer-Verlag, 2011. Part I may be found here, and part II here.
  3. Luca Aceto, Monika Henzinger and Jiri Sgall. 38th International Colloquium on Automata, Languages and Programming (ICALP 2011), Information and Computation 222, pages 1-306, January 2013.
  4. Luca Aceto and MohammadReza Mousavi. Proceedings of the First International Workshop on Process Algebra and Coordination (PACO 2011), volume 60 of Electronic Proceedings in Theoretical Computer Science, 6 August 2011.
  5. Luca Aceto and Pawel Sobocinski. Proceedings of the Seventh Workshop on Structural Operational Semantics, volume 32 of Electronic Proceedings in Theoretical Computer Science, 11th August 2010.

PhD Theses

  1. Georgiana Caltais. Coalgebraic Tools for Bisimilarity and Decorated Trace Semantics. PhD thesis in Computer Science, Reykjavik University and Radboud University Nijmegen. Date of defence: 16 December 2013.
  2. Matteo Cimini. Contributions to the Meta-theory of Structural Operational Semantics. PhD thesis in Computer Science, Reykjavik University. Date of defence: 18 November 2011.
  3. Eugen-Ioan Goriac. Axiomatizations from Structural Operational Semantics: Theory and Tools. PhD thesis in Computer Science, Reykjavik University. Date of defence: 22 August 2013.

MSc Theses

  1. Oddur Óskar Kjartansson. On the Formal Semantics of Bluespec System Verilog. MSc thesis in Computer Science, Reykjavik University. Date of defence: 29 August 2012.

Chapters in Books and Collections

  1. Luca Aceto, Anna Ingolfsdottir and Jiri Srba. The Algorithmics of Bisimilarity.
    Chapter 3 of Advanced Topics in Bisimulation and Coinduction (Jan Rutten and Davide Sangiorgi editors), volume 52 of Cambridge Tracts in Theoretical Computer Science, pp. 100-172, Cambridge University Press.

Journal Papers

  1. Luca Aceto, Arnar Birgisson, Anna Ingolfsdottir, MohammadReza Mousavi and Michel Reniers. Rule Formats for Determinism and Idempotence.
    Journal version to appear in a Special Issue of Science of Computer Programming devoted to FSEN 2009 (Farhad Arbab and Marjan Sirjani guest editors).
    Version dated 31 March 2010.
    The official journal version is here.
  2. Luca Aceto, Taolue Chen, Anna Ingolfsdottir, Bas Luttik and Jaco van de Pol. On the Axiomatizability of Priority II. Theoretical Computer Science 412(28):3035-3044, 2011. The official journal paper is here.
  3. Luca Aceto, Matteo Cimini and Anna Ingolfsdottir.
    Proving the validity of equations in GSOS languages using rule-matching bisimilarity.
    Version dated 18 October 2010.
    Mathematical Structures in Computer Science 22(2):291--331, Cambridge University Press, 2012.
  4. Luca Aceto, Matteo Cimini, Anna Ingolfsdottir, MohammadReza Mousavi and Michel Reniers. SOS Rule Formats for Zero and Unit Elements. Theoretical Computer Science 412(28):3045-3071, 2011. The official journal paper is here.
  5. Luca Aceto, Matteo Cimini, Anna Ingolfsdottir, MohammadReza Mousavi and Michel Reniers. Rule Formats for Distributivity. Theoretical Computer Science, Elsevier. To appear.
  6. Luca Aceto, Matteo Cimini, Anna Ingolfsdotti, Ali Jafari, Arni Hermann Reynisson, Steinar Hugi Sigurdarson and Marjan Sirjani. Modelling and Simulation of Real-Time Systems using Timed Rebeca. Science of Computer Programming, Elsevier. To appear.
  7. Luca Aceto, David de Frutos Escrig, Carlos Gregorio-Rodriguez and Anna Ingolfsdottir.
    Complete and ready simulation semantics are not finitely based over BCCSP, even with a singleton alphabet. Information Processing Letters 111(9):408-413, Elsevier, 2011.
  8. Luca Aceto, David de Frutos Escrig, Carlos Gregorio-Rodriguez and Anna Ingolfsdottir.
    Axiomatizing Weak Simulation Semantics over BCCSP.
    To appear in the journal Theoretical Computer Science..
  9. Luca Aceto, Eugen-Ioan Goriac and Anna Ingolfsdottir. SOS Rule Formats for Idempotent Terms and Idempotent Unary Operators.. Journal of Logic and Algebraic Programming, Elsevier, 2013. To appear.
  10. Bonsangue, M.M., Caltais, G., Goriac, E., Lucanu, D., Rutten, J.J.M.M. and Silva, A. Automatic equivalence proofs for non-deterministic coalgebras. To appear in Science of Computer Programming. Also available as CWI report SEN-1113, December 2011.

Conference and Workshop Papers

  1. Luca Aceto, Arnar Birgisson, Anna Ingolfsdottir, MohammadReza Mousavi. Decompositional Reasoning about the History of Parallel Processes.
    To appear in the Proceedings of IPM International Conference on Fundamentals of Software Engineering (FSEN 2011), Tehran, Iran, April 20-22, 2011. Lecture Notes in Computer Science, Springer-Verlag.
  2. Luca Aceto, Georgiana Caltais, Eugen-Ioan Goriac and Anna Ingolfsdotti. PREG Axiomatizer - A Ground Bisimilarity Checker for GSOS with Predicates..
    Version dated 21 April 2011.
    Proceedings of CALCO 2011 as a contribution to CALCO Tools, Lecture Notes in Computer Science 6859, pp. 378-385, Springer Verlag 2011.
    The associated PREG Axiomatizer tool is available here. PREG Axiomatizer is a tool for automatically deriving ground-complete axiomatizaitons of the bisimilarity over GSOS systems (extended with predicates). The official version from Springer is here.
  3. Luca Aceto, Georgiana Caltais, Eugen-Ioan Goriac and Anna Ingolfsdottir. Axiomatizing GSOS with Predicates. Proceedings of SOS 2011, Electronic Proceedings in Theoretical Computer Science 62, pp. 1-15, 2011.
  4. Luca Aceto, Arnaud Carayol, Zoltan Esik and Anna Ingolfsdottir. Algebraic Synchronization Trees and Processes. Proceedings of ICALP 2012, Lecture Notes in Computer Science, Springer, July 2012. To appear.
  5. Luca Aceto, Matteo Cimini, Anna Ingolfsdottir, MohammadReza Mousavi and Michel Reniers. On Rule Formats for Zero and Unit Elements. Proceedings of the Twenty-Sixth Conference on the Mathematical Foundations of Programming Semantics, University of Ottawa Thursday May 6 - Monday May 10, 2010. Electronic Notes in Theoretical Computer Science 256, pp. 145-160, Elsevier.
  6. Luca Aceto, Matteo Cimini, Anna Ingolfsdottir, MohammadReza Mousavi and Michel Reniers. Rule Formats for Distributivity. Proceedings of LATA 2011, Lecture Notes in Computer Science 6638, pp. 80-91, Springer Verlag, 2011. The official version from Springer is here.
  7. Luca Aceto, Matteo Cimini, Anna Ingolfsdotti, Arni Hermann Reynisson, Steinar Hugi Sigurdarson and Marjan Sirjani. Modelling and Simulation of Real-Time Systems using Timed Rebeca.
    Version dated 19 February 2011.
    Proceedings of FOCLASA 2011, Electronic Proceedings in Theoretical Computer Science 58, pp. 1-19, 2011.
  8. Luca Aceto, David de Frutos Escrig, Carlos Gregorio-Rodriguez and Anna Ingolfsdottir.
    Axiomatizing Weak Ready Simulation Semantics over BCCSP.
    Version dated 3 June 2011.
    Proceedings of the 8th International Colloquium on Theoretical Aspects of Computing, ICTAC 2011, Lecture Notes in Computer Science 6919, pp. 7-24, Springer-Verlag, 2011.
  9. Luca Aceto, David de Frutos Escrig, Carlos Gregorio-Rodriguez and Anna Ingolfsdottir. The Equational Theory of Weak Complete Simulation Semantics over BCCSP.
    Version dated 26 June 2011.
    To appear in the Proceedings of the 38th International Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM 2012) (M. Bieliková et al. (Eds.)), Lecture Notes in Computer Science 7147, pages 141-152, Springer-Verlag, 2012.
  10. Luca Aceto, Eugen-Ioan Goriac and Anna Ingolfsdottir. SOS Rule Formats for Idempotent Terms and Idempotent Unary Operators.. Proceedings of SOFSEM 2013: The 39th International Conference on Current Trends in Theory and Practice of Computing, Lecture Notes in Computer Science 7741, pp. 108-120, Springer-Verlag, 2013.
  11. Luca Aceto, Eugen-Ioan Goriac and Anna Ingolfsdottir. Meta SOS - A Maude Based SOS Meta-Theory Framework. Proceeedings of EXPRESS/SOS 2013, Electronic Proceedings in Theoretical Computer Science, 2013.
  12. Luca Aceto, Eugen-Ioan Goriac, Anna Ingolfsdottir, MohammadReza Mousavi and Michel Reniers. Exploiting Algebraic Laws to Improve Mechanized Axiomatizations. To appear in the Proceedings of the 5th Conference on Algebra and Coalgebra in Computer Science, Warsaw, Poland, 3-6 September 2013. Springer-Verlag, 2013.
  13. Luca Aceto, Anna Ingolfsdottir, MohammadReza Mousavi and Michel Reniers. A Rule Format for Unit Elements. Proceedings of SOFSEM 2010: The 36th International Conference on Current Trends in Theory and Practice of Computing, Lecture Notes in Computer Science 5901, pp. 141-152, Springer-Verlag, 2010.
  14. Filippo Bonchi, Marcello Bonsangue, Georgiana Caltais, Jan Rutten and Alexandra Silva. Final semantics for decorated traces. To appear in the Proceedings of the Twenty-eighth Conference on the Mathematical Foundations of Programming Semantics, Electronic Notes in Theoretical Computer Science, Elsevier, 2012.
  15. Marcello Bonsangue, Georgiana Caltais, Eugen-Ioan Goriac, Dorel Lucanu, Jan Rutten and Alexandra Silva. A decision procedure for bisimilarity of generalized regular expressions. Proceedings of the 13th Brazilian Symposium on Formal Methods (SBMF'2010), Lecture Notes in Computer Science 6527, pp. 226-241, Springer 2011.
  16. Matteo Cimini, MohammadReza Mousavi, Michel Reniers and Murdoch Gabbay. Nominal SOS. To appear in the Proceedings of the Twenty-eighth Conference on the Mathematical Foundations of Programming Semantics, Electronic Notes in Theoretical Computer Science, Elsevier, 2012.
  17. Daniel Gebler, Eugen-Ioan Goriac and Mohammad Reza Mousavi. Algebraic Meta-Theory of Processes with Data. Proceedings of EXPRESS/SOS 2013, volume 120 of Electronic Proceedings in Theoretical Computer Science, pp. 63-77, 2013
  18. E. I. Goriac, D. Lucanu, G. Roşu. Automating Coinduction with Case Analysis. Proceedings of ICFEM 2010, Lecture Notes in Computer Science 6447, pp. 220-236, Springer-Verlag.

Unpublished and Submitted Papers

  1. Luca Aceto, Eugen-Ioan Goriac and Anna Ingolfsdottir. A Ground-Complete Axiomatization of Stateless Bisimilarity over Linda.
    Version dated 21 June 2013. Submitted for publication.
  2. Filippo Bonchi, Marcello Bonsangue, Georgiana Caltais, Jan Rutten and Alexandra Silva. Final semantics for decorated traces, October 2012. Submitted for journal publication.

Software

  1. Luca Aceto, Georgiana Caltais, Eugen-Ioan Goriac and Anna Ingolfsdotti. PREG Axiomatizer. PREG Axiomatizer is a tool for automatically deriving ground-complete axiomatizaitons of the bisimilarity over GSOS systems (extended with predicates).
  2. Luca Aceto, Matteo Cimini, Anna Ingolfsdotti, Arni Hermann Reynisson, Steinar Hugi Sigurdarson and Marjan Sirjani. Translator from Timed Rebeca to Erlang.
  3. Luca Aceto, Eugen-Ioan Goriac and Anna Ingolfsdottir. Meta SOS - A Maude Based SOS Meta-Theory Framework.