RESEARCH

In control theory, complicated dynamics such as systems of (nonlinear) differential equations are mostly controlled to achieve stability and to optimize a cost. In the area of formal methods in computer science, simple systems such as finite state transition graphs modeling computer programs and digital circuits are verified and controlled from specifications such as safety, liveness, or richer requirements expressed as formulas of temporal logics. Our group bridges the gaps among control theory, formal methods, and machine learning to develop verification and control synthesis tools for safety-critical cyber physical and data-driven systems. We use our algorithms to solve challenging problems in robotics and biology.

Safe, Interpretable, and Composable Reinforcement Learning

Growing interest in reinforcement learning approaches to robotic planning and control raises concerns of predictability and safety of robot behaviors realized solely through learned control policies. In addition, formally defining reward functions for complex tasks is challenging, and faulty rewards are prone to exploitation by the learning agent. We develop formal methods approaches to reinforcement learning that provide (1) formal specification languages that integrate high-level, rich, task specifications with a priori, domain-specific knowledge; (2) make the reward generation process easily interpretable; (3) guide the policy generation process according to the specification; and (4) guarantee the satisfaction of the (critical) safety component of the specification.

Wenliang Liu, Mirai Duintjer Tebbens Nishioka, Calin Belta, Safe Model-based Control from Signal Temporal Logic Specifications Using Recurrent Neural Networks, IEEE International Conference on Robotics and Automation (ICRA), 2023 (pdf)

Xiao Li, Zachary Serlin, Guang Yang, Calin Belta, A Formal Methods Approach to Interpretable Reinforcement Learning for Robotic Planning, Science: Robotics, vol. 4, issue 37, 2019 (pdf)

Formal Methods to Comply with Rules of the Road in Autonomous Driving

Autonomous vehicles (AV) should follow complex and possibly conflicting traffic laws with different priorities. They should also meet cultural expectations of reasonable driving behavior. For example, an AV has to avoid collisions with other road users (higher priority), maintain longitudinal clearance with the lead car (lower priority), and drive faster than the minimum speed limit (still lower priority). We formulate these behavior specifications as sets of rules with priority structures that capture their importance. We use predicate Boolean and temporal logics to formalize the rules. Both rules and priority structures are constructed manually or learned from traffic data. We formulate AV control problems as optimal control problems, in which the satisfaction of the rules and some vehicle limitations are enforced by Control Barrier Functions (CBF), and convergence to desired states is achieved through Control Lyapunov Functions. We also investigate hierarchical, receding-horizon control architectures.

Wei Xiao, Noushin Mehdipour, Anne Collin, Amitai Bin-Nun, Emilio Frazzoli, Radboud Tebbens and Calin Belta, Rule-based Optimal Control for Autonomous Driving, 12^th ACM/IEEE International Conference on Cyber-Physical Systems (ICCPS), 2021 (pdf)

Erfan Aasi, Cristian Ioan Vasile, Calin Belta, A Control Architecture for Provably-Correct Autonomous Driving, American Control Conference (ACC), New Orleans, Louisiana, 2021 (pdf)

Formal Methods for Motion Planning and Control

We have been creating computational frameworks for automatic synthesis of provably correct motion plans and control strategies from user-friendly specifications resembling temporal logics. We have developed such techniques for deterministic, non-deterministic, and probabilistic robot models. We developed abstractions techniques to map realistic, continuous robotic models to finite representations, which enabled formal analysis and synthesis for most used continuous-space robot models. For robotic systems with large configurations spaces, we have also employed sampling and mixed-integer encodings. We showed that such approaches are also feasible for robotic teams. We have implemented such computational frameworks in several experimental setups consisting of both ground and air vehicles. This work has been funded by NSF, AFOSR, ARO, and ONR.

Calin Belta, Boyan Yordanov, and Ebru Aydin Gol, Formal Methods for Discrete-Time Dynamical Systems, Springer, 2017 (link)

Safety-Critical Control

Optimal control of autonomous systems is a fundamental and challenging problem, especially when many stringent safety constraints and tight control limitations are involved. It has been shown that optimizing quadratic costs while stabilizing an affine control system to a desired (sets of) states subject to state and control constraints can be reduced to a sequence of Quadratic Programs (QPs) by using Control Barrier Functions (CBFs) and Control Lyapunov Functions (CLFs). Although computationally efficient, this method is limited by several factors, which we have been addressing during the past four years. We have extended CBFs to high order CBFs (HOCBFs) that can accommodate arbitrary relative degree systems and constraints. We have also proposed analytical methods to derive sufficient conditions that guarantee the QP feasibility. For complex safety constraints, we developed machine learning techniques to learn HOCBF feasibility constraints. When time-varying control bounds and noisy dynamics are involved, we proposed adaptive CBFs. For uncertain systems, we have developed data-driven approaches that ensure safety by extending techniques from adaptive control.

