Synthesis of Reactive(1) designs
By Roderick Bloem, Barbara Jobstmann, Nir Piterman, Amir Pnueli, Yaniv Sa'ar. Journal of computer and system sciences (Print), 2006
882 citations recorded by the source corpus.
We address the problem of automatically synthesizing digital designs from linear-time specifications. We consider various classes of specifications that can be synthesized with effort quadratic in the number of states of the reactive system, where we measure effort in symbolic steps. The synthesis algorithm is based on a novel type of game called General Reactivity of rank 1 (gr(1)), with a winning condition of the form(@?@?@?p"1@?...@?@?@?@?p"m)->(@?@?@?q"1@?...@?@?@?@?q"n), where each p"i and q"i is a Boolean combination of atomic propositions. We show symbolic algorithms to solve this game, to build a winning strategy and several ways to optimize the winning strategy and to extract a system from it. We also show how to use gr(1) games to solve the synthesis of ltl specifications in many interesting cases. As empirical evidence to the generality and efficiency of our approach we include a significant case study. We describe the formal specifications and the synthesis process applied to a bus arbiter, which is a realistic industrial hardware specification of modest size.
Subfields: Computational Theory and Mathematics, Hardware and Architecture, Software
View Paper: https://www.semanticscholar.org/paper/3fec934272736ed73b86ecdbc4f96542fdc24166
How researchers see this paper
The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.
In Computational Theory and Mathematics
In Hardware and Architecture
In Software
Citations in the corpus
- Receding Horizon Temporal Logic Planning (2012, methodology): “The approach presented in [20] allows checking the realizability of this class of specifications and synthesizing the corresponding finite state automaton to be performed in time O(∣V ∣3) where ∣V ∣ is the size of the state space of the finite state abstraction D of the system.”
- Control Barrier Functions for Signal Temporal Logic Tasks (2019, methodology): “Computationally-efficient frameworks for LTL have been presented in [4], [5] by considering a game theory-based approach and in [6] by considering a deductive proof system-based”