BEHRMANN, Gerd, Kim G. LARSEN and Radek PELÁNEK. To Store or Not To Store. In Computer Aided Verification (CAV 2003). Boulder (Colorado, USA): Springer-Verlag, 2003, p. 433-445. ISBN 3-540-40524-0.
Other formats:   BibTeX LaTeX RIS
Basic information
Original name To Store or Not To Store
Authors BEHRMANN, Gerd (208 Denmark), Kim G. LARSEN (208 Denmark) and Radek PELÁNEK (203 Czech Republic, guarantor).
Edition Boulder (Colorado, USA), Computer Aided Verification (CAV 2003), p. 433-445, 13 pp. 2003.
Publisher Springer-Verlag
Other information
Original language English
Type of outcome Proceedings paper
Field of Study 10201 Computer sciences, information science, bioinformatics
Country of publisher Germany
Confidentiality degree is not subject to a state or trade secret
RIV identification code RIV/00216224:14330/03:00008588
Organization unit Faculty of Informatics
ISBN 3-540-40524-0
UT WoS 000185145800040
Keywords in English explicit model checking; syntax analysis
Tags explicit model checking, syntax analysis
Tags International impact, Reviewed
Changed by Changed by: doc. Mgr. Radek Pelánek, Ph.D., učo 4297. Changed: 21/11/2006 14:02.
Abstract
To limit the explosion problem encountered during reachability analysis we suggest a variety of techniques for reducing the number of states to be stored during exploration, while maintaining the guarantee of termination and keeping the number of revisits small. The techniques include static analysis methods for component automata in order to determine small sets of covering transitions. We carry out extensive experimental investigation of the techniques within the real-time verification tool Uppaal. Our experimental results are extremely encouraging: a best combination is identified which for a variety of industrial case-studies reduces the space-consumption to less than 10% with only a moderate overhead in time-performance.
Links
GA201/03/0509, research and development projectName: Automatizovaná verifikace paralelních a distribuovaných systémů
Investor: Czech Science Foundation, Automated Verification of Parallel and Distributed Systems
MSM 143300001, plan (intention)Name: Nesekvenční modely výpočtů - kvantové a souběžné distribuované modely výpočetních procesů
Investor: Ministry of Education, Youth and Sports of the CR, Non-sequential Models of Computing -- Quantum and Concurrent Distributed Models of Computing
PrintDisplayed: 19/9/2024 23:45