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”

Comparison of LTL to Deterministic Rabin Automata Translators

Identifikátory výsledku

  • Kód výsledku v IS VaVaI

    <a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F13%3A00066512" target="_blank" >RIV/00216224:14330/13:00066512 - isvavai.cz</a>

  • Výsledek na webu

    <a href="http://dx.doi.org/10.1007/978-3-642-45221-5_12" target="_blank" >http://dx.doi.org/10.1007/978-3-642-45221-5_12</a>

  • DOI - Digital Object Identifier

    <a href="http://dx.doi.org/10.1007/978-3-642-45221-5_12" target="_blank" >10.1007/978-3-642-45221-5_12</a>

Alternativní jazyky

  • Jazyk výsledku

    angličtina

  • Název v původním jazyce

    Comparison of LTL to Deterministic Rabin Automata Translators

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

    Increasing interest in control synthesis and probabilistic model checking caused recent development of LTL to deterministic omega-automata translation. The standard approach represented by ltl2dstar tool employs Safra's construction to determinize a Büchi automaton produced by some LTL to Büchi automata translator. Since 2012, three new LTL to deterministic Rabin automata translators appeared, namely Rabinizer, LTL3DRA, and Rabinizer 2. They all avoid Safra's construction and work on LTL fragments only.We compare performance and automata produced by the mentioned tools, where ltl2dstar is combined with several LTL to Büchi automata translators: besides traditionally used LTL2BA, we also consider LTL-&gt;NBA, LTL3BA, and Spot.

  • Název v anglickém jazyce

    Comparison of LTL to Deterministic Rabin Automata Translators

  • Popis výsledku anglicky

    Increasing interest in control synthesis and probabilistic model checking caused recent development of LTL to deterministic omega-automata translation. The standard approach represented by ltl2dstar tool employs Safra's construction to determinize a Büchi automaton produced by some LTL to Büchi automata translator. Since 2012, three new LTL to deterministic Rabin automata translators appeared, namely Rabinizer, LTL3DRA, and Rabinizer 2. They all avoid Safra's construction and work on LTL fragments only.We compare performance and automata produced by the mentioned tools, where ltl2dstar is combined with several LTL to Büchi automata translators: besides traditionally used LTL2BA, we also consider LTL-&gt;NBA, LTL3BA, and Spot.

Klasifikace

  • Druh

    D - Stať ve sborníku

  • CEP obor

    IN - Informatika

  • OECD FORD obor

Návaznosti výsledku

  • Projekt

    <a href="/cs/project/GAP202%2F10%2F1469" target="_blank" >GAP202/10/1469: Formální metody pro analýzu a verifikaci komplexních systémů</a><br>

  • Návaznosti

    P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>S - Specificky vyzkum na vysokych skolach

Ostatní

  • Rok uplatnění

    2013

  • 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

    Logic for Programming Artificial Intelligence and Reasoning, LPAR-19

  • ISBN

    9783642452208

  • ISSN

    0302-9743

  • e-ISSN

  • Počet stran výsledku

    9

  • Strana od-do

    164-172

  • Název nakladatele

    Springer

  • Místo vydání

    Berlin Heidelberg

  • Místo konání akce

    Stellenbosch, South Africa

  • Datum konání akce

    1. 1. 2013

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

    WRD - Celosvětová akce

  • Kód UT WoS článku