This repository contains a functional implementation in Haskell of the algorithms included in the article Efficient On-the-Fly Model Checking for CTL★ (Bhat, Girish, Rance Cleaveland, and Orna Grumberg).
It's important to say this method works without Büchi automatons. In the words of the authors:
In this paper we present an on-the-fly algorithm for checking finite-state Kripke structures against CTL★ formulas.
Our routine constructs the state space of the system under consideration in a need-driven fashion and will therefore perform better in practice.
See Efficient On-the-Fly Model Checking for CTL★ for more details.