New Developments in Operational Semantics
Rannis Project nr. 080039021 (2008-2010)


PUBLICATIONS

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

Books and Edited Volumes

  1. L. Aceto, J. Baeten, W. Fokkink, A. Ingolfsdottir and U. Nestmann. IFIP WG1.8 Workshop on Applying Concurrency Research in Industry, Journal of Logic and Algebraic Programming 78(4):191-288 (April 2009).
  2. L. Aceto and A. Ingolfsdottir. Special Issue: The 16th Nordic Workshop on Programming Theory (NWPT 2006). Journal of Logic and Algebraic Programming 77(1-2):1-156 (September-October 2008).
  3. L. Aceto and A. Ingolfsdottir. Special Issue in memory of Nadia Busi of Mathematical Structures in Computer Science, Volume 19 - Special Issue 06 (Dedicated to Nadia Busi), pp. 1061-1287. Cambridge University Press, 2009.
  4. L. Aceto, I. Damgaard, L.A. Goldberg, M.M. Halldorsson, A. Ingolfsdottir and I. Walukiewicz. Automata, Languages and Programming, 35th International Colloquium, ICALP 2008, Reykjavik, Iceland, July 7-11, 2008, Proceedings, Parts I and II. Lecture Notes in Computer Science volumes 5125 and 5126, Springer-Verlag, July 2008.
  5. L. Aceto, M. Bravetti, W. Fokkink and A.D. Gordon. Special Issue: Algebraic Process Calculi (The First Twenty Five Years and Beyond): Volume 3. Journal of Logic and Algebraic Programming Volume 75, Issue 1, Pages 1-166 (February-March 2008).
  6. 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. Matteo Cimini. Contributions to the Meta-theory of Structural Operational Semantics. PhD thesis in Computer Science, Reykjavik University. Date of defence: 18 November 2011. Matteo was supported by tis grant throughout his studies.

