CSI Seminar 2019-01-16
10h00 Counterexample searches in Spot – Clément Gillard
Spot is an '"`UNIQ--math-00000028-QINU`"'-automata manipulation library who aims to help doing '"`UNIQ--math-00000029-QINU`"'-automata-theoretic approach to model checking or develop tools for '"`UNIQ--math-0000002A-QINU`"'-automata transformation. As such, it provides many algorithms, with many different implementations depending of the specificities of each '"`UNIQ--math-0000002B-QINU`"'-automaton. Of those algorithms, emptiness check algorithms and counterexample search algorithms are often used, with various goals, and since their results are linked, they are often used together. However, some implementations of emptiness check algorithms lack a similar counterexample search implementation which is able to work in the same way on the same automata. We introduce two implementations of counterexample computation, which complete two already existing implementations of emptiness check algorithms by walking in their footsteps and reusing some of the data they gathered to efficiently compute counterexamples.
10h30 State compression in Spot – Arthur Remaud
To represent a system by an automaton, we have to save the values of all variables of this system in each state. This can take a lot of memory when there is a lot of variables and/or a lot of states, and also can grow the execution time due to cache misses. To avoid this problem in Spot, we compress the array of variables of each state, which already reduces the memory consumption and the execution time. In this report, we present a datastructure for a better compression of variables in states, using the redundancy of the values in each states of the automatonand the different constraints encounter to add it in Spot.
11h00 Implementation of Invisible and Transparent Transitions in Spot – Vincent Tourneur
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.