Semi-external LTL Model Checking

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.

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

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