Select Publications
Journal articles
2024, 'Shoggoth: A Formal Foundation for Strategic Rewriting', Proceedings of the ACM on Programming Languages, 8, pp. 61 - 89, http://dx.doi.org/10.1145/3633211
,2023, 'Comparing the Expressiveness of the π-calculus and CCS', ACM Transactions on Computational Logic, 25, http://dx.doi.org/10.1145/3611013
,2023, 'Modelling mutual exclusion in a process algebra with time-outs', Information and Computation, 294, http://dx.doi.org/10.1016/j.ic.2023.105079
,2023, 'Cross-chain payment protocols with success guarantees', Distributed Computing, 36, pp. 137 - 157, http://dx.doi.org/10.1007/s00446-023-00446-0
,2023, 'Reactive bisimulation semantics for a process algebra with timeouts', Acta Informatica, 60, pp. 11 - 57, http://dx.doi.org/10.1007/s00236-022-00417-1
,2022, 'Abstract processes in the absence of conflicts in general place/transition systems', Information and Computation, 289, http://dx.doi.org/10.1016/j.ic.2022.104939
,2021, 'Abstract processes and conflicts in place/transition systems', Information and Computation, 281, http://dx.doi.org/10.1016/j.ic.2021.104706
,2021, 'Failure trace semantics for a process algebra with time-outs', Logical Methods in Computer Science, 17, http://dx.doi.org/10.23638/LMCS-17(2:11)2021
,2020, 'Progress, justness, and fairness', ACM Computing Surveys, 52, http://dx.doi.org/10.1145/3329125
,2020, 'Rooted divergence-preserving branching bisimilarity is a congruence', Logical Methods in Computer Science, 16, pp. 1 - 14, http://dx.doi.org/10.23638/LMCS-16(3:14)2020
,2019, 'Ensuring liveness properties of distributed systems: Open problems', Journal of Logical and Algebraic Methods in Programming, 109, http://dx.doi.org/10.1016/j.jlamp.2019.100480
,2019, 'Divide and congruence III: From decomposition of modal formulas to preservation of stability and divergence', Information and Computation, 268, http://dx.doi.org/10.1016/j.ic.2019.104435
,2018, 'On the validity of encodings of the synchronous in the asynchronous π-calculus', Information Processing Letters, 137, pp. 17 - 25, http://dx.doi.org/10.1016/j.ipl.2018.04.015
,2017, 'Divide and congruence II: From decomposition of modal formulas to preservation of delay and weak bisimilarity', Information and Computation, 257, pp. 79 - 113, http://dx.doi.org/10.1016/j.ic.2017.10.003
,2016, 'Modelling and verifying the AODV routing protocol', Distributed Computing, 29, pp. 279 - 315, http://dx.doi.org/10.1007/s00446-015-0262-7
,2016, 'Mechanizing a Process Algebra for Network Protocols', Journal of Automated Reasoning, 56, pp. 309 - 341, http://dx.doi.org/10.1007/s10817-015-9358-9
,2015, 'Proceedings Workshop on Models for Formal Analysis of Real Systems', Electronic Proceedings in Theoretical Computer Science, 196, http://dx.doi.org/10.4204/eptcs.196.0
,2015, 'On the axiomatizability of impossible futures', Logical Methods in Computer Science, 11, http://dx.doi.org/10.2168/LMCS-11(3:17)2015
,2015, 'Special issue on “Combining Compositionality and Concurrency”: part 2', Acta Informatica, http://dx.doi.org/10.1007/s00236-015-0240-3
,2015, 'CCS: It’s not fair!: Fair schedulers cannot be implemented in CCS-like languages even under progress and certain fairness assumptions', Acta Informatica, 52, pp. 175 - 205, http://dx.doi.org/10.1007/s00236-015-0221-6
,2015, 'Special issue on “Combining Compositionality and Concurrency”: part 1', Acta Informatica, 52, pp. 3 - 4, http://dx.doi.org/10.1007/s00236-014-0213-y
,2014, 'Real-reward testing for probabilistic processes', Theoretical Computer Science, 538, pp. 16 - 36, http://dx.doi.org/10.1016/j.tcs.2013.07.016
,2013, 'On characterising distributability', Logical Methods in Computer Science, 9, http://dx.doi.org/10.2168/LMCS-9(3:17)2013
,2012, 'Divide and Congruence: From Decomposition of Modal Formulas to Preservation of Branching and η-Bisimilarity', Information and Computation, 214, pp. 59 - 85, http://dx.doi.org/10.1016/j.ic.2011.10.011
,2012, 'Preface - Morgan: a suitable case for treatment', Formal Aspects of Computing, 24, pp. 417 - 422, http://dx.doi.org/10.1007/s00165-012-0257-0
,2011, 'Abstract processes of place/transition systems', Information Processing Letters, 111, pp. 626 - 633, http://dx.doi.org/10.1016/j.ipl.2011.03.013
,2011, 'On cool congruence formats for weak bisimulations', Theoretical Computer Science, 412, pp. 3283 - 3302, http://dx.doi.org/10.1016/j.tcs.2011.02.036
,2009, 'Branching bisimilarity with explicit divergence', Fundamenta Informaticae, 93, pp. 371 - 392
,2009, 'Computation Tree Logic with Deadlock Detection', Logical Methods in Computer Science, 5, pp. 1 - 21, http://dx.doi.org/10.2168/LMCS-5(4:5)2009
,2009, 'Configuration structures, event structures and Petri nets', Theoretical Computer Science, 410, pp. 4111 - 4159, http://dx.doi.org/10.1016/j.tcs.2009.06.014
,2009, 'Special issue on structural operational semantics: Preface', Information and Computation, 207, pp. 83 - 84, http://dx.doi.org/10.1016/j.ic.2008.10.006
,2009, 'Symmetric and Asymmetric Asynchronous Interaction', Electronic Notes in Theoretical Computer Science, 229, pp. 77 - 95, http://dx.doi.org/10.1016/j.entcs.2009.06.040
,2008, 'Characterising Testing Preorders for Finite Probabilistic Processes', Logical Methods in Computer Science, 4, http://dx.doi.org/10.2168/LMCS-4(4:4)2008
,2008, 'Ready to preorder: The case of weak process semantics', Information Processing Letters, 109, pp. 104 - 111
,2007, 'Preface', Electronic Notes in Theoretical Computer Science, 175, pp. 1 - 2, http://dx.doi.org/10.1016/j.entcs.2006.11.016
,2007, 'Preface', Electronic Notes in Theoretical Computer Science, 75
,2007, 'Preface', Electronic Notes in Theoretical Computer Science, 192
,2007, 'Remarks on Testing Probabilistic Processes', Electronic Notes in Theoretical Computer Science, 172, pp. 359 - 397, http://dx.doi.org/10.1016/j.entcs.2007.02.013
,2006, 'Erratum to "On the expressiveness of higher dimensional automata". [Theoret. Comput. Sci. 356 (2006) 265-290] (DOI:10.1016/j.tcs.2006.02.012)', Theoretical Computer Science, 368, pp. 168 - 194, http://dx.doi.org/10.1016/j.tcs.2006.06.024
,2006, 'Divide and congruence: From decomposition of modalities to preservation of branching bisimulation', Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 4111 LNCS, pp. 195 - 218, http://dx.doi.org/10.1007/11804192_10
,2006, 'Compositionality of Hennessy-Milner logic by structural operational semantics', Theoretical Computer Science, 354, pp. 421 - 440
,2006, 'On Specifying Timeouts', Electronic Notes in Theoretical Computer Science, 162, pp. 173 - 175, http://dx.doi.org/10.1016/j.entcs.2005.12.083
,2006, 'On the expressiveness of higher dimensional automata', Theoretical Computer Science, 356, pp. 265 - 290, http://dx.doi.org/10.1016/j.tcs.2006.02.012
,2006, 'On the expressiveness of higher dimensional automata (vol 356, pg 265, 2006)', Theoretical Computer Science, 368, pp. 168 - 194
,2005, 'On cool congruence formats for weak bisimulations', Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 3722 LNCS, pp. 318 - 333, http://dx.doi.org/10.1007/11560647_21
,2005, 'Proof nets for unit-free multiplicative additive linear logic', ACM Transactions on Computational Logic, 6 (4), pp. 784 - 842
,2004, 'Nested semantics over finite trees are equationally hard', Information and Computation, 191, pp. 203 - 232, http://dx.doi.org/10.1016/j.ic.2004.02.001
,2004, 'Well-behaved flow event structures for parallel composition and action refinement', Theoretical Computer Science, 311, pp. 463 - 478, http://dx.doi.org/10.1016/j.tcs.2003.10.031
,2004, 'Event structures for resolvable conflict', Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 3153, pp. 550 - 561, http://dx.doi.org/10.1007/978-3-540-28629-5_42
,2004, 'Precongruence formats for decorated trace semantics', ACM Transactions on Computational Logic, 5, pp. 26 - 78, http://dx.doi.org/10.1145/963927.963929
,