Model checking / Edmund M. Clarke, Jr., Orna Grumberg and Doron A. Peled. - Clarke, Edmund M. (MIT, 2000)