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},
   pdf="http://wcl.cs.rpi.edu/papers/paul_phd_dissertation_new.pdf",
   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).} 
   }
   

1. Saswata Paul, Gul A. Agha, Stacy Patterson, and Carlos A. Varela. Eventual Consensus in Synod: Verification using a Failure-Aware Actor Model. Innovations in Systems and Software Engineering - A NASA Journal, 2022. Keyword(s): formal verification, Athena, distributed systems, distributed computing, air traffic management, consensus, actor model. Abstract:

   Successfully attaining consensus in the absence of a centralized coordinator is a fundamental problem in distributed multi-agent systems. We analyze progress in the Synod consensus protocol — which does not assume a unique leader — under the assumptions of asynchronous communication and potential agent failures. We identify a set of sufficient conditions under which it is possible to guarantee that a set of agents will eventually attain consensus using Synod. First, a subset of the agents must not permanently fail or exhibit Byzantine failure until consensus is reached, and second, at least one proposal must be eventually uninterrupted by higher-numbered proposals. To formally reason about agent failures, we introduce a failure-aware actor model (FAM). Using FAM, we model the identified conditions and provide a formal proof of eventual progress in Synod. Our proof has been mechanically verified using the Athena proof assistant and, to the best of our knowledge, it is the first machine-checked proof of eventual progress in Synod.

   
   

   @article{paul-isse-2022,
   author = {Saswata Paul and Gul A. Agha and Stacy Patterson and Carlos A. Varela},
   title = {Eventual Consensus in Synod: Verification using a Failure-Aware Actor Model},
   journal="Innovations in Systems and Software Engineering - A NASA Journal",
   year="2022",
   publisher="Springer Nature",
   address="Cham",
   pdf="http://wcl.cs.rpi.edu/papers/paul-ISSE-2022.pdf",
   doi="https://doi.org/10.1007/s11334-022-00463-5",
   keywords = {formal verification, Athena, distributed systems, distributed computing, air traffic management, consensus, actor model},
   abstract = {Successfully attaining consensus in the absence of a centralized coordinator is a fundamental problem in distributed multi-agent systems. We analyze progress in the Synod consensus protocol — which does not assume a unique leader — under the assumptions of asynchronous communication and potential agent failures. We identify a set of sufficient conditions under which it is possible to guarantee that a set of agents will eventually attain consensus using Synod. First, a subset of the agents must not permanently fail or exhibit Byzantine failure until consensus is reached, and second, at least one proposal must be eventually uninterrupted by higher-numbered proposals. To formally reason about agent failures, we introduce a failure-aware actor model (FAM). Using FAM, we model the identified conditions and provide a formal proof of eventual progress in Synod. Our proof has been mechanically verified using the Athena proof assistant and, to the best of our knowledge, it is the first machine-checked proof of eventual progress in Synod.} 
   }
   




