LICS and POMIV

A trip report

R. Ramanujam

The Institute of Mathematical Sciences, Madras 600 113, India.
E-mail: jam@imsc.ernet.in

This year the (11th) annual IEEE symposium on Logic in Computer Science (LICS) was part of a 4-meeting mela under the banner Federated Logic Conference. The other three were:

LICS and RTA were held in parallel (July 27 to 30, 1996) and afterwards, CAV and CADE were paralleled (a verb I learnt during the meetings) from July 31 to August 3. The meetings took place at the Student Center, College Avenue campus of Rutgers University at New Brunswick, New Jersey, in the U.S.A.

There were also several pre- and post-conference workshops: Foundations of object-oriented languages, Partial order methods in verification (POMIV), Teaching logic and reasoning in an illogical world, Computational complexity and programming languages, SPIN (a verification tool), Internet ... . There were three participants from India -- Anil Seth and I, both from IMSc, Madras, and Krishna Rao from TIFR, Bombay (currently visiting MPI, Saarbrucken). I attended POMIV, LICS and a few talks in RTA.

LICS

There were two sessions each (session = 4 papers) on finite model theory, type theory and model checking. Concurrency, semantics and domains, temporal logic and $\mu$-calculus, unification, complexity and reasoning about programs had one session each. There was a joint plenary session with RTA in which G\'erard Huet (Paris) spoke on the design of proof assistants. At the end of (LICS $\parallel$ RTA), there was a plenary session at the intersection of all four conferences, and this was a lecture by Robin Milner (Cambridge) on calculi for interactions. There were also two tutorials, one by Tom Henzinger (Berkeley) on the theory of hybrid automata, and the other by Andr\'e Joyal (Montreal) on lattices, categories and communication. Dana Scott gave an after-banquet speech, his reflections on logic and logicians.

The Kleene award for best student papers went to Juha Nurmonen (Counting modulo quantifiers on finite linearly ordered trees) and Guy McCusker (Games and full abstraction for FPC).

Robin Milner's plenary lecture (a formal occasion, in a grand ballroom of Hyatt Hotel) started off with the differences in emphasis between studying computation and interaction (prescription vs description, and so on). He argued the need for a calculus for interactions with generic rather than ad-hoc notions, and then presented his (and his students') recent efforts towards such a calculus. Milner's generic notions: binding structure, naming and ``boxing''.

Henzinger gave an excellent tutorial on hybrid automata. States usually represent values of system variables, and in hybrid systems, some variables vary continuously. Such systems are presented using conditions on derivatives (a clock is a variable whose derivative is always 1, a stopwatch is a variable whose derivative is always 1 or 0, and so on). Mahler, Manna and Pnueli initiated the study of hybrid systems, and the area has seen good results recently, many by Alur and Henzinger among others. In this tutorial, Henzinger surveyed results on the complexity of reachability and gave intuitive reasons for both positive and negative results, showing how far one can push techniques from discrete-state system theory to mixed systems, and where one needs new ideas.

Joyal's tutorial was on a game-theoretic interpretation of bi-complete categories. The games have three players: two opponents and a mediator. Joyal talked about when the mediator has complete communication strategies (iff the pair of terms on which the game is played are ordered in the free lattice). Equivalent strategies define the same arrow. The amazing (and entertaining part) was that he had examples from share markets. (Indeed, according to gossip from Prakash Panangaden, Joyal is an expert on finance.)

Of what I understood of the finite model theory papers, the one by Kolaitis and Vardi on logics with a fixed finite number of variables was very interesting. Gregory McColm's presentation on zero-one laws for Gilbert-random graphs was more fascinating for the applications of these graphs in biological models and percolation theory than for the main theorem itself. In model checking, the emphasis continued to be on practical verification problems on one hand (QBDDs, reactive modules etc.) and on deepening our understanding of Rabin tree automata on the other. In temporal logic the paper by Etessami and Wilke showing strictness of the until-hierarchy was notable. A number of papers were on decision problems (unification, paramodulation, semi-thue systems, abduction, subtyping dependent types, ... ). Palliath Narendran (Albany) gave a nice talk on polynomials in semirings.

