SPLASH 2020
Sun 15 - Sat 21 November 2020 Online Conference
Fri 20 Nov 2020 13:20 - 13:40 at SPLASH-I - F-4A Chair(s): Louis Mandel, Ruben Martins
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

Displayed time zone: Central Time (US & Canada) change

13:00 - 14:20
F-4AOOPSLA at SPLASH-I +12h
Chair(s): Louis Mandel IBM Research, USA, Ruben Martins Carnegie Mellon University
13:00
20m
Talk
A Modular Cost Analysis for Probabilistic Programs
OOPSLA
Martin Avanzini Inria, Georg Moser University of Innsbruck, Michael Schaper University of Innsbruck
Link to publication DOI Media Attached
13:20
20m
Talk
Interactive Synthesis of Temporal Specifications from Examples and Natural Language
OOPSLA
Ivan Gavran MPI-SWS, Eva Darulova MPI-SWS, Rupak Majumdar MPI-SWS
Link to publication DOI Media Attached
13:40
20m
Talk
Scaling Exact Inference for Discrete Probabilistic ProgramsDistinguished Paper
OOPSLA
Steven Holtzen University of California at Los Angeles, Guy Van den Broeck University of California at Los Angeles, Todd Millstein University of California at Los Angeles
Link to publication DOI Pre-print Media Attached
14:00
20m
Talk
Digging for Fold: Synthesis-Aided API Discovery for Haskell
OOPSLA
Michael B. James University of California at San Diego, Zheng Guo University of California, San Diego, Ziteng Wang University of California at San Diego, Shivani Doshi University of California at San Diego, Hila Peleg University of California at San Diego, Ranjit Jhala University of California at San Diego, Nadia Polikarpova University of California at San Diego
Link to publication DOI Media Attached

Sat 21 Nov

Displayed time zone: Central Time (US & Canada) change

01:00 - 02:20
F-4AOOPSLA at SPLASH-I
Chair(s): Hidehiko Masuhara Tokyo Institute of Technology
01:00
20m
Talk
A Modular Cost Analysis for Probabilistic Programs
OOPSLA
Martin Avanzini Inria, Georg Moser University of Innsbruck, Michael Schaper University of Innsbruck
Link to publication DOI Media Attached
01:20
20m
Talk
Interactive Synthesis of Temporal Specifications from Examples and Natural Language
OOPSLA
Ivan Gavran MPI-SWS, Eva Darulova MPI-SWS, Rupak Majumdar MPI-SWS
Link to publication DOI Media Attached
01:40
20m
Talk
Scaling Exact Inference for Discrete Probabilistic ProgramsDistinguished Paper
OOPSLA
Steven Holtzen University of California at Los Angeles, Guy Van den Broeck University of California at Los Angeles, Todd Millstein University of California at Los Angeles
Link to publication DOI Pre-print Media Attached
02:00
20m
Talk
Digging for Fold: Synthesis-Aided API Discovery for Haskell
OOPSLA
Michael B. James University of California at San Diego, Zheng Guo University of California, San Diego, Ziteng Wang University of California at San Diego, Shivani Doshi University of California at San Diego, Hila Peleg University of California at San Diego, Ranjit Jhala University of California at San Diego, Nadia Polikarpova University of California at San Diego
Link to publication DOI Media Attached