Process Algebra
- Aim: study process algebraic languages and their semantics, in order to provide a firm theoretical basis for the specification, analysis and verification of concurrent systems
- Context: Process algebra is an algebraic approach to the study of concurrent processes. Its tools are algebraic languages for the specification of processes and the formulation of statements about them, together with calculi for the verification of these statements.
- Collaboration: VU Amsterdam, TU Eindhoven, University of Edinburgh
People
Current |
Past
|
Activities
- AWN, a process algebra for wireless mesh networks: We development a new process algebra that enables us to formalise routing protocols for wireless mesh networks.
- Structural operational semantics: We aim to derive congruence properties for suitable equivalences and refinement preorders, through syntactic requirements in operational specifications of processes.
- Process algebras with probabilistic as well as nondeterministic choice: We study the addition of probabilistic choice to the process algebra CSP.
- Expressiveness of process calculi: We propose and elaborate a definition of what it means for one process calculus to encode another one, thereby enabling an ordering of process calculi with respect to expressive power. Our definition requires a process to be behaviourally equivalent with its encoding, and thus is parametrised with the choice of a suitable semantic equivalence on processes. By means of a series of case studies we hope to ascertain which semantic equivalences are most suitable for certain applications. Finally, we hope to apply the framework to compare the expressiveness of existing process calculi, in particular focussing on calculi with synchronous and with asynchronous communication primitives.
Publications
2017
|
 |
