摘要 : Fixpoint logic with chop extends the modal it-calculus with a sequential composition operator which results in an increase in expressive power. We develop a game-theoretic characterisation of its model checking problem and use the... 展开 Fixpoint logic with chop extends the modal it-calculus with a sequential composition operator which results in an increase in expressive power. We develop a game-theoretic characterisation of its model checking problem and use these games to show that the alternation hierarchy in this logic is strict. The structure of this result follows the lines of Arnold's proof showing that the alternation hierarchy in the modal mu-calculus is strict over the class of binary trees. (C) 2006 Elsevier Inc. All rights reserved. 收起