Support LTL controller synthesis
Given the capabilities of Spot, we should be able to solve reactive synthesis.
An instance of the reactive synthesis problem is given as a set of input (uncontrollable) atomic propositions, a set of output (controllable) atomic propositions, and a formula (typically an LTL formula, but a PSL formula is OK too) over these atomic propositions. The classical way to solve this problem is through the transformation of the input problem into a (deterministic) parity game between the controller and the environment. The controller wins the latter if and only if the synthesis instance has a solution. Furthermore, a winning strategy in this game gives a concrete solution to the synthesis problem instance.
SYNTCOMP is a competition of LTL controller synthesis, whose models could be used for tests and benchmarks. Although its input is AIGER or TLSF, the tool Syfco provides a translation from TLSF to LTL which we can use.
-
Implement a parity_game
class. -
Implement a transformation from a synthesis instance to a parity game. -
Implement algorithms to solve parity games. We could use the well-known recursive algorithm by Zielonka, or the recent quasipolynomial time algorithm by Calude et al. Jurdzińsky and Lazić propose another quasipolynomial time algorithm which could be worth implementing. -
Implement the computation of a winning strategy, and its translation to the AIGER format required to participate to SYNTCOMP. -
Package the whole toolchain in a binary, with options to select the algorithm used to solve the parity game.