Trustworthy Systems

Predicate abstraction for reactive synthesis


Adam Christopher Walker and Leonid Ryzhyk


University of Toronto


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

    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         = {},
    title            = {Predicate Abstraction for Reactive Synthesis},
    year             = {2014}