Distributed LTL Model Checking with Hash Compaction

Logo poskytovatele

Varování

Publikace nespadá pod Pedagogickou fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.
Název česky Distribuované ověřování modelů LTL za pomoci hash compaction
Autoři

BARNAT Jiří HAVLÍČEK Jan ROČKAI Petr

Rok publikování 2013
Druh Článek ve sborníku
Konference Electronic Notes in Theoretical Computer Science, Volume 296
Fakulta / Pracoviště MU

Fakulta informatiky

Citace
www http://dx.doi.org/10.1016/j.entcs.2013.07.006
Doi http://dx.doi.org/10.1016/j.entcs.2013.07.006
Obor Informatika
Klíčová slova model checking; LTL; hash compaction
Popis Rozšiřujeme distribuovaný algoritmus OWCTY pro realizaci verifikační metody enumerativní ověřování modelu o možnost uchovávat navštívené stavy pouze jako jejich otisky z hashovací funkce. Podáváme detailní popis algoritmu a důkaz korektnosti. Součástí výsledku je implementace algoritmu v prostředí verifikačního nástroje DIVINE a experimentální vyhodnocení.
Související projekty:

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