2021-07-28 –, Green
Autonomous systems are often required to operate in partially observable environments. They must reliably execute a specified objective even with incomplete information about the state of the environment. Model checking allows us to synthesize a decision policy that satisfies a linear temporal logic (LTL) formula in a POMDP. By reformulating the model checking problem into an AI planning problem, we can use state-of-the-art POMDP planning algorithms to solve model checking problems.
In this talk we will show how we built a model checking library in a few lines of Julia by integrating an LTL manipulation library to the JuliaPOMDP ecosystem. With this library we can compute decision policies with probabilistic guarantees for various range of partially observable problems: drone surveillance, robot exploration, pedestrian avoidance for autonomous driving.
This lightning talk will be organized as follows:
- Introduction to the problem of POMDP/MDP model checking: quick overview of JuliaPOMDP [1]
- Introduction to linear temporal logic manipulation using Spot.jl [2]: Spot.jl is a wrapper of spot [3], a c++ library for LTL manipulation. The Julia wrapper is built using CxxWrap.jl. We will demonstrate some visual examples of how spot is used to convert a temporal logic formula into a finite state machine and how we can visualize it (material will be inspired from the Spot.jl tutorial but remodeled to fit the talk format).
- Introduction to POMDPModelChecking.jl [4]: we will show how we can reuse the whole JuliaPOMDP ecosystem to solve model checking problems. Our library exposes two solvers (ModelCheckingSolver and ReachabilitySolver), which takes as input any Julia POMDP model and an LTL formula and outputs a policy. Internally, the solver creates a new POMDP model which is a composition of the original model, and a finite state machine created by Spot.jl. This new model can then be solved by any JuliaPOMDP planning algorithm. The theoretical justification of reformulating the model checking problem into a planning problem has been detailed in previous work [5].
- Gallery: We will show visual examples of decision policies computed using POMDPModelChecking.jl on the rock sample POMDP problem [6].
References:
[1] https://github.com/JuliaPOMDP
[2] https://github.com/sisl/Spot.jl
[3] https://spot.lrde.epita.fr/index.html
[4] https://github.com/sisl/POMDPModelChecking.jl
[5] M. Bouton, J. Tumova, and M. J. Kochenderfer, "Point-Based Methods for Model Checking in Partially Observable Markov Decision Processes," in AAAI Conference on Artificial Intelligence (AAAI), 2020.
[6] https://github.com/JuliaPOMDP/RockSample.jl
[7] M. Bouton, "Safe and Scalable Planning Under Uncertainty for Autonomous Driving", PhD thesis, Stanford University, 2020.
I am an AI Researcher at Ericsson Research. My research interests lie in reinforcement learning, planning under uncertainty, and AI safety. Prior to joining Ericsson I completed my PhD at Stanford University under the supervision of Prof. Mykel Kochenderfer. My thesis was about safe and scalable planning under uncertainty for autonomous driving and all the code was written in Julia. At Juliacon 2021 I will present work I did during my thesis.