Automated Control of Cyber-Physical Systems
In the near future, we expect to see fully autonomous vehicles, aircrafts, robots, and software, all of which should be able to make their own decisions without direct human involvement. Although this technology theme provides many potential advantages, e.g., fewer traffic collisions, reduced traffic congestion, increased roadway capacity, and relief of vehicle occupants from driving, guaranteeing safety and reliability of such systems in a formal as well as time- and cost-effective way is the main challenge in the study of those complex systems. With my PhD thesis “Automated Verification and Control of Large-Scale Stochastic Cyber-Physical Systems: Compositional Techniques”, I contributed to the corresponding potential challenges.
According to a report done by University of Texas in 2013, if only 10% of the cars on U.S. roads were autonomous, more than $37 billion of savings could be achieved via less wasted time and fuel, as well as fewer injuries and deaths. At 90%, the benefit goes over $450 billion a year. Similar proportionalized savings are also expected in Germany and China. Over the past one decade, a number of advances has been made in developing various techniques for autonomous vehicles, especially in the areas of perception, planning, and control.
Those techniques have relied on methods from artificial intelligence (AI), machine learning, and control theory. While, at least in relatively controlled environments, autonomous vehicles have been demonstrated to be functioning, they are still not ready to be deployed for regular use. One stumbling block in their deployment is the lack of any guarantee of correctness. In other words, even if such vehicles are extensively tested in varied environments, there is no guarantee that something unforeseen would not happen in a new environment. This in turn opens up several unanswered questions related to liability in the case of accidents or other unforeseen events. While one may, in the unlikely case, even be able to design provably correct methods for navigation and control in specific scenarios, the moment either the scenario or the specifications of correctness change, a completely new design will be required (along with the associated proof of correctness).
My Ph.D. dissertation studies the challenges arising in the automated analysis and synthesis of large-scale stochastic cyber-physical systems. Towards this, my thesis relies on formal techniques that do not require any costly and exhaustive post facto verification and validation, which are necessary for current controllers. Since the algorithmic complexity of automated controller synthesis in a centralized fashion grows exponentially with the number of components, my thesis provides novel compositional techniques to analyze and control complex stochastic CPSs in an automated as well as formal fashion.
by Abolfazl Lavaei