Model checking of macro processes

Abstract

Decidability of modal logics is not limited to finite systems. The alternationfree modal mu-calculus has already been shown to be decidable for contextfree processes, with a worst case complexity which is linear in the size of the system description and exponential in the size of the formula. Like contextfree processes correspond to the concept of procedures without parameters, macro processes correspond to procedures with procedure parameters. They too allow deciding mu-calculus formulae, as is shown in this paper by presenting both global (iterative) and local (tableaux-based) procedures. These decision procedures handle correctly also process systems which are defined by unguarded recursion. As expected, the worst case complexity depends on the highest type level in the process description, and it is k-exponential in the size of the formula for a system description with type level k.