תקציר
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 techniques in Boolean functional synthesis, we define dependent variables in reactive synthesis 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 that exploits dependent variables can solve some problems beyond the reach of existing techniques. Furthermore, we observe that among benchmarks with dependent variables, if the count of non-dependent variables is low (≤3 in our experiments), our method outperforms state-of-the-art tools for synthesis.
שפה מקורית | אנגלית |
---|---|
כותר פרסום המארח | Tools and Algorithms for the Construction and Analysis of Systems - 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Proceedings |
עורכים | Bernd Finkbeiner, Laura Kovács |
מוציא לאור | Springer Science and Business Media Deutschland GmbH |
עמודים | 123-143 |
מספר עמודים | 21 |
מסת"ב (מודפס) | 9783031572456 |
מזהי עצם דיגיטלי (DOIs) | |
סטטוס פרסום | פורסם - 2024 |
אירוע | 30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2024, which was held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024 - Luxembourg City, לוקסמבורג משך הזמן: 6 אפר׳ 2024 → 11 אפר׳ 2024 |
סדרות פרסומים
שם | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
---|---|
כרך | 14570 LNCS |
ISSN (מודפס) | 0302-9743 |
ISSN (אלקטרוני) | 1611-3349 |
כנס
כנס | 30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2024, which was held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024 |
---|---|
מדינה/אזור | לוקסמבורג |
עיר | Luxembourg City |
תקופה | 6/04/24 → 11/04/24 |
הערה ביבליוגרפית
Publisher Copyright:© The Author(s) 2024.