Predicate Abstraction for Reactive Synthesis

Select |




Print


Walker, Adam Christopher; Ryzhyk, Leonid

Walker, Adam Christopher; Ryzhyk, Leonid


2014-10-21


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


http://www.cs.utexas.edu/users/hunt/FMCAD/FMCAD14/index.shtml


nicta:8141


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)