and
An Update Meeting on ``Reasoning about Timed Systems'' was held at the Institute of Mathematical Sciences, Madras, during June 16--20. The dates were conveniently arranged to coincide with the end of NSTCS which was held earlier at Madras. The meeting was a good opportunity for researchers in the area of distributed systems to ``update'' themselves on a new and related topic of research.
The study of timed systems arises naturally when addressing questions about quantitative timing properties of systems. Often, we are interested in knowing not only that event $b$ always follows the event $a$, but maybe also in the fact that $b$ always follows $a$ within a period of $10$ seconds. Much of the research in this area is based on a model of timed systems proposed by Alur and Dill, which essentially uses a standard finite-state automaton equipped with a set of clocks (or more appropriately, stop-watches) with transitions being guarded by conditions on clock values. Expectedly, a question that has received considerable attention is whether the successful verification techniques for untimed finite-state systems (particularly those based on temporal logic) can be extended to the case of timed systems. Another important topic of research in this area are Hybrid Systems. Hybrid Systems are discrete systems with a ``continuous'' component; a typical example is a digital controller of an analog plant.
The meeting began with an introduction to the Alur-Dill model of timed automata presented by Narayan Kumar. Over the next couple of lectures he showed that emptiness was decidable (via the region construction) and proved a couple of undecidability results which led to the fact that timed automata are not closed under complementation -- a rather serious limitation from the verification point of view.
R. Ramanujam talked about extensions of temporal logics which can express properties of timed systems. He also addressed the question of deciding satisfiability of formulas in these logics using timed automata. There was a considerable amount of debate on the naturalness of the timed logics which have been proposed so far.
Madhavan Mukund introduced Henzinger's theory of Hybrid Systems where he attempts to give a theoretical basis for model-checking for such systems.
Kamal Lodaya presented the gist of Thomas Wilke's work on characterising timed languages using monadic second order logic.
Paritosh Pandya in his series of talks showed how properties of intervals can be expressed naturally using Interval Logics.
R. K. Shyamsundar talked about Esterel with clocks while S. Ramesh talked on Synchronous Languages. The other speakers at the meeting included P.~S.~Subramanian (``Combining Temporal Logics'') and Xu Qiwen of UNU/IIST, Macau, who gave a talk on Proof Theory for Duration Calculus.
Probably the most novel feature of the meeting was the level of participation on behalf of the attendees, particularly by way of presenting talks. This goes for the student researchers too, who chipped in with their bit. Suman Roy spoke on ``Neighbourhood logic'', Swarup Mohalik presented Manna and Pnueli's paper on ``Models for Reactivity'', while Deepak D'Souza presented Asarin, Caspi and Maler's recent result on a Kleene-style theorem for timed automata.
Another notable feature of the meeting was that as a rule no talks were scheduled for the afternoon. Instead, the post-lunch session was utilised for some interesting discussions, with Paritosh playing the role of mediator. As a result, we got to share in some of the lunch table discussions and discoveries that usually elude us.
In conclusion, credit must go to Paritosh and Ramanujam for their initiative and effort in bringing about a successful meeting. Thanks also to Anil Seth for enlivening the proceedings with his entertaining choice of tea-time snacks and savouries!