Show simple item record

dc.contributor.authorWare, Simon
dc.contributor.authorMalik, Robi
dc.date.accessioned2012-11-13T21:52:46Z
dc.date.available2012-11-13T21:52:46Z
dc.date.issued2012-01
dc.identifier.citationWare, 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.issn1445-1336
dc.identifier.urihttp://hdl.handle.net/10289/6834
dc.description.abstractGeneralised 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.mimetypeapplication/pdf
dc.language.isoen
dc.publisherAustralian Computer Society, Inc.en_NZ
dc.relation.urihttp://crpit.com/confpapers/CRPITV119Ware.pdfen_NZ
dc.rights© 2011 Australian Computer Society, Inc.
dc.subjectCompositional verificationen_NZ
dc.subjectDecision procedureen_NZ
dc.subjectFinite-state automataen_NZ
dc.subjectLiveness propertiesen_NZ
dc.subjectNon-blockingen_NZ
dc.subjectSemantic Modelen_NZ
dc.subjectTransition structuresen_NZ
dc.subjectSemanticsen_NZ
dc.subjectAutomata theoryen_NZ
dc.titleA process-algebraic semantics for generalised nonblocking.en_NZ
dc.typeConference Contributionen_NZ
pubs.elements-id20613


Files in this item

This item appears in the following Collection(s)

Show simple item record