Trustworthy Systems

Predicate abstraction for reactive synthesis

Authors

Adam Christopher Walker and Leonid Ryzhyk

NICTA

University of Toronto

Abstract

We present a predicate-based abstraction refinement algorithm for solving reactive games. We develop solutions to the key problems involved in implementing efficient predicate abstraction, which previously have not been addressed in game settings: (1) keeping abstractions concise by identifying relevant predicates only, (2) solving abstract games efficiently, and (3) computing and solving abstractions symbolically. We implemented the algorithm as part of an automatic device driver synthesis toolkit and evaluated it by synthesising drivers for several real-world I/O devices. This involved solving game instances that could not be feasibly solved without using abstraction or using simpler forms of abstraction.

BibTeX Entry

  @techreport{Walker_Ryzhyk_14:tr,
    address          = {Sydney, Australia},
    author           = {Walker, Adam Christopher and Ryzhyk, Leonid},
    institution      = {NICTA},
    issn             = {1833-9646-8281},
    keywords         = {termite, device drivers, abstraction refinement, predicate abstraction},
    month            = aug,
    number           = {NRL-8281},
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/8281.pdf},
    title            = {Predicate Abstraction for Reactive Synthesis},
    year             = {2014}
  }

Download