State compression in Spot

Authors

Arthur Remaud

Type

techreport

Year

2019

Number

1902

Abstract

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 statesand 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 statesusing the redundancy of the values in each states of the automaton, and the different constraints encounter to add it in Spot.