Local model checking for parallel compositions of context-free processes

Decidability of modal logics is not limited to finite systems. The alternation-free mu-calculus can be model checked for sequential systems given in a context-free form (or even a more general one). But the parallel composition of such systems introduces undecidabilities. Nevertheless, several instances can be handled as it is shown in this paper. The known model check techniques prove to be not extendable to parallel compositions. A new tableau system is introduced which is complete in the sequential case and for parallel compositions involving at most one infinite system. The verification of a queue which results from the parallel composition of two (context-free) stacks demonstrates its ability to cope with nontrivial compositions of infinite systems, too.