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.

      Divergent stutter bisimulation abstraction for controller synthesis with linear temporal logic specifications

      Mohajerani, Sahar; Malik, Robi; Wintenberg, Andrew; Lafortune, Stephane; Ozay, Necmiye
      Thumbnail
      Files
      1-s2.0-S0005109821002430-main.pdf
      Published version, 990.5Kb
      DOI
       10.1016/j.automatica.2021.109723
      Find in your library  
      Citation
      Export citation
      Mohajerani, S., Malik, R., Wintenberg, A., Lafortune, S., & Ozay, N. (2021). Divergent stutter bisimulation abstraction for controller synthesis with linear temporal logic specifications. Automatica, 130, 109723–109723. https://doi.org/10.1016/j.automatica.2021.109723
      Permanent Research Commons link: https://hdl.handle.net/10289/14366
      Abstract
      This paper proposes a method to synthesise controllers for systems with possibly infinite number of states that satisfy a specification given as an LTL\◦ formula. A common approach to handle this problem is to first compute a finite-state abstraction of the original state space and then synthesise a controller for the abstraction. This paper proposes to use an abstraction method called divergent stutter bisimulation to abstract the state space of the system. As divergent stutter bisimulation factors out stuttering steps, it typically results in a coarser and therefore smaller abstraction, at the expense of not preserving the temporal ‘‘next’’ operator. The paper leverages results about divergent stutter bisimulation from model checking and shows that divergent stutter bisimulation is a sound and complete abstraction method when synthesising controllers subject to specifications in LTL\◦.
      Date
      2021
      Type
      Journal Article
      Publisher
      Elsevier BV
      Rights
      © 2021 The Author(s). Published by Elsevier Ltd. This is an open access article under the CC BY license (http://creativecommons.org/licenses/by/4.0/).
      Collections
      • Computing and Mathematical Sciences Papers [1455]
      Show full item record  

      Usage

      Downloads, last 12 months
      46
       
       
       

      Usage Statistics

      For this itemFor all of Research Commons

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