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 Decidability of LTL Model Checking for Weakly Extended Process Rewrite 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%2F06%3A00015439" target="_blank" >RIV/00216224:14330/06:00015439 - 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

    On Decidability of LTL Model Checking for Weakly Extended Process Rewrite Systems

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

    We establish a decidability boundary of the model checking problem for infinite-state systems defined by emph{Process Rewrite Systems} (PRS) or emph{weakly extended Process Rewrite Systems} (wPRS), % possibly extended with a weak finite-state control unit, and properties described by basic fragments of action-based emph{Linear Temporal Logic} (LTL). It is known that the problem for general LTL properties is decidable for Petri nets and for pushdown processes, while it is undecidable for PA processes.As our main result, we show that the problem is decidable for wPRS if we consider properties defined by formulae with only modalities emph{strict eventually} and emph{strict always}. Moreover, we show that the problem remains undecidable for PA processes even with respect to the LTL fragment with the only modality emph{until} or the fragment with modalities emph{next} and emph{infinitely often}.

  • Název v anglickém jazyce

    On Decidability of LTL Model Checking for Weakly Extended Process Rewrite Systems

  • Popis výsledku anglicky

    We establish a decidability boundary of the model checking problem for infinite-state systems defined by emph{Process Rewrite Systems} (PRS) or emph{weakly extended Process Rewrite Systems} (wPRS), % possibly extended with a weak finite-state control unit, and properties described by basic fragments of action-based emph{Linear Temporal Logic} (LTL). It is known that the problem for general LTL properties is decidable for Petri nets and for pushdown processes, while it is undecidable for PA processes.As our main result, we show that the problem is decidable for wPRS if we consider properties defined by formulae with only modalities emph{strict eventually} and emph{strict always}. Moreover, we show that the problem remains undecidable for PA processes even with respect to the LTL fragment with the only modality emph{until} or the fragment with modalities emph{next} and emph{infinitely often}.

Klasifikace

  • Druh

    A - Audiovizuální tvorba

  • CEP obor

    IN - Informatika

  • OECD FORD obor

Návaznosti výsledku

  • Projekt

    Výsledek vznikl pri realizaci vícero projektů. Více informací v záložce Projekty.

  • Návaznosti

    P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>Z - Vyzkumny zamer (s odkazem do CEZ)

Ostatní

  • Rok uplatnění

    2006

  • 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

  • ISBN

  • Místo vydání

    Brno

  • Název nakladatele resp. objednatele

    FI MU

  • Verze

    FIMU-RS-2006-05

  • Identifikační číslo nosiče