FlyFast: On-the-fly model checker
FlyFast is an on-the-fly mean field probabilistic model checker. Its purpose is the automatic verification of time-bounded PCTL (Probabilistic Computation Tree Logic) properties of a selected individual in the context of systems that consist of a large number of (similar, but) independent, interacting objects.