TOP
Suche auf der Schloss Dagstuhl Webseite
Sie suchen nach Informationen auf den Webseiten der einzelnen Seminare? - Dann:
Nicht fündig geworden? - Einige unserer Dienste laufen auf separaten Webseiten mit jeweils eigener Suche. Bitte beachten Sie folgende Liste:
Schloss Dagstuhl - LZI - Logo
Schloss Dagstuhl Services
Seminare
Innerhalb dieser Seite:
Externe Seiten:
  • DOOR (zum Registrieren eines Dagstuhl Aufenthaltes)
  • DOSA (zum Beantragen künftiger Dagstuhl Seminare oder Dagstuhl Perspektiven Workshops)
Publishing
Innerhalb dieser Seite:
Externe Seiten:
dblp
Innerhalb dieser Seite:
Externe Seiten:
  • die Informatik-Bibliographiedatenbank dblp


Dagstuhl-Seminar 00181

Probabilistic Methods in Verification

( 30. Apr – 05. May, 2000 )

(zum Vergrößern in der Bildmitte klicken)

Permalink
Bitte benutzen Sie folgende Kurz-Url zum Verlinken dieser Seite: https://www.dagstuhl.de/00181

Organisatoren
  • Ch. Meinel (Trier)
  • M. Kwiatkowska (Birmingham)
  • M. Vardi (Houston)
  • U. Herzog (Erlangen)


Externe Veranstaltungsseite


Motivation

This seminar is a follow-on meeting for the PROBMIV'98 Workshop on Probabilistic Methods in Verification held as a satellite meeting of the IEEE Symposium on Logic in Computer Science (LICS'98). The PROBMIV'98 workshop was the first of its kind, gathering together researchers working across the whole spectrum of probabilistic methods in verification, from theory, through specification and verification techniques, to practical applications and experimental work. It became apparent during PROBMIV'98 that there is substantial convergence of interests of the different subgroups, and also commonality of the themes: as the verification field is maturing and becoming ready to tackle new application domains, those in performance analysis and randomization would like to see verification tools tailored to their needs.

Model checking, an algorithmic method for checking whether a system (typically an enriched automaton) satisfies a specification (e.g. a temporal or modal logic formula), has become an established industrial practice, and is being used widely in practical applications, particularly for checking hardware and communication protocols. A "model checker" is a software tool which inputs a description of a system, which it then converts to some space efficient representation (an automaton, or a BDD data structure), and a *specification* (e.g. a formula of logic, or an automaton), and produces an answer *yes* or *no* depending on whether the system satisfies the specification.

In conventional model checking, the answer computed by the model checker is delivered with certainty. The term "probabilistic model checking" (or "probabilistic verification") refers to a range of techniques where true-or-false answers are replaced with estimates of likelihood. There are two ways in which probability features in this area. The first approach concerns applying model checking to systems which inherently include probabilistic information: for example, communication protocols are probabilistic in the sense that they guarantee message delivery only with suitably high probability, say 0.95; and mean time to failure for hardware components typically follows a certain probability distribution. In this context, system descriptions are given in terms of variants of Markov processes, specifications as formulas of probabilistic extensions of temporal/modal logic, and the model checking algorithms compute *the probability* of a non-probabilistic formula being satisfied, based on an appropriately chosen probability space. This typically involves solving linear equation systems, or linear inequalities plus optimization if non-determinism is allowed.

The second, distinct but closely related, approach concerns systems which are non-probabilistic, but of size which makes exhaustive checking impractical or unfeasible. The aim is to use randomization to make model checking more efficient, albeit at a cost of establishing satisfaction with high probability, possibly with a one-sided error, rather than certainty. This can be achieved by randomizing branching points, and performing checks (of correctness or equivalence) on a proportion of paths through the system.

Model checking of non-probabilistic systems has developed very quickly from first algorithms into implementations of industrially relevant software tools, to mention smv, SPIN, fdr2. In contrast, model checking of probabilistic systems has not followed the same path: although the algorithms and proof systems have been known since mid-80's (Vardi, Courcoubetis & Yannakakis, Pnueli), little implementation work has been done up until now. As yet, there are no industrial strength probabilistic model checkers, and few proposals exist for heuristics and how to combat the state explosion problem. This unsatisfactory state of affairs is a result of the inherent difficulty of the issues, but these are not unsurmountable given the recent successes of model checking in practical applications.

One area likely to have an impact on probabilistic verification is performance modeling. Although the performance and probabilistic verification communities use different methodologies, their overall goals are quite similar. As in probabilistic verification, performance analysis involves building a probabilistic model of the system being considered (typically a continuous time Markov chain), and then performing a number of computational tasks to calculate steady-state probabilities and the associated performance measures. Currently the research focuses on designing description languages (for example, stochastic Petri nets and process algebras), and formulating efficient numerical methods and tools for solving thus derived models. Performance modeling can evidently serve as a useful source of expertise in Markovian analysis techniques and numerical computations not normally employed in conventional model checking, and in addition supply case studies for probabilistic verification.

The goal of this meeting is to promote cross-fertilization of ideas which have been developed independently in different contexts. More specifically, we aim:

  • to bring together researchers that do not necessarily meet at conferences, other than the specialist meetings such as this one,
  • facilitate exchange of expertise, for example the transfer of computational Markovian analysis techniques from performance analysis to verification, and state compression techniques from verification to other fields.

Teilnehmer
  • Ch. Meinel (Trier)
  • M. Kwiatkowska (Birmingham)
  • M. Vardi (Houston)
  • U. Herzog (Erlangen)