Paper Info
Title
Predicate abstraction for reactive synthesis
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.
Year
DOI
Venue
2014
10.1109/FMCAD.2014.6987617
Formal Methods in Computer-Aided Design
Keywords
Field
DocType
device drivers,game theory,program diagnostics,abstract games,automatic device driver synthesis toolkit,predicate abstraction,predicate-based abstraction refinement algorithm,reactive games,reactive synthesis,real-world I/O devices
Abstraction,Programming language,Predicate abstraction,Computer science,Theoretical computer science,Reactive synthesis,Abstraction refinement,Predicate (grammar)
Conference
Citations 
PageRank 
References 
7
0.49
19
Authors
2
Name
Order
Citations
PageRank
Adam Walker1282.90
Leonid Ryzhyk221216.05