What to do next? Analysing and optimising system behaviour in time
Anton Wijs · Data Archiving and Networked Services (DANS) · 2007
HIS THESIS DEALS WITH THE incorporation of timing aspects in (mostly)explicit state model checking.Therefore, time as a concept appears everywhere in the thesis, whether as an aspect of timed modelling languages, as a notion of cost in weighted state spaces, or encoded in timed labelled transition systems.Besides that, different notions of time are also represented in the work; it considers both discrete relative time, where periods of time can be divided into atomic time intervals and moments in time are always referred to in relation to earlier moments in time, and continuous absolute time, where no atomic time interval can be identified, and moments in time are referred to with respect to a global clock.There is, however, one more aspect of time present in the thesis, but only implicitly, and only visible, often partially, to people involved with the work in between these covers.This book is more than just a list of chapters, and more than the contents, at least to me.It embodies a four year period of work at CWI, a period which I enjoyed very much, and as I flip through this thesis, memories come flooding back to me.Although I can hardly cover them all, in this preface, I will try to make this very personal aspect of time somewhat more explicit to the reader.For example, the work on translating χ t to µCRL is, besides appearing in the first chapters, also chronologically speaking the first subject I looked at within those four years.I remember being introduced to Elena Bortnik and Nikola Trčka in Eindhoven, and the three of us being assigned to deal with a turntable case study, in order to get familiar with model checking.Little did we know that this small case study would, almost literally, haunt us for the complete first year.I say haunt, since on a few occasions, it even caused me to dream at night about products being rotated, drilled, and tested.Luckily it turned out that every product eventually leaves the table, and likewise, the turntable eventually left our focus.Anyway, I enjoyed working with Elena and Nikola very much, and wish to thank them here.The first part is concluded by a chapter, which stems from, funnily enough, work created almost at the very end of my PhD period.In a way, it therefore completes a circle.This particular chapter is one of my personal favourites, as I feel that I was only able to write this chapter because I had done the work encompassed by Parts II and III.Though these parts might, at first sight, not appear to be that related to that chapter, writing them helped me to get more into touch with aspects such as the inclusion of time in process algebras, and the design of search algorithms.Part II is the result of very different events, at different locations.Chronologically, xv Preface the whole part grew out of one particular moment, which I can still remember well.I was looking into pruning techniques, as Mohammad Torabi Dashti appeared in my room, asking whether it would be possible in the µCRL toolset to associate priority values with action labels, allowing a search algorithm to only traverse transitions whose action labels have high enough priorities.Right at that moment, I was implementing that very mechanism in the toolset.What followed was a collaboration, resulting in papers on beam search, which form the basis of Chapters 8 and 9, and papers on partial order reduction.It was an enjoyable experience, and I thank him for this.Chapter 7 of Part II is based on my contribution to a, yet to appear, survey paper on the area of Directed Model Checking, which grew out of a Dagstuhl seminar on Directed Model Checking.I thank the people involved in that seminar for inviting me, and Husain Aljazzar, Dragan Bošnački, Stefan Edelkamp, Ansgar Fehnker, and Viktor Schuppan in particular, with whom I wrote the survey paper.Both the seminar and the writing of the survey paper were very helpful for me to get into the subject of Directed Model Checking.This experience finally helped me to create Chapter 6, which I associate with Braga, Portugal, as the basis of it was written by me in between and after the talks at the TACAS 2007 conference.For Part III of the thesis, I thank my supervisor Wan Fokkink and co-author Jun Pang.In fact, I thank Wan for all his supervision, but specifically the theory of timed bisimilarities was a subject which I would not have been able to deal with without him.I am glad that I got involved in this research, which happened when I was explaining my initial ideas for modelling time in µCRL to Wan.Part III forms, in my opinion, a nice theoretical addition to this otherwise practically oriented thesis.I thank all my colleagues in the TIPSy project which I have not mentioned already, namely Jos Baeten, Koos Rooda, Asia van de Mortel-Fronczak, Bas Luttik, and Ralph Meijer, for all the useful discussions at the regular meetings, and Bert van Beek for the discussions on χ.Of course, I thank Jaco van de Pol, my other supervisor, for his help, mostly concerning Part II.His comments pushed me to go further in my research.I thank all my former colleagues at CWI, in particular Bert Lisser, who was always there to implement new techniques and explain the inner workings of the µCRL toolset, and Jens Calamé, for helping to solve the occasional L A T E X2ε problem