Research Commons

A process-algebraic semantics for generalised nonblocking.

Research Commons

Show simple item record

dc.contributor.author Ware, Simon
dc.contributor.author Malik, Robi
dc.date.accessioned 2012-11-13T21:52:46Z
dc.date.available 2012-11-13T21:52:46Z
dc.date.issued 2012-01
dc.identifier.citation 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). en_NZ
dc.identifier.issn 1445-1336
dc.identifier.uri http://hdl.handle.net/10289/6834
dc.description.abstract 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. en_NZ
dc.format.mimetype application/pdf
dc.language.iso en
dc.publisher Australian Computer Society, Inc. en_NZ
dc.relation.uri http://crpit.com/confpapers/CRPITV119Ware.pdf en_NZ
dc.rights © 2011 Australian Computer Society, Inc.
dc.subject Compositional verification en_NZ
dc.subject Decision procedure en_NZ
dc.subject Finite-state automata en_NZ
dc.subject Liveness properties en_NZ
dc.subject Non-blocking en_NZ
dc.subject Semantic Model en_NZ
dc.subject Transition structures en_NZ
dc.subject Semantics en_NZ
dc.subject Automata theory en_NZ
dc.title A process-algebraic semantics for generalised nonblocking. en_NZ
dc.type Conference Contribution en_NZ


Full-text options:

This item appears in the following Collection(s)

Show simple item record

Search Research Commons


Advanced Search

Browse

Theses

About Research Commons

My Account

Usage Statistics

Share

  • Bookmark and Share