About: We introduce and study good-enough synthesis (ge-synthesis) – a variant of synthesis in which the system is required to satisfy a given specification [Formula: see text] only when it interacts with an environments for which a satisfying interaction exists. Formally, an input sequence x is hopeful if there exists some output sequence y such that the induced computation [Formula: see text] satisfies [Formula: see text], and a system ge-realizes [Formula: see text] if it generates a computation that satisfies [Formula: see text] on all hopeful input sequences. ge-synthesis is particularly relevant when the notion of correctness is multi-valued (rather than Boolean), and thus we seek systems of the highest possible quality, and when synthesizing autonomous systems, which interact with unexpected environments and are often only expected to do their best. We study ge-synthesis in Boolean and multi-valued settings. In both, we suggest and solve various definitions of ge-synthesis, corresponding to different ways a designer may want to take hopefulness into account. We show that in all variants, ge-synthesis is not computationally harder than traditional synthesis, and can be implemented on top of existing tools. Our algorithms are based on careful combinations of nondeterministic and universal automata. We augment systems that ge-realize their specifications by monitors that provide satisfaction information. In the multi-valued setting, we provide both a worst-case analysis and an expectation-based one, the latter corresponding to an interaction with a stochastic environment.   Goto Sponge  NotDistinct  Permalink

An Entity of Type : fabio:Abstract, within Data Space : covidontheweb.inria.fr associated with source document(s)

AttributesValues
type
value
  • We introduce and study good-enough synthesis (ge-synthesis) – a variant of synthesis in which the system is required to satisfy a given specification [Formula: see text] only when it interacts with an environments for which a satisfying interaction exists. Formally, an input sequence x is hopeful if there exists some output sequence y such that the induced computation [Formula: see text] satisfies [Formula: see text], and a system ge-realizes [Formula: see text] if it generates a computation that satisfies [Formula: see text] on all hopeful input sequences. ge-synthesis is particularly relevant when the notion of correctness is multi-valued (rather than Boolean), and thus we seek systems of the highest possible quality, and when synthesizing autonomous systems, which interact with unexpected environments and are often only expected to do their best. We study ge-synthesis in Boolean and multi-valued settings. In both, we suggest and solve various definitions of ge-synthesis, corresponding to different ways a designer may want to take hopefulness into account. We show that in all variants, ge-synthesis is not computationally harder than traditional synthesis, and can be implemented on top of existing tools. Our algorithms are based on careful combinations of nondeterministic and universal automata. We augment systems that ge-realize their specifications by monitors that provide satisfaction information. In the multi-valued setting, we provide both a worst-case analysis and an expectation-based one, the latter corresponding to an interaction with a stochastic environment.
Subject
  • Proteomics
  • Biotechnology
  • Signal transduction
  • Biophysics
  • Biochemistry methods
  • Internet architecture
  • Protein–protein interaction assays
  • Quantum chemistry
part of
is abstract of
is hasSource of
Faceted Search & Find service v1.13.91 as of Mar 24 2020


Alternative Linked Data Documents: Sponger | ODE     Content Formats:       RDF       ODATA       Microdata      About   
This material is Open Knowledge   W3C Semantic Web Technology [RDF Data]
OpenLink Virtuoso version 07.20.3229 as of Jul 10 2020, on Linux (x86_64-pc-linux-gnu), Single-Server Edition (94 GB total memory)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2024 OpenLink Software