A Compositional Approach for Verifying Generalised Nonblocking

This paper proposes a compositional approach to verify the generalised nonblocking property of discrete-event systems. Generalised nonblocking is introduced in [1] to overcome weaknesses of the standard nonblocking check in discrete-event systems and increase the scope of liveness properties that can be handled. This paper addresses the question of how generalised nonblocking can be verified efficiently. The explicit construction of the …