In semantics, the story of full abstraction via game semantics continued on. I should also mention the series of papers by Abbas Edalat and others from Imperial College bringing analytical methods like integration and differentiation into the context of domain theory. This LICS also had a couple of papers of this kind. (During the discussion, Dana Scott remarked: ``I am glad that at last, after 20 years, someone is doing the kind of mathematics domain theory was meant for''.)

Type theory had, as usual, papers on subtyping and polymorphism. (I was surprised to see very few papers on linear logic in this year's LICS; one of these few was very amusingly presented by Phil Wadler (Glasgow)). Ong (Oxford and Singapore) had an interesting paper which addressed the question of which category corresponds to classical proofs (in the same way as cartesian closed categories capture intuitionistic ones).

In the concurrency session, Ian Stark (Aarhus) gave a very nice presentation on a domain model for the $\pi$-calculus. Among the other presentations, one high point was an exchange between Vladimiro Sassone (Pisa) and Rob van Glabbeek (Stanford) on what constituted a degeneracy.

The next LICS (to be chaired by Glynn Winskel) will pair with CONCUR in Warsaw.

POMIV

Much of verification theory centres around the reachability of subsets of nodes in finite graphs. These graphs represent (global) state spaces of communicating finite state machines, and their size is exponential in the number of components. In such situations, it is advantageous to come up with techniques which cut down the number of paths to be explored. One idea is to equate paths which represent different interleavings of independent actions of different machines. To verify properties insensitive to interleavings, it suffices to consider representatives of an equivalence class. (When $a$ and $b$ are local actions of two different machines, it may be immaterial whether a system run proceeds as $ab$ or $ba$ when all we want is to check whether both machines eventually synchronize on $c$.) Such techniques are referred to as partial-order based methods (the equivalence classes above represent certain kinds of partial orders), and they have received a great deal of attention in the last few years in the concurrency and verification community.

This workshop, organized by Gerard Holtzmann, Doron Peled and Vaughan Pratt, was an attempt to bring together researchers from both the concurrency and verification communities with the specific idea of discussing partial order theory in the two contexts. The workshop was held at Princeton from July 24 to 26.

There were only about 50 participants, almost everyone an active researcher in a related area, with nearly half being speakers (there were 24 invited presentations). This meant that more often than not, the audience was actually following what the speaker said! There was a great deal of discussion and interaction, and in this respect, this was one of the best workshops I have ever attended. (Rob van Glabbeek could always be relied on for interesting questions; one talk saw a remark (not by Rob): ``Can you please show that slide again $\ldots$ do the last three lines mean anything at all?'')

In my opinion, the workshop demonstrated the state of the art rather clearly. We understand partial-order based models of concurrency reasonably well (Glynn Winskel and Mogens Nielsen gave nice unifying presentations on these, with van Glabbeek and Pratt making a case for studying observations of partial orders). Identifying regular behaviours is hard (a convincing demonstration in the context of branching behaviours by Thiagarajan, and an excellent exposition on automata which accept partial orders---rather than strings or trees---by Wolfgang Thomas). On the logic side, there is darkness---what is a good logic, amenable to such methods? how much expressiveness can we get? ... (a clear elucidation by Rajeev Alur, and a wide-ranging survey by Allan Emerson). Current proof methods are inadequate (the presentations by Katz and Reisig were more interesting for the problems they pointed out than their own solutions). On the practical front, there is a feeling of frustration (a typical reaction is, ``OK, we can do this, but how far can we push these techniques?'').

Doron Peled hopes that this workshop is the beginning of a series and that others will take it up. I don't know about that, but there are many interesting unanswered questions here and these will certainly keep researchers occupied for a while yet.