Informace o publikaci
Distributed LTL Model Checking with Hash Compaction
| Název česky | Distribuované ověřování modelů LTL za pomoci hash compaction |
|---|---|
| Autoři | |
| Rok publikování | 2013 |
| Druh | Článek ve sborníku |
| Konference | Electronic Notes in Theoretical Computer Science, Volume 296 |
| Fakulta / Pracoviště MU | |
| 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: |