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.

      Conflict-preserving abstraction of discrete event systems using annotated automata

      Ware, Simon; Malik, Robi
      Thumbnail
      Files
      Conflict-preserving.pdf
      204.8Kb
      DOI
       10.1007/s10626-012-0133-3
      Link
       www.springerlink.com
      Find in your library  
      Citation
      Export citation
      Ware, S. & Malik, R. (2012). Conflict-preserving abstraction of discrete event systems using annotated automata. Discrete Event Dynamic Systems, 22(4), 451-477.
      Permanent Research Commons link: https://hdl.handle.net/10289/6387
      Abstract
      This paper proposes to enhance compositional verification of the nonblocking property of discrete event systems by introducing annotated automata. Annotations store nondeterministic branching information, which would otherwise be stored in extra states and transitions. This succinct representation makes it easier to simplify automata and enables new efficientmeans of abstraction, reducing the size of automata to be composed and thus the size of the synchronous product state space encountered in verification. The abstractions proposed are of polynomial complexity, and they have been successfully applied to model check the nonblocking property of the same set of large-scale industrial examples as used in related work.
      Date
      2012
      Type
      Journal Article
      Publisher
      Springer
      Rights
      This is an author’s accepted version of an article published in the journal: Discrete Event Dynamic Systems. © 2012 Springer.
      Collections
      • Computing and Mathematical Sciences Papers [1452]
      Show full item record  

      Usage

      Downloads, last 12 months
      74
       
       
       

      Usage Statistics

      For this itemFor all of Research Commons

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