Semi-External LTL Model Checking
| Název česky | Semi-externí ověřování LTL vlastností modelů |
|---|---|
| Autoři | |
| Rok publikování | 2008 |
| Druh | Konferenční abstrakty |
| Fakulta / Pracoviště MU | |
| 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: |