Formální verifikace stochastických systémů s reálným časem

Poskytovatel

Grantová agentura České republiky

Program

Postdoktorandské granty

Veřejná soutěž

Postdoktorandské granty 12 (SGA02012GA1PD)

Hlavní účastníci

—

Druh soutěže

VS - Veřejná soutěž

Číslo smlouvy

P202-12-P612

Název projektu anglicky

Formal Verification of Stochastic Real-Time Systems

Anotace anglicky

We investigate formal verification techniques for systems that exhibit random behavior and operate under various real-time constraints (stochastic real-time systems, SRTS). Random aspects of systems are usually modeled using various kinds of stochastic processes. Real-time systems are typically modeled using variants of timed automata. In order to model SRTS, these formalisms have to be combined together. We concentrate on structural properties of such systems and computational complexity of basic verification problems. Another feature that is often present in real-world systems is nondeterminism, i.e. uncertainty without any statistical information. Nondeterminism also naturally occurs in problems where the goal is to synthesize an efficient controller of a system. SRTS with nondeterminism can be modeled using continuous-time decision processes with timed automata objectives. Here we are mainly interested in existence of controllers that achieve the objective and can be efficiently computed.

Kategorie VaV

ZV - Základní výzkum

CEP - hlavní obor

IN - Informatika

CEP - vedlejší obor

—

CEP - další vedlejší obor

—

OECD FORD - odpovídající obory <br>(dle <a href="http://www.vyzkum.cz/storage/att/E6EF7938F0E854BAE520AC119FB22E8D/Prevodnik_oboru_Frascati.pdf">převodníku</a>)

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Hodnocení poskytovatelem

U - Uspěl podle zadání (s publikovanými či patentovanými výsledky atd.)

Zhodnocení výsledků projektu

Projekt přinesl nové kvalitní výsledky v oblasti analýzy a verifikace stochastických systémů. Několik prací bylo přijato k publikaci a prezentováno na špičkových výzkumných fórech (jako jsou konference typu ICALP či LICS) a některé výsledky mají také po?

Zahájení řešení

1. 1. 2012

Ukončení řešení

31. 12. 2014

Poslední stav řešení

U - Ukončený projekt

Poslední uvolnění podpory

19. 3. 2014

Důvěrnost údajů

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

Systémové označení dodávky dat

CEP15-GA0-GP-U/02:2

Datum dodání záznamu

6. 5. 2016

Celkové uznané náklady

827 tis. Kč

Výše podpory ze státního rozpočtu

827 tis. Kč

Ostatní veřejné zdroje financování

0 tis. Kč

Neveřejné tuz. a zahr. zdroje finan.

0 tis. Kč