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/10.1073/pnas.1802918115),
which propounds the pursuit of "the
dual goals of breakthrough theories in published papers and validated
solutions that are ready for widespread dissemination." Could you say a
few words on your research philosophy?
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.
