O rozhodnutelnosti problému ověřování modelu pro LTL a procesové přepisovací systémy

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F06%3A00015417" target="_blank" >RIV/00216224:14330/06:00015417 - isvavai.cz</a>

Výsledek na webu

—

DOI - Digital Object Identifier

—

Jazyk výsledku

angličtina

Název v původním jazyce

On Decidability of LTL Model Checking for 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 Process Rewrite Systems (PRS), possibly extended with a weak finite-state control unit, and properties described by basic fragments of action-based 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 weconsider properties defined by formulae with only modalities "strict eventually" and "strict always". Moreover, we show that the problem remains undecidable for PA processes even with respect to the LTL fragment with the only modality "until" or the fragment with modalities "next" and "infinitely often".

Název v anglickém jazyce

On Decidability of LTL Model Checking for Process Rewrite Systems

Popis výsledku anglicky

We establish a decidability boundary of the model checking problem for infinite-state systems defined by Process Rewrite Systems (PRS), possibly extended with a weak finite-state control unit, and properties described by basic fragments of action-based 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 weconsider properties defined by formulae with only modalities "strict eventually" and "strict always". Moreover, we show that the problem remains undecidable for PA processes even with respect to the LTL fragment with the only modality "until" or the fragment with modalities "next" and "infinitely often".

Druh

D - Stať ve sborníku

CEP obor

IN - Informatika

OECD FORD obor

—

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)

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ů

Název statě ve sborníku

FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science, 26th International Conference, Kolkata, India, December 13-15, 2006, Proceedings

ISBN

978-3-540-49994-7

ISSN

—

e-ISSN

—

Počet stran výsledku

12

Strana od-do

248-259

Název nakladatele

Springer-Verlag

Místo vydání

Berlin

Místo konání akce

Kolkata, India

Datum konání akce

1. 1. 2006

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

WRD - Celosvětová akce

Kód UT WoS článku

—