SearcharxivSearch

arXiv subjects

Mahmoud Elfar

Publications and source records attributed to Mahmoud Elfar.

4 recordsLinked to original sources

Correct-by-Construction Vision-based Pose Estimation using Geometric Generative Models

We consider the problem of vision-based pose estimation for autonomous systems. While deep neural networks have been successfully used for vision-based tasks, they inherently lack provable guarantees on the correctness of their output, which is crucial for safety-critical applications. We present a framework for designing certifiable neural networks (NNs) for perception-based pose estimation that integrates physics-driven modeling with learning-based estimation. The proposed framework begins by leveraging the known geometry of planar objects commonly found in the environment, such as traffic signs and runway markings, referred to as target objects. At its core, it introduces a geometric generative model (GGM), a neural-network-like model whose parameters are derived from the image formation process of a target object observed by a camera. Once designed, the GGM can be used to train NN-based pose estimators with certified guarantees in terms of their estimation errors. We first demonstrate this framework in uncluttered environments, where the target object is the only object present in the camera's field of view. We extend this using ideas from NN reachability analysis to design certified object NN that can detect the presence of the target object in cluttered environments. Subsequently, the framework consolidates the certified object detector with the certified pose estimator to design a multi-stage perception pipeline that generalizes the proposed approach to cluttered environments, while maintaining its certified guarantees. We evaluate the proposed framework using both synthetic and real images of various planar objects commonly encountered by autonomous vehicles. Using images captured by an event-based camera, we show that the trained encoder can effectively estimate the pose of a traffic sign in accordance with the certified bound provided by the framework.

cs.RO

Certified Learning-Enabled Noise-Aware Motion Planning for Urban Air Mobility

Urban Air Mobility (UAM) has emerged as a promising solution to alleviate urban congestion and transportation challenges. Nevertheless, the noise generated by eVTOL aircrafts poses a significant barrier to public acceptance and regulatory approval, potentially limiting the operational scope and scalability of UAM systems. Hence, the successful adoption of UAM systems hinges on the ability to predict generated noise levels, and further develop motion planning strategies that comply with community-level noise regulations while maintaining operational efficiency. To this end, this paper proposes a novel noise-aware motion planning framework for UAM systems that ensures compliance with noise regulations. We first develop a certifiable neural network model to accurately predict eVTOL noise propagation patterns in urban environments, providing provable bounds on its correctness. To achieve a desired level of accuracy, we propose an active sampling strategy to efficiently build the dataset used to train and test the noise model. Next, we develop a noise-aware motion planning algorithm that utilizes the noise model to generate eVTOL trajectories that guarantee compliance with community noise regulations. The algorithm exploits the monotonic structure of the noise model to efficiently sample the configuration space, ensuring that the generated trajectories are both noise-compliant and operationally efficient. We demonstrate the effectiveness of the proposed framework through a number of experiments for Vahana eVTOLs. The results show that the framework can generate noise-compliant flight plans for a fleet of eVTOLs that adhere to community noise regulations while optimizing operational efficiency.

eess.SY

Context-Aware Temporal Logic for Probabilistic Systems

In this paper, we introduce the context-aware probabilistic temporal logic (CAPTL) that provides an intuitive way to formalize system requirements by a set of PCTL objectives with a context-based priority structure. We formally present the syntax and semantics of CAPTL and propose a synthesis algorithm for CAPTL requirements. We also implement the algorithm based on the PRISM-games model checker. Finally, we demonstrate the usage of CAPTL on two case studies: a robotic task planning problem, and synthesizing error-resilient scheduler for micro-electrode-dot-array digital microfluidic biochips.

cs.LO

Security-Aware Synthesis Using Delayed-Action Games

Stochastic multiplayer games (SMGs) have gained attention in the field of strategy synthesis for multi-agent reactive systems. However, standard SMGs are limited to modeling systems where all agents have full knowledge of the state of the game. In this paper, we introduce delayed-action games (DAGs) formalism that simulates hidden-information games (HIGs) as SMGs, where hidden information is captured by delaying a player's actions. The elimination of private variables enables the usage of SMG off-the-shelf model checkers to implement HIGs. Furthermore, we demonstrate how a DAG can be decomposed into subgames that can be independently explored, utilizing parallel computation to reduce the model checking time, while alleviating the state space explosion problem that SMGs are notorious for. In addition, we propose a DAG-based framework for strategy synthesis and analysis. Finally, we demonstrate applicability of the DAG-based synthesis framework on a case study of a human-on-the-loop unmanned-aerial vehicle system under stealthy attacks, where the proposed framework is used to formally model, analyze and synthesize security-aware strategies for the system.

cs.GT