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”

On clock-aware LTL parameter synthesis of timed 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%2F18%3A00101069" target="_blank" >RIV/00216224:14330/18:00101069 - isvavai.cz</a>

  • Výsledek na webu

    <a href="https://www.sciencedirect.com/science/article/pii/S2352220817300354" target="_blank" >https://www.sciencedirect.com/science/article/pii/S2352220817300354</a>

  • DOI - Digital Object Identifier

    <a href="http://dx.doi.org/10.1016/j.jlamp.2018.05.004" target="_blank" >10.1016/j.jlamp.2018.05.004</a>

Alternativní jazyky

  • Jazyk výsledku

    angličtina

  • Název v původním jazyce

    On clock-aware LTL parameter synthesis of timed automata

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

    The parameter synthesis problem for timed automata is undecidable in general even for very simple reachability properties. In this paper we introduce restrictions on parameter valuations under which the parameter synthesis problem is decidable for Clock-Aware LTL properties. The investigated bounded integer parameter synthesis problem could be solved using an explicit enumeration of all possible parameter valuations. We propose an alternative symbolic zone-based method for this problem which can result in a faster computation. Our technique adapts the ideas of the automata-based approach to Clock-Aware LTL model checking of timed automata. In order to simplify the explanation of our method, we first introduce a parameter synthesis algorithm for timed automata, then we describe method for checking Clock-Aware LTL properties of timed automata and finally we combine these two methods together to provide general parameter synthesis algorithm for Clock-Aware LTL properties. To demonstrate the usefulness of our approach, we provide experimental evaluation and compare the proposed method with the explicit enumeration technique.

  • Název v anglickém jazyce

    On clock-aware LTL parameter synthesis of timed automata

  • Popis výsledku anglicky

    The parameter synthesis problem for timed automata is undecidable in general even for very simple reachability properties. In this paper we introduce restrictions on parameter valuations under which the parameter synthesis problem is decidable for Clock-Aware LTL properties. The investigated bounded integer parameter synthesis problem could be solved using an explicit enumeration of all possible parameter valuations. We propose an alternative symbolic zone-based method for this problem which can result in a faster computation. Our technique adapts the ideas of the automata-based approach to Clock-Aware LTL model checking of timed automata. In order to simplify the explanation of our method, we first introduce a parameter synthesis algorithm for timed automata, then we describe method for checking Clock-Aware LTL properties of timed automata and finally we combine these two methods together to provide general parameter synthesis algorithm for Clock-Aware LTL properties. To demonstrate the usefulness of our approach, we provide experimental evaluation and compare the proposed method with the explicit enumeration technique.

Klasifikace

  • Druh

    J<sub>imp</sub> - Článek v periodiku v databázi Web of Science

  • CEP obor

  • OECD FORD obor

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

Návaznosti výsledku

  • Projekt

    <a href="/cs/project/GA18-02177S" target="_blank" >GA18-02177S: Abstrakce a jiné techniky v semi-symbolické verifikaci programů</a><br>

  • Návaznosti

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

Ostatní

  • Rok uplatnění

    2018

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

    Journal of Logical and Algebraic Methods in Programming

  • ISSN

    2352-2208

  • e-ISSN

  • Svazek periodika

    99

  • Číslo periodika v rámci svazku

    Oct

  • Stát vydavatele periodika

    US - Spojené státy americké

  • Počet stran výsledku

    29

  • Strana od-do

    114-142

  • Kód UT WoS článku

    000437073800005

  • EID výsledku v databázi Scopus

    2-s2.0-85083038238