Semi-External LTL Model Checking

ŠIMEČEK, Pavel. Semi-External LTL Model Checking. Co-authors of the original paper in CAV 2008 proceedings. In EDELKAMP, Stefan a Peter SANDERS. Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science. 2008. ISBN 978-80-7355-082-0.

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: ŠIMEČEK, Pavel.; Co-authors of the original paper in CAV 2008 proceedings.
• Vydání: Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science, 2008.

Další údaje

• Originální jazyk: angličtina
• Typ výsledku: Konferenční abstrakt
• Obor: 10201 Computer sciences, information science, bioinformatics
• Stát vydavatele: Česká republika
• Utajení: není předmětem státního či obchodního tajemství
• Organizační jednotka: Fakulta informatiky
• ISBN: 978-80-7355-082-0
• 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

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: In comparison to former external memory algorithms, the new algorithm is faster, but its internal memory complexity is proportional to the size of a state space. 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. Perfect hash function construction is based on the algorithm by Botelho et al. With perfect hash function, the search itself stores only one bit per vertex denoting which vertices have already been visited. Since storage of the perfect hash function takes also only the constant number of bits per state, the overall number of bits per state is constant. 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 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ů.

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ů