Skip to main content

2004 | OriginalPaper | Buchkapitel

Verifying Qualitative Properties of Probabilistic Programs

verfasst von : Benedikt Bollig, Martin Leucker

Erschienen in: Validation of Stochastic Systems

Verlag: Springer Berlin Heidelberg

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

In this chapter, we present procedures for checking linear temporal logic and automata specifications of sequential and concurrent probabilistic programs. We follow two different approaches: For LTL and sequential probabilistic programs, our method proceeds in a tableau style fashion, while the remaining procedures are based on automata theory.

Metadaten
Titel
Verifying Qualitative Properties of Probabilistic Programs
verfasst von
Benedikt Bollig
Martin Leucker
Copyright-Jahr
2004
Verlag
Springer Berlin Heidelberg
DOI
https://doi.org/10.1007/978-3-540-24611-4_4