2. Sida Chen, Shigeru Imai, Wennan Zhu, and Carlos A. Varela. Towards Learning Spatio-Temporal Data Stream Relationships for Failure Detection in Avionics, pages 103-127. Springer International Publishing, Cham, 2022. ISBN: 978-3-030-74568-4. Keyword(s): programming languages, data streaming, cyber physical systems. Abstract:

   Spatio-temporal data streams are often related in complex ways, for example, while the airspeed that an aircraft attains in cruise phase depends on the weight it carries, it also depends on many other factors. Some of these factors are controllable such as engine inputs or the airframe's angle of attack, while others contextual, such as air density, or turbulence. It is therefore critical to develop failure models that can help recognize errors in the data, such as an incorrect fuel quantity, a malfunctioning pitot-static system, or other abnormal flight conditions. In this paper, we extend our PILOTS programming language [1] to support machine learning techniques that will help data scientists: (1) create parameterized failure models from data and (2) continuously train a statistical model as new evidence (data) arrives. The linear regression approach learns parameters of a linear model to minimize least squares error for given training data. The Bayesian approach classifies operating modes according to supervised offline training and can discover new statistically significant modes online. As shown in Tuninter 1153 simulation result, dynamic Bayes classifier finds discrete error states on the fly while the error signatures approach requires every error state predefined. Using synthetic data, we compare the accuracy, response time, and adaptability of these machine learning techniques. Future dynamic data driven applications systems (DDDAS) using machine learning can identify complex dynamic data-driven failure models, which will in turn enable more accurate flight planning and control for emergency conditions.

   
   

   @Inbook{chen-springer-2022,
   author="Chen, Sida and Imai, Shigeru and Zhu, Wennan and Varela, Carlos A.",
   editor="Blasch, Erik P. and Darema, Frederica and Ravela, Sai and Aved, Alex J.",
   title="Towards Learning Spatio-Temporal Data Stream Relationships for Failure Detection in Avionics",
   bookTitle="Handbook of Dynamic Data Driven Applications Systems: Volume 1",
   year="2022",
   publisher="Springer International Publishing",
   address="Cham",
   pages="103--127",
   abstract="Spatio-temporal data streams are often related in complex ways, for example, while the airspeed that an aircraft attains in cruise phase depends on the weight it carries, it also depends on many other factors. Some of these factors are controllable such as engine inputs or the airframe's angle of attack, while others contextual, such as air density, or turbulence. It is therefore critical to develop failure models that can help recognize errors in the data, such as an incorrect fuel quantity, a malfunctioning pitot-static system, or other abnormal flight conditions. In this paper, we extend our PILOTS programming language [1] to support machine learning techniques that will help data scientists: (1) create parameterized failure models from data and (2) continuously train a statistical model as new evidence (data) arrives. The linear regression approach learns parameters of a linear model to minimize least squares error for given training data. The Bayesian approach classifies operating modes according to supervised offline training and can discover new statistically significant modes online. As shown in Tuninter 1153 simulation result, dynamic Bayes classifier finds discrete error states on the fly while the error signatures approach requires every error state predefined. Using synthetic data, we compare the accuracy, response time, and adaptability of these machine learning techniques. Future dynamic data driven applications systems (DDDAS) using machine learning can identify complex dynamic data-driven failure models, which will in turn enable more accurate flight planning and control for emergency conditions.",
   keywords = {programming languages, data streaming, cyber physical systems},
   isbn="978-3-030-74568-4",
   doi="10.1007/978-3-030-74568-4_5",
   url="https://doi.org/10.1007/978-3-030-74568-4_5" 
   }
   




3. Michael Giancola, Selmer Bringsjord, Naveen Sundar Govindarajulu, and Carlos Varela. Making Maximally Ethical Decisions via Cognitive Likelihood and Formal Planning, pages 127-142. Springer International Publishing, Cham, 2022. ISBN: 978-3-031-09823-9. Abstract:

   This chapter attempts to give an answer to the following question: Given an obligation and a set of potentially-inconsistent, ethically-charged beliefs, how can an artificially-intelligent agent ensure that its actions maximize the likelihood that the obligation is satisfied? Our approach to answering this question is in the intersection of several areas of research, including automated planning, reasoning with uncertainty, and argumentation. We exemplify our reasoning framework in a case study based on the famous, heroic ditching of US Airways Flight 1549, an event colloquially known as the ``Miracle on the Hudson.''

   
   

   @Inbook{Giancola2022,
   author="Giancola, Michael and Bringsjord, Selmer and Govindarajulu, Naveen Sundar and Varela, Carlos",
   editor="Ferreira, Maria Isabel Aldinhas and Tokhi, Mohammad Osman",
   title="Making Maximally Ethical Decisions via Cognitive Likelihood and Formal Planning",
   bookTitle="Towards Trustworthy Artificial Intelligent Systems",
   year="2022",
   publisher="Springer International Publishing",
   address="Cham",
   pages="127--142",
   abstract="This chapter attempts to give an answer to the following question: Given an obligation and a set of potentially-inconsistent, ethically-charged beliefs, how can an artificially-intelligent agent ensure that its actions maximize the likelihood that the obligation is satisfied? Our approach to answering this question is in the intersection of several areas of research, including automated planning, reasoning with uncertainty, and argumentation. We exemplify our reasoning framework in a case study based on the famous, heroic ditching of US Airways Flight 1549, an event colloquially known as the ``Miracle on the Hudson.''",
   isbn="978-3-031-09823-9",
   doi="10.1007/978-3-031-09823-9_10",
   url="https://doi.org/10.1007/978-3-031-09823-9_10" 
   }
   

