Preface Volume 22

AbstractThis volume contains the proceedings of the First International Workshop on Probabilistic Methods in Verification (PROBMIV′98) held 19-20 June 1998 in Indianapolis, Indiana, USA, as a satellite event to the Thirteenth International IEEE Symposium on Logic in Computer Science (LICS′98).Probabilistic reasoning and modelling inherently features in the design processes for software and hardware systems, either as a means to derive efficient solutions (e.g. randomisation), or as a result of unreliable or unpredictable behaviour (e.g. in fault-tolerant systems, computer networks, etc.). Probabilistic verificationencompasses a range of theoretical, algorithmic and programming methods that assist in establishing the correctness of probabilistic systems against specifications. Typically such methods involve calculating the probability bounds for a temporal logic formula being satisfied, based on an appropriate probability space on computations, but also include the analysis of properties with respect to cost and long-run average behaviour. Additionally, probabilistic verification can provide guarantees that specifications hold with satisfactory probability in cases when conventional property verification, such as model checking, is not feasible.This two-day workshop aimed to and succeeded in getting together researchers whose work ranges across the whole spectrum of probabilistic methods, from computational linear algebra and semantics, through probabilistic languages and logics, to model checking algorithms and implementation work. The workshop was held in an informal atmosphere, with lively discussions. Its programme consisted of ten invited lectures, seven accepted submissions and a panel discussion. The invited speakers were: Rajeev Alur(University of Pennsylvania)Luca de Alfaro(University of California at Berkeley)Christel Baier &Vicky Hartonas-Garmhausen(Mannheim University)(Carnegie Mellon University)Jeremy Gunawardena(BRIMS, Hewlett-Packard Labs)Marek Karpinski(University of Bonn)Annabelle McIver(Oxford University)Prakash Panangaden(McGill University)Roberto Segala(University of Bologna)K Narayan Kumar(SUNY Stony Brook)Moshe Vardi(Rice University)The panel discussion focused on the question“What tools and theory are needed in order to make probabilistic verification practical?”It began with a position statement by Moshe Vardi who identified the key reasons for, in his view, the success of conventional model checking in practice, and the challenges that researchers in probabilistic verification have yet to address: efficient data structures, good heuristics, methods for dealing with very large state-space systems, the ability to generate insightful counter-traces if systems fail to meet a specified property, and convincing applications and case studies. Marek Karpinski emphasised one advantage of probabilistic verification: that it can compute epsilon-approximations to otherwise infeasible problems with high probability. Rajeev Alur pointed out the lack of existing tools in this area and encouraged work on probabilistic on-the-fly model checking. Prakash Panangaden argued for the development of a robust mathematical theory for modelling and reasoning about probabilistic systems. He also wanted to see a closer connection of such work with the contributions of performance modelling, which has well developed tools and analysis methodologies. Jeremy Gunawardena encouraged this scientific community to design appropriate languages, models, algorithms and tools that are capable of reasoning about, e.g., internet traffic. It was felt that probabilistic verification will continue to gain in importance because of the many real-world phenomena in need of a probabilistic and stochastic analysis: computer networks, the Ethernet, etc.As we write this foreword, the second PROBMIV workshop, PROBMIV′99, is well underway and there is a Dagstuhl Seminar on this subject planned for May 2000. We thus offer you this collection of papers, and hope you will find it useful and stimulating!The organisers gratefully acknowledge partial support from Basic Research Institute in the Mathematical Sciences (BRIMS), Hewlett-Packard, Bristol, and also the European Commission via Esprit Working Group FIREworks (23531).Christel Baier, Michael Huth (Co-Chair), Marta Kwiatkowska (Co-Chair)Mark Ryan, Guest Editor