Under-Approximation Generation using Partial Order Reduction

Investor logo

Warning

This publication doesn't include Faculty of Economics and Administration. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

BRIM Luboš ČERNÁ Ivana MORAVEC Pavel ŠIMŠA Jiří

Year of publication 2005
Type Monograph
MU Faculty or unit

Faculty of Informatics

Citation
Description 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:

You are running an old browser version. We recommend updating your browser to its latest version.