On compositional model checking in the modal Mu-calculus and its extension with multiple clocks

This paper includes several results concerning with compositional model checking (CMC) for finite-state systems with multiple clocks. We describe a model of time [6], and  a method of reducing a timed (infinite) model to a finite untimed model. We also present a new Finite Process Algebra (FPA) and its extension by multiple clocks.  Further we give “Pure” Compositional Model Checking (PCMC) for the V-free fragment ofthe modal μ-calculus with its generalization for the full μ-calculus as a) tableau-based model checking proof system and b) direct decomposition of a formula. The worst case complexity analysis is done for all variants. In particular, we extend the result of H. Andersen in [2] on the complexity of model checking to the FPA and μ-calculus with more general simultaneous fixed points.  Weshow also that any finite Labeled Transition System (LTS) with 2n states can be equivalently represented by a compositional system of processes with the sum of all their states 2n.  It means that for anylogic with at least linear model checking procedure on the size of amodel, no efficient compositional proof system can be built, that does not use any other special properties except hierarchy.