2013/02/28 by Benedikt Brütsch
Computer Science · Mathematics · #Artificial intelligence #Automaton #Bounded function #Class (philosophy) #Computer science #Formal Methods in Verification #Logic, programming, and type systems #Mathematics #Programming language #Representation (politics) #Semantics (computer science) #Set (abstract data type) #Symbol (formal) #Theoretical computer science #Transition system #Tree (set theory) #cs.LO #semigroups and automata theory
paper · pdf · doi:10.4204/eptcs.112.16
published as EPTCS 112, 2013, pp. 107-113 · In Proceedings SR 2013, arXiv:1303.0071
openalex publication_date 2013/02/28 · arxiv created 2013/03/04 · arxiv updated 2013/03/05 · openalex created_date 2025/10/10 · openalex updated_date 2026/08/05
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.