kouzmin.pdf914.51 KB

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...