Synthesizing structured reactive programs via deterministic tree automata

DOI10.1016/J.IC.2015.03.013MaRDI QIDQ2346409zbMATH OpenOpenAlexFDO

Authors Benedikt Brütsch

Publication date 1 June 2015

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

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

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)

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.

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

Cites work

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

Cited in

(5)

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

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)