D 2003

To Store or Not To Store

BEHRMANN, Gerd; Kim G. LARSEN a Radek PELÁNEK

Základní údaje

Originální název

To Store or Not To Store

Autoři

BEHRMANN, Gerd; Kim G. LARSEN a Radek PELÁNEK

Vydání

Boulder (Colorado, USA), Computer Aided Verification (CAV 2003), od s. 433-445, 13 s. 2003

Nakladatel

Springer-Verlag

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Německo

Utajení

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

Kód RIV

RIV/00216224:14330/03:00008588

Organizační jednotka

Fakulta informatiky

ISBN

3-540-40524-0

UT WoS

000185145800040

Klíčová slova anglicky

explicit model checking; syntax analysis

Příznaky

Mezinárodní význam, Recenzováno
Změněno: 21. 11. 2006 14:02, doc. Mgr. Radek Pelánek, Ph.D.

Anotace

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.

Návaznosti

GA201/03/0509, projekt VaV
Název: Automatizovaná verifikace paralelních a distribuovaných systémů
Investor: Grantová agentura ČR, Automatizovaná verifikace paralelních a distribuovaných systémů
MSM 143300001, záměr
Název: Nesekvenční modely výpočtů - kvantové a souběžné distribuované modely výpočetních procesů
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Nesekvenční modely výpočtů -- kvantové a souběžné distribuované modely výpočetních procesů