Formal Methods in Robotics: Understanding Logic and Verification Techniques
Dive into the world of formal methods in robotics, exploring topics such as logic, program verification, and specification reasoning. Discover favorite problems in formal methods like verification techniques and specifications in computer science.
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
You are allowed to download the files provided on this website for personal or commercial use, subject to the condition that they are used lawfully. All files are the property of their respective owners.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.
E N D
Presentation Transcript
Formal Methods for Robotics Spring 2021: CSCI 699 Instructor: Jyo Deshmukh USC Viterbi School of Engineering Department of Computer Science 1
What are formal methods? Sub-area of computer science, as old as computer science itself Arguably at the dawn of CS, all of CS was formal methods Meaning has evolved over the years, but favorite topics include Use of Logic : Propositional, Temporal, First-order, Monadic second-order, Second-order, Higher-order logics Emphasis on proving properties of programs, reasoning about programs View of programs as state machines : Automata, Markov chains, Turing machines USC Viterbi 2 School of Engineering Department of Computer Science
Favorite problems in formal methods: I Verification How do you prove that the program works correctly under all possible inputs? How do you show that a program satisfies its given specification? Verification Techniques Theorem proving (deductive verification) Model checking (inductive verification) USC Viterbi 3 School of Engineering Department of Computer Science
Specifications Programmer Assertions assert(x>0); // if the assertion fails, bad things happen Implicit assertions Don t dereference a null pointer, don t exceed array bounds, don t deallocate freed memory, don t divide by zero, don t get stuck in an infinite loop (i.e. do terminate) Input/output examples (for terminating programs) USC Viterbi 4 School of Engineering Department of Computer Science
Specifications First-order logic (propositional logic + quantifiers + function symbols + operators) Reactive systems/Cyber-physical systems: Very different style of specifications, because these systems do not terminate Specifications reason about infinite program behaviors Temporal logic specifications: Linear Temporal Logic (LTL), Signal Temporal Logic (STL), Probabilistic Computation-Tree Logic (PCTL) USC Viterbi 5 School of Engineering Department of Computer Science
Model checking For system of type M , do all its behaviors satisfy specification of type S ? M = deterministic, nondeterministic, probabilistic, stochastic, continuous- time, discrete-time, hybrid (continuous+discrete) S = LTL, CTL, PCTL, STL, MTL etc. Important considerations: Is it decidable? What is its complexity? Abstraction/Refinement/Counterexamples USC Viterbi 6 School of Engineering Department of Computer Science
Cyber-Physical / Robotic systems Physical component Actuators Sensors Environment/Plant Controller (Some embedded code) USC Viterbi 7 School of Engineering Department of Computer Science
Further Challenges in Robotic systems What is the system model? System model needs to also include model of the environment Environment is noisy, continuous-time, time-varying, full of things you did not foresee Lot more software than just the control software Software for Perception, Communication Software for Sensor/Actuator calibration System subject to hardware failures : software is just one part of the robot USC Viterbi 8 School of Engineering Department of Computer Science
Favorite problems in formal methods: II (Functional) Program Synthesis How do you find a program that matches given input/output data Reactive Synthesis (from logical, temporal specifications) Find a supervisor, controller, policy that ensures that the system satisfies its specification Important problems: Is it decidable? What is its complexity? What are the assumptions under which it is possible (what kinds of environments)? USC Viterbi 9 School of Engineering Department of Computer Science
Controller/Policy Synthesis Formal methods community has focused on correct by construction design from specifications Robotics community has traditionally focused on performance objectives No one typically starts a new robot project by saying, these are all the things I want my robot behaviors to formally satisfy Popular techniques for controlling a robot through software Many hours of debugging Reinforcement Learning (training the robot through carrots and sticks) Learning from Demonstrations (training the robot by showing it what to do) USC Viterbi 10 School of Engineering Department of Computer Science
What is the aim of this course? How do we bridge the gap between formal methods for reasoning about system correctness w.r.t. behavioral specifications and correct-by-construction design from logical specifications with techniques and applications from the robotics domain? USC Viterbi 11 School of Engineering Department of Computer Science
What is the instructional goal of this course? Learn to digest papers from formal methods and (theoretical) learning- based techniques in robotics Learn to write papers in these areas Learn to review papers in these areas USC Viterbi 12 School of Engineering Department of Computer Science
Jyo will be very happy if Each one of you can take your term paper for this semester and submit it to a conference/journal with some extra effort Your advisor says, This is such a well-written paper review. Amazing! You feel like the mathy topics you read about in this course bring excitement to your life USC Viterbi 13 School of Engineering Department of Computer Science
Okay, so what do we plan to learn? Read papers in 6 different areas Background for verification of robotic systems Temporal logic specifications Synthesis from logical specifications Path planning from specifications Reinforcement Learning from specifications, reasoning about correctness of RL/deep RL Learning specifications and learning from demonstrations USC Viterbi 14 School of Engineering Department of Computer Science
Course grunt work Every week read one, two or three papers Turn in a decent paragraph or two about each paper read on Slack Early bird gets the worm: try to avoid overlap with your peers Comment on some cool math trick you noticed in the paper Comment on ideas that it inspired in you, ways to extend the paper I will grade in the bulk: no individual grading for summaries, but subjective grading based on the bulk of your summaries and their quality Volunteer (or be volunteered) for presenting one paper each week Some papers may need two voluneers USC Viterbi 15 School of Engineering Department of Computer Science
Presentation and Discussion Present the paper like its your own paper that you are presenting at a conference that is very generous in time Plan for a 30-45 min presentation! Discuss: What did you not get in the paper? What things did you find interesting and feel like sharing with others Criticize! How could they have improved <blah>? Explain! Whiteboard stuff! USC Viterbi 16 School of Engineering Department of Computer Science
Peer Review! In my opinion the most fun part of this class First two weeks: we will reserve 30-45 mins to discuss your project ideas March 1: Paper Skeleton Due Intro + Related work + Prelims + Problem Definition + Solution Overview March 15: You get reviews from a PC of your peers (2 to 3 reviews / paper) Use the reviews to refine your paper April 5 : Almost-Paper Due Almost paper = Paper Skeleton + Summary of main results / experimental setup April 19: You get reviews May 12 : Polished paper due USC Viterbi 17 School of Engineering Department of Computer Science
Peer Review You grade your peers papers Bad grade: Not clear motivation? Typos/Grammar issues? Problem not defined clearly? Solution sketch unclear? Related work not surveyed? You grade your peers reviews Bad review: <1 page, single spaced, 11 size font, focuses only on one aspect (e.g. language/grammar) USC Viterbi 18 School of Engineering Department of Computer Science
Grading and Evaluation Breakdown Paper Reviews: 45% (includes presentations) Peer Review: 20% (includes peer-assisted instructor assessment) Final Paper: 35% (includes instructor assessment of each draft) USC Viterbi 19 School of Engineering Department of Computer Science
Everything is on Slack Time Accommodations: discuss USC Viterbi 20 School of Engineering Department of Computer Science
Introductions What s your background? What do you expect to get out of it? Do you have a project in mind? USC Viterbi 21 School of Engineering Department of Computer Science
