modelcheck Check logical models describing transition systems Implemented Transition Systems Pure CCS Logics Model Mu-Calculus