arXiv subjects

Sasinee Pruekprasert

Publications and source records attributed to Sasinee Pruekprasert.

15 recordsLinked to original sources

arXiv2026

ETA Coordination at UAM Corridor Merging Points Using Worst-Case and Stochastic Trajectory Bounds

We study an Estimated Time of Arrival (ETA)-based traffic-coordination framework for Urban Air Mobility corridors with merging at constrained waypoints (CWPs), where approved ETAs at CWPs serve as Required Times of Arrival (RTAs). Vehicle operators submit ETA plans at the merging point for approval by corridor-management authorities before corridor entry. Corridor entry is then scheduled by enforcing pairwise ETA gaps that maintain inter-vehicle separation on shared corridor sections. We develop two trajectory bounds to compute sufficient ETA gaps: a worst-case bound based on prescribed speed limits, and a stochastic bound based on probabilistic position envelopes under acceleration uncertainty. Using these bounds, we formulate sufficient ETA-gap computation and first-come, first-served corridor entrance scheduling. Simulations show that ETA coordination improves safety over an unscheduled baseline. The worst-case bound provides stronger robustness under higher disturbance levels, whereas the stochastic bound allows higher throughput under mild disturbances while relying on probabilistic modeling assumptions.

eess.SY↗

arXiv2026

Safe Arrival Scheduling at Constraint Waypoints in UAM Corridors

This study introduces a novel Air Traffic Control (ATC) concept to support self-separation between vehicles in Urban Air Mobility (UAM) corridors. Our proposed scheme involves sharing intended arrival schedules at Constrained Waypoints (CWPs) among UAM operators. We propose two approaches to assist the arrival scheduling at CWPs by computing the minimum arrival time gap necessary for each pair of vehicles to ensure their safety throughout the flights within the corridor. The first approach considers the minimum separation distance required by the Near Mid-Air-Collision (NMAC) avoidance rules, while the second one is based on the Responsibility-Sensitive Safety (RSS) rules. We demonstrate that the NMAC-rule-based approach can effectively prevent collisions in normal circumstances, where the vehicles adhere to the speed limits of the corridor. However, this approach does not guarantee safety if vehicles exceed the speed limits. Conversely, while the RSS-rule-based approach ensures collision prevention during emergencies when vehicles exceed speed limits, it may require larger arrival time gaps under normal circumstances, which may lead to reduced traffic flow. Our results are confirmed through numerical simulations.

eess.SY↗

arXiv2026

Safety-Assured Arrival Scheduling in Sequential UAM Corridor Sections under Speed and Separation Constraints

This paper presents a safety-assured arrival-scheduling framework for Urban Air Mobility (UAM) corridor operations. We propose an analytical method to compute a sufficient ETA gap at Constrained Waypoints (CWPs) that guarantees longitudinal separation along sequential corridor sections with heterogeneous speed limits. The resulting ETA-gap condition depends on section-specific speed bounds and the required separation distance, providing an efficiently computable rule suitable for integration into future digital ETA-scheduling and air traffic management systems. We show that the computed ETA gap ensures safe separation across all corridor sections under prescribed section travel times and speed limits. Numerical simulations for a decreasing-speed corridor confirm that vehicles coordinated with the proposed mechanism adjust their speeds to maintain the required spacing, avoid potential collisions, and support improved traffic flow compared with unscheduled operations.

eess.SY↗

arXiv2026

From Visual to Digital: Coordination Scheduling and Its Effect on Safety and Efficiency in UAM Corridors

This paper explores scalable coordination strategies for urban air mobility (UAM) corridors by comparing two representative approaches. The first, inspired by visual flight rules (VFR), is a local coordination strategy relying on spatial information available to each vehicle. The second, conceptually aligned with digital flight rules (DFR), is a global coordination strategy based on shared estimated times of arrival (ETAs) at constrained waypoints (CWPs). To support this comparison, we introduce a lightweight disturbance-avoidance mechanism that enables vehicles to adjust their ETAs in response to forecasted disruptions using shared information. We evaluate these approaches through numerical simulations under varying disturbance levels, comparing the locally reactive VFR-style scheme with the globally coordinated DFR-style scheme. Results show that VFR achieves high throughput in low-traffic scenarios but becomes increasingly prone to collisions at higher traffic densities unless conservative separation is enforced, which reduces traffic efficiency. In contrast, DFR maintains more consistent safety performance and traffic efficiency, even under moderate ETA update propagation delays. These findings highlight the advantages of DFR-style global coordination in managing high-density air traffic control (ATC) operations within UAM corridors.

