ATL/CTL model checking