Berezin S. On compositional model checking in the modal Mu-calculus and its extension with multiple clocks // Computer Science. — 1995. — # 3 — P. 19-37
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