Interactive Synthesis of Temporal Specifications from Examples and Natural Language
Sat 21 Nov 2020 01:20 - 01:40 at SPLASH-I - F-4A Chair(s): Hidehiko Masuhara
Motivated by applications in robotics, we consider the task of synthesizing linear temporal logic (LTL) specifications based on examples and natural language descriptions. While LTL is a flexible, expressive, and unambiguous language to describe robotic tasks, it is often challenging for non-expert users. In this paper, we present an interactive method for synthesizing LTL specifications from a single example trace and a natural language description. The interaction is limited to showing a small number of behavioral examples to the user who decides whether or not they exhibit the original intent. Our approach generates candidate LTL specifications and distinguishing examples using an encoding into optimization modulo theories problems. Additionally, we use a grammar extension mechanism and a semantic parser to generalize synthesized specifications to parametric task descriptions for subsequent use. Our implementation in the tool LtlTalk starts with a domain-specific language that maps to a fragment of LTL and expands it through example-based user interactions, thus enabling natural language-like robot programming, while maintaining the expressive power and precision of a formal language. Our experiments show that the synthesis method is precise, quick, and asks only a few questions to the users, and we demonstrate in a case study how LtlTalk generalizes from the synthesized tasks to other, yet unseen, tasks.
Fri 20 Nov Times are displayed in time zone: Central Time (US & Canada) change
13:00 - 14:20: F-4AOOPSLA at SPLASH-I +12h Chair(s): Ruben MartinsCarnegie Mellon University, Louis MandelIBM Research, USA | |||
13:00 - 13:20 Talk | A Modular Cost Analysis for Probabilistic Programs OOPSLA Link to publication DOI Media Attached | ||
13:20 - 13:40 Talk | Interactive Synthesis of Temporal Specifications from Examples and Natural Language OOPSLA Link to publication DOI Media Attached | ||
13:40 - 14:00 Talk | Scaling Exact Inference for Discrete Probabilistic Programs OOPSLA Steven HoltzenUniversity of California at Los Angeles, Guy Van den BroeckUniversity of California at Los Angeles, Todd MillsteinUniversity of California at Los Angeles Link to publication DOI Pre-print Media Attached | ||
14:00 - 14:20 Talk | Digging for Fold: Synthesis-Aided API Discovery for Haskell OOPSLA Michael B. JamesUniversity of California at San Diego, Zheng GuoUniversity of California, San Diego, Ziteng WangUniversity of California at San Diego, Shivani DoshiUniversity of California at San Diego, Hila PelegUniversity of California at San Diego, Ranjit JhalaUniversity of California at San Diego, Nadia PolikarpovaUniversity of California at San Diego Link to publication DOI Media Attached |