This post is devoted to an interview with Kim G. Larsen, who received the CONCUR 2022 Test-of-Time Award for the paper The Impressive Power of Stopwatches (available also here), which appeared at CONCUR 2000 and was co-authored with Franck Cassez. On behalf of the concurrency theory community, I thank Kim for taking the time to answer my questions. I trust that readers of this blog will enjoy reading Kim's answer as much as I did.
Luca: You receive the CONCUR ToT Award 2022 for your paper The Impressive Power of Stopwatches, which appeared at CONCUR 2000. In that article, you showed that timed automata enriched with stopwatches and unobservable time delays have the same expressive power of linear hybrid automata. Could you briefly explain to our readers what timed automata with stopwatches are? Could you also tell us how you came to study the question addressed in your award-winning article? Which of the results in your paper did you find most surprising or challenging?
Kim: Well, in timed automata all clocks grow with rate 1 in all locations of the automata. Thus you can tell the amount of time that has elapsed since a particular clock was last reset, e.g. due to an external event of interest. A stopwatch is a real-valued variable similar to a regular clock. In contrast to a clock, a stopwatch will in certain locations grow with rate 1 and in other locations grow with rate 0, i.e. it is stopped. As such, a stopwatch gives you information about the accumulated time spent in a certain parts of the automata.
In modelling schedulability problems for real-time systems, the use of stopwatches is crucial in order to adequately capture preemption. I definitely believe that it was our shared interest in schedulability that brought us to study timed automata with stopwatches. We knew from earlier results by Alur et al. that properties such as reachability was undecidable. But what could we do about this? And how much expressive power would the addition of stopwatches provide?
In the paper we certainly put the most emphasis on the latter question, in that we showed that stopwatch automata and linear hybrid automata accept the same class of timed languages, and this was at least for me the most surprising and challenging result. However, focusing on impact, I think the approximate zone-based method that we apply in the paper has been extremely important from the point of view of having our verification tool UPPAAL being taken-up at large by the embedded systems community. It has been really interesting to see how well the over-approximation method actually works.
Luca: In your article, you showed that linear hybrid automata and stopwatch automata accept the same class of timed languages. Would this result still hold if all delays were observable? Do the two models have the same expressive power with respect to finer notions of equivalence such as timed bisimilarity, say? Did you, or any other colleague, study that problem, assuming that it is an interesting one?
Kim: These are definitely very interesting questions, and should be studied. As for finer notions of equivalences – e.g. timed bisimilarity – I believe that our translation could be shown to be correct up to some timed variant of chunk-by-chunk simulation introduced by Anders Gammelgaard in his Licentiat Thesis from Aarhus University in 1991. That could be a good starting point.
Luca: Did any of your subsequent research build explicitly on the
results and the techniques you developed in your award-winning paper?
Which of your subsequent results on timed and hybrid automata do
you like best? Is there any result obtained by other researchers that
builds on your work and that you like in particular or found surprising?
Kim: Looking up in DBLP, I see that I have some 28 papers containing the word “scheduling”. For sure stopwatches will have been used in one way or another in these. One thing that we never really examined thoroughly is to investigate how well the approximate zone-based will worked when applied to the translation of linear hybrid automata through the translation to stopwatch automata. This would definitely be interesting to find out.
This was the first joint publication between me and Franck. I enjoyed fully the collaboration on all the next 10 joint papers. Here the most significant ones are probably the paper at CONCUR 2005, where we presented the symbolic on-the-fly algorithms for synthesis for timed games and the branch UPPAAL TIGA. And later in a European project GASICS with Jean-Francois Raskin, we used the TIGA in the synthesis of optimal and robust control of a hydraulic system.
Franck: Using the result in our paper, we can analyse scheduling problems where tasks can be stopped and restarted, using real-time model-checking and a tool like UPPAAL.
To do so, we build a
network of stopwatch automata modelling the set of tasks and a
scheduling policy, and reduce schedulability to a safety verification
problem: avoid reaching states where tasks do not meet their deadlines.
Because we over-approximate the state space, our analysis may yield some
false positives and may wrongly declare a set of tasks non-schedulable
because the over-approximation is too coarse.
In the period 2003–2005, in cooperation with Francois Laroussinie we tried to identify some classes of stopwatch automata for which the over-approximation does not generate false positives. We never managed to find an interesting subclass.
This may look like a serious problem in terms of applicability of our result, but in practice, it does not matter too much. Most of the time, we are interested in the schedulability of a specific set of tasks (e.g. controlling a plant, a car, etc.) and for these instances, we can use our result: if we have false positives, we can refine the model tasks and scheduler and rule them out. Hopefully after a few iterations of refinement, we can prove that the set of tasks is schedulable.
The subsequent result on timed and hybrid automata of mine that I probably like best is the one we obtained on solving optimal reachability in timed automata.
We had a paper at FSTTCS in 2004
presenting the theoretical results, and a companion paper at GDV 2004
with an implementation using HyTech, a tool for analysing hybrid
automata.
I like these results because we ended up with a rather simple proof, after 3-4 years working on this hard problem.
Luca: Could you tell us how you started your collaboration on the award-winning paper? I recall that Franck was a regular visitor to our department at Aalborg University for some time, but I can't recall how his collaboration with the Uppaal group started.
Kim: I am not quite sure I remember how and when I first met Franck. For some time we already worked substantially with French researchers, in particular from LSV Cachan (Francois Larroussinie and Patricia Bouyer). I have the feeling that there were quite some strong links between Nantes (were Franck was) and LSV on timed systems in those days. Also Nantes was the organizer of the PhD school MOVEP five times in the period 1994-2002, and I was lecturing there in one of the years, meeting Olivier Roux and Franck who were the organizers. Funny enough, this year we are organizing MOVEP in Aalborg. Anyway, at some point Franck became a regular visitor to Aalborg, often for long periods of time – playing on the Squash team of the city when he was not working.
Franck: As Kim mentioned, I was in Nantes at that time, but I was working with Francois Laroussinie who was in Cachan. Francois had spent some time in Aalborg working with Kim and his group and he helped organise a mini workshop with Kim in 1999, in Nantes. That’s when Kim invited me to spend some time in Aalborg, and I visited Aalborg University for the first time from October 1999 until December 1999. This is when we worked on the stopwatch automata paper. We wanted to use UPPAAL to verify systems beyond timed automata.
I visited Kim and his group almost every year from 1999 until 2007, when I moved to Australia. There were always lots of visitors at Aalborg University and I was very fortunate to be there and learn from the Masters.
I always felt at home at Aalborg University, and loved all my visits there. The only downside was that I never managed to defeat Kim at badminton. I thought it was a gear issue, but Kim gave me his racket (I still have it) and the score did not change much.
Luca: What are the research topics that you find most interesting right now?
Is there any specific problem in your current field of interest that you'd like to see solved?
Kim: Currently I am spending quite some time on marrying symbolic synthesis with reinforcement learning for Timed Markov Decision Processes in order to achieve optimal as well as safe strategies for Cyber-Physical Systems.
Luca: Both Franck and you have a very strong track record in developing theoretical results and in applying them to real-life problems.
In my, admittedly biased, opinion, your work exemplifies Ben Schneiderman's Twin-Win Model (https://www.pnas.org/doi/pdf/
Kim: I completely subscribe to this. Several early theoretically findings – as the paper on stopwatch automata – have been key in our sustainable transfer to industry.
Franck: Kim has been a mentor to me for a number of years now, and I certainly learned this approach/philosophy from him and his group.
We always started from a concrete problem, e.g. scheduling tasks/checking schedulability, and to validate the solutions, building a tool to demonstrate applicability. The next step was to improve the tool to solve larger and larger problems.
UPPAAL is a fantastic example of this philosophy: the reachability problem for timed automata is PSPACE-complete. That would deter a number of people to try and build tools to solve this problem. But with smart abstractions, algorithms and data-structures, and constant improvement over a number of years, UPPAAL can analyse very large and complex systems. It is amazing to see how UPPAAL is used in several areas from traffic control to planning and to precisely guiding a needle for an injection.
Luca: What advice would you give to a young researcher who is keen to start working on topics related to formal methods?
Kim: Come to Aalborg, and participate in year's MOVEP.
No comments:
Post a Comment