A modal fixpoint logic with chop

Abstract

We study a logic called FLC (Fixpoint Logic with Chop) that extends the modal mu-calculus by a chop-operator and termination formulae. For this purpose formulae are interpreted by predicate transformers instead of predicates. We show that any context-free process can be characterized by an FLC-formula up to bisimulation or simulation. Moreover, we establish the following results: FLC is strictly more expressive than the modal mu-calculus; it is decidable for finite-state processes but undecidable for context-free processes; satisfiability and validity are undecidable; FLC does not have the finite-model property.