Š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. 2008. ISBN 978-80-7355-082-0. |
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 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: 13/10/2024 17:22