A linear-time model-checking algorithm for the alternation-free modal mu- calculus
automated verification tools for finite-state processes
scientific article; zbMATH DE number 205352