EDELKAMP, Stefan, Peter SANDERS and Pavel ŠIMEČEK. Semi-external LTL Model Checking. In 20th International Conference on Computer Aided Verification. Berlin, Heidelberg: Springer, 2008, p. 530-542. ISBN 978-3-540-70543-7. |
Other formats:
BibTeX
LaTeX
RIS
|
Basic information | |
---|---|
Original name | Semi-external LTL Model Checking |
Name in Czech | Semi-externí ověřování LTL vlastností modelů |
Authors | EDELKAMP, Stefan (276 Germany), Peter SANDERS (276 Germany) and Pavel ŠIMEČEK (203 Czech Republic, guarantor). |
Edition | Berlin, Heidelberg, 20th International Conference on Computer Aided Verification, p. 530-542, 13 pp. 2008. |
Publisher | Springer |
Other information | |
---|---|
Original language | English |
Type of outcome | Proceedings paper |
Field of Study | 10201 Computer sciences, information science, bioinformatics |
Country of publisher | United States of America |
Confidentiality degree | is not subject to a state or trade secret |
Impact factor | Impact factor: 0.402 in 2005 |
RIV identification code | RIV/00216224:14330/08:00024282 |
Organization unit | Faculty of Informatics |
ISBN | 978-3-540-70543-7 |
ISSN | 0302-9743 |
UT WoS | 000257539900050 |
Keywords in English | semi-external;model checking;external;I/O complexity |
Tags | external, I/O complexity, Model checking, semi-external |
Tags | International impact, Reviewed |
Changed by | Changed by: RNDr. Pavel Šimeček, Ph.D., učo 51636. Changed: 25/5/2009 11:42. |
Abstract |
---|
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. |
Abstract (in Czech) |
---|
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ů. |
Links | |
---|---|
GA201/06/1338, research and development project | Name: Automatizovaná verifikace softwaru |
Investor: Czech Science Foundation, Automated software verification | |
MSM0021622419, plan (intention) | Name: Vysoce paralelní a distribuované výpočetní systémy |
Investor: Ministry of Education, Youth and Sports of the CR, Highly Parallel and Distributed Computing Systems | |
1ET408050503, research and development project | Name: Techniky automatické verifikace a validace softwarových a hardwarových systémů |
Investor: Academy of Sciences of the Czech Republic, Techniques for automatic verification and validation of software nad hardware systems |
PrintDisplayed: 11/9/2024 11:22