Select Publications
Conference Papers
2018, 'A theory of encodings and expressiveness', in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), pp. 183 - 202, http://dx.doi.org/10.1007/978-3-319-89366-2_10
,2017, 'Analysing mutual exclusion using process algebra with signals', in Electronic Proceedings in Theoretical Computer Science, EPTCS, Open Publishing Association, Berlin; Germany, pp. 18 - 34, presented at 24th International Workshop on Expressiveness in Concurrency and 14th Workshop on Structural Operational Semantics, Berlin; Germany, 31 August 2017 - 04 September 2017, http://dx.doi.org/10.4204/EPTCS.255.2
,2017, 'Precongruence formats with lookahead through modal decomposition', in Leibniz International Proceedings in Informatics, LIPIcs, Stockholm University, Sweden, presented at 26th EACSL Annual Conference on Computer Science Logic (CSL 2017), Stockholm University, Sweden, 20 August 2017 - 24 August 2017, http://dx.doi.org/10.4230/LIPIcs.CSL.2017.25
,2017, 'Lean and full congruence formats for recursion', in Proceedings - Symposium on Logic in Computer Science, Reykjavik, Iceland, presented at 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Reykjavik, Iceland, 20 June 2017 - 23 June 2017, http://dx.doi.org/10.1109/LICS.2017.8005142
,2017, 'Split, send, reassemble: A formal specification of a CAN bus protocol stack', in Electronic Proceedings in Theoretical Computer Science, EPTCS, Open Publishing Association, Uppsala, Sweden, pp. 14 - 52, presented at 2nd Workshop on Models for Formal Analysis of Real Systems, Uppsala, Sweden, 29 April 2017 - 29 April 2017, http://dx.doi.org/10.4204/EPTCS.244.2
,2016, 'Divide and Congruence II: Delay and Weak Bisimilarity', in Proceedings - Symposium on Logic in Computer Science, pp. 778 - 787, http://dx.doi.org/10.1145/2933575.2933590
,2016, 'A timed process algebra for wireless networks with an application in routing', in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Eindhoven, pp. 95 - 122, presented at 25th European Symposium on Programming (ESOP), Eindhoven, 03 April 2016 - 08 August 2016, http://dx.doi.org/10.1007/978-3-662-49498-1_5
,2015, 'Preface', in Electronic Proceedings in Theoretical Computer Science, EPTCS, http://dx.doi.org/10.4204/EPTCS.196
,2015, 'Analysing and comparing encodability criteria', in Electronic Proceedings in Theoretical Computer Science, EPTCS, pp. 46 - 60, http://dx.doi.org/10.4204/EPTCS.190.4
,2015, 'Structure preserving bisimilarity, supporting an operational petri net semantics of CCSP', in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), pp. 99 - 130, http://dx.doi.org/10.1007/978-3-319-23506-6_9
,2014, 'A mechanized proof of loop freedom of the (untimed) AODV routing protocol', in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Sydney, pp. 47 - 63, presented at Automated Technology for Verification and Analysis, Sydney, 03 November 2014 - 06 November 2014, http://dx.doi.org/10.1007/978-3-319-11936-6_5
,2014, 'Showing invariance compositionally for a process algebra for network protocols', in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), pp. 144 - 159, http://dx.doi.org/10.1007/978-3-319-08970-6_10
,2013, 'Sequence numbers do not guarantee loop freedom - AODV can yield routing loops', in MSWiM 2013 - Proceedings of the 16th ACM International Conference on Modeling, Analysis and Simulation of Wireless and Mobile Systems, pp. 91 - 100, http://dx.doi.org/10.1145/2507924.2507943
,2012, 'A Rigorous Analysis of AODV and its Variants', in MSWIM'12, ACM, New York, NY, USA ©2012, pp. 203 - 212, presented at 15th ACM International Conference on Modeling, Analysis and Simulation of Wireless and Mobile Systems (MSWIM 2012), Paphos, Cyprus, 21 October 2012 - 25 October 2012, http://dx.doi.org/10.1145/2387238.2387274
,2012, 'Musings on Encodings and Expressiveness', in Proceedings Combined 19th International Workshop on Expressiveness in Concurrency and 9th Workshop on Structured Operational Semantics, Open Publishing Association, Sydney, Australia, pp. 81 - 98, presented at Combined 19th International Workshop on Expressiveness in Concurrency and 9th Workshop on Structured Operational Semantics, Newcastle upon Tyne, UK, 03 September 2012, http://dx.doi.org/10.4204/EPTCS.89.7
,2012, 'A process algebra for wireless mesh networks', in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) v. 7211, Springer, Tallinn, Estonia, pp. 295 - 315, presented at 21st European Symposium on Programming, ESOP 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, 24 March 2012 - 01 April 2012, http://dx.doi.org/10.1007/978-3-642-28869-2_15
,2012, 'Automated analysis of AODV using UPPAAL', in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) v. 7214, Springer, Tallinn, Estonia, pp. 173 - 187, presented at 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2012, Tallinn, Estonia, 24 March 2012 - 01 April 2012, http://dx.doi.org/10.1007/978-3-642-28756-5_13
,2012, 'On distributability of petri nets', in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) v. 7213, Springer, Tallinn, Estonia, pp. 331 - 345, presented at 15th International Conference on Foundations of Software Science and Computational Structures, FOSSACS 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, 24 March 2012 - 01 April 2012, http://dx.doi.org/10.1007/978-3-642-28729-9_22
,2011, 'Modelling and Analysis of AODV in UPPAAL', in Proceedings 1st International Workshop on Rigorous Protocol Engineering, WRiPE 2011, Philadelphia, PA, USA, pp. 1 - 6, presented at Proceedings 1st International Workshop on Rigorous Protocol Engineering (WRiPE 2011), Vancouver, Canada, 17 October 2011, http://wripe11.cis.upenn.edu/program/papers/wripe11-paper10.pdf
,2011, 'On causal semantics of Petri nets', in Katoen JP; König B (ed.), CONCUR 2011 - Concurrency Theory, Springer-Verlag, Berlin, pp. 43 - 59, presented at 22nd Conference on Concurrency Theory, CONCUR 2011, Aachen, Germany, 06 September 2011 - 09 September 2011, http://dx.doi.org/10.1007/978-3-642-23217-6_4
,2011, 'On Causal Semantics of Petri Nets (Extended Abstract)', in Katoen JP; Konig B (ed.), CONCUR 2011: CONCURRENCY THEORY, SPRINGER-VERLAG BERLIN, GERMANY, Aachen, pp. 43 - +, presented at 22nd Conference on Concurrency Theory (CONCUR 2011), GERMANY, Aachen, 06 September 2011 - 09 September 2011, https://www.webofscience.com/api/gateway?GWVersion=2&SrcApp=PARTNER_APP&SrcAuth=LinksAMR&KeyUT=WOS:000307082500004&DestLinkType=FullRecord&DestApp=ALL_WOS&UsrCustomerID=891bb5ab6ba270e68a29b250adbe88d1
,2011, 'Real-Reward Testing for Probabilistic Processes (extended abstract)', in Proceedings Ninth Workshop on Quantitative Aspects of Programming Languages, Open Publishing Association, Sydney, Australia, pp. 61 - 73, presented at Ninth Workshop on Quantitative Aspects of Programming Languages, Saarbrücken, Germany, http://dx.doi.org/10.4204/EPTCS.57.5
,2010, 'The Coarsest Precongruences Respecting Safety and Liveness Properties', in Calude CS; Sassone V (ed.), Proceedings 6th IFIP TC 1/WG 2.2 International Conference, TCS 2010, Held as Part of WCC 2010, Springer, Berlin, pp. 32 - 52, presented at Theoretical Computer Science, Brisbane, Australia, 20 September 2010 - 23 September 2010
,2009, 'On finite bases for weak semantics:Failures versus impossible futures', in 12th European Conference, JELIA 2010 Helsinki, Finland, September 13-15, 2010 Proceedings, Springer, Berlin, Germany, presented at 35th Conference on Current Trends in Theory and Practice of Computer Science, Špindlerův Mlýn, Czech Republic
,2009, 'Testing Finitary Probabilistic Processes', in Proceedings of the First International Conference on Advances in Natural Computation (ICNC 2005), Part III, Lecture Notes in Computer Science 3612/2005, Springer, Berlin, Germany, presented at 20th International Conference on Concurrency Theory, Bologna, Italy, http://dx.doi.org/10.1007/978-3-642-04081-8_19
,2008, 'Characterising Probabilistic Processes Logically (extended abstract)', in Logic for Programming, Artificial Intelligence, and Reasoning - 17th International Conference, Springer, Yogyakarta, Indonesia, presented at 2010 International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, Yogyakarta, Indonesia, 22 November 2008 - 27 November 2008, http://dx.doi.org/10.1007/978-3-642-16242-8_20
,2008, 'On synchronous and asynchronous interaction in distributed systems', in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), pp. 16 - 35, http://dx.doi.org/10.1007/978-3-540-85238-4_2
,2008, 'Five determinisation algorithms', in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), pp. 161 - 170, http://dx.doi.org/10.1007/978-3-540-70844-5_17
,2008, 'Correcting a Space-Efficient Simulation Algorithm', in Gupta A; Malik S (ed.), Proceedings 20th International Conference on Computer Aided Verification (CAV 2008), Princeton, USA, July 2008, Springer, Berlin, Heidelberg, pp. 517 - 529, presented at 20th International Conference on Computer Aided Verification (CAV 2008, Princeton, USA, 07 July 2008 - 14 July 2008, http://dx.doi.org/10.1007/978-3-540-70545-1_49
,2007, 'Characterising testing preorders for finite probabilistic processes', in 22nd Annual IEEE symposium on logic in computer science, Institute of Electrical and Electronics Engineers Inc., 445 Hoes Lane / P.O. Box 1331, Piscataway, NJ 08855-1331, United States, Wroclaw, Poland, pp. 313 - 322, presented at 22nd Annual IEEE symposium on logic in computer science, Wroclaw, Poland, 10 July 2007 - 14 July 2007, http://dx.doi.org/10.1109/LICS.2007.15
,2007, 'Scalar outcomes suffice for finitary probabilistic testing', in 16th European symposium on programming, 2007, Braga, Portugal, presented at 16th European symposium on programming, 2007, Braga, Portugal, 24 March 2007 - 01 April 2007
,2006, 'Liveness, fairness and impossible futures', in 17th international conference on Concurrency theory---CONCUR 2006, Bonn, Germany, presented at 17th international conference on Concurrency theory---CONCUR 2006, Bonn, Germany
,2005, 'Divide and congruence: From decomposition of modalities to preservation of branching bisimulation', in 4th international symposium on Formal methods for components and objects, Amsterdam, Netherlands, presented at 4th international symposium on Formal methods for components and objects, Amsterdam, Netherlands, 01 November 2005 - 04 November 2005
,2005, 'On cool congruence formats for weak bisimulations', in international colloquium on theoretical aspects of computing, Hanoi, Vietnam, presented at international colloquium on theoretical aspects of computing, Hanoi, Vietnam, 17 October 2005 - 21 October 2005
,2005, 'The individual and collective token interpretations of Petri nets', in 16th international conference on concurrency theory, San Francisco, California USA, presented at 16th international conference on concurrency theory, San Francisco, California USA, 23 August 2005 - 26 August 2005
,2005, 'Divide and Congruence Applied to n-Bisimulation', in Electronic Notes in Theoretical Computer Science, Elsevier BV, Lisbon, Portugal, presented at 2nd Workshop on Structural Operational Semantics, Lisbon, Portugal, 10 July 2005
,2004, 'On the Expressiveness of Higher Dimensional Automata: (Extended Abstract)', in Electronic Notes in Theoretical Computer Science, Elsevier BV, London, England, presented at EXPRESS 2004, London, England, 30 August 2004, http://www.sciencedirect.com/science/article/B75H1-4FW17DG-2/2/dc02332c27dc63ffb00f32b03bcb4efb
,1998, 'Scheduling algebra', in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), pp. 278 - 292, http://dx.doi.org/10.1007/3-540-49253-4_21
,1997, 'Axiomatizing flat iteration', in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), pp. 228 - 242, http://dx.doi.org/10.1007/3-540-63141-0_16
,1996, 'The meaning of negative premises in transition system specifications II', in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), pp. 502 - 513, http://dx.doi.org/10.1007/3-540-61440-0_154
,1993, 'A complete axiomatization for branching bisimulation congruence of finite-state behaviours', in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), pp. 473 - 484, http://dx.doi.org/10.1007/3-540-57182-5_39
,1993, 'The linear time - branching time spectrum II: The semantics of sequential systems with silent moves', in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), pp. 66 - 81, http://dx.doi.org/10.1007/3-540-57208-2_6
,1990, 'Equivalences and refinement', in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), pp. 309 - 333, http://dx.doi.org/10.1007/3-540-53479-2_13
,1990, 'Refinement of actions in causality based models', in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), pp. 267 - 300, http://dx.doi.org/10.1007/3-540-52559-9_68
,1990, 'The linear time-branching time spectrum', in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), pp. 278 - 297, http://dx.doi.org/10.1007/BFb0039066
,1989, 'Equivalence notions for concurrent systems and refinement of actions', in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), pp. 237 - 248, http://dx.doi.org/10.1007/3-540-51486-4_71
,1989, 'Modular specifications in process Algebra', in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), pp. 465 - 506, http://dx.doi.org/10.1007/BFb0015049
,1987, 'Another look at abstraction in process algebra: Extended abstract', in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), pp. 84 - 94, http://dx.doi.org/10.1007/3-540-18088-5_8
,1987, 'Bounded nondeterminism and the approximation induction principle in process algebra', in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), pp. 336 - 347, http://dx.doi.org/10.1007/BFb0039617
,1987, 'Merge and termination in process algebra', in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), pp. 153 - 172, http://dx.doi.org/10.1007/3-540-18625-5_49
,