
   
PUBLICATIONS
The following scientific publications have resulted from the project
work so far.
Books and Edited Volumes
 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):191288 (April 2009).
 L. Aceto and A. Ingolfsdottir.
Special Issue: The 16th Nordic Workshop on Programming Theory
(NWPT 2006). Journal of Logic and Algebraic Programming
77(12):1156 (SeptemberOctober 2008).
 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. 10611287. Cambridge University Press, 2009.
 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 711, 2008, Proceedings, Parts I and II. Lecture
Notes in Computer Science volumes 5125
and 5126,
SpringerVerlag, July 2008.
 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 1166 (FebruaryMarch 2008).
 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
 Matteo Cimini. Contributions to the Metatheory 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

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:113129, February 2008.

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. 100172, Cambridge University Press.
 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.

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

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.
 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:220240, June 2008.
 Luca
Aceto, Silvio Capobianco, Anna Ingolfsdottir and Bas Luttik. The
Equational Theory of Prebisimilarity over Basic CCS with
Divergence. Information Processing
Letters 108(5):255338 (15 November 2008).

Luca Aceto,
Taolue Chen, Anna
Ingolfsdottir, Bas
Luttik and Jaco
van de
Pol.
On the Axiomatizability of Priority II. Theoretical
Computer Science 412(28):30353044, 2011. The official journal paper
is here.
 Luca Aceto, Matteo Cimini and Anna Ingolfsdottir.
Proving
the validity of equations in GSOS languages using rulematching
bisimilarity. Version dated 18 October 2010. Mathematical
Structures in Computer Science 22(2):291331, Cambridge
University Press, 2012.

Luca Aceto,
Matteo Cimini, Anna
Ingolfsdottir, MohammadReza
Mousavi and Michel
Reniers.
SOS Rule Formats for Zero and Unit
Elements. Theoretical
Computer Science 412(28):30453071, 2011. The official journal
paper
is here

Luca Aceto, David de Frutos Escrig, Carlos GregorioRodriguez and Anna
Ingolfsdottir.
Complete
and ready simulation semantics are not finitely based over BCCSP,
even with a singleton
alphabet. Information
Processing Letters 111(9):408413, Elsevier, 2011.
 Luca Aceto
and Anna Ingolfsdottir. On the
Expressibility of
Priority. Information
Processing Letter 109:8385, 2008.
 Luca Aceto, Anna
Ingolfsdottir, Paul Blain
Levy and Joshua
Sack.
Characteristic
Formulae for FixedPoint Semantics: A General Framework. To
appear
in Mathematical
Structures in Computer Science, special issue devoted to
selected papers from EXPRESS 2009, Cambridge University Press.
 M.R. Mousavi, I.C.C. Phillips, M.A. Reniers, I. Ulidowski. Semantics and
Expressiveness of Ordered SOS. Information and Computation
207(2):85119, February 2009. [Link to the journal
version]
 Joshua Sack. Extending Probabilistic
Dynamic Epistemic Logic. Knowledge, Rationality and
Action, a special section of Synthese,
169:2, pp. 241257, 2009.
 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

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 2022, 2011. Lecture Notes in Computer Science,
SpringerVerlag.
 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 1517 2009. Lecture
Notes in Computer Science, SpringerVerlag, 2009. To
appear.

Luca Aceto,
Georgiana Caltais, EugenIoan 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. 378385,
Springer Verlag 2011. The associated PREG Axiomatizer tool is
available here. PREG
Axiomatizer is a tool for automatically deriving groundcomplete
axiomatizaitons of the bisimilarity over GSOS systems (extended with
predicates). The official version from Springer is
here.
 Luca Aceto, Georgiana Caltais, EugenIoan Goriac and Anna
Ingolfsdottir.
Axiomatizing GSOS with Predicates. Proceedings of SOS 2011,
Electronic Proceedings in Theoretical Computer Science 62, pp. 115, 2011.
 Luca Aceto, Matteo Cimini and Anna Ingolfsdottir. A
Bisimulationbased 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).

Luca Aceto,
Matteo Cimini, Anna
Ingolfsdottir, MohammadReza
Mousavi and Michel
Reniers.
On Rule Formats for Zero and Unit Elements. Proceedings of
the TwentySixth
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. 145160, Elsevier.

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. 8091, Springer Verlag,
2011. The official version from Springer is
here.
 Luca Aceto,
Matteo Cimini, Anna
Ingolfsdotti, Arni Hermann Reynisson,
Steinar Hugi Sigurdarson and
Marjan Sirjani.
Modelling and Simulation of RealTime Systems using Timed
Rebeca.
Version dated 19 February 2011. To appear in
the Proceedings of FOCLASA
2011, Electronic Proceedings in Theoretical Computer Science,
2011.
 Luca Aceto, Wan Fokkink, Anna Ingolfsdottir and MohammadReza Mousavi.
Lifting NonFinite Axiomatizability Results to Extensions of
Process Algebras.
Technical Report CSR0805,
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, SpringerVerlag, September 2008.
 Luca Aceto, David de Frutos Escrig,
Carlos GregorioRodriguez 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. 724, SpringerVerlag, 2011.

Luca Aceto, David de Frutos Escrig,
Carlos GregorioRodriguez 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 141152, SpringerVerlag, 2012.
 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).
 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, SpringerVerlag, September 2008. A full version of
this paper is available as Technical Report
CSR0808, TU/Eindhoven, February 2008.
 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. 141152, SpringerVerlag, 2010.
 Luca Aceto, Anna Ingolfsdottir
and Joshua
Sack.
Characteristic
Formulae for FixedPoint 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. 115, 2009.
 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.

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. 7386, Springer
2010. The official Springer version is
here.
 Sjoerd Cranen, MohammadReza Mousavi and Michel A. Reniers. A
Rule Format for Associativity. Proceedings of CONCUR
2008, SpringerVerlag, August 2008.
 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.

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).
 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.

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 (LORIII), Chongqing, China,
October 811, 2009, FoLLILNAI series, SpringerVerlag, 2009.
Unpublished and Submitted Papers

Luca Aceto, David de Frutos Escrig,
Carlos GregorioRodriguez and Anna Ingolfsdottir.
Axiomatizing Weak Simulation
Semantics over BCCSP. Version dated 3 January 2011.
 Luca Aceto, Matteo Cimini, Anna Ingolfsdotti, Ali Jafari, Arni
Hermann Reynisson, Steinar Hugi Sigurdarson and Marjan Sirjani. Modelling
and Simulation of RealTime Systems using Timed
Rebeca. Submitted for journal publication. (Version dated 31
January 2012.)
 Arnar Birgisson. CCS+HML:
A basic model checker in Haskell.
 Arnar Birgisson. Topics in
Structural Operational Semantics. M.Sc. Thesis, Reykjavik
University, May 2009.
Software
 Luca Aceto, Georgiana Caltais, EugenIoan Goriac and Anna
Ingolfsdotti. PREG
Axiomatizer. PREG Axiomatizer is a tool for automatically
deriving groundcomplete axiomatizaitons of the bisimilarity over
GSOS systems (extended with predicates).
 Luca Aceto, Matteo Cimini, Anna Ingolfsdotti, Arni Hermann Reynisson,
Steinar Hugi Sigurdarson and Marjan Sirjani.
Translator
from Timed Rebeca to Erlang.
 Arnar Birgisson. CCS+HML in
Haskell.
