Ware, S., & Malik, R. (2011). A process-algebraic semantics for generalised nonblocking. In proceedings of the Theory of Computing 2011 - 17th Computing: The Australasian Theory Symposium. Perth, WA, January 17-20, Perth, WA (pp 75-84).
Permanent Research Commons link: http://hdl.handle.net/10289/6834
Generalised nonblocking is a weak liveness property to express the ability of a system to terminate under given preconditions. This paper studies the notions of equivalence and refinement that preserve generalised nonblocking and proposes a semantic model that characterises generalised nonblocking equivalence. The model can be constructed from the transition structure of an automaton, and has a finite representation for every finite-state automaton. It is used to construct a unique automaton representation for all generalised nonblocking equivalent automata. This gives rise to effective decision procedures to verify generalised nonblocking equivalence and refinement, and to a method to simplify automata while preserving generalised nonblocking equivalence. The results of this paper provide for better understanding of nonblocking in a compositional framework, with possible applications in compositional verification.
Australian Computer Society, Inc.
© 2011 Australian Computer Society, Inc.