Model Checking Large Finite-State Systems and Beyond

• Název česky: Ověřování modelu pro rozsáhlé konečně stavové systémy a za jejich hranicemi
• Autoři: BRIM Luboš; KŘETÍNSKÝ Mojmír
• Rok publikování: 2007
• Druh: Článek ve sborníku
• Konference: 33rd Conference on Current Trends in Theory and Practice of Computer Science
• Fakulta / Pracoviště MU: Fakulta informatiky
• Obor: Informatika
• Klíčová slova: finite and infinite-state systems; reachability; linear time logic; model checking; decidability
• Popis: Je ustanovena hranice rozhodnutelnosti pro problém ověřování modelu pro fragmenty logik HM resp. LTL a nekonečně stavové systémy generované tzv. procesovými přepisovacími systémy (eventuelně rozšířenými o tzv.slabou 59dic9 jednotku.

Související projekty

• 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