Efficient algorithms for behavioural equivalences such as strong bisimulation and branching bisimulation rely on refinable partition data structures . We recently developed an O(m log n) algorithm for computing branching bisimulation equivalence of labelled transition systems , 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.
The data structures used in the branching bisimulation algorithm are, in essence, based on the refinable partition data structures by Valmari . Previously, students in the FSA seminar have made initial formalizations of this data structure in Coq and in TLA+. From this, it appears promising to fully formalize the data structure in TLA+, and prove properties about it using TLAPS.
Towards verifying the branching bisimulation algorithm, in this project, the following problems are addressed.
- Complete the TLA+ formalization of the refinable partition data structure used for strong bisimulation minimization. In particular, ensure the invariants identified in  are maintained.
- Based on the literature, specify the pseudocode of a strong bisimulation algorithm for Kripke structures with complexity O(m log n) that uses Valmari’s refinable partition data structure, and formalize this algorithm in TLA+.
 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.
 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