This package is an implementation of the bisimulation algorithm in [DEP], a modification of Cleaveland's algorithm [Cle]. It gives a way to distinguish states that do not satisfy the same formulas in a minimalist logic (L0). The main use of that is to simplify LMP's by grouping bisimilar state (to "lump" bisimilar states). See [DEP] for more information on bisimilarity, the L0 logic, the proof of characterization of bisimilarity by the L0 logic and the proof of correctness of the algorithm.