To Store or Not To Store

Warning

This publication doesn't include Faculty of Education. It includes Faculty of Informatics. Official publication website can be found on muni.cz.

Authors	BEHRMANN Gerd LARSEN Kim G. PELÁNEK Radek
Year of publication	2003
Type	Article in Proceedings
Conference	Computer Aided Verification (CAV 2003)
MU Faculty or unit	Faculty of Informatics
Citation
Field	Informatics
Keywords	explicit model checking; syntax analysis
Description	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.
Related projects:	Automated Verification of Parallel and Distributed Systems Non-sequential Models of Computing -- Quantum and Concurrent Distributed Models of Computing