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”

Model checking LTL with regular valuations for pushdown systems

Identifikátory výsledku

  • Kód výsledku v IS VaVaI

    <a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F03%3A00008160" target="_blank" >RIV/00216224:14330/03:00008160 - isvavai.cz</a>

  • Výsledek na webu

  • DOI - Digital Object Identifier

Alternativní jazyky

  • Jazyk výsledku

    angličtina

  • Název v původním jazyce

    Model checking LTL with regular valuations for pushdown systems

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

    Recent works have proposed pushdown systems as a tool for analyzing programs with (recursive) procedures, and the model-checking problem for LTL has been devoted special attention. However, all these works impose a strong restriction on the possible valuations of atomic propositions: whether a configuration of the pushdown system satisfies an atomic proposition or not can only depend on the current control state of the pushdown automaton and on its topmost stack symbol. In this paper we consider LTL with regular valuations: the set of configurations satisfying an atomic proposition can be an arbitrary regular language. The model-checking problem is solved via two different techniques, with an eye on efficiency. The resulting algorithms are proved to beasymptotically optimal. We show that the extension to regular valuations allows to model problems in different areas, like data-flow analysis and analysis of systems with checkpoints. We claim that our model-checking algorithms provide a

  • Název v anglickém jazyce

    Model checking LTL with regular valuations for pushdown systems

  • Popis výsledku anglicky

    Recent works have proposed pushdown systems as a tool for analyzing programs with (recursive) procedures, and the model-checking problem for LTL has been devoted special attention. However, all these works impose a strong restriction on the possible valuations of atomic propositions: whether a configuration of the pushdown system satisfies an atomic proposition or not can only depend on the current control state of the pushdown automaton and on its topmost stack symbol. In this paper we consider LTL with regular valuations: the set of configurations satisfying an atomic proposition can be an arbitrary regular language. The model-checking problem is solved via two different techniques, with an eye on efficiency. The resulting algorithms are proved to beasymptotically optimal. We show that the extension to regular valuations allows to model problems in different areas, like data-flow analysis and analysis of systems with checkpoints. We claim that our model-checking algorithms provide a

Klasifikace

  • Druh

    J<sub>x</sub> - Nezařazeno - Článek v odborném periodiku (Jimp, Jsc a Jost)

  • CEP obor

    IN - Informatika

  • OECD FORD obor

Návaznosti výsledku

  • Projekt

    <a href="/cs/project/GA201%2F00%2F1023" target="_blank" >GA201/00/1023: Algoritmy a nástroje pro praktickou verifikaci souběžných systémů</a><br>

  • Návaznosti

    Z - Vyzkumny zamer (s odkazem do CEZ)

Ostatní

  • Rok uplatnění

    2003

  • 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

    Information and Computation

  • ISSN

    0890-5401

  • e-ISSN

  • Svazek periodika

    186

  • Číslo periodika v rámci svazku

    2

  • Stát vydavatele periodika

    US - Spojené státy americké

  • Počet stran výsledku

    22

  • Strana od-do

    355

  • Kód UT WoS článku

  • EID výsledku v databázi Scopus