Model checking μ-calculus in well-structured transition systems

We study the model checking problem for fixpoint logics in well-structured multiaction transition systems. P.A. Abdulla et al. (1996) and Finkel & Schnoebelen (2001) examined the decidability problem for liveness (reachability) and progress (eventuality) properties in well-structured single action transition systems. Our main result is as follows: the model checking problem is decidable for disjunctive formulae of the propositional μ-calculus of D. Kozen (1983) in well-structured transition systems where propositional variables are interpreted by upward cones. We also discuss the model checking problem for the intuitionistic modal logic of Fisher Servi (1984) extended by least fixpoint.