On Dependent Variables in Reactive Synthesis
Fuente:
arXiv
Guardado en:
| Autores principales: | , , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2024
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866909078390833152 |
|---|---|
| author | Akshay, S. Basa, Eliyahu Chakraborty, Supratik Fried, Dror |
| author_facet | Akshay, S. Basa, Eliyahu Chakraborty, Supratik Fried, Dror |
| contents | Given a Linear Temporal Logic (LTL) formula over input and output variables, reactive synthesis requires us to design a deterministic Mealy machine that gives the values of outputs at every time step for every sequence of inputs, such that the LTL formula is satisfied. In this paper, we investigate the notion of dependent variables in the context of reactive synthesis. Inspired by successful pre-processing steps in Boolean functional synthesis, we define dependent variables as output variables that are uniquely assigned, given an assignment, to all other variables and the history so far. We describe an automata-based approach for finding a set of dependent variables. Using this, we show that dependent variables are surprisingly common in reactive synthesis benchmarks. Next, we develop a novel synthesis framework that exploits dependent variables to construct an overall synthesis solution. By implementing this framework using the widely used library Spot, we show that reactive synthesis using dependent variables can solve some problems beyond the reach of several existing techniques. Further, among benchmarks with dependent variables, if the number of non-dependent variables is low (at most 3 in our experiments), our method is able outperform all state-of-the-art tools for synthesis. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2401_11290 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | On Dependent Variables in Reactive Synthesis Akshay, S. Basa, Eliyahu Chakraborty, Supratik Fried, Dror Logic in Computer Science Formal Languages and Automata Theory Given a Linear Temporal Logic (LTL) formula over input and output variables, reactive synthesis requires us to design a deterministic Mealy machine that gives the values of outputs at every time step for every sequence of inputs, such that the LTL formula is satisfied. In this paper, we investigate the notion of dependent variables in the context of reactive synthesis. Inspired by successful pre-processing steps in Boolean functional synthesis, we define dependent variables as output variables that are uniquely assigned, given an assignment, to all other variables and the history so far. We describe an automata-based approach for finding a set of dependent variables. Using this, we show that dependent variables are surprisingly common in reactive synthesis benchmarks. Next, we develop a novel synthesis framework that exploits dependent variables to construct an overall synthesis solution. By implementing this framework using the widely used library Spot, we show that reactive synthesis using dependent variables can solve some problems beyond the reach of several existing techniques. Further, among benchmarks with dependent variables, if the number of non-dependent variables is low (at most 3 in our experiments), our method is able outperform all state-of-the-art tools for synthesis. |
| title | On Dependent Variables in Reactive Synthesis |
| topic | Logic in Computer Science Formal Languages and Automata Theory |
| url | https://arxiv.org/abs/2401.11290 |