Refining our confidence in refinable partition data structures

Efficient algorithms for behavioural equivalences such as stuttering
bisimulation and branching bisimulation rely on refinable partition
data structures [1].
We recently developed an O(m log n) algorithm for computing branching
bisimulation equivalence of labelled transition systems [2], and
implemented it in the mCRL2 toolset. Since the proofs of correctness and
of the time complexity of the algorithm are highly non-trivial, it is
desired to formally verify these proofs.

In this project, you formalise the refinable partition data structures used in
the branching bisimulation algorithm.
For this, you use one of the theorem provers Coq or Isablle.
You also identify and prove some of the properties that the branching
bisimulation algorithm requires to hold in the correctness or complexity
arguments.


[1] Valmari, A., Lehtinen, P.: Efficient Minimization of DFAs with Partial
Transition Functions. In: Albers, S. and Weil, P. (eds.) 25th International
Symposium on Theoretical Aspects of Computer Science. pp. 645-656 Schloss
Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany (2008).
https://doi.org/10.4230/LIPIcs.STACS.2008.1328.

[2] Jansen D.N., Groote J.F., Keiren J.J.A., Wijs A. (2020) An O(m log n)
algorithm for branching bisimilarity on labelled transition systems.
In: Biere A., Parker D. (eds) Tools and Algorithms for the Construction and
Analysis of Systems. TACAS 2020. Lecture Notes in Computer Science, vol 12079.
Springer, Cham https://doi.org/10.1007/978-3-030-45237-7_1