C
[CS92] Rance Cleaveland and Bernhard Steffen. A Linear-Time Model-Checking Algorithm for the Alternation-Free Modal Mu-Calculus. Formal Methods in System Design 2(2):121-147. Kluwer Academic, 1992. 
@article{fmsd2(2)-CS,
  author =              {Cleaveland, Rance and Steffen, Bernhard},
  title =               {A Linear-Time Model-Checking Algorithm for the
                         Alternation-Free Modal Mu-Calculus},
  publisher =           {Kluwer Academic},
  journal =             {Formal Methods in System Design},
  volume =              {2},
  number =              {2},
  pages =               {121-147},
  year =                {1992},
  doi =                 {10.1007/BF01383878},
}
List of authors