eess.SY↗

arXiv2025

Strategy Templates for Almost-Sure and Positive Winning of Stochastic Parity Games towards Permissive and Resilient Control

Stochastic games are fundamental in various applications, including the control of cyber-physical systems (CPS), where both controller and environment are modeled as players. Traditional algorithms typically aim to determine a single winning strategy to develop a controller. However, in CPS control and other domains, permissive controllers are essential, as they enable the system to adapt when additional constraints arise and remain resilient to runtime changes. This work generalizes the concept of (permissive winning) strategy templates, originally introduced by Anand et al. at TACAS and CAV 2023 for deterministic games, to incorporate stochastic games. These templates capture an infinite number of winning strategies, allowing for efficient strategy adaptation to system changes. We focus on two winning criteria (almost-sure and positive winning) and five winning objectives (safety, reachability, Büchi, co-Büchi, and parity). Our contributions include algorithms for constructing templates for each winning criterion and objective and a novel approach for extracting a winning strategy from a given template. Discussions on comparisons between templates and between strategy extraction methods are provided.

eess.SY↗

arXiv2025

AP-observation Automata for Abstraction-based Verification of Continuous-time Systems (Extended Version)

A key challenge in abstraction-based verification and control under complex specifications such as Linear Temporal Logic (LTL) is that abstract models retain significantly less information than their original systems. This issue is especially true for continuous-time systems, where the system state trajectories are split into intervals of discrete actions, and satisfaction of atomic propositions is abstracted to a whole time interval. To tackle this challenge, this work introduces a novel translation from LTL specifications to AP-observation automata, a particular type of Büchi automata specifically designed for abstraction-based verification. Based on this automaton, we present a game-based verification algorithm played between the system and the environment, and an illustrative example for abstraction-based system verification under several LTL specifications.

eess.SY↗

arXiv2023

Moment Propagation of Polynomial Systems Through Carleman Linearization for Probabilistic Safety Analysis

We develop a method to approximate the moments of a discrete-time stochastic polynomial system. Our method is built upon Carleman linearization with truncation. Specifically, we take a stochastic polynomial system with finitely many states and transform it into an infinite-dimensional system with linear deterministic dynamics, which describe the exact evolution of the moments of the original polynomial system. We then truncate this deterministic system to obtain a finite-dimensional linear system, and use it for moment approximation by iteratively propagating the moments along the finite-dimensional linear dynamics across time. We provide efficient online computation methods for this propagation scheme with several error bounds for the approximation. Our results also show that precise values of certain moments at a given time step can be obtained when the truncated system is sufficiently large. Furthermore, we investigate techniques to reduce the offline computation load using reduced Kronecker power. Based on the obtained approximate moments and their errors, we also provide hyperellipsoidal regions that are safe for some given probability bound. Those bounds allow us to conduct probabilistic safety analysis online through convex optimization. We demonstrate our results on a logistic map with stochastic dynamics and a vehicle dynamics subject to stochastic disturbance.

eess.SY↗

arXiv2022

Dynamic Shielding for Reinforcement Learning in Black-Box Environments

It is challenging to use reinforcement learning (RL) in cyber-physical systems due to the lack of safety guarantees during learning. Although there have been various proposals to reduce undesired behaviors during learning, most of these techniques require prior system knowledge, and their applicability is limited. This paper aims to reduce undesired behaviors during learning without requiring any prior system knowledge. We propose dynamic shielding: an extension of a model-based safe RL technique called shielding using automata learning. The dynamic shielding technique constructs an approximate system model in parallel with RL using a variant of the RPNI algorithm and suppresses undesired explorations due to the shield constructed from the learned model. Through this combination, potentially unsafe actions can be foreseen before the agent experiences them. Experiments show that our dynamic shield significantly decreases the number of undesired events during training.

cs.LG↗

arXiv2022

Goal-Aware RSS for Complex Scenarios via Program Logic

We introduce a goal-aware extension of responsibility-sensitive safety (RSS), a recent methodology for rule-based safety guarantee for automated driving systems (ADS). Making RSS rules guarantee goal achievement -- in addition to collision avoidance as in the original RSS -- requires complex planning over long sequences of manoeuvres. To deal with the complexity, we introduce a compositional reasoning framework based on program logic, in which one can systematically develop RSS rules for smaller subscenarios and combine them to obtain RSS rules for bigger scenarios. As the basis of the framework, we introduce a program logic dFHL that accommodates continuous dynamics and safety conditions. Our framework presents a dFHL-based workflow for deriving goal-aware RSS rules; we discuss its software support, too. We conducted experimental evaluation using RSS rules in a safety architecture. Its results show that goal-aware RSS is indeed effective in realising both collision avoidance and goal achievement.

