2008
Semi-External LTL Model Checking
ŠIMEČEK, PavelZákladní údaje
Originální název
Semi-External LTL Model Checking
Název česky
Semi-externí ověřování LTL vlastností modelů
Autoři
Vydání
Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science, 2008
Další údaje
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
Příznaky
Mezinárodní význam
Změněno: 26. 11. 2008 09:05, RNDr. Pavel Šimeček, Ph.D.
V originále
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.
Č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 |
| ||
| MSM0021622419, záměr |
| ||
| 1ET408050503, projekt VaV |
|