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

Varování

Publikace nespadá pod Ústav výpočetní techniky, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.

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 KŘETÍNSKÝ Mojmír ŘEHÁK Vojtěch STREJČEK Jan
Rok publikování	2006
Druh	Prezentace v oblasti VaV (AV tvorba, WEB aplikace apod.)
Fakulta / Pracoviště MU	Fakulta informatiky
Citace
Popis	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".
Související projekty:	Integrovaný přístup k výchově studentů DSP v oblasti paralelních a distribuovaných systémů Techniky automatické verifikace a validace softwarových a hardwarových systémů Institut Teoretické Informatiky Vysoce paralelní a distribuované výpočetní systémy Automatizovaná verifikace softwaru