BACK TO INDEX

Publications of year 2022
Thesis
  1. Saswata Paul. Formal Verification of Decentralized Coordination in Autonomous Multi-Agent Aerospace Systems. PhD thesis, Rensselaer Polytechnic Institute, 2022. Keyword(s): formal verification, Athena, distributed systems, distributed computing, air traffic management, autonomous systems, runtime verification, cyber physical systems.
    Abstract:
    As autonomous vehicular technologies such as self-driving cars and uncrewed aircraft systems (UAS) evolve to become more accessible and cost-efficient, autonomous multi-agent systems, that comprise of such entities, will become ubiquitous in the near future. The close operational proximity between such autonomous agents will warrant the need for multi-agent coordination to ensure safe operations. In this thesis, we adopt a formal methods-based approach to investigate multi-agent coordination for safety-critical autonomous multi-agent systems. We explore algorithms that can be used for decentralized multi-agent coordination among autonomous mobile agents by communicating over asynchronous vehicle-to-vehicle (V2V) networks that can be prone to agent failures. In particular, we study two types of distributed algorithms that are useful for decentralized coordination — consensus, which can be used by autonomous agents to agree on a set of compatible operations; and knowledge propagation, which can be used to ensure sufficient situational awareness in autonomous multi-agent systems. We develop the first machine-checked proof of eventual progress for the Synod consensus algorithm, that does not assume a unique leader. To consider agent failures while reasoning about progress, we introduce a novel Failure-Aware Actor Model (FAM). We then propose a formally verified Two-Phase Acknowledge Protocol (TAP) for knowledge propagation that can establish a safe state of knowledge suitable for autonomous vehicular operations. The non-deterministic and dynamic operating conditions of distributed algorithms deployed over asynchronous V2V networks make it challenging to provide appropriate formal guarantees for the algorithms. To address this, we introduce probabilistic correctness properties that can be developed by stochastically modeling the systems. We present a formal proof library that can be used for reasoning about probabilistic properties of distributed algorithms deployed over V2V networks. We also propose a Dynamic Data-Driven Applications Systems (DDDAS)-based approach for the runtime verification of distributed algorithms. This approach uses parameterized proofs, which can be instantiated at runtime, and progress envelopes, which can divide the operational state space into distinct regions where a proof of progress may or may not hold. To motivate our verification of decentralized coordination, we introduce an autonomous air traffic management (ATM) technique for multi-aircraft systems called Decentralized Admission Control (DAC).

    @PhdThesis{paul-phd-2022,
    author = {Saswata Paul},
    title = {Formal Verification of Decentralized Coordination in Autonomous Multi-Agent Aerospace Systems},
    school = {Rensselaer Polytechnic Institute},
    year = 2022,
    keywords = {formal verification, Athena, distributed systems, distributed computing, air traffic management, autonomous systems, runtime verification, cyber physical systems},
    abstract = {As autonomous vehicular technologies such as self-driving cars and uncrewed aircraft systems (UAS) evolve to become more accessible and cost-efficient, autonomous multi-agent systems, that comprise of such entities, will become ubiquitous in the near future. The close operational proximity between such autonomous agents will warrant the need for multi-agent coordination to ensure safe operations. In this thesis, we adopt a formal methods-based approach to investigate multi-agent coordination for safety-critical autonomous multi-agent systems. We explore algorithms that can be used for decentralized multi-agent coordination among autonomous mobile agents by communicating over asynchronous vehicle-to-vehicle (V2V) networks that can be prone to agent failures. In particular, we study two types of distributed algorithms that are useful for decentralized coordination — consensus, which can be used by autonomous agents to agree on a set of compatible operations; and knowledge propagation, which can be used to ensure sufficient situational awareness in autonomous multi-agent systems. We develop the first machine-checked proof of eventual progress for the Synod consensus algorithm, that does not assume a unique leader. To consider agent failures while reasoning about progress, we introduce a novel Failure-Aware Actor Model (FAM). We then propose a formally verified Two-Phase Acknowledge Protocol (TAP) for knowledge propagation that can establish a safe state of knowledge suitable for autonomous vehicular operations. The non-deterministic and dynamic operating conditions of distributed algorithms deployed over asynchronous V2V networks make it challenging to provide appropriate formal guarantees for the algorithms. To address this, we introduce probabilistic correctness properties that can be developed by stochastically modeling the systems. We present a formal proof library that can be used for reasoning about probabilistic properties of distributed algorithms deployed over V2V networks. We also propose a Dynamic Data-Driven Applications Systems (DDDAS)-based approach for the runtime verification of distributed algorithms. This approach uses parameterized proofs, which can be instantiated at runtime, and progress envelopes, which can divide the operational state space into distinct regions where a proof of progress may or may not hold. To motivate our verification of decentralized coordination, we introduce an autonomous air traffic management (ATM) technique for multi-aircraft systems called Decentralized Admission Control (DAC).} 
    }
    



BACK TO INDEX




Disclaimer:

This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All person copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. In most cases, these works may not be reposted without the explicit permission of the copyright holder.

Les documents contenus dans ces répertoires sont rendus disponibles par les auteurs qui y ont contribué en vue d'assurer la diffusion à temps de travaux savants et techniques sur une base non-commerciale. Les droits de copie et autres droits sont gardés par les auteurs et par les détenteurs du copyright, en dépit du fait qu'ils présentent ici leurs travaux sous forme électronique. Les personnes copiant ces informations doivent adhérer aux termes et contraintes couverts par le copyright de chaque auteur. Ces travaux ne peuvent pas être rendus disponibles ailleurs sans la permission explicite du détenteur du copyright.




Last modified: Mon Apr 25 14:28:21 2022
Author: pauls4.


This document was translated from BibTEX by bibtex2html