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 2*n* states can be equivalently represented by a compositional system of processes with the sum of all their states 2*n*. 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.

Abstract

File

berezin.pdf7.14 MB

Pages

19-37