Berezin S., Shilov N., Shneider P. An effective model checking for Mu-calculus: from finite systems towards systems with real time // Computer Science. — 1993. — # 1 — P. 73-86
