Under-Approximation Generation using Partial Order Reduction
| Název česky | Generování stavového prostoru s použitím under-aproximace a partial order reduction |
|---|---|
| Autoři | |
| Rok publikování | 2005 |
| Druh | Odborná kniha |
| Fakulta / Pracoviště MU | |
| Citace | |
| Popis | V práci je navržen nový způsob generování stavových prostorů kombinující metody partial order reduction s under-approximacemi pro ověřování LTL-X vlastností modelu. Používá relaci sensitivity a modifikované podmínky na ample-sets. Výsledný redukovaný stavový prostor není plně ekvivalentní původnímu, v práci jsou proto navrženy rozšíření under-aproximací, které lze provádět automaticky a nepotřebují další pomocné mechanismy jako jsou theorem-proovers nebo SAT solvery. |
| Související projekty: |