Quantitative Multi-Objective Verification for Probabilistic Systems

Varování

Publikace nespadá pod Filozofickou fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.
Autoři

FOREJT Vojtěch KWIATKOWSKA Marta NORMAN Gethin PARKER David QU Hongyang

Rok publikování 2011
Druh Článek ve sborníku
Konference Proc. 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'11)
Fakulta / Pracoviště MU

Fakulta informatiky

Citace
Doi http://dx.doi.org/10.1007/978-3-642-19835-9_11
Obor Informatika
Klíčová slova stochastic systems; verification; multi-objective optimisation
Popis 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.
Související projekty:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.