Wei Xiao, Christos G. Cassandras, and Calin Belta, Safe Autonomy with Control Barrier Functions: Theory and Applications, Springer, 2023 (link)

Max H. Cohen, Calin Belta, Adaptive and Learning-based Control of Safety-Critical Systems, Springer, 2023 (link)

Interpretable Classification of Temporal Data using Temporal Logics

Anomaly detection and mitigation are important problems that find applications in various areas including surveillance, power networks, automotive industry, and biology. We have proposed a formal methods approach to this problem. In short, in our approach, the classifiers are temporal logic formulas that have quantitative semantics. This enables efficient learning of classifiers from data and monitoring of satisfaction. We proposed supervised and unsupervised versions of this machine learning problem. Funded by ONR and DENSO Japan, we worked on applications involving maritime surveillance and monitoring of automotive parts. With funding from NSF, we are currently extending these methods. Recent results include the use of boosted decision trees and neural networks for classification, and frameworks allowing for simultaneous classification and prediction of satisfaction of the classifiers.

Giuseppe Bombara, Calin Belta, Offline and Online Learning of Signal Temporal Logic Formulae Using Decision Trees, ACM Transactions on Cyber-Physical Systems, vol. 5, no. 3, pp. 1-23, 2021 (pdf)

Erfan Aasi, Cristian Ioan Vasile, Mahroo Bahreinian, Calin Belta, Classification of Time-Series Data Using Boosted Decision Trees,IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS), Kyoto, Japan, 2022 (pdf)

Classification and Synthesis of Spatio-Temporal Patterns

Achieving desired global behavior in networks of locally interacting entities is a fundamental problem with applications in various areas such as robotics (swarming), power networks, and biological networks. By using tools from geometric control theory and formal methods, we are developing top-down approaches allowing for synthesis of local communication and control strategies from global, rich specifications. We have applied such techniques for swarms of mobile robots. As part of an NSF STC and an NSF CPS Frontier project, we have been developing such approaches for populations of engineered bacterial and mammalian cells. The latter project involves the design and fabrication of a robotic system that interacts with cell cultures to optimize the formation of desired global structures. With funding from started an NIH R01 and an NSF GCR, we are currently developing novel spatio-temporal logics for specifying temporal sequences of patterns, and algorithms to learn such formulas from data. We are developing algorithms in which system parameters, experimental protocols, and micro robot interventions can be automatically derived by solving optimization problems.

Ashley RG Libby, Demarcus Briers, Iman Haghighi, David A. Joy, Bruce R. Conklin, Calin Belta, Todd C. McDevitt, Automated Design of Pluripotent Stem Cell Self-Organization, Cell Systems, vol. 9, pp.1-13, 2019 (pdf)

Suhail Alsalehi, Erfan Aasi, Ron Weiss, Calin Belta, Learning Spatio-Temporal Specifications for Dynamical Systems, Proceedings of the 4th Annual Learning for Dynamics and Control Conference (L4DC) 2022, in Proceedings of Machine Learning Research, vol. 168, pp. 968-980, 2022 (pdf)

Analysis and Control of Biological Systems

In biology, we have developed computational tools for analysis and control of two types of networks: (very large) genome-scale metabolic networks and (very small) synthetic gene networks. For the first, we studied metabolite essentiality and characterized minimal nutrient sets and cut sets (i.e., sets of gene deletions that you kill a cell). For the second, we have used formal methods and control theory to verify, design, and control synthetic gene networks. As part of large collaborative projects, we have also been working on establishing a connection between the seemingly unrelated areas of robotics and biology. We used synthetic biology to equip micron-scale robots with sensing, communication, and decision making capabilities, and used them to affect the evolution of populations of mammalian stem cells, with the goal of differentiating them into desired tissue. Very recently, we have been working on combining machine learning, optimization, and synthetic biology to design feedback controllers that can achieve rich neural network function.

M. Imielinski and C. Belta, Exploiting the pathway structure of metabolism to reveal high-order epistasis, BMC Systems Biology, 2:40, 2008 (pdf)