Quantitative Multi-objective Verification for Probabilistic Systems.
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 performa...
| Main Authors: | , , , , |
|---|---|
| Other Authors: | |
| Format: | Journal article |
| Language: | English |
| Published: |
Springer
2011
|
| _version_ | 1797056202566270976 |
|---|---|
| author | Forejt, V Kwiatkowska, M Norman, G Parker, D Qu, H |
| author2 | Abdulla, P |
| author_facet | Abdulla, P Forejt, V Kwiatkowska, M Norman, G Parker, D Qu, H |
| author_sort | Forejt, V |
| collection | OXFORD |
| description | 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. © 2011 Springer-Verlag. |
| first_indexed | 2024-03-06T19:20:01Z |
| format | Journal article |
| id | oxford-uuid:19c1bcc0-15ef-40cb-8c84-ddd13388cd14 |
| institution | University of Oxford |
| language | English |
| last_indexed | 2024-03-06T19:20:01Z |
| publishDate | 2011 |
| publisher | Springer |
| record_format | dspace |
| spelling | oxford-uuid:19c1bcc0-15ef-40cb-8c84-ddd13388cd142022-03-26T10:50:51ZQuantitative Multi-objective Verification for Probabilistic Systems.Journal articlehttp://purl.org/coar/resource_type/c_dcae04bcuuid:19c1bcc0-15ef-40cb-8c84-ddd13388cd14EnglishSymplectic Elements at OxfordSpringer2011Forejt, VKwiatkowska, MNorman, GParker, DQu, HAbdulla, PLeino, KWe 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. © 2011 Springer-Verlag. |
| spellingShingle | Forejt, V Kwiatkowska, M Norman, G Parker, D Qu, H Quantitative Multi-objective Verification for Probabilistic Systems. |
| title | Quantitative Multi-objective Verification for Probabilistic Systems. |
| title_full | Quantitative Multi-objective Verification for Probabilistic Systems. |
| title_fullStr | Quantitative Multi-objective Verification for Probabilistic Systems. |
| title_full_unstemmed | Quantitative Multi-objective Verification for Probabilistic Systems. |
| title_short | Quantitative Multi-objective Verification for Probabilistic Systems. |
| title_sort | quantitative multi objective verification for probabilistic systems |
| work_keys_str_mv | AT forejtv quantitativemultiobjectiveverificationforprobabilisticsystems AT kwiatkowskam quantitativemultiobjectiveverificationforprobabilisticsystems AT normang quantitativemultiobjectiveverificationforprobabilisticsystems AT parkerd quantitativemultiobjectiveverificationforprobabilisticsystems AT quh quantitativemultiobjectiveverificationforprobabilisticsystems |