Select Publications
Conference Papers
, 2017, 'Precongruence formats with lookahead through modal decomposition', in Leibniz International Proceedings in Informatics, LIPIcs, Stockholm University, Sweden, presented at
, 2017, 'Lean and full congruence formats for recursion', in Proceedings - Symposium on Logic in Computer Science, Reykjavik, Iceland, presented at
, 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
, 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
, 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
, 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
, 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
, 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
, 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
, 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
, 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
, 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
, 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
, 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
, 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
, 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
, 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
, 2008, 'Characterising Probabilistic Processes Logically (extended abstract)', in Logic for Programming, Artificial Intelligence, and Reasoning - 17th International Conference, Springer, Yogyakarta, Indonesia, presented at
, 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
, 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
, 2007, 'Scalar outcomes suffice for finitary probabilistic testing', in 16th European symposium on programming, 2007, Braga, Portugal, presented at
, 2006, 'Liveness, fairness and impossible futures', in 17th international conference on Concurrency theory---CONCUR 2006, Bonn, Germany, presented at
, 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
, 2005, 'On cool congruence formats for weak bisimulations', in international colloquium on theoretical aspects of computing, Hanoi, Vietnam, presented at
, 2005, 'The individual and collective token interpretations of Petri nets', in 16th international conference on concurrency theory, San Francisco, California USA, presented at
, 2005, 'Divide and Congruence Applied to n-Bisimulation', in Electronic Notes in Theoretical Computer Science, Elsevier BV, Lisbon, Portugal, presented at
, 2004, 'On the Expressiveness of Higher Dimensional Automata: (Extended Abstract)', in Electronic Notes in Theoretical Computer Science, Elsevier BV, London, England, presented at
, 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
, 1987, 'Petri net models for algebraic theories of concurrency: Extended abstract', in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), pp. 224 - 242, http://dx.doi.org/10.1007/3-540-17945-3_13
, 'Configuration structures', in Proceedings of Tenth Annual IEEE Symposium on Logic in Computer Science, IEEE, presented at