Dor Ma'ayan

Reactive synthesis is an automated procedure to obtain a correct-by-construction reactive system from its temporal logic specification. Despite significant research progress over the past few decades, reactive synthesis is still in its early stages of practical adoption. One significant barrier to using reactive synthesis outside academia is the long realizability checking and synthesis time of specifications. This paper introduces a novel, evolution-aware approach for realizability checking. Our approach leverages the key observation that realizability checking is an operation that developers frequently perform during iterative specification development; therefore, utilizing intermediate data from previous realizability checks can substantially improve running times. Our approach computes a local semantic diff between previous and current versions of the specification, and, based on the diff and the previous realizability checking result, applies a set of sound heuristics. These heuristics reuse intermediate data collected during the previous specification’s realizability checking to accelerate the current specification’s realizability checking. Our evaluation demonstrates that these heuristics are applicable in 70% of cases from a real-world dataset containing thousands of specifications, and that their application significantly improves the running time of realizability checking.

Reactive synthesis is an automated procedure to obtain a correct-by-construction reactive system from its temporal logic specification. Despite significant research progress in the past decades, reactive synthesis is still in early-stage of use. Previous studies found that the lack of development methods for reactive synthesis specifications is one barrier to its wider adoption. In this paper, we adapt two development methods, an incremental method and a modular method, to the context of reactive synthesis specifications. The methods are based on existing software development methods on the one hand and studies about reactive synthesis on the other hand. Then, we report on an exploratory case study in which participants developed specifications using the two methods. We evaluated the methods using a mixed-method analysis that combines grounded theory analysis of Slack communication with participants, quantitative exploratory data analysis of the synthesis IDE usage logs, and qualitative independent expert review of the final specifications. Our findings show clear benefits of modular specification development in terms of ease of planning, synthesis time, fewer unrealizability issues, and faster debugging. However, the incremental development method was more natural and easy to use, and specifications developed incrementally were also easier to validate during the development process.

Reactive synthesis is an automated procedure to obtain a correct-by-construction reactive system from its temporal logic specification. Despite its attractiveness and major research progress in the past decades, reactive synthesis is still in early-stage and has not gained popularity outside academia. We conducted an exploratory case study in which we followed students in a semester-long university workshop class on their end-to-end use of a reactive synthesizer, from writing the specifications to executing the synthesized controllers. The data we collected includes more than 500 versions of more than 80 specifications, as well as more than 2500 Slack messages, all written by the class participants. Our grounded theory analysis reveals that the use of reactive synthesis has clear benefits for certain tasks and that adequate specification language constructs assist in the specification writing process. However, inherent issues such as unrealizabilty, non-well-separation, the gap of knowledge between the users and the synthesizer, and considerable running times prevent reactive synthesis from fulfilling its promise. Based on our analysis, we propose action items in the directions of language and specification quality, tools for analysis and execution, and process and methodology, all towards making reactive synthesis more applicable for software engineers.

Reactive synthesis is an automated procedure to obtain a correct-by-construction reactive system from its temporal logic specification. Two of the main challenges in bringing reactive synthesis to practice are its very high worst-case complexity and the difficulty of writing declarative specifications using basic LTL operators. To address the first challenge, researchers have suggested the GR(1) fragment of LTL, which has an efficient polynomial time symbolic synthesis algorithm. To address the second challenge, specification languages include higher-level constructs that aim at allowing engineers to write succinct and readable specifications. One such construct is the triggers operator, as supported, e.g., in the Property Specification Language (PSL). In this work we introduce triggers into specifications for reactive synthesis. The effectiveness of our contribution relies on a novel encoding of regular expressions using symbolic finite automata (SFA) and on a novel semantics for triggers that, in contrast to PSL triggers, admits an efficient translation into GR(1). We show that our triggers are expressive and succinct, and prove that our encoding is optimal. We have implemented our ideas on top of the Spectra language and synthesizer. We demonstrate the usefulness and effectiveness of using triggers in specifications for synthesis, as well as the challenges involved in using them, via a study of more than 300 triggers written by undergraduate students who participated in a project class on writing specifications for synthesis. To the best of our knowledge, our work is the first to introduce triggers into specifications for reactive synthesis.

We introduce a system called Penrose for creating mathematical diagrams. Its basic functionality is to translate abstract statements written in familiar math-like notation into one or more possible visual representations. Rather than rely on a fixed library of visualization tools, the visual representation is user-defined in a constraint-based specification language; diagrams are then generated automatically via constrained numerical optimization. The system is user-extensible to many domains of mathematics, and is fast enough for iterative design exploration. In contrast to tools that specify diagrams via direct manipulation or low-level graphics programming, Penrose enables rapid creation and exploration of diagrams that faithfully preserve the underlying mathematical meaning. We demonstrate the effectiveness and generality of the system by showing how it can be used to illustrate a diverse set of concepts from mathematics and computer graphics.

Conceptual diagrams are used extensively to understand abstract relationships, explain complex ideas, and solve difficult problems. To illustrate concepts effectively, experts find appropriate visual representations and translate concepts into concrete shapes. This translation step is not supported explicitly by current diagramming tools. This paper investigates how domain experts create conceptual diagrams via semi-structured interviews with 18 participants from diverse backgrounds. Our participants create, adapt, and reuse visual representations using both sketches and digital tools. However, they had trouble using current diagramming tools to transition from sketches and reuse components from earlier diagrams. Our participants also expressed frustration with the slow feedback cycles and barriers to automation of their tools. Based on these results, we suggest four opportunities of diagramming tools — exploration support, representation salience, live engagement, and vocabulary correspondence — that together enable a natural diagramming experience. Finally, we discuss possibilities to leverage recent research advances to develop natural diagramming tools.