cs.RO↗

arXiv2021

Fast Synthesis for Symbolic Self-triggered Control under Right-recursive LTL Specifications

We extend previous work on symbolic self-triggered control for non-deterministic continuous-time nonlinear systems without stability assumptions to a larger class of specifications. Our goal is to synthesise a controller for two objectives: the first one is modelled as a right-recursive LTL formula, and the second one is to ensure that the average communication rate between the controller and the system stays below a given threshold. We translate the control problem to solving a mean-payoff parity game played on a discrete graph. Apart from extending the class of specifications, we propose a heuristic method to shorten the computation time. Finally, we illustrate our results on the example of a navigating nonholonomic robot with several specifications.

eess.SY↗

arXiv2021

Local Opacity Verification for Distributed Discrete Event Systems

This paper studies current-state opacity and initial-state opacity verification of distributed discrete event systems. The distributed system's global model is the parallel composition of multiple local systems: each of which represents a component. We propose sufficient conditions for verifying opacity of the global system model based only on the opacity of the local systems. We also present efficient approaches for the opacity verification problem that only rely on the intruder's observer automata of the local systems.

eess.SY↗

arXiv2021

Moment Propagation of Discrete-Time Stochastic Polynomial Systems using Truncated Carleman Linearization

We propose a method to compute an approximation of the moments of a discrete-time stochastic polynomial system. We use the Carleman linearization technique to transform this finite-dimensional polynomial system into an infinite-dimensional linear one. After taking expectation and truncating the induced deterministic dynamics, we obtain a finite-dimensional linear deterministic system, which we then use to iteratively compute approximations of the moments of the original polynomial system at different time steps. We provide upper bounds on the approximation error for each moment and show that, for large enough truncation limits, the proposed method precisely computes moments for sufficiently small degrees and numbers of time steps. We use our proposed method for safety analysis to compute bounds on the probability of the system state being outside a given safety region. Finally, we illustrate our results on two concrete examples, a stochastic logistic map and a vehicle dynamics under stochastic disturbance.

eess.SY↗

arXiv2020

Symbolic Self-triggered Control of Continuous-time Non-deterministic Systems without Stability Assumptions for 2-LTL Specifications

We propose a symbolic self-triggered controller synthesis procedure for non-deterministic continuous-time nonlinear systems without stability assumptions. The goal is to compute a controller that satisfies two objectives. The first objective is represented as a specification in a fragment of LTL, which we call 2-LTL. The second one is an energy objective, in the sense that control inputs are issued only when necessary, which saves energy. To this end, we first quantise the state and input spaces, and then translate the controller synthesis problem to the computation of a winning strategy in a mean-payoff parity game. We illustrate the feasibility of our method on the example of a navigating nonholonomic robot.

eess.SY↗

arXiv2020

A Game-Theoretic Approach to Decision Making for Multiple Vehicles at Roundabout

In this paper, we study the decision making of multiple autonomous vehicles at a roundabout. The behaviours of the vehicles depend on their aggressiveness, which indicates how much they value speed over safety. We propose a distributed decision-making process that balances safety and speed of the vehicles. In the proposed process, each vehicle estimates other vehicles' aggressiveness and formulates the interactions among the vehicles as a finite sequential game. Based on the Nash equilibrium of this game, the vehicle predicts other vehicles' behaviours and makes decisions. We perform numerical simulations to illustrate the effectiveness of the proposed process, both for safety (absence of collisions), and speed (time spent within the roundabout).

eess.SY↗

arXiv2019

Decision Making for Autonomous Vehicles at Unsignalized Intersection in Presence of Malicious Vehicles

In this paper, we investigate the decision making of autonomous vehicles in an unsignalized intersection in presence of malicious vehicles, which are vehicles that do not respect the law by not using the proper rules of the right of way. Each vehicle computes its control input as a Nash equilibrium of a game determined by the priority order based on its own belief: each of non-malicious vehicle bases its order on the law, while a malicious one considers itself as having priority. To illustrate our method, we provide numerical simulations, with different scenarios given by different cases of malicious vehicles.

eess.SY↗