Publication details
Partial Order Reduction for State/Event LTL
| Basic information | |
|---|---|
| Original title: | Partial Order Reduction for State/Event LTL |
| Authors: | Nikola Beneš, Luboš Brim, Ivana Černá, Jiří Sochor, Pavlína Vařeková, Barbora Zimmerová |
| Further information | |
|---|---|
| Citation: | BENEŠ, Nikola  - BRIM, Luboš - ČERNÁ, Ivana - SOCHOR, Jiří - VAŘEKOVÁ, Pavlína - ZIMMEROVÁ, Barbora. Partial Order Reduction for State/Event LTL. Brno, Czech Republic : Faculty of Informatics, Masaryk University, 2008. Technical report FIMU-RS-2008-07. |
| Original language: | English |
| Field: | Informatika |
| WWW: |  FIMU Technical Reports URL |
| Type: | R&D Presentation |
| Keywords: | Partial order reduction; state/event LTL; formal verification |
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
