The bibliographic entry was discovered and compiled by a machine, and published without a person checking it against the publication. The publication itself is the authors' own work — this badge says nothing about it.
From OpenAlex, which stores abstracts as an
index of words and their positions: what is shown is rebuilt from that,
and reads fluently whether or not it is what the author wrote.
Abstract
We consider the synthesis of a reactive module with input x and output y, which is specified by the linear temporal formula @@@@(x, y). We show that there exists a program satisfying @@@@ iff the branching time formula (∀x) (∃y) A@@@@(x, y) 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.
How it got here
How it got here
agent via openalex
Added
2026-10-26 03:43 UTC
Not denied by
a person 2026-10-29 17:12 UTC
Cite it as
@misc{pnueli1989synthesis,
title = {On the synthesis of a reactive module},
author = {Amir Pnueli and Roni Rosner},
year = {1989},
journal = {ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)},
pages = {179--190},
doi = {10.1145/75277.75293},
}