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; 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
• 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