This volume contains the proceedings of the First International Workshop on Verification of Infinite State Systems (Infinity'96), which took place at the University of Pisa (Italy), 30-31 August, 1996, as a satelite of CONCUR'96, the 7th International Conference on Concurrency Theory.
Aim of the workshop is to provide a forum for researchers interested in the development of mathematical techniques for the analysis of infinite state systems, a topic which has received a concerted effort within the Concurrency Theory community over the past few years. 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. Possible topics for inclusion are: decidability issues for equivalence and model checking over various classes of infinite state systems; complexity results for decidability results; connections and applications to questions in classical automata and formal language theory; and tools and case studies involving nontrivial applications of methods for the analysis of infinite state systems.
In addition to the regular sessions, Infinity featured three invited talks, given by Yoram Hirschfeld, Thomas A. Henzinger, and Javier Esparza.
We would like to thank the program committee, composed by Julian Bradfield (Edinburgh), Didier Caucal (Rennes), Faron Moller (Stockholm), Bernhard Steffen (Passau), and all the referees who assisted in the selection of the regular contributions among the 24 submissions received.
Finally, our warm thanks are due to the Local Organization Committee, in particular to Vladimiro Sassone, Corrado Priami, Pierpaolo Degano, and Ugo Montanari, who made Infinity possible.
July 1996
Bernhard Steffen
Tiziana Margaria
Ulrike Peiker, Martin Griebl