The alternation hierarchy in fixpoint logic with chop is strict too

摘要

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.