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

Result code in 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>

Result on the web

—

DOI - Digital Object Identifier

—

Result language

angličtina

Original language name

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

Original language description

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}.

Czech name

—

Czech description

—

Type

A - Audiovisual production

CEP classification

IN - Informatics

OECD FORD branch

—

Project

Result was created during the realization of more than one project. More information in the Projects tab.

Continuities

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

Publication year

2006

Confidentiality

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

ISBN

—

Place of publication

Brno

Publisher/client name

FI MU

Version

FIMU-RS-2006-05

Carrier ID

—