Campus Event Calendar
Event Entry
What and Who
Planning and Specification Problems for Multi-Robot Systems, Powered by Formal Methods
Ivan Gavran
MMCI
SWS Student Defense Talks - Thesis Defense
SWS
MPI Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Friday, 24 June 2022
10:30
60 Minutes
E1 5
113
Kaiserslautern
Abstract
This talk will be based on my PhD work on using formal methods to
enhance both programming of robotic systems and learning of autonomous
agents.
After giving a broad overview of the work, I will focus on the problem
of inferring specifications from examples.
In particular, we will discuss the problem of inferring a linear
temporal logic (LTL) formula from sets of positive and negative example
traces, as well as from a set of positive examples only.
Building on this method, I will describe LTLTalk, a tool that helps
users of a robotic system transfer their intent into an LTL specification.
The approach combines the intent signals from a single demonstration and
a natural language description given by a user.
A set of candidate specifications is inferred by encoding the problem as
a satisfiability problem for propositional logic.
This set is narrowed down to a single specification through interaction
with the user: the user approves or declines generated simulations of
the robot's behavior in different situations.
enhance both programming of robotic systems and learning of autonomous
agents.
After giving a broad overview of the work, I will focus on the problem
of inferring specifications from examples.
In particular, we will discuss the problem of inferring a linear
temporal logic (LTL) formula from sets of positive and negative example
traces, as well as from a set of positive examples only.
Building on this method, I will describe LTLTalk, a tool that helps
users of a robotic system transfer their intent into an LTL specification.
The approach combines the intent signals from a single demonstration and
a natural language description given by a user.
A set of candidate specifications is inferred by encoding the problem as
a satisfiability problem for propositional logic.
This set is narrowed down to a single specification through interaction
with the user: the user approves or declines generated simulations of
the robot's behavior in different situations.
Contact
--email hidden
Virtual Meeting Details
Zoom
972 6087 0197
passcode not visible
logged in users only
Maria-Louise Albrecht, 06/14/2022 13:41 -- Created document.