Anzeige
Erschienen in:
2011 | OriginalPaper | Buchkapitel
Quantitative Multi-objective Verification for Probabilistic Systems
verfasst von : Vojtěch Forejt, Marta Kwiatkowska, Gethin Norman, David Parker, Hongyang Qu
Erschienen in: Tools and Algorithms for the Construction and Analysis of Systems
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
We present a verification framework for analysing multiple quantitative objectives of systems that exhibit both nondeterministic and stochastic behaviour. These systems are modelled as probabilistic automata, enriched with cost or reward structures that capture, for example, energy usage or performance metrics. Quantitative properties of these models are expressed in a specification language that incorporates probabilistic safety and liveness properties, expected total cost or reward, and supports multiple objectives of these types. We propose and implement an efficient verification framework for such properties and then present two distinct applications of it: firstly,
controller synthesis
subject to multiple quantitative objectives; and, secondly, quantitative
compositional verification
. The practical applicability of both approaches is illustrated with experimental results from several large case studies.