
Saswata Paul.
Formal Verification of Decentralized Coordination in Autonomous MultiAgent 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 selfdriving cars and uncrewed aircraft systems (UAS) evolve to become more accessible and costefficient, autonomous multiagent 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 multiagent coordination to ensure safe operations. In this thesis, we adopt a formal methodsbased approach to investigate multiagent coordination for safetycritical autonomous multiagent systems. We explore algorithms that can be used for decentralized multiagent coordination among autonomous mobile agents by communicating over asynchronous vehicletovehicle (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 multiagent systems. We develop the first machinechecked 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 FailureAware Actor Model (FAM). We then propose a formally verified TwoPhase Acknowledge Protocol (TAP) for knowledge propagation that can establish a safe state of knowledge suitable for autonomous vehicular operations. The nondeterministic 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 DataDriven 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 multiaircraft systems called Decentralized Admission Control (DAC). 
@PhdThesis{paulphd2022,
author = {Saswata Paul},
title = {Formal Verification of Decentralized Coordination in Autonomous MultiAgent 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 selfdriving cars and uncrewed aircraft systems (UAS) evolve to become more accessible and costefficient, autonomous multiagent 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 multiagent coordination to ensure safe operations. In this thesis, we adopt a formal methodsbased approach to investigate multiagent coordination for safetycritical autonomous multiagent systems. We explore algorithms that can be used for decentralized multiagent coordination among autonomous mobile agents by communicating over asynchronous vehicletovehicle (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 multiagent systems. We develop the first machinechecked 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 FailureAware Actor Model (FAM). We then propose a formally verified TwoPhase Acknowledge Protocol (TAP) for knowledge propagation that can establish a safe state of knowledge suitable for autonomous vehicular operations. The nondeterministic 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 DataDriven 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 multiaircraft systems called Decentralized Admission Control (DAC).}
}

Elkin CruzCamacho,
Ahmad Amer,
Fotis Kopsaftopoulos,
and Carlos A. Varela.
Formal Safety Envelopes for Provably Accurate State Classification by DataDriven Flight Models.
Journal of Aerospace Information Systems,
2022.
Keyword(s): Formal verification,
Agda,
Safety envelopes,
Runtime verification,
dddas.
Abstract:
We present a novel approach to formally verify datadriven models for state classification in the domain of aerospace. Dynamic datadriven application systems (DDDAS) extend firstprinciples models with dynamically sensed data enabling the diagnosis and healing of aircrafts during flight. The intrinsic complexity of these systems makes them prone to spurious errors caused by unseen conditions. Formal (software) verification is a technique that goes beyond unit testing or statistical model checking, which can only guarantee system correctness over a fraction of the system's input space. {\em Safety envelopes} bound regions of the system's input space where a formal proof of correctness of state classification holds. We focus on two questions for defining safety envelope boundaries: ({\em i}) does the data follow the model? and ({\em ii}) what is the most likely state of the system given the data? We evaluate safety envelopes with data derived from a wind tunnel experiment tackling the problem of stall detection given piezoelectric sensor measurements over a wing's skin. We define tailored metrics to show the quality of different datadriven models. We encode safety envelopes in the proof assistant Agda, and illustrate their applicability across a variety of input dimensions and Gaussian Process Regression Model (GPRM)generated data. 
@article{cruzjais2022,
author = {Elkin CruzCamacho and Ahmad Amer and Fotis Kopsaftopoulos and Carlos A. Varela},
title = {Formal Safety Envelopes for Provably Accurate State Classification by DataDriven Flight Models},
journal={Journal of Aerospace Information Systems},
year={2022},
publisher={American Institute of Aeronautics and Astronautics},
doi="https://doi.org/10.2514/1.I011073" pdf="http://wcl.cs.rpi.edu/papers/cruzjais2022.pdf",
keywords = {Formal verification, Agda, Safety envelopes, Runtime verification, dddas},
abstract = {We present a novel approach to formally verify datadriven models for state classification in the domain of aerospace. Dynamic datadriven application systems (DDDAS) extend firstprinciples models with dynamically sensed data enabling the diagnosis and healing of aircrafts during flight. The intrinsic complexity of these systems makes them prone to spurious errors caused by unseen conditions. Formal (software) verification is a technique that goes beyond unit testing or statistical model checking, which can only guarantee system correctness over a fraction of the system's input space. {\em Safety envelopes} bound regions of the system's input space where a formal proof of correctness of state classification holds. We focus on two questions for defining safety envelope boundaries: ({\em i}) does the data follow the model? and ({\em ii}) what is the most likely state of the system given the data? We evaluate safety envelopes with data derived from a wind tunnel experiment tackling the problem of stall detection given piezoelectric sensor measurements over a wing's skin. We define tailored metrics to show the quality of different datadriven models. We encode safety envelopes in the proof assistant Agda, and illustrate their applicability across a variety of input dimensions and Gaussian Process Regression Model (GPRM)generated data.}
}

Saswata Paul,
Gul A. Agha,
Stacy Patterson,
and Carlos A. Varela.
Eventual Consensus in Synod: Verification using a FailureAware 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 multiagent 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 highernumbered proposals. To formally reason about agent failures, we introduce a failureaware 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 machinechecked proof of eventual progress in Synod. 
@article{paulisse2022,
author = {Saswata Paul and Gul A. Agha and Stacy Patterson and Carlos A. Varela},
title = {Eventual Consensus in Synod: Verification using a FailureAware 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/paulISSE2022.pdf",
doi="https://doi.org/10.1007/s11334022004635",
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 multiagent 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 highernumbered proposals. To formally reason about agent failures, we introduce a failureaware 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 machinechecked proof of eventual progress in Synod.}
}

Michael Giancola,
Selmer Bringsjord,
Naveen Sundar Govindarajulu,
and Carlos Varela.
Making Maximally Ethical Decisions via Cognitive Likelihood and Formal Planning,
pages 127142.
Springer International Publishing,
Cham,
2022.
ISBN: 9783031098239.
Abstract:
This chapter attempts to give an answer to the following question: Given an obligation and a set of potentiallyinconsistent, ethicallycharged beliefs, how can an artificiallyintelligent 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="127142",
abstract="This chapter attempts to give an answer to the following question: Given an obligation and a set of potentiallyinconsistent, ethicallycharged beliefs, how can an artificiallyintelligent 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="9783031098239",
doi="10.1007/9783031098239_10",
url="https://doi.org/10.1007/9783031098239_10"
}

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 247256,
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 highlyresourced 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 nonadaptive 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={247256},
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 highlyresourced 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 nonadaptive baseline approach.}
}

