D 2003

To Store or Not To Store

BEHRMANN, Gerd, Kim G. LARSEN and Radek PELÁNEK

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

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Germany

Confidentiality degree

není předmětem státního či obchodního tajemství

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

Tags

International impact, Reviewed
Změněno: 21/11/2006 14:02, doc. Mgr. Radek Pelánek, Ph.D.

Abstract

V originále

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 project
Name: 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