Relaxed Cycle Condition Improves Partial Order Reduction

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