Implementation of Invisible and Transparent Transitions in Spot
From LRDE
- Authors
- Vincent Tourneur
- Type
- techreport
- Year
- 2018
- Number
- 1809
Abstract
In the model checking field, Partial Order Reduction (POR) is a method which allows to notably reduce the size of datastructures used to represent the different possible executions of program model, by considering only representative execution paths, insteed of all. This has a cost: information is lost. When the goal is only to check the absence of deadlocks, enough information is kept, so POR works well. But when in comes to LTL model checkingrelevent information may be dropped: execution paths which modifiy the value of AP (Atomic Proposition) occuring in the LTL formula. Moreover, it is only possible to use POR for LTL X. Invisible and transparent transitions are methods which add additional conditions to fulfill during the POR, in order to keep all execution paths which may modify the value of the AP. We explain these methods and how they have been implemented in the Spot model checking library.