1. Saswata Paul, Chris McCarthy, Stacy Patterson, and Carlos Varela. Formal verification of timely knowledge propagation in airborne networks. Science of Computer Programming, 239, 2025. ISSN: 0167-6423. Keyword(s): Formal methods, Distributed systems, Autonomous systems, Probabilistic properties, Theorem proving, Proof library. Abstract:

   Ensuring timely coordination between autonomous aircraft is a challenging problem in decentralized air traffic management (ATM) applications for urban air mobility (UAM) scenarios. This paper presents an approach for formally guaranteeing timely progress in a Two-Phase Acknowledge distributed knowledge propagation protocol by probabilistically modeling the delays using the theory of the Multicopy Two-Hop Relay protocol and the M/M/1 queue system. The guarantee states a probabilistic upper bound to the time for progress as a function of the probabilities of the total transmission and processing delays following two specific distributions. The proof uses a general library of formal theories, that can be used for the rigorous mechanical verification of autonomous aircraft coordination protocols using the Athena proof checker and assistant.

   
   

   @article{PAUL2025103184,
   title = {Formal verification of timely knowledge propagation in airborne networks},
   journal = {Science of Computer Programming},
   volume = {239},
   year = {2025},
   issn = {0167-6423},
   doi = {https://doi.org/10.1016/j.scico.2024.103184},
   url = {https://www.sciencedirect.com/science/article/pii/S0167642324001072},
   author = {Saswata Paul and Chris McCarthy and Stacy Patterson and Carlos Varela},
   keywords = {Formal methods, Distributed systems, Autonomous systems, Probabilistic properties, Theorem proving, Proof library},
   abstract = {Ensuring timely coordination between autonomous aircraft is a challenging problem in decentralized air traffic management (ATM) applications for urban air mobility (UAM) scenarios. This paper presents an approach for formally guaranteeing timely progress in a Two-Phase Acknowledge distributed knowledge propagation protocol by probabilistically modeling the delays using the theory of the Multicopy Two-Hop Relay protocol and the M/M/1 queue system. The guarantee states a probabilistic upper bound to the time for progress as a function of the probabilities of the total transmission and processing delays following two specific distributions. The proof uses a general library of formal theories, that can be used for the rigorous mechanical verification of autonomous aircraft coordination protocols using the Athena proof checker and assistant.} pdf = "http://wcl.cs.rpi.edu/papers/paul_SCP_2024.pdf",
   
   }
   

1. Dylan Le. Exploring Formal Methods for Provably Safe Autonomous Cyber-Physical Systems. Master's thesis, Rensselaer Polytechnic Institute, May 2025. Keyword(s): autonomous systems, cyber-physical systems, formal methods, model checking, theorem proving. Abstract:

   The increasing complexity of autonomous cyber-physical systems (CPS) necessitates rigorous verification techniques to ensure safety and reliability. Safety-critical systems, such as those in aerospace, automotive, and medical domains, operate under strict constraints where failures can have catastrophic consequences. Modelling autonomous CPS as a hybrid system allows for verification of safety properties. Current verification methods, including model checking and Satisfiability Modulo Theories (SMT) solvers, face scalability challenges when dealing with large state spaces and complex non-linear dynamics. This thesis investigates theorem proving as a means to provide more scalable and explainable safety guarantees for cyber-physical systems. As a case study, we analyze the Mountain Car problem. We develop a discrete and continuous model for the dynamics. In this thesis we provide a formal proof using theorem proving and physical properties that shows that a simple controller for Mountain Car, under specific conjectures, ensures it reaches the goal position from any valid initial condition and without a finite time bound for verification. The findings of this thesis highlight the potential for theorem proving to enhance the explainability and scalability of safety verification in autonomous cyber-physical systems.

   
   

   @MastersThesis{led2_thesis,
   author = {Dylan Le},
   title = {Exploring Formal Methods for Provably Safe Autonomous Cyber-Physical Systems},
   school = {Rensselaer Polytechnic Institute},
   year = 2025,
   month = {May},
   pdf = "http://wcl.cs.rpi.edu/theses/led2_thesis.pdf",
   keywords = "autonomous systems, cyber-physical systems, formal methods, model checking, theorem proving",
   abstract = {The increasing complexity of autonomous cyber-physical systems (CPS) necessitates rigorous verification techniques to ensure safety and reliability. Safety-critical systems, such as those in aerospace, automotive, and medical domains, operate under strict constraints where failures can have catastrophic consequences. Modelling autonomous CPS as a hybrid system allows for verification of safety properties. Current verification methods, including model checking and Satisfiability Modulo Theories (SMT) solvers, face scalability challenges when dealing with large state spaces and complex non-linear dynamics. This thesis investigates theorem proving as a means to provide more scalable and explainable safety guarantees for cyber-physical systems. As a case study, we analyze the Mountain Car problem. We develop a discrete and continuous model for the dynamics. In this thesis we provide a formal proof using theorem proving and physical properties that shows that a simple controller for Mountain Car, under specific conjectures, ensures it reaches the goal position from any valid initial condition and without a finite time bound for verification. The findings of this thesis highlight the potential for theorem proving to enhance the explainability and scalability of safety verification in autonomous cyber-physical systems.} 
   }
   

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