Yesterday at CWI, there was a celebration of (the funeral service for) 25 years of concurrency theory, practiced at SEN2.
The meeting was attended by some 100 participants. All SEN2 leaders and all its graduated Ph.D. students were present. Four distinguished speakers gave four very interesting talks. What comes next is a brief summary of what I can recall from these interesting presentations. An abstract of the talks can be found here.
- Jos Baeten gave a brief history of 25 years of concurrency theory and practice at CWI. It all started with Jan Bergstra who cooperated with John Tucker (then at Leiden) and went on with the leadership of Jan Willem Klop, Jos Baeten, Frits Vaandrager, Jan Friso Groote, Wan Fokkink and Jaco van de Pol, all of whom after a short while became full professor at universities around the Netherlands. SEN2 has produced: about 1000 PAM talks (the last to begin given on June 18, 2008 by Jan Willem Klop), about 10 research projects, 25 Ph.D. thesis (2 in progress), hundreds of articles and CONCUR conferences (of which till now, 18 conference are held), which is a truly impressive track record.
- Then, Gerard Holzmann gave a wonderful talk on the history and state of the art on Model Checking (with an emphasis on Spin). He divided the history of model checking into 4 development phases: formalisms (from 1978-1988), algorithms (from 1988-1998), veracity (from 1998-2008) and multi-core model-checking (I am not sure if I recall this one well, from 2008-2018).
- The third speaker was Jan Bergstra, who is the father of concurrency theory in the Netherlands. (Mathematics Genealogy project counts about 50 pupils of his, see here.) He gave a very intriguing talk about many foundational issues for algebraic specification and process algebras. He said that he always believed in a number of dogmas including: superiority of total functions over partial functions, and also superiority of projective limit models to those induced by structural operational semantics. He made his point by defining a theory of meadows, which defines division as a total function (with 1/0 = 0). He showed that a very sensible algebraic theory can then be developed for meadows. Jan Bergstra stated (and to some extent showed) that this can simplify the foundations of mathematics even at the level taught in primary and high schools. His talk touched upon many other fundamental issues such as suitability of Turing Machines as the (only) foundational model for computability.
- Finally, Moshe Vardi presented a nice overview of the development of temporal logics for industrial applications. He gave an overview on expressiveness and verification complexity for linear and branching temporal logics and the developments led to practical versions of such logics such as PSL and SVA (SystemVerilog Assertion). He concluded that SEN2 has not only produced a lot of fish, but trained many skilled fishermen for the Dutch TCS community and the latter is the main contribution of SEN2, which will last forever.