Preface Volume 9

AbstractThis volume contains a selection of the papers which were presented at Infinity'97, the Second International Workshop on Verification of Infinite State Systems, which took place in Bologna (Italy) during 11-12 July 1997 as a satellite of ICALP'97, the 24th International Colloquium on Automata, Languages and Programming. The aim of the workshop was to provide a forum for researchers interested in the development of mathematical techniques for the analysis of infinite state systems. This topic has received a concerted effort over the past few years, particularly within the Concurrency Theory community. The basis of this effort has been the realization that an understanding of infinite state systems is necessary in order to have a complete picture of general process algebras, Petri nets, or other formalisms incorporating value-passing, real-time, hybrid, and/or probabilistic aspects. Its importance has grown however by the further realization that techniques which are developed for infinite state systems - particularly structural techniques - can potentially provide elegant solutions to the state-space explosion problem in the analysis of finite state systems, as well as to classical problems in language theory. Infinity'97 featured an invited talk given by Géraud Sénizergues (Bordeaux), who presented an overview of his recent proof of the long-standing open problem concerning the decidability of deterministic push-down automata. A lengthy extended abstract of this talk is included in this volume.The Program Committee for Infinity'97 included Ahmed Bouajjani (Grenoble), Julian Bradfield (Edinburgh), Didier Caucal (Rennes), Karel Culik II (South Carolina), Tom Henzinger (Berkeley), Kim Larsen (Aalborg), Faron Moller (Uppsala) and Bernhard Steffen (Passau). We would like to thank the above for their efforts, as well as the referees who assisted in the selection of the regular contributions among the submissions received. We also wish to thank the members of the local organising committee, in particular Roberto Gorrieri (Bologna), who made it possible to hold Infinity'97 as a satellite workshop of ICALP'97Faron MollerNovember 199