Generalised Rabin(1) synthesis

TL;DR

This paper introduces a new, efficient method for synthesizing finite state systems from linear-time temporal logic specifications with Rabin index one, using a parity game approach that is suitable for symbolic implementation.

Contribution

It generalizes the Rabin(1) synthesis approach, providing a parity game construction with at most five colors for specifications with Rabin index one, and proves limitations for higher Rabin indices.

Findings

Constructs parity games with at most five colors for Rabin index one specifications.

Shows the tightness of the approach and the computational hardness for higher Rabin indices.

Provides an efficient symbolic implementation framework for the synthesis method.

Abstract

We present a novel method for the synthesis of finite state systems that is a generalisation of the generalised reactivity(1) synthesis approach by Piterman, Pnueli and Sa'ar. In particular, we describe an efficient method to synthesize systems from linear-time temporal logic specifications for which all assumptions and guarantees have a Rabin index of one. We show how to build a parity game with at most five colours that captures all solutions to the synthesis problem from such a specification. This parity game has a structure that is amenable to symbolic implementations. We furthermore show that the results obtained are in some sense tight, i.e., that there does not exist a similar synthesis method for assumptions and specifications of higher Rabin index, unless P=NP.