Chapters in Books and Collections

  1. Luca Aceto, Jos Baeten, Wan Fokkink, Anna Ingolfsdottir and Uwe Nestmann. Applying Concurrency Research in Industry: Report on a Strategic Workshop. Bulletin of the European Association for Theoretical Computer Science 94:113-129, February 2008.
  2. 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.
  3. M.R. Mousavi, M.A. Reniers, T. Basten, M.R.V. Chaudron, PARS: A Process Algebraic Approach to Resources and Schedulers, A chapter of M. Alexander and W. Gardner, editors, Process Algebra for Parallel and Distributed Processing. Chapman and Hall/CRC, November 2008.
  4. Luca Aceto, Anna Ingolfsdottir, MohammadReza Mousavi and Michel Reniers. Algebraic Properties for Free!.
    Version dated 16 September 2009.
    Concurrency Column, Bulletin of the EATCS, volume 99, October 2009.

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, Silvio Capobianco and Anna Ingolfsdottir. On the Existence of a Finite Base for Complete Trace Equivalence over BPA with Interrupt . Bulletin of the European Association for Theoretical Computer Science 95:220--240, June 2008.
  3. Luca Aceto, Silvio Capobianco, Anna Ingolfsdottir and Bas Luttik. The Equational Theory of Prebisimilarity over Basic CCS with Divergence. Information Processing Letters 108(5):255-338 (15 November 2008).
  4. 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.
  5. 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.
  6. 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
  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 and Anna Ingolfsdottir. On the Expressibility of Priority. Information Processing Letter 109:83--85, 2008.
  9. Luca Aceto, Anna Ingolfsdottir, Paul Blain Levy and Joshua Sack.
    Characteristic Formulae for Fixed-Point Semantics: A General Framework. To appear in Mathematical Structures in Computer Science, special issue devoted to selected papers from EXPRESS 2009, Cambridge University Press.
  10. M.R. Mousavi, I.C.C. Phillips, M.A. Reniers, I. Ulidowski. Semantics and Expressiveness of Ordered SOS. Information and Computation 207(2):85-119, February 2009. [Link to the journal version]
  11. Joshua Sack. Extending Probabilistic Dynamic Epistemic Logic. Knowledge, Rationality and Action, a special section of Synthese, 169:2, pp. 241-257, 2009.
  12. J. Sack. Logic for Update Products and Steps into the Past. Annals of Pure and Applied Logic. 161:12, 2010. pp. 1431–1461.
    Author created version: pdf

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, Arnar Birgisson, Anna Ingolfsdottir, MohammadReza Mousavi and Michel Reniers. Rule Formats for Determinism and Idempotence.
    To appear in the Proceedings of Third FSEN: IPM International Conference on Fundamentals of Software Engineering (FSEN09), Iran, April 15-17 2009. Lecture Notes in Computer Science, Springer-Verlag, 2009. To appear.
  3. 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.
  4. 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.
  5. Luca Aceto, Matteo Cimini and Anna Ingolfsdottir. A Bisimulation-based Method for Proving the Validity of Equations in GSOS Languages. To appear in the Proceedings of Structural Operational Semantics 2009, August 31, 2009, Bologna (Italy).
  6. 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.
  7. 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.
  8. 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.
    To appear in the Proceedings of FOCLASA 2011, Electronic Proceedings in Theoretical Computer Science, 2011.
  9. Luca Aceto, Wan Fokkink, Anna Ingolfsdottir and MohammadReza Mousavi. Lifting Non-Finite Axiomatizability Results to Extensions of Process Algebras.
    Technical Report CSR-08-05, TU/Eindhoven, February 2008.
    An extended abstract of this paper will appear in the Proceedings of TCS 2008, 5th IFIP International Conference on Theoretical Computer Science, Springer-Verlag, September 2008.
  10. 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.
  11. 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.
  12. Luca Aceto, Anna Ingolfsdottir, Kim G. Larsen and Jiri Srba. Teaching Concurrency: Theory in Practice. To appear in the Proceedings of TFM2009, 2nd Int. FME Conference on Teaching Formal Methods, "Widening Access to Formal Methods", Friday, November 6th 2009, Eindhoven (The Netherlands).
  13. Luca Aceto, Anna Ingolfsdottir, Bas Luttik and Paul van Tilburg. Finite Equational Bases for Fragments of CCS with Restriction and Relabelling (extended abstract).
    An extended abstract of this paper will appear in the Proceedings of TCS 2008, 5th IFIP International Conference on Theoretical Computer Science, Springer-Verlag, September 2008.
    A full version of this paper is available as Technical Report CSR-08-08, TU/Eindhoven, February 2008.
  14. 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.
  15. Luca Aceto, Anna Ingolfsdottir and Joshua Sack.
    Characteristic Formulae for Fixed-Point Semantics: A General Framework. Proceedings of EXPRESS'09, 16th International Workshop on Expressiveness in Concurrency, Saturday, September 5th, 2009 Bologna (Italy), EPTCS volume 8, pp. 1-15, 2009.
  16. Arnar Birgisson and Úlfar Erlingsson. An Implementation and Semantics for Transactional Memory Introspection in Haskell . Proceedings of the 4th ACM SIGPLAN Workshop on Programming Languages and Analysis for Security.
  17. M. Cimini, C. Sacerdoti Coen, and Davide Sangiorgi. Functions as processes: termination and the lambda mu mu~ - calculus Proceedings of TGC'10, LNCS 6084, pp. 73-86, Springer 2010. The official Springer version is here.
  18. Sjoerd Cranen, MohammadReza Mousavi and Michel A. Reniers. A Rule Format for Associativity. Proceedings of CONCUR 2008, Springer-Verlag, August 2008.
  19. H. Hojjat, M.R. Mousavi, M. Sirjani, Process Algebraic Verification of SystemC Codes, Proceedings of the 8th International Conference on Application of Concurrency to System Design (ACSD'08), Xi'an, China,, IEEE CS, June 2008.
  20. M.R. Mousavi. Causality in the Semantics of Esterel: Revisited. To appear in the Proceedings of Structural Operational Semantics 2009, August 31, 2009, Bologna (Italy).
  21. M. Raffelsiper, J.-W. Roorda, and M.R. Mousavi. Model Checking Verilog Descriptions of Cell Libraries. Proceedings of the 9th International Conference on Application of Concurrency to System Design (ACSD'09), Augsburg, Germany, IEEE CS, 2009.
  22. Bryan Renne, Joshua Sack and Audrey Yap. Dynamic Epistemic Temporal Logic. To appear in the Proceedings of the Second International Workshop on Logic, Rationality and Interaction (LORI-II), Chongqing, China, October 8-11, 2009, FoLLI-LNAI series, Springer-Verlag, 2009.

Unpublished and Submitted Papers

  1. Luca Aceto, David de Frutos Escrig, Carlos Gregorio-Rodriguez and Anna Ingolfsdottir.
    Axiomatizing Weak Simulation Semantics over BCCSP.
    Version dated 3 January 2011.
  2. 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. Submitted for journal publication. (Version dated 31 January 2012.)
  3. Arnar Birgisson. CCS+HML: A basic model checker in Haskell.
  4. Arnar Birgisson. Topics in Structural Operational Semantics. M.Sc. Thesis, Reykjavik University, May 2009.

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. Arnar Birgisson. CCS+HML in Haskell.