The design of reliable embedded control systems inherits the difficulties involved in designing both control systems and distributed (concurrent) computing systems. Design bugs in these systems may arise from the unforeseen interactions among the computing, communication and control subsystems. Motivated by the difficulties of finding this type of design bugs, this project focuses on developing mathematical frameworks, based on formal methods, to facilitate the design and analysis of such embedded systems. This work incorporates methodology from computer science and control, including model checking, theorem proving, synthesis of digital designs, reachability analysis, Lyapunov-type methods and receding horizon control. Various applications have been considered, including autonomy, vehicle management and multi-target tracking.
Tichakorn (Nok) Wongpiromsarn
Assistant Professor
My research focuses on formal methods, motion planning, situational reasoning, hybrid systems, and distributed control systems.
Related
- DARPA Urban Challenge 2007
- Planning with Conflicting Specifications
- Formal Specifications of Autonomous Systems
- Sharing the World with Autonomous Systems: What Goes Wrong and How to Fix It (NSF)
- CAREER: Establishing Correctness of Learning-Enabled Autonomous Systems with Conflicting Requirements (NSF)
Publications
Automata Theory Meets Barrier Certificates: Temporal Logic Verification of Nonlinear Systems
We consider temporal logic verification of (possibly nonlinear) dynamical systems evolving over continuous state spaces. Our approach …
Tichakorn Wongpiromsarn, Ufuk Topcu, Andrew Lamperski
Online horizon selection in receding horizon temporal logic planning
Temporal logics have proven effective for correct-by-construction synthesis of controllers for a wide range of robotic applications. …
Vasumathi Raman, Mattias Fält, Tichakorn Wongpiromsarn, Richard M. Murray
Incremental Controller Synthesis in Probabilistic Environments with Temporal Logic Constraints
In this paper, we consider automatic computation of optimal control strategies for a robot interacting with a set of independent …
Alphan Ulusoy, Tichakorn Wongpiromsarn, Calin Belta
Incremental synthesis of control policies for heterogeneous multi-agent systems with linear temporal logic specifications
We consider automatic synthesis of control policies for non-independent, heterogeneous multi-agent systems with the objective of …
Tichakorn Wongpiromsarn, Alphan Ulusoy, Calin Belta, Emilio Frazzoli, Daniela Rus
Synthesis of Control Protocols for Autonomous Systems
This article provides a review of control protocol synthesis techniques that incorporate methodologies from formal methods andcontrol …
Tichakorn Wongpiromsarn, Ufuk Topcu, Richard M. Murray
Verifying Cyber-Physical Interactions in Safety-Critical Systems
Safety-compromising bugs in software-controlled systems are often hard to detect. In a 2007 DARPA Urban Challenge vehicle, such a …
Sayan Mitra, Tichakorn Wongpiromsarn, Richard M. Murray
Control of probabilistic systems under dynamic, partially known environments with temporal logic specifications
We consider the synthesis of control policies for probabilistic systems, modeled by Markov decision processes, operating in partially …
Tichakorn Wongpiromsarn, Emilio Frazzoli
Incremental control synthesis in probabilistic environments with Temporal Logic constraints
In this paper, we present a method for optimal control synthesis of a plant that interacts with a set of agents in a graph-like …
Alphan Ulusoy, Tichakorn Wongpiromsarn, Calin Belta
Incremental temporal logic synthesis of control policies for robots interacting with dynamic agents
We consider the synthesis of control policies from temporal logic specifications for robots that interact with multiple dynamic …
Tichakorn Wongpiromsarn, Alphan Ulusoy, Calin Belta, Emilio Frazzoli, Daniela Rus
Receding Horizon Temporal Logic Planning
We present a methodology for automatic synthesis of embedded control software that incorporates a class of linear temporal logic (LTL) …
Tichakorn Wongpiromsarn, Ufuk Topcu, Richard M. Murray
Verification of Periodically Controlled Hybrid Systems: Application to an Autonomous Vehicle
This article introduces Periodically Controlled Hybrid Automata (PCHA) for modular specification of embedded control systems. In a …
Tichakorn Wongpiromsarn, Sayan Mitra, Andrew Lamperski, Richard M. Murray
Correct, Reactive, High-Level Robot Control
In this article, we presented an overview of how temporal logic synthesis, coupled with abstractions and continuous bisimilar …
Hadas Kress-Gazit, Tichakorn Wongpiromsarn, Ufuk Topcu
Distributed Synthesis of Control Protocols for Smart Camera Networks
We considered the problem of designing control protocols for pan-tilt-zoom (PTZ) cameras within a smart camera network where the goal …
Necmiye Ozay, Ufuk Topcu, Richard M. Murray, Tichakorn Wongpiromsarn
Formal Synthesis of Embedded Control Software: Application to Vehicle Management Systems
Motivated by the transition from federated to integrated architectures in aerial vehicles, we propose an automated methodology for the …
Tichakorn Wongpiromsarn, Ufuk Topcu, Richard Murray
Synthesis of provably correct controllers for autonomous vehicles in urban environments
This paper considers automatic synthesis of provably correct controllers for autonomous vehicles operating in an urban environment …
Tichakorn Wongpiromsarn, Sertac Karaman, Emilio Frazzoli
Formal Methods for Design and Verification of Embedded Control Systems: Application to an Autonomous Vehicle
The design of reliable embedded control systems inherits the difficulties involved in designing both control systems and distributed …
Tichakorn Wongpiromsarn
Automatic Synthesis of Robust Embedded Control Software
We propose a methodology for automatic synthesis of embedded control software that accounts for exogenous disturbances. The resulting …
Tichakorn Wongpiromsarn, Ufuk Topcu, Richard M. Murray
Receding Horizon Control for Temporal Logic Specifications
In this paper, we describe a receding horizon framework that satisfies a class of linear temporal logic specifications sufficient to …
Tichakorn Wongpiromsarn, Ufuk Topcu, Richard M. Murray
Periodically Controlled Hybrid Systems
This paper introduces Periodically Controlled Hybrid Automata (PCHA) for describing a class of hybrid control systems. In a PCHA, …
Tichakorn Wongpiromsarn, Sayan Mitra, Richard M. Murray, Andrew Lamperski
Receding horizon temporal logic planning for dynamical systems
This paper bridges the advances in computer science and control to allow automatic synthesis of control strategies for complex …
Tichakorn Wongpiromsarn, Ufuk Topcu, Richard M. Murray