Partial Order Reduction for State/Event LTL

Warning

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

Authors	BENEŠ Nikola BRIM Luboš ČERNÁ Ivana SOCHOR Jiří VAŘEKOVÁ Pavlína ZIMMEROVÁ Barbora
Year of publication	2008
MU Faculty or unit	Faculty of Informatics
Web	FIMU Technical Reports URL
Description	The paper introduces a partial order reduction technique for verification of state/event LTL properties. The core of the partial order reduction is a novel notion of stuttering equivalence which we call state/event stuttering equivalence. The positive attribute of the equivalence is that it can be resolved with existing methods for partial order reduction. State/event LTL properties are, in general, not preserved under state/event stuttering equivalence. To this end we define a new logic, called weak state/event LTL, which is invariant under the new equivalence.
Related projects:	Techniques for automatic verification and validation of software nad hardware systems Realistic application of formal methods in component systems Highly Parallel and Distributed Computing Systems