Synthesizing structured reactive programs via deterministic tree automata

DOI10.1016/J.IC.2015.03.013zbMATH Open1317.68029arXiv1303.0797OpenAlexW2001101279MaRDI QIDQ2346409FDOQ2346409

Authors: Benedikt Brütsch 

Publication date: 1 June 2015

Published in: Information and Computation (Search for Journal in Brave)

Abstract: Existing approaches to the synthesis of reactive systems typically involve the construction of transition systems such as Mealy automata. However, in order to obtain a succinct representation of the desired system, structured programs can be a more suitable model. In 2011, Madhusudan proposed an algorithm to construct a structured reactive program for a given omega-regular specification without synthesizing a transition system first. His procedure is based on two-way alternating omega-automata on finite trees that recognize the set of "correct" programs. We present a more elementary and direct approach using only deterministic bottom-up tree automata that compute so-called signatures for a given program. In doing so, we extend Madhusudan's results to the wider class of programs with bounded delay, which may read several input symbols before producing an output symbol (or vice versa). As a formal foundation, we inductively define a semantics for such programs.

Full work available at URL: https://arxiv.org/abs/1303.0797

Recommendations

• Synthesizing structured reactive programs via deterministic tree automata
• Bounded synthesis of reactive programs
• Verification and synthesis of reactive programs
• Synthesizing reactive programs
• scientific article; zbMATH DE number 4085004

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Cites Work

• Graph searching and a min-max theorem for tree-width
• Title not available (Why is that?)
• A partial k-arboretum of graphs with bounded treewidth
• Church's Problem Revisited
• Bounded Synthesis
• Synthesis from Component Libraries
• Synthesizing reactive programs
• Title not available (Why is that?)
• The treewidth and pathwidth of hypercubes
• Solving Sequential Conditions by Finite-State Strategies
• All structured programs have small tree width and good register allocation
• Degrees of lookahead in regular infinite games
• Strategy machines and their complexity

Cited In (5)

• Bounded synthesis of reactive programs
• Incorporating monitors in reactive synthesis without paying the price
• Synthesizing reactive programs
• Synthesizing structured reactive programs via deterministic tree automata
• Synthesis for Structure Rewriting Systems

This page was built for publication: Synthesizing structured reactive programs via deterministic tree automata

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2346409)