Starting Date: July 2026
Prerequisites: Strong programming skills (functional programming preferred); interest in formal logic and verification
Will results be assigned to University: No
The modal mu-calculus [1] is a logic for expressing properties of abstract state transition systems, and generalises other logics like Linear Temporal Logic (LTL) and Computation Tree Logic (CTL). Because of this, it is a very useful tool for describing and verifying the behaviour of computer systems.
The aim of this project is to support the evaluation of automatic provers for modal mu-calculus (such as COOL [2] and MLSolver [3]) by building a collection of modal mu-calculus formulas that can be used to test and compare the performance of such provers.
A starting point would be to collate any test suites belonging to the individual provers themselves. Next, we can look at randomly generating formulas, perhaps using the functional enumeration technique [4].
One important decision to be made is the format for representing these formulas for the benchmark suite. One option here is SMTLib [5].
References
[1] https://en.wikipedia.org/wiki/Modal_%CE%BC-calculus
[2] Görlitz, O., Hausmann, D., Humml, M., Pattinson, D., Prucker, S., Schröder, L. (2023). COOL 2 – A Generic Reasoner for Modal Fixpoint Logics (System Description). In: Pientka, B., Tinelli, C. (eds) Automated Deduction – CADE 29. CADE 2023. Lecture Notes in Computer Science, vol 14132. Springer, Cham. https://doi.org/10.1007/978-3-031-38499-8_14
[3] Oliver Friedmann, Martin Lange. A Solver for Modal Fixpoint Logics. Electronic Notes in Theoretical Computer Science, Volume 262, 2010, Pages 99-111, ISSN 1571-0661, https://doi.org/10.1016/j.entcs.2010.04.008
[4] Jonas Duregård, Patrik Jansson, and Meng Wang. 2012. Feat: functional enumeration of algebraic types. In Proceedings of the 2012 Haskell Symposium (Haskell ’12). Association for Computing Machinery, New York, NY, USA, 61–72. https://doi.org/10.1145/2364506.2364515
[5] Clark Barrett, Aaron Stump, and Cesare Tinelli. The SMT-LIB Standard – Version 2.0. Proceedings of the 8th International Workshop on Satisfiability Modulo Theories (Edinburgh, England), 2010.