Publication details
Under
-Approximation Generation using Partial Order Reduction
| Basic information | |
|---|---|
| Original title: | Under-Approximation Generation using Partial Order Reduction |
| Authors: | Luboš Brim, Ivana Černá, Pavel Moravec, Jiří Šimša |
| Further information | |
|---|---|
| Citation: | BRIM, Luboš - ČERNÁ, Ivana - MORAVEC, Pavel - ŠIMŠA, Jiří. Under-Approximation Generation using Partial Order Reduction. Brno : Faculty of Informatics, 2005. 21 pp. Technical Reports, FIMU-RS-2005-04. |
| Original language: | English |
| Field: | Informatika |
| WWW: |  http://www.fi.muni.cz/informatics/reports/files/2004/FIMU-RS-2005-04.pdf |
| Type: | Monograph |
| Keywords: | under-aproximation; state space generation; partial order reduction |
We propose a new on-the-fly approach which combines partial order reduction with the under-approximation technique for falsification and verification of LTL-X properties. It uses sensitivity relation and modified ample conditions to generate a reduced state space that is not fully stutter equivalent to the original one and it checks the desired property using representatives. Widening of under-approximations is fully automatic and does not rely on any supporting mechanisms like theorem-provers or SAT solvers.
Related projects:
