Trustworthy Systems

Predicate abstraction for reactive synthesis

Authors

Adam Christopher Walker and Leonid Ryzhyk

NICTA

UNSW

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 imple- mented the algorithm as part of an automatic device driver syn- thesis 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

  @inproceedings{Walker_Ryzhyk_14,
    address          = { Lausanne, Switzerland},
    author           = {Walker, Adam Christopher and Ryzhyk, Leonid},
    booktitle        = {Conference on Formal Methods in Computer-Aided Design},
    keywords         = {termite, device drivers, abstraction refinement, predicate abstraction},
    month            = oct,
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/8141.pdf},
    title            = {Predicate Abstraction for Reactive Synthesis},
    year             = {2014}
  }

Download