Semi-External LTL Model Checking

Logo poskytovatele

Varování

Publikace nespadá pod Filozofickou fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.
Název česky Semi-externí ověřování LTL vlastností modelů
Autoři

ŠIMEČEK Pavel EDELKAMP Stefan SANDERS Peter

Rok publikování 2008
Druh Konferenční abstrakty
Fakulta / Pracoviště MU

Fakulta informatiky

Citace
Popis V tomto článku zavádíme c-bit semi-externí grafové algoritmy -- tj. algoritmy, které potřebují pouze konstantní počet c bitů v interní paměti na každý vrchol grafu. V tomto uspořádání dostávámé nový kompromis mezi využitím času a paměti v I/O-efektivním ověřování LTL vlastností modelů: V porovnání s dřívějšími externími algoritmy je nový algoritmus rychlejší, ale jeho vnitřní paměťová složitost je závislá na velikosti stavového prostoru. Nejdříve navrhujeme c-bit semi-externí algoritmus pro prohledávání do hloubky. Abychom dosáhli nízkou spotřebu vnitřní paměti, vytváříme perfektní hašovací funkci efektivní vzhledem k paměti RAM z množiny vrcholů uložené na disku. Konstrukce perfektní hašovací funkce je založena na algoritmu autorského kolektivu kolem Fabiana C. Botelha. S danou perfektní hašovací funkcí, prohledávání do hlouky ukládá pouze jeden bit pro každý vrchol značující, které vrcholy již byly navštíveny. Protože uložení perfektní hašovací funkce zabírá rovněž jen konstantní počet bitů na stav, celkový počet bitů na stav je konstantní. Podobný algoritmus vytváříme rovněž pro dvojité prohledávání do hloubky, které ověřuje přítomnost akceptujícího cyklu a tímto způsobem řeší problém ověřování LTL vlastností modelů. I/O složitost samotného hledání je úměrná času hledání v prohledáváném prostoru. Pro ověřování modelů za běhu používáme v strategii iterativního prohlubování známou z ohraničeného ověřování modelů.
Související projekty:

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