| Popis: |
As autonomous systems become more widely used in society, they will necessarily have to make more decisions in order to meet increasingly complex objectives. However, to facilitate greater deployment of autonomous systems, especially in safety-critical contexts, it is crucial to provide guarantees that the decisions made by these systems will be safe and achieve the desired objective. This dissertation studies techniques for assuring decision-making in complex and large-scale autonomous systems. The dissertation uses synthesis techniques from the fields of formal methods to provide guarantees of correctness with respect to specifications provided in temporal logic. Synthesis methods often suffer from scalability issues limiting their applicability in realistic systems. To address this issue, the dissertation provides abstraction methods and decentralized synthesis architectures to provide guarantees in systems with partial-information as well as large numbers of interacting agents. The dissertation provides a systematic approach to assured decision-making in this dissertation that is agnostic to the specifics of the implementation details of the autonomous systems. Such an approach avoids having to assure systems case-by-case and will facilitate certification and deployment of autonomous systems in more application areas. Finally, the dissertation illustrates this concept in traffic management for urban air mobility operations and provide a synthesis architecture that can adapt to changing specifications or vehicle capabilities. |
