Creation of an antichain library

Authors

Arthur Remaud

Type

techreport

Year

2018

Number

1803

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.