1. Lorson Blair, Carlos A. Varela, and Stacy Patterson. A Continuum Approach for Collaborative Task Processing in UAV MEC Networks. In 2022 IEEE 15th International Conference on Cloud Computing (CLOUD), pages 247-256, 2022. Keyword(s): Edge Computing, Cloud Computing, Distributed Computing, Cyber Physical Systems. Abstract:

   Unmanned aerial vehicles (UAVs) are becoming a viable platform for sensing and estimation in a wide variety of applications including disaster response, search and rescue, and security monitoring. These sensing UAVs have limited battery and computational capabilities, and thus must offload their data so it can be processed to provide actionable intelligence. We consider a compute platform consisting of a limited number of highly-resourced UAVs that act as mobile edge computing (MEC) servers to process the workload on premises. We propose a novel distributed solution to the collaborative processing problem that adaptively positions the MEC UAVs in response to the changing workload that arises both from the sensing UAVs’ mobility and the task generation. Our solution consists of two key building blocks: (1) an efficient workload estimation process by which the UAVs estimate the task field—a continuous approximation of the number of tasks to be processed at each location in the airspace, and (2) a distributed optimization method by which the UAVs partition the task field so as to maximize the system throughput. We evaluate our proposed solution using realistic models of surveillance UAV mobility and show that our method achieves up to 28% improvement in throughput over a non-adaptive baseline approach.

   
   

   @INPROCEEDINGS{9861025,
   author={Blair, Lorson and Varela, Carlos A. and Patterson, Stacy},
   booktitle={2022 IEEE 15th International Conference on Cloud Computing (CLOUD)},
   title={A Continuum Approach for Collaborative Task Processing in UAV MEC Networks},
   year={2022},
   keywords={Edge Computing, Cloud Computing, Distributed Computing, Cyber Physical Systems},
   pdf="http://wcl.cs.rpi.edu/papers/IEEE_CLOUD_2022.pdf",
   volume={},
   number={},
   pages={247-256},
   doi={10.1109/CLOUD55607.2022.00046},
   abstract={Unmanned aerial vehicles (UAVs) are becoming a viable platform for sensing and estimation in a wide variety of applications including disaster response, search and rescue, and security monitoring. These sensing UAVs have limited battery and computational capabilities, and thus must offload their data so it can be processed to provide actionable intelligence. We consider a compute platform consisting of a limited number of highly-resourced UAVs that act as mobile edge computing (MEC) servers to process the workload on premises. We propose a novel distributed solution to the collaborative processing problem that adaptively positions the MEC UAVs in response to the changing workload that arises both from the sensing UAVs’ mobility and the task generation. Our solution consists of two key building blocks: (1) an efficient workload estimation process by which the UAVs estimate the task field—a continuous approximation of the number of tasks to be processed at each location in the airspace, and (2) a distributed optimization method by which the UAVs partition the task field so as to maximize the system throughput. We evaluate our proposed solution using realistic models of surveillance UAV mobility and show that our method achieves up to 28% improvement in throughput over a non-adaptive baseline approach.} 
   }
   

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.

This document was translated from BibT_EX by bibtex2html