Safety Verification for Probabilistic Hybrid Systems

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F67985807%3A_____%2F12%3A00388817" target="_blank" >RIV/67985807:_____/12:00388817 - isvavai.cz</a>

Výsledek na webu

—

DOI - Digital Object Identifier

—

Jazyk výsledku

angličtina

Název v původním jazyce

Safety Verification for Probabilistic Hybrid Systems

Popis výsledku v původním jazyce

The interplay of random phenomena and continuous dynamics deserves increased attention, especially in the context of wireless sensing and control applications. Safety verification for such systems thus needs to consider probabilistic variants of systemswith hybrid dynamics. In safety verification of classical hybrid systems, we are interested in whether a certain set of unsafe system states can be reached from a set of initial states. In the probabilistic setting, we may ask instead whether the probability of reaching unsafe states is below some given threshold. In this paper, we consider probabilistic hybrid systems and develop a general abstraction technique for verifying probabilistic safety problems. This gives rise to the first mechanisable technique that can, in practice, formally verify safety properties of non-trivial continuous-time stochastic hybrid systems. Moreover, being based on abstractions computed by tools for the analysis of non-probabilistic hybrid systems, improvem

Název v anglickém jazyce

Safety Verification for Probabilistic Hybrid Systems

Popis výsledku anglicky

The interplay of random phenomena and continuous dynamics deserves increased attention, especially in the context of wireless sensing and control applications. Safety verification for such systems thus needs to consider probabilistic variants of systemswith hybrid dynamics. In safety verification of classical hybrid systems, we are interested in whether a certain set of unsafe system states can be reached from a set of initial states. In the probabilistic setting, we may ask instead whether the probability of reaching unsafe states is below some given threshold. In this paper, we consider probabilistic hybrid systems and develop a general abstraction technique for verifying probabilistic safety problems. This gives rise to the first mechanisable technique that can, in practice, formally verify safety properties of non-trivial continuous-time stochastic hybrid systems. Moreover, being based on abstractions computed by tools for the analysis of non-probabilistic hybrid systems, improvem

Druh

J_x - Nezařazeno - Článek v odborném periodiku (Jimp, Jsc a Jost)

CEP obor

IN - Informatika

OECD FORD obor

—

Projekt

Výsledek vznikl pri realizaci vícero projektů. Více informací v záložce Projekty.

Návaznosti

Z - Vyzkumny zamer (s odkazem do CEZ)

Rok uplatnění

2012

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název periodika

European Journal of Control

ISSN

0947-3580

e-ISSN

—

Svazek periodika

18

Číslo periodika v rámci svazku

6

Stát vydavatele periodika

GB - Spojené království Velké Británie a Severního Irska

Počet stran výsledku

15

Strana od-do

572-587

Kód UT WoS článku

000314389900006

EID výsledku v databázi Scopus

—