Automated Verification and Control of Large-Scale Stochastic Cyber-Physical Systems: Compositional Techniques
Abolfazl Lavaei · 2019
This dissertation provides novel compositional techniques to analyze and control large-scale stochastic CPSs in an automated as well as formal fashion with three different compositional techniques including classic small-gain, max small-gain and dissipativity approaches. We also develop a software tool, called AMYTISS, in C++/OpenCL that provides scalable parallel algorithms for (i) constructing finite abstractions and (ii) synthesizing controllers automatically that satisfy complex logic properties including safety, reachability, and reach-avoid specifications.