During my studies in computer science at the University of Naples Federico II, I attended the Automated Software Verification course, which delves into Model Checking. The course covered various verification algorithms for LTL, CTL and others. To deepen my understanding of these concepts, and simply for fun, I decided to implement some of them in Rust.
For now, I have focused on implementing an algorithm that converts an LTL formula into a Büchi automaton. This project is purely educational and experimental.
Feel free to explore the code!