model checking

Bodin has applied SPIN to solve puzzles like the Japanese river puzzle, an advanced version of the famous wolf-goat-cabbage puzzle. Defining a Promela model can become cumbersome and debugging can be very time-consuming, since SPIN does the syntax check (e.g. type checking) only at runtime and developers might have decided...

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