Informační systém Masarykovy univerzity 

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

česky | in English

BOZZELLI, Laura, Mojmír KŘETÍNSKÝ, Vojtěch ŘEHÁK a Jan STREJČEK. On Decidability of LTL Model Checking for Weakly Extended Process Rewrite Systems. Brno: FI MU, 2006. FIMU-RS-2006-05.
Další formáty:   BibTeX LaTeX RIS
Základní údaje
Originální název On Decidability of LTL Model Checking for Weakly Extended Process Rewrite Systems
Název česky O rozhodnutelnosti problému ověřování modelu pro LTL a slabě royšířené procesové přepisovací systémy
Autoři BOZZELLI, Laura (380 Itálie), Mojmír KŘETÍNSKÝ (203 Česká republika, garant), Vojtěch ŘEHÁK (203 Česká republika) a Jan STREJČEK (203 Česká republika).
Vydání Brno, FIMU-RS-2006-05, 2006.
Nakladatel FI MU
Další údaje
Originální jazyk angličtina
Typ výsledku Audiovizuální tvorba
Obor Informatika
Stát vydavatele Česká republika
Utajení není předmětem státního či obchodního tajemství
WWW URL
Kód RIV RIV/00216224:14330/06:00015439
Organizační jednotka Fakulta informatiky
Klíčová slova anglicky infinite-state systems; linear time logic; decidability; model checking
Štítky decidability, infinite-state systems, linear time logic, Model checking
Příznaky Mezinárodní význam
Změnil Změnil: RNDr. Vojtěch Řehák, Ph.D., učo 3721. Změněno: 31. 3. 2010 15:19.
Anotace
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}.
Anotace česky
Je ustanovena hranice rozhodnutelnosti pro problém ověřování modelu pro fragmenty logiky LTL a nekonečně stavové systémy generované tzv. procesovými přepisovacími systémy (eventuelně rozšířenými o tzv. slabou konečně stavovou řídicí jednotku). Zejména je ukázáno, že tento problém je rozhodnutelný na celé zmíněné třídě pro LTL frament s modalitami "strict always" a "strict eventually". Problém je nerozhodnutelný pro třídu PA procesů a fragment s modalitou "until" resp. fragment s modalitami "next" a "infinitely often".
Návaznosti
GA201/06/1338, projekt VaVNázev: Automatizovaná verifikace softwaru
Investor: Grantová agentura ČR, Standardní projekty
GD102/05/H050, projekt VaVNázev: Integrovaný přístup k výchově studentů DSP v oblasti paralelních a distribuovaných systémů
Investor: Grantová agentura ČR, Doktorské granty
MSM0021622419, záměrNázev: Vysoce paralelní a distribuované výpočetní systémy
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Výzkumné záměry
1ET408050503, projekt VaVNázev: Techniky automatické verifikace a validace softwarových a hardwarových systémů
Investor: Akademie věd ČR, Informační společnost (Národní program výzkumu)
1M0545, projekt VaVNázev: Institut Teoretické Informatiky
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Výzkumná centra (Národní program výzkumu)
VytisknoutZobrazeno: 14. 12. 2017 14:00

Relevantní odkazy 


Nahoru | Aktuální datum a čas: 14. 12. 2017 14:00, 50. (sudý) týden

Kontakty: istech(zavináč/atsign)fi(tečka/dot)muni(tečka/dot)cz, studijní odd., správci práv, is-technici, e-technici, IT podpora | Použití cookies | Více o Informačním systému