Select Publications
Book Chapters
, 2023, 'Just Testing', in , pp. 498 - 519, http://dx.doi.org/10.1007/978-3-031-30829-1_24
, 2022, 'Fair Must Testing for I/O Automata', in A Journey from Process Algebra via Timed Automata to Model Learning: Essays Dedicated to Frits Vaandrager on the Occasion of His 60th Birthday, pp. 559 - 574, http://dx.doi.org/10.1007/978-3-031-15629-8_30
, 2019, 'A Complete Axiomatization of Branching Bisimilarity for a Simple Process Language with Probabilistic Choice: (Extended Abstract)', in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), pp. 139 - 162, http://dx.doi.org/10.1007/978-3-030-31175-9_9
, 2019, 'Reward testing equivalences for processes', in Models, Languages, and Tools for Concurrent and Distributed Programming, pp. 45 - 70, http://dx.doi.org/10.1007/978-3-030-21485-2_5
, 2019, 'Stronger Validity Criteria for Encoding Synchrony', in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), pp. 182 - 205, http://dx.doi.org/10.1007/978-3-030-31175-9_11
, 2017, 'A Branching Time Model of CSP', in Lecture Notes in Computer Science, Springer International Publishing, pp. 272 - 293, http://dx.doi.org/10.1007/978-3-319-51046-0_14
, 2011, 'Bisimulation', in Padua D (ed.), Encyclopedia of Parallel Computing, Springer, Heidelberg, pp. 136 - 139, http://dx.doi.org/10.1007/978-0-387-09766-4_149
, 2010, 'On CSP and the Algebraic Theory of Effects', in Wood K; Roscoe AW; Jones CB (ed.), Reflections on the work of C.A.R. Hoare, Springer, New York, pp. 333 - 370, http://dx.doi.org/10.1007/978-1-84882-912-1_15
, 2005, 'A characterisation for weak bisimulation congruence', in Middeldorp A (ed.), Processes, terms and cycles: Steps on the road to infinity, Springer Publishing Company, Berlin, pp. 26 - 39
, 2001, 'The Linear Time - Branching Time Spectrum I.**This is an extension of [20]. The research reported in this paper has been initiated at CWI in Amsterdam, continued at the Technical University of Munich, and finalized at Stanford University. It has been supported by Sonderforschungsbereich 342 of the TU München and by ONR under grant number N00014-92-J-1974. Part of it was carried out in the preparation of a course Comparative Concurrency Semantics, given at the University of Amsterdam, Spring 1988. A coloured version of this paper is available at http://boole.stanford.edu/pub/spectruml.ps.gz. The Semantics of Concrete, Sequential Processes', in Handbook of Process Algebra, Elsevier, pp. 3 - 99, http://dx.doi.org/10.1016/b978-044482830-9/50019-9
, 1995, 'On the Expressiveness of ACP', in Workshops in Computing, Springer London, pp. 188 - 217, http://dx.doi.org/10.1007/978-1-4471-2120-6_8
, 1994, 'Full Abstraction in Structural Operational Semantics (extended abstract)', in Workshops in Computing, Springer London, pp. 75 - 82, http://dx.doi.org/10.1007/978-1-4471-3227-1_7
, 1992, 'Interleaving semantics and action refinement with atomic choice', in Lecture Notes in Computer Science, Springer Berlin Heidelberg, pp. 89 - 107, http://dx.doi.org/10.1007/3-540-55610-9_169
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