A compositional #mu#-calculus proof system for statecharts processes

摘要

In this paper we propose a quite general process language called yj, which can be suitably instantiated to model the synchronous language statecharts. The main novelty of the language is an operator of process refinement for representing statecharts hierarchy. Moreover, we define a compositional proof system for checking #mu#-calculus properties of yj processes. Such a proof system is sound in general and it is complete for finite-state processes including the one corresponding to statecharts.