Lazy Controller Synthesis using Three-valued Abstractions for Safety and Reachability Specifications

  • Authors:
    Omar Hussien (UCLA), Paulo Tabuada (UCLA)
    Publication ID:
    P093454
    Publication Type:
    Paper
    Received Date:
    25-Apr-2018
    Last Edit Date:
    24-Jul-2018
    Research:
    2779.002 (University of California/Berkeley)
    2779.014 (University of California/Los Angeles)

Abstract

The synthesis of correct-by-design control software is a promising direction to address the well known difficulties in formally verifying complex cyber-physical systems. Despite the promise of this approach, it is currently limited to small systems since it typically requires the computation of a finite-state abstraction whose size grows exponentially with the number of continuous states. In this paper we present a new way to tackle the lack of scalability of control software synthesis by adopting a lazy controller synthesis approach. Instead of synthesizing a controller using a precomputed abstraction of the full system, the abstraction is computed lazily as needed for safety and reachability specifications. We illustrate, through different examples, how this lazy approach significantly reduces the total time required for the synthesis of correct-by-design controllers.

4819 Emperor Blvd, Suite 300 Durham, NC 27703 Voice: (919) 941-9400 Fax: (919) 941-9450

Important Information for the SRC website. This site uses cookies to store information on your computer. By continuing to use our site, you consent to our cookies. If you are not happy with the use of these cookies, please review our Cookie Policy to learn how they can be disabled. By disabling cookies, some features of the site will not work.