Peiyuan Zhou,
Saswata Paul,
Airin Dutta,
Carlos Varela,
and Fotis Kopsaftopoulos.
On formal verification of datadriven flight awareness: Leveraging the CramérRao lower bound of stochastic functional time series models.
In ,
2022.
Abstract:
This work investigates applying critically verified CramerRao Lower Bound theorem, within the framework of Dynamic Data Driven Applications Systems (DDDAS), on a stochastic Vectordependent Functionally Pooled AutoRegressive (VFPAR) model. (i) The VFPAR model is identified via data obtained from wind tunnel experiments on a “flybyfeel” wing structure under multiple flight states (i.e. angle of attack, velocity). (ii) CRLB is estimated at each true flight state reflecting the state estimation capability of the model. At the estimated flight states, corresponding CRLBs are given by testing data segment. (iii) Apart from the CRLB given by pristine data and model, CRLBs are estimated using either artificially corrupted testing data or suboptimal models. Comparisons are made between CRLB and state estimations from corrupted and pristine conditions. (iv) The effect of corrupted data and degraded model is evaluated regarding the mechanically verified formal proof of the CramerRao Lower Bound (CRLB) Theorem using Athena, which provides irrefutable guarantee of soundness as long as specified assumptions are followed. The results of the study indicate the potential of using a CRLBbased formal verification framework for state estimation via stochastic FP time series models 
@INPROCEEDINGS{DDDAS2022_Zhou_etal,
author={Zhou, Peiyuan and Paul, Saswata and Dutta, Airin and Varela, Carlos and Kopsaftopoulos, Fotis},
title={On formal verification of datadriven flight awareness: Leveraging the CramérRao lower bound of stochastic functional time series models},
year={2022},
keywods={AR models, CRLB, flybyfeel, state awareness.},
pdf={http://wcl.cs.rpi.edu/papers/DDDAS2022_Zhou_etal.pdf},
abstract={This work investigates applying critically verified CramerRao Lower Bound theorem, within the framework of Dynamic Data Driven Applications Systems (DDDAS), on a stochastic Vectordependent Functionally Pooled AutoRegressive (VFPAR) model. (i) The VFPAR model is identified via data obtained from wind tunnel experiments on a “flybyfeel” wing structure under multiple flight states (i.e. angle of attack, velocity). (ii) CRLB is estimated at each true flight state reflecting the state estimation capability of the model. At the estimated flight states, corresponding CRLBs are given by testing data segment. (iii) Apart from the CRLB given by pristine data and model, CRLBs are estimated using either artificially corrupted testing data or suboptimal models. Comparisons are made between CRLB and state estimations from corrupted and pristine conditions. (iv) The effect of corrupted data and degraded model is evaluated regarding the mechanically verified formal proof of the CramerRao Lower Bound (CRLB) Theorem using Athena, which provides irrefutable guarantee of soundness as long as specified assumptions are followed. The results of the study indicate the potential of using a CRLBbased formal verification framework for state estimation via stochastic FP time series models}
}