This paper investigates FLC, fixed point logic with chop, which
extends modal mu-calculus with a sequential composition operator.
We prove some interesting properties of FLC, like the tree model
property and bisimulation invariance. Furthermore, we give examples
of formulas that cannot be expressed in modal mu-calculus. The main
part of the paper deals with FLC's model checking problem. A tableau
system is defined and proved sound and complete. It gives rise to
an EXPTIME model checking algorithm. It is also shown that FLC
model checking can be done in PSPACE for formulas with fixed
alternation depth. Finally, the problem is proved to be PSPACE-hard.
