Relaxed Cycle Condition Improves Partial Order Reduction

Varování

Publikace nespadá pod Ekonomicko-správní fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.

Název česky	Oslabení podmínky na cykly zlepšující redukci pomocí reprezentantů
Autoři	MORAVEC Pavel ŠIMŠA Jiří
Rok publikování	2007
Druh	Článek ve sborníku
Konference	3rd Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2007)
Fakulta / Pracoviště MU	Fakulta informatiky
Citace
Obor	Informatika
Klíčová slova	model checking; partial order reduction; proviso checking
Popis	Redukce pomocí reprezentantů je metoda široce používaná na boj se stavovou explozí. V článku se zaměřujeme na teoretické zjemnění konkrétní instance této redukce pro logiku LTL. Tato instance je representována množinou podmínek C0 až C3 které popisují platné redukce stavového prostoru. Navrhujeme hierarchii alternativ k podmínce C3. V této hierarchii ukážeme které alternativy k C3 garantují platnou redukci vzhledem k LTL vlastnostem.
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