| Time |
Details |
|
1430-1515
|
|
Jana Tumova
|
| Title: |
Safe multi-agent collaboration via formal synthesis
|
| Abstract: |
Imagine an autonomous robot that aims to accomplish a task while operating around or in interaction with people. In this settings, safety (such as avoidance of collision or contact) is of the utmost importance. Yet, the robot often cannot guarantee safety on its own, without posing some assumptions on the humans’ behaviors. In this talk, we discuss a particular type of assume-guarantee synthesis. We aim for the assumptions to be minimal, or least-limiting for a human in the robot’s environment and we present algorithms for simultaneous formal synthesis of least-limiting assumptions (advisers) for the human and a provably safe plan for the robot. Furthermore, we discuss how we can use this concept as a decentralized approach to coordination of fully autonomous multi-agent systems. |
| Bio: |
Jana Tumova is an associate professor at the School of Electrical Engineering and Computer Science at KTH Royal Institute of Technology. She received PhD in computer science from Masaryk University and was awarded ACCESS postdoctoral fellowship at KTH in 2013. She was also a visiting researcher at MIT, Boston University, and Singapore-MIT Alliance for Research and Technology. Her research interests include formal methods applied in decision making, motion planning, and control of autonomous systems. Among other projects, she is a recipient of a Swedish Research Council Starting Grant to explore compositional planning for multi-agent systems under temporal logic goals and a WASP Expeditions project focusing on design of correct-by-design and socially acceptable autonomous systems. She was selected to give an Early Career Spotlight talk at Robotics: Science and Systems 2021.
|
|
|
|
1515-1600
|
|
Necmiye Ozay
|
| Title: |
Learning temporal logic constraints from suboptimal demonstrations
|
| Abstract: |
In this talk, I will present a method for learning multi-stage tasks from demonstrations by learning the logical structure and atomic propositions of a consistent linear temporal logic (LTL) formula. The learner is given successful but potentially suboptimal demonstrations, where the demonstrator is optimizing a cost function while satisfying the LTL formula. Our algorithm uses the Karush-Kuhn-Tucker (KKT) optimality conditions of the demonstrations together with a counterexample-guided falsification strategy to learn the atomic proposition parameters and logical structure of the LTL formula, respectively. We provide theoretical guarantees on the conservativeness of the recovered atomic proposition sets, as well as completeness (in the limit) in the search for finding an LTL formula consistent with the demonstrations. We will illustrate the method both with simulated and hardware experiments.
|
| Bio: |
Necmiye received her B.S. degree in Electrical and Electronics Engineering from Bogazici University, Istanbul in 2004, her M.S. degree in Electrical Engineering from the Pennsylvania State University, University Park, PA in 2006 and her Ph.D degree again in Electrical Engineering from Northeastern University, Boston, MA in 2010. Between 2010 and 2013, she was a Control and Dynamical Systems postdoctoral scholar at the Department of Computing and Mathematical Sciences at California Institute of Technology, Pasadena, CA. She joined the Electrical Engineering and Computer Science Department at the University of Michigan, Ann Arbor, MI, in Fall 2013, where she is currently an associate professor. She is part of the Michigan Controls Group, a core member of Michigan Robotics and also affiliated with the Michigan Institute for Data Science (MIDAS) and Michigan Institute for Computational Discovery & Engineering (MICDE).
|
|
|
|
1600-1615
|
Fika
|
|
1615-1700
|
|
Anne-Kathrin Schmuck
|
| Title: | Let's play! - Solving controller synthesis games for cyber-physical system design
|
| Abstract: |
Cyber-Physical Systems (CPS) are technical systems where a large software stack orchestrates
the interaction of physical and digital components.
Such systems are omnipresent in our daily life and their correct behavior is crucial.
However, developing safe, reliable and performant CPS is challenging.
A promising research direction towards this goal is the combination of formal methods from
computer science and controller synthesis techniques from automation.
In my talk I will discuss how infinite two-player games over finite graphs,
originating from the formal methods community, can be utilized and enhanced for higher layer control of CPS.
In particular, I will discuss how the use of environment assumptions -
used to model particularities of the system under control within these games -
has to be rethought in order to effectively solve controller synthesis tasks for CPS.
|
| Bio: |
Anne-Kathrin Schmuck is an independent research group leader at the
Max Planck Institute for Software Systems (MPI-SWS) in Kaiserslautern, Germany,
funded by the Emmy Noether Programme of the German Science Foundation (DFG).
She received the Dipl.-Ing. (M.Sc) degree in engineering cybernetics from OvGU Magdeburg, Germany,
in 2009 and the Dr.-Ing. (Ph.D.) degree in electrical engineering from TU Berlin, Germany, in 2015.
Between 2015 and 2020 she was a Postdoctoral researcher at MPI-SWS. She currently serves as the co-chair of the
IEEE CSS Technical Committee on Discrete Event Systems and as associate editor for the Springer Journal on
Discrete Event Dynamical Systems.
Her current research interests include abstraction based controller design, reactive synthesis,
supervisory control theory, hierarchical control and contract-based distributed synthesis.
|
|
|