Jeroen Keiren

Jeroen Keiren

Formal methods researcher at TU/e

Refining our confidence in refinable partition data structures

Efficient algorithms for behavioural equivalences such as strong 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.

The data structures used in the branching bisimulation algorithm are, in essence, based on the refinable partition data structures by Valmari [1]. 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.

  1. Complete the TLA+ formalization of the refinable partition data structure used for strong bisimulation minimization. In particular, ensure the invariants identified in [1] are maintained.
  2. 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+.

[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