Semi-external LTL Model Checking

EDELKAMP, Stefan, Peter SANDERS a Pavel ŠIMEČEK. Semi-external LTL Model Checking. In 20th International Conference on Computer Aided Verification. Berlin, Heidelberg: Springer, 2008, s. 530-542. ISBN 978-3-540-70543-7.

Základní údaje

• Originální název: Semi-external LTL Model Checking
• Název česky: Semi-externí ověřování LTL vlastností modelů
• Autoři: EDELKAMP, Stefan (276 Německo), Peter SANDERS (276 Německo) a Pavel ŠIMEČEK (203 Česká republika, garant).
• Vydání: Berlin, Heidelberg, 20th International Conference on Computer Aided Verification, od s. 530-542, 13 s. 2008.
• Nakladatel: Springer

Další údaje

• Originální jazyk: angličtina
• Typ výsledku: Stať ve sborníku
• Obor: 10201 Computer sciences, information science, bioinformatics
• Stát vydavatele: Spojené státy
• Utajení: není předmětem státního či obchodního tajemství
• Impakt faktor: Impact factor: 0.402 v roce 2005
• Kód RIV: RIV/00216224:14330/08:00024282
• Organizační jednotka: Fakulta informatiky
• ISBN: 978-3-540-70543-7
• ISSN: 0302-9743
• UT WoS: 000257539900050
• Klíčová slova anglicky: semi-external;model checking;external;I/O complexity
• Štítky: external, I/O complexity, Model checking, semi-external
• Příznaky: Mezinárodní význam, Recenzováno

Anotace

In this paper we establish c-bit semi-external graph algorithms, - i.e., algorithms which need only a constant number c of bits per vertex in the internal memory. In this setting, we obtain new trade-offs between time and space for I/O efficient LTL model checking. First, we design a c-bit semi-external algorithm for depth-first search. To achieve a low internal memory consumption, we construct a RAM-efficient perfect hash function from the vertex set stored on disk. We give a similar algorithm for double depth-first search, which checks for presence of accepting cycles and thus solves the LTL model checking problem. The I/O complexity of the search itself is proportional to the time for scanning the search space. For on-the-fly model checking we apply iterative-deepening strategy known from bounded model checking.

Anotace česky

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ů.

Návaznosti

• GA201/06/1338, projekt VaV: Název: Automatizovaná verifikace softwaru

Investor: Grantová agentura ČR, Automatizovaná verifikace softwaru

• MSM0021622419, záměr: Název: Vysoce paralelní a distribuované výpočetní systémy

Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Vysoce paralelní a distribuované výpočetní systémy

• 1ET408050503, projekt VaV: Název: Techniky automatické verifikace a validace softwarových a hardwarových systémů

Investor: Akademie věd ČR, Techniky automatické verifikace a validace softwarových a hardwarových systémů