ŠIMEČEK, Pavel. Semi-External LTL Model Checking. Co-authors of the original paper in CAV 2008 proceedings. In EDELKAMP, Stefan and Peter SANDERS. Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science. ISBN 978-80-7355-082-0. 2008.
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 ŠIMEČEK, Pavel.
Co-authors of the original paper in CAV 2008 proceedings.
Edition Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science, 2008.
Other information
Original language English
Type of outcome Conference abstract
Field of Study 10201 Computer sciences, information science, bioinformatics
Country of publisher Czech Republic
Confidentiality degree is not subject to a state or trade secret
Organization unit Faculty of Informatics
ISBN 978-80-7355-082-0
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
Changed by Changed by: RNDr. Pavel Šimeček, Ph.D., učo 51636. Changed: 26/11/2008 09:05.
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: 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.
Abstract (in Czech)
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ů.
Links
GA201/06/1338, research and development projectName: 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 projectName: 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: 28/3/2024 10:27