To Store or Not To Store

Logo poskytovatele

Varování

Publikace nespadá pod Ekonomicko-správní fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.
Autoři

BEHRMANN Gerd LARSEN Kim G. PELÁNEK Radek

Rok publikování 2003
Druh Článek ve sborníku
Konference Computer Aided Verification (CAV 2003)
Fakulta / Pracoviště MU

Fakulta informatiky

Citace
Obor Informatika
Klíčová slova explicit model checking; syntax analysis
Popis 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.
Související projekty:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.