» CSIS » Faculty/Staff
|
|
Ph.D. - 2021 - Kansas State University, USA |
Ratan Lal is a Ph.D. candidate in the department of computer science at Kansas State University, USA. He obtained his master in computer science from Indian Statistical Institute, India in 2014. He was a research assistant at IMDEA Software Institute, Spain from July 2014 to December 2015. He was a research intern at Toyota Motor North America, Research and Development (TMNA R&D) in summer 2019. His main research interest is in the Formal Analysis of (Stochastic) Cyber-Physical Systems and its applications in automotive, robotics, unmanned aerial vehicle (UAV), and autonomous underwater vehicle (AUV), with emphasis on both theoretical and practical methods for the design and verification of hybrid control systems. He has been awarded the Gattani Outstanding Graduate Student Award for his research outstanding at Kansas State University. He has been serving as a member of research evaluation program committee for the top conferences: International Conference on Hybrid Systems: Computation and Control (HSCC), International Conference on Computer-Aided Verification (CAV). Also, he has been serving as a technical program committee for the international conferences: Advances in Computation, Communications and Services (ACCSE). He has reviewed more than 50 papers for the international conferences and journals related to cyber-physical systems.
Safety is an important challenge for the critical systems, specifically cyber physical systems (CPS), such as robots and drones. It becomes even more challenging when uncertainties are involved in CPS due to the disturbance in noise or sensor/actuator noise. Hence, our broad goal is to develop safety verification methods/tools for CPS using formal methods towards enabling the formal verification practical. Towards this, we have developed tool BEAVer: bounded error approximation based verifier for linear hybrid systems and networked linear hybrid systems, and tool ProCEGARVer: probabilistic counter-example guided abstraction refinement based verifier for probabilistic polyhedral hybrid systems.
Cyber physical systems are commonly developed according to model-based design. Engineers use Verification-Validation (V-V) approach to implement the model-based design. In V-V approach, The requirement specification of CPS is divided into sub-requirements in top-down fashion, and the system is implemented and validated its requirement in bottom-up fashion. At any stage, if validation is failed, then one possibility is that the requirement may not be formulated correctly. Hence, our broad goal is to develop methods for identifying inconsistencies in the requirement prior to the development. Towards this,we have developed an automatic trace generation method which generates a set of satisfying and violating behaviors of the system with respect to its requirement. In the method, the requirement is expressed in the form of signal temporal logic (STL), which is a popular formalism of expressing continuous behaviors. The development of tool STLTraceGen: Signal Temporal Logic Trace Generator is under the process.
Autonomous systems are popularly used in many applications, such as mail delivery, pesticide spraying, data collection from the crops, which are performed using autonomous vehicles, ground robots, and drones, respectively. Due to limited resources, these tasks are required to be performed in an optimal way. Hence, optimal path/motion for the autonomous systems save both energy and time. Towards this, we have developed an optimal multi-robot path planning and a time-optimal multi quad-rotor trajectory generation for pesticide spraying in an agricultural field. We have developed tools MRPPlaner: multi-robot path planer and MQTGen: multi quad-rotor trajectory generator for pesticide spraying in an agricultural field.
Ratan Lal and Pavithra Prabhakar
Time-Optimal Multi-Quadrotor Trajectory Planning for Pesticide Spraying
International Conference on Robotics and Automation (ICRA), 2021
Ratan Lal, Weikang Duan, and Pavithra Prabhakar
Bayesian Statistical Model Checking for Continuous Stochastic Logic
ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE), 2020
Ratan Lal and Pavithra Prabhakar
Safety Analysis of Linear Discrete-time Stochastic Systems
International Conference on Embedded Software (EMSOFT) (WIP), 2020
Daksh Shukla, Ratan Lal, Dustin Hauptman, Shawn S. Keshmiri, Pavithra Prabhakar and Nicole Beckage
Flight Test Validation of a Safety-Critical Neural Network Based Longitudinal Controller for a Fixed-Wing UAS
AIAA AVIATION, 2020
Ratan Lal and Pavithra Prabhakar
Compositional construction of bounded error over-approximations of acyclic interconnected continuous dynamical systems
ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE), 2019
Ratan Lal and Pavithra Prabhakar
Counterexample guided abstraction refinement for polyhedral probabilistic hybrid systems
ACM Transactions on Embedded Computing Systems (TECS), Accepted at EMSOFT, 2019
Pavithra Prabhakar, Ratan Lal and James Kapinski
Automatic Trace Generation for Signal Temporal Logic
39th IEEE Real-Time Systems Symposium (RTSS), 2018
Ratan Lal and Pavithra Prabhakar
Bounded Verification of Reachability of Probabilistic Hybrid Systems
International Conference on Quantitative Evaluation of Systems (QEST), 2018
Ratan Lal and Pavithra Prabhakar
Hierarchical Abstractions for Reachability Analysis of Probabilistic Hybrid Systems
Annual Allerton Conference on Communication, Control, and Computing (Allerton), 2018
Ratan Lal and Pavithra Prabhakar
Safety Analysis using Compositional Bounded Error Approximations of Communicating Hybrid Systems
IEEE Conference on Decision and Control (CDC), 2017
Ratan Lal, Ajay Sharda and Pavithra Prabhakar
Optimal Multi-robot Path Planning for Pesticide Spraying in Agricultural Fields
IEEE Conference on Decision and Control (CDC), 2017
Pavithra Prabhakar, Miriam Garcia Soto and Ratan Lal
Verification Techniques for Hybrid Systems
International Symposium, ISoLA 2016
Pierre Ganty, Samir Genaim, Ratan Lal and Pavithra Prabhakar
From Non-Zenoness Verification to Termination (best paper award)
ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE), 2015
Ratan Lal and Pavithra Prabhakar
Bounded error flowpipe computation of parameterized linear systems
International Conference on Embedded Software (EMSOFT), 2015
| Course Name | Semester/Year | University |
|---|---|---|
| Formal Language and Theory (CIS-770) | Spring 2021 | Kansas State University |
| Analysis/Algorithms (CIS-775) | Fall 2019 | Kansas State University |
| Formal Language and Theory (CIS-770) | Spring 2019 | Kansas State University |
