I/O Efficient Model Checking

Logo poskytovatele

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 I/O-efektivní ověřování modelů
Autoři

ŠIMEČEK Pavel

Rok publikování 2008
Druh Další prezentace na konferencích
Fakulta / Pracoviště MU

Fakulta informatiky

Citace
Popis Jednou z cest, jak navýšit dostupnou paměť pro algoritmy ověřování modelů, je využití externí paměti, obzvláště hard disků. Naneštěstí, není znám žádný algoritmus založený na DFS, který by se choval efektivně v prostředí externí paměti. Ukazujeme, jak adaptovat existující algoritmy OWCTY a MAP pro detekci akceptujících cyklů založené na BFS pro I/O-efektivní použití a porovnáváme jejich I/O efektivitu a praktický výkon s existujícím přístupem k I/O-efektivnímu ověřování LTL vlastností modelů od autorů Stefana Edelkampa a Shahida Jabbara. Nové algoritmy vykazují podobnou I/O složitost s ohledem na velikost grafu, ale vyhýbají se kvadratickému nárůstu velikosti vstupního grafu. Proto je počet vykonaných I/O operací podstatně nižší a algoritmy vykazují lepší praktický výkon.
Související projekty:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.