On Dependent Variables in Reactive Synthesis

S. Akshay, Eliyahu Basa, Supratik Chakraborty, Dror Fried

פרסום מחקרי: פרק בספר / בדוח / בכנספרסום בספר כנסביקורת עמיתים

תקציר

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 אפר׳ 202411 אפר׳ 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/2411/04/24

הערה ביבליוגרפית

Publisher Copyright:
© The Author(s) 2024.

טביעת אצבע

להלן מוצגים תחומי המחקר של הפרסום 'On Dependent Variables in Reactive Synthesis'. יחד הם יוצרים טביעת אצבע ייחודית.

פורמט ציטוט ביבליוגרפי