Research Commons
      • Browse 
        • Communities & Collections
        • Titles
        • Authors
        • By Issue Date
        • Subjects
        • Types
        • Series
      • Help 
        • About
        • Collection Policy
        • OA Mandate Guidelines
        • Guidelines FAQ
        • Contact Us
      • My Account 
        • Sign In
        • Register
      View Item 
      •   Research Commons
      • University of Waikato Research
      • Computing and Mathematical Sciences
      • Computing and Mathematical Sciences Papers
      • View Item
      •   Research Commons
      • University of Waikato Research
      • Computing and Mathematical Sciences
      • Computing and Mathematical Sciences Papers
      • View Item
      JavaScript is disabled for your browser. Some features of this site may not work without it.

      A process-algebraic semantics for generalised nonblocking.

      Ware, Simon; Malik, Robi
      Thumbnail
      Files
      cats2011.pdf
      193.4Kb
      Link
       crpit.com
      Find in your library  
      Citation
      Export 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).
      Permanent Research Commons link: https://hdl.handle.net/10289/6834
      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.
      Date
      2012-01
      Type
      Conference Contribution
      Publisher
      Australian Computer Society, Inc.
      Rights
      © 2011 Australian Computer Society, Inc.
      Collections
      • Computing and Mathematical Sciences Papers [1454]
      Show full item record  

      Usage

      Downloads, last 12 months
      27
       
       

      Usage Statistics

      For this itemFor all of Research Commons

      The University of Waikato - Te Whare Wānanga o WaikatoFeedback and RequestsCopyright and Legal Statement