Semi-external LTL Model Checking
| Název česky | Semi-externí ověřování LTL vlastností modelů |
|---|---|
| Autoři | |
| Rok publikování | 2008 |
| Druh | Článek ve sborníku |
| Konference | 20th International Conference on Computer Aided Verification |
| Fakulta / Pracoviště MU | |
| Citace | |
| Obor | Informatika |
| Klíčová slova | semi-external;model checking;external;I/O complexity |
| Popis | V tomto článku zavádíme pojem c-bit semi-externích grafových algoritmů - tj. algoritmů, které potřebují pouze konstantní počet bitů ve vnitřní paměti na každý vrchol. V takovém uspořádání dostáváme nové vyvážení nákladů mezi časem a pamětí pro I/O-efektivní ověřování LTL vlastností modelů. Nejdříve navrhujeme c-bit semi-externí algoritmus pro prohledávání do hloubky. Abychom dosáhli nízké spotřeby vnitřní paměti, vytváříme paměťově efektivní perfektní hašovací funkci z množiny vrcholů uložených na disku. Podobný algoritmus uvádíme také pro dvojité prohledávání do hloubky, které dokáže hledat akceptující cykly a tak řešit problém ověřování LTL vlastností modelů. I/O složitost samotného hledání je úměrná času potřebnému k prohledání grafu. Pro lokální ověřování modelů používáme iterativně-prohlubující strategii známou z omezeného ověřování modelů. |
| Související projekty: |