|
| | | |
A Process-Algebraic Semantics for Generalised Nonblocking
Ware, S. and Malik, R.
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. |
Cite as: Ware, S. and Malik, R. (2011). A Process-Algebraic Semantics for Generalised Nonblocking. In Proc. Computing: The Australasian Theory Symposium (CATS 2011) Perth, Australia. CRPIT, 119. Alex Potanin and Taso Viglas Eds., ACS. 75-84 |
(from crpit.com)
(local if available)
|
|