Wan Fokkink, Rob van Glabbeek and Bas Luttik Divide and congruence III: Stability & divergence 28th International Conference on Concurrency Theory (CONCUR'17), pp. 15:1-15:16, Berlin, Germany, September, 2017 |
|
|
|
Wan Fokkink and Rob van Glabbeek Precongruence formats with lookahead through modal decomposition 26th EACSL Annual Conference on Computer Science Logic (CSL'17), Stockholm, Sweden, August, 2017 |
|
|
 |
Rob van Glabbeek Lean and full congruence formats for recursion Proceedings 32nd Annual IEEE Symposium on Logic in Computer Science (LICS 2017), Reykjavik, Iceland, June, 2017 |
|
|
|
Rob van Glabbeek and Peter Hoefner Split, send, reassemble: A formal specification of a CAN bus protocol stack 2nd Workshop on Models for Formal Analysis of Real Systems (MARS 2017), pp. 14–52, Uppsala, Sweden, March, 2017 |
|
|
|
Rob van Glabbeek A branching time model of CSP Concurrency, Security, and Puzzles — Essays Dedicated to Andrew William Roscoe on the Occasion of His 60th Birthday, pp. 272–293, Volume 10160 in Lecture Notes in Computer Science, Springer, 2017 |
2016
|
|
|
Rob van Glabbeek An algebraic treatment of recursion Liber Amicorum for Jan A. Bergstra, pp. 58–59, Informatics Institute, University of Amsterdam, 2016 |
|
|
|
Rob van Glabbeek, Peter Hoefner, Marius Portmann and Wee Lum Tan Modelling and verifying the AODV routing protocol Distributed Computing, Volume 29, Number 4, pp. 279–315, August, 2016 |
|
|
|
Wan Fokkink and Rob van Glabbeek Divide and congruence II: delay and weak bisimilarity Thirty-First Annual ACM/IEEE Symposium on Logic in Computer Science, pp. 778–787, New York City, USA, July, 2016 |
|
|
|
Emile Bres, Rob van Glabbeek and Peter Hoefner A timed process algebra for wireless networks with an application in routing (extended abstract) European Symposium on Programming, pp. 95–122, Eindhoven, The Netherlands, April, 2016 |
|
|
|
Wan Fokkink and Rob van Glabbeek Divide and congruence II: From decomposition of modal formulas to preservation of delay and weak bisimilarity Technical Report 9351, NICTA, April, 2016 |
|
|
|
Timothy Bourke, Rob van Glabbeek and Peter Hoefner Mechanizing a process algebra for network protocols Journal of Automated Reasoning, Volume 56, Number 3, pp. 309–341, March, 2016 |
|
|
|
Emile Bres, Rob van Glabbeek and Peter Hoefner A timed process algebra for wireless networks with an application in routing Technical Report, NICTA, February, 2016 |
2015
|
|
|
Peter Hoefner Using process algebra to design better protocols (abstract) Forum “Math-for-Industry” 2015, pp. 31–33, Fukuoka, Japan, October, 2015 |
|
|
|
Rob van Glabbeek Structure preserving bisimilarity, supporting an operational petri net semantics of CCSP Correct System Design — Symposium in Honor of Ernst-Rüdiger Olderog on the Occasion of His 60th Birthday, pp. 99–130, Oldenburg, Germany, September, 2015 |
|
|
|
Rob van Glabbeek, Taolue Chen and Wan Fokkink On the axiomatizability of impossible futures Logical Methods in Computer Science, Volume 11, Number 3, pp. 1–31, September, 2015 |
|
|
|
Kirstin Peters and Rob van Glabbeek Analysing and comparing encodability criteria Combined 22th International Workshop on Expressiveness in Concurrency and 12th Workshop on Structural Operational Semantics, pp. 46–60, Madrid, Spain, August, 2015 |
|
|
|
Rob van Glabbeek and Peter Hoefner CCS: It's not fair! Fair schedulers cannot be implemented in CCS-like languages even under progress and certain fairness assumptions Acta Informatica, Volume 52, Number 2-3, pp. 175–205, April, 2015 |
|
|
|
Rob van Glabbeek and Peter Hoefner Progress, fairness and justness in process algebra Technical Report 8501, NICTA, January, 2015 |
2014
|
|
|
Timothy Bourke, Rob van Glabbeek and Peter Hoefner A mechanized proof of loop freedom of the (untimed) AODV routing protocol International Symposium on Automated Technology for Verification and Analysis (ATVA), pp. 47–63, Sydney, Australia, November, 2014 |
|
|
|
Timothy Bourke, Rob van Glabbeek and Peter Hoefner Showing invariance compositionally for a process algebra for network protocols International Conference on Interactive Theorem Proving, pp. 44–59, Vienna, Austria, July, 2014 |
2013
|
|
|
Ansgar Fehnker, Rob van Glabbeek, Peter Hoefner, Annabelle McIver, Marius Portmann and Wee Lum Tan A process algebra for wireless mesh networks used for modelling, verifying and analysing AODV Technical Report 5513, NICTA, December, 2013 |
|
|
|
Rob van Glabbeek, Peter Hoefner, Wee Lum Tan and Marius Portmann Sequence numbers do not guarantee loop freedom — AODV can yield routing loops 16th ACM International Conference on Modeling, Analysis and Simulation of Wireless and Mobile Systems, pp. 91–100, Barcelona, Spain, November, 2013 |
2012
|
|
|
Peter Hoefner and Sarah Edenhofer Towards a rigorous analysis of AODVv2 (DYMO) 2nd International Workshop on Rigorous Protocol Engineering (WRiPE 2012), pp. 1–6, Austin, Texas, October, 2012 |
|
|
|
Peter Hoefner, Rob van Glabbeek, Wee Lum Tan, Marius Portmann, Annabelle McIver and Ansgar Fehnker A rigorous analysis of AODV and its variants 15th ACM/IEEE International Conference on Modelling, Analysis and Simulation of Wireless and Mobile Systems (MSWIM 2012), pp. 203–212, Paphos, Cyprus, October, 2012 |
|
|
|
Rob van Glabbeek Musings on encodings and expressiveness Combined 19th International Workshop on Expressiveness in Concurrency and 9th Workshop on Structural Operational Semantics, pp. 81—98, Newcastle upon Tyne, United Kingdom, August, 2012 |
|
|
|
Wan Fokkink, Rob van Glabbeek and Paulien de Wind Divide and congruence: From decomposition of modal formulas to preservation of branching and η-bisimilarity Information and Computation (I&C), Volume 214, Number , pp. 59–85, May, 2012 |
|
|
|
Ansgar Fehnker, Rob van Glabbeek, Peter Hoefner, Annabelle McIver, Marius Portmann and Wee Lum Tan A process algebra for wireless mesh networks 22nd European Symposium on Programming (ESOP 2012), pp. 295–315, Tallinn, Estonia, March, 2012 |
|
|
|
Ansgar Fehnker, Rob van Glabbeek, Peter Hoefner, Annabelle McIver, Marius Portmann and Wee Lum Tan Automated analysis of AODV using UPPAAL 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2012), pp. 173–187, Tallinn, Estonia, March, 2012 |
2011
|
|
|
Rob van Glabbeek Bisimulation Encyclopedia of Parallel Computing, pp. 136–139, Volume 1 in , Springer, 2011 |
|
|
|
Rob van Glabbeek On cool congruence formats for weak bisimulations Theoretical Computer Science, Volume 412, Number 28, pp. 3283–3302, June, 2011 |
2010
|
|
|
Rob van Glabbeek The coarsest precongruences respecting safety and liveness properties Theoretical Computer Science 2010, pp. 32–52, Brisbane, September, 2010 |
|
|
|
Rob van Glabbeek and Gordon Plotkin On CSP and the algebraic theory of effects Reflections on the Work of C.A.R. Hoare, pp. 333–369, Volume in History of Computing, Springer, 2010 |
2009
|
|
|
Rob van Glabbeek, Bas Luttik and Nikola Trčka Computation tree logic with deadlock detection Logical Methods in Computer Science, Volume 5, Number 4:5, pp. 1–24, December, 2009 |
|
|
|
Yuxin Deng, Rob van Glabbeek, Matthew Hennessy and Carroll Morgan Testing finitary probabilistic processes (extended abstract) 20th International Conference on Concurrency Theory (CONCUR 2009), pp. 274–288, Bologna, Italy, August, 2009 |
|
|
|
Rob van Glabbeek, Bas Luttik and Nikola Trčka Branching bisimilarity with explicit divergence Fundamenta Informaticae, Volume 93, Number 4, pp. 371–392, June, 2009 |
|
|
|
Rob van Glabbeek and Peter D. Mosses Preface, special issue on structural operational semantics Information and Computation, pp. 83–84, Elsevier, 2009 |
|
|
|
Taolue Chen, Wan Fokkink and Rob van Glabbeek On finite bases for weak semantics: Failures versus impossible futures 35th Conference on Current Trends in Theory and Practice of Computer Science, pp. 167–180, Spindleruv Mlyn, Czech Republic , January, 2009 |
2008
|
|
|
Taolue Chen, Wan Fokkink and Rob van Glabbeek Ready to preorder: The case of weak process semantics Information Processing Letters, Volume 109, Number 2, pp. 104–111, December, 2008 |
|
|
|
Yuxin Deng, Rob van Glabbeek, Matthew Hennessy and Carroll Morgan Characterising testing preorders for finite probabilistic processes Logical Methods in Computer Science, Volume 4, Number 4, pp. 1–33, October, 2008 |
2007
|
|
|
Rob van Glabbeek and Matthew Hennessy Preface, proceedings of the 4th workshop on structural operational semantics Electronic Notes in Theoretical Computer Science, pp. 1–3, Elsevier, 2007 |
|
|
|
Yuxin Deng, Rob van Glabbeek, Matthew Hennessy, Carroll Morgan and Cuicui Zhang Characterising testing preorders for finite probabilistic processes 22nd Annual IEEE Symposium on Logic in Computer Science, LICS 2007, pp. 313–322, Wroclaw, Poland, July, 2007 |
|
|
|
Rob van Glabbeek and Peter D. Mosses Preface, proceedings of the 3rd workshop on structural operational semantics Electronic Notes in Theoretical Computer Science, pp. 1–2, Elsevier, 2007 |
|
|
|
Yuxin Deng, Rob van Glabbeek, Matthew Hennessy, Carroll Morgan and Cuicui Zhang Remarks on testing probabilistic processes Electronic Notes in Theoretical Computer Science, Volume 172, Number , pp. 359–397, April, 2007 |
