Predicate Abstraction for Reactive Synthesis

Select |


Walker, Adam Christopher; Ryzhyk, Leonid

Walker, Adam Christopher; Ryzhyk, Leonid


Conference Material

Formal Methods in Computer-Aided Design (FMCAD)

Lausanne, Switzerland

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.

Termite, device drivers, abstraction refinement, predicate abstraction


Walker, Adam Christopher; Ryzhyk, Leonid. Predicate Abstraction for Reactive Synthesis. In: Formal Methods in Computer-Aided Design (FMCAD); Lausanne, Switzerland. 2014-10-21.

Loading citation data...

Citation counts
(Requires subscription to view)