@article {12770,
	title = {A linear-time model-checking algorithm for the alternation-free modal mu-calculus},
	journal = {Formal methods in system design},
	volume = {2},
	year = {1993},
	month = {1993///},
	pages = {121 - 147},
	author = {Cleaveland, Rance and Steffen,B.}
}
