Creation of an antichain library

From LRDE

The printable version is no longer supported and may have rendering errors. Please update your browser bookmarks and please use the default browser print function instead.

Abstract

In order theory, an antichain is a subset of elements incomparable with one another, following a given order. In the automata theory, some algorithms use antichains as data structures to store sets of states all disjointed, in simulation algorithms to reduce an automaton for example. The implementation of antichain consists to verify at the insertion if the new element is not comparable to another already in the antichain, which is costly because at each insertion we need to do a linear path. In this report, we detail different algorithms to implement the antichain optimizing the insertion of a new element. Then we will show the results of these implementations with our model checker Spot to compare their performances.