Vše

Co hledáte?

Vše
Projekty
Výsledky výzkumu
Subjekty

Rychlé hledání

  • Projekty podpořené TA ČR
  • Významné projekty
  • Projekty s nejvyšší státní podporou
  • Aktuálně běžící projekty

Chytré vyhledávání

  • Takto najdu konkrétní +slovo
  • Takto z výsledků -slovo zcela vynechám
  • “Takto můžu najít celou frázi”

MoChiBA: Probabilistic {LTL} Model Checking Using Limit-Deterministic Büchi Automata

Identifikátory výsledku

  • Kód výsledku v IS VaVaI

    <a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F16%3A00088473" target="_blank" >RIV/00216224:14330/16:00088473 - isvavai.cz</a>

  • Výsledek na webu

    <a href="http://dx.doi.org/10.1007/978-3-319-46520-3_9" target="_blank" >http://dx.doi.org/10.1007/978-3-319-46520-3_9</a>

  • DOI - Digital Object Identifier

    <a href="http://dx.doi.org/10.1007/978-3-319-46520-3_9" target="_blank" >10.1007/978-3-319-46520-3_9</a>

Alternativní jazyky

  • Jazyk výsledku

    angličtina

  • Název v původním jazyce

    MoChiBA: Probabilistic {LTL} Model Checking Using Limit-Deterministic Büchi Automata

  • Popis výsledku v původním jazyce

    The limiting factor for quantitative analysis of Markov decision processes (MDP) against specifications given in linear temporal logic (LTL) is the size of the generated product. As recently shown, a special subclass of limit-deterministic Büchi automata (LDBA) can replace deterministic Rabin automata in quantitative probabilistic model checking algorithms. We present an extension of PRISM for LTL model checking of MDP using LDBA. While existing algorithms can be used only with minimal changes, the new approach takes advantage of the special structure and the smaller size of the obtained LDBA to speed up the model checking. We demonstrate the speed up experimentally by a comparison with other approaches.

  • Název v anglickém jazyce

    MoChiBA: Probabilistic {LTL} Model Checking Using Limit-Deterministic Büchi Automata

  • Popis výsledku anglicky

    The limiting factor for quantitative analysis of Markov decision processes (MDP) against specifications given in linear temporal logic (LTL) is the size of the generated product. As recently shown, a special subclass of limit-deterministic Büchi automata (LDBA) can replace deterministic Rabin automata in quantitative probabilistic model checking algorithms. We present an extension of PRISM for LTL model checking of MDP using LDBA. While existing algorithms can be used only with minimal changes, the new approach takes advantage of the special structure and the smaller size of the obtained LDBA to speed up the model checking. We demonstrate the speed up experimentally by a comparison with other approaches.

Klasifikace

  • Druh

    D - Stať ve sborníku

  • CEP obor

    IN - Informatika

  • OECD FORD obor

Návaznosti výsledku

  • Projekt

    <a href="/cs/project/GA15-17564S" target="_blank" >GA15-17564S: Teorie her jako prostředek pro formální analýzu a verifikaci počítačových systémů</a><br>

  • Návaznosti

    P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Ostatní

  • Rok uplatnění

    2016

  • 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ů

Údaje specifické pro druh výsledku

  • Název statě ve sborníku

    Automated Technology for Verification and Analysis - 14th International Symposium, ATVA 2016

  • ISBN

    9783319465197

  • ISSN

    0302-9743

  • e-ISSN

  • Počet stran výsledku

    8

  • Strana od-do

    130-137

  • Název nakladatele

    Springer

  • Místo vydání

    Switzerland

  • Místo konání akce

    Switzerland

  • Datum konání akce

    1. 1. 2016

  • Typ akce podle státní příslušnosti

    CST - Celostátní akce

  • Kód UT WoS článku