On the synthesis of a reactive module

By Amir Pnueli, Roni Rosner. 1989

We consider the synthesis of a reactive module with input <italic>x</italic> and output <italic>y</italic>, which is specified by the linear temporal formula @@@@(<italic>x</italic>, <italic>y</italic>). We show that there exists a program satisfying @@@@ iff the branching time formula (∀<italic>x</italic>) (∃<italic>y</italic>) <italic>A</italic>@@@@(<italic>x</italic>, <italic>y</italic>) is valid over all tree models. For the restricted case that all variables range over finite domains, the validity problem is decidable, and we present an algorithm for constructing the program whenever it exists. The algorithm is based on a new procedure for checking the emptiness of Rabin automata on infinite trees in time exponential in the number of pairs, but only polynomial in the number of states. This leads to a synthesis algorithm whose complexity is double exponential in the length of the given specification.

Subfields: Program Analysis & Verification

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Program Analysis & Verification

Citations in the corpus

Program Synthesis with Large Language Models (2021, background): “Program synthesis is a longstanding goal of artificial intelligence research [Manna and Waldinger, 1971, Waldinger et al., 1969, Summers, 1977, Shaw et al., 1975, Pnueli and Rosner, 1989, Manna and Waldinger, 1975], dating as far back as the 1940s and 50s [Copeland, 2012, Backus et al., 1957].”
Synthesis of Reactive(1) designs (2006, methodology): “This problem has been considered again in [PR89a] in the context of synthesizing reactive modules from a specification given in Linear Temporal Logic (LTL).”
From Nondeterministic Buchi and Streett Automata to Deterministic Parity Automata (2006, methodology): “For example, in order to solve a game in which the goal is an LTL formula, one first converts the LTL formula to a deterministic automaton and then solves the resulting Rabin game [22] (cf.”
Temporal-Logic-Based Reactive Mission and Motion Planning (2009, background): “such an automaton is proven to be doubly exponential in the size of the formula [33].”
Program Synthesis (2017, background): “Pnueli considered program synthesis to be one of the most central problems in the theory of programming [110].”
Branching vs. Linear Time: Final Showdown (2001, background): “synthesis of reactive systems, one has to consider a branching-time framework, since all possible strategies by the environment need to be considered [83,84].”
Small Progress Measures for Solving Parity Games (2000, methodology): “This compares favourably with other algorithms for the linear-time equivalent problem of checking non-emptiness of non-deterministic Rabin (Streett) tree automata [4, 14, 10], and makes it the best algorithm known for this NP-complete (co-NP-complete) [4] problem.”
Structural Language Models of Code (2019, background): “Program Generation Learning to generate programs is one of the oldest problems in machine learning (Waldinger & Lee, 1969) and has been considered by some as the “holy grail of computer science” (Pnueli & Rosner, 1989; Gul-wani et al., 2017).”
Strategy logic (2007, methodology): “Zero-sum graph games have been widely used in the synthesis (or control) of reactive systems [22, 24], as well as for defining and checking the realizability of specifications [1, 8], the compatibility of interfaces [7], simulation relations between transition systems [11, 19], and for generating te”
Agent-Oriented Software Engineering: The State of the Art (2009, background): “Perhaps the closest to our view is the work of Pnueli and Rosner [58] on the automatic synthesis of reactive systems from branching time temporal logic specifications.”
Structural Language Models for Any-Code Generation (2019, background): “Program Generation Learning to generate programs is one of the oldest problems in machine learning (Waldinger and Lee, 1969) and has been considered by some as the “holy grail of computer science” (Pnueli and Rosner, 1989; Gulwani et al., 2017).”
Learning to Represent Programs with Property Signatures (2020, background): “Program synthesis is a longstanding goal of computer science research (Manna & Waldinger, 1971; Waldinger et al., 1969; Summers, 1977; Shaw; Pnueli & Rosner, 1989; Manna & Waldinger, 1975), arguably dating to the 1940s and 50s (Copeland, 2012; Backus et al., 1957).”
A Survey of Symbolic Execution Techniques (2016, background): “Program synthesis automatically constructs a program satisfying a high-level specification [82].”