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. |
Další formáty:
BibTeX
LaTeX
RIS
|
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 |
Změnil | Změnil: RNDr. Pavel Šimeček, Ph.D., učo 51636. Změněno: 25. 5. 2009 11:42. |
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ů |
VytisknoutZobrazeno: 3. 10. 2024 08:19