arXiv subjects

Murat Arcak

Publications and source records attributed to Murat Arcak.

At least 19 recordsLinked to original sources

arXiv2026

Complete Abstractions of Monotone Control Systems: From Model-based to Data-Driven Systems

In this paper, we introduce the approximate strong upper alternating simulation (ASUAS), a new behavioral relation for transition systems. Building on this relation, we construct upper- and lower-sparse abstractions for monotone systems that together form a complete abstraction pair: any controller synthesized for the upper-sparse abstraction can be refined into a controller for the original system, and the absence of a controller for the lower-sparse abstraction implies the absence of a controller for the original system. A key feature of our approach is the ability to provably tune the conservativeness gap between the two abstractions by tuning the space-discretization parameter. We further extend these results, beyond the model-based setting, to data-driven systems, where the abstraction is constructed directly from finite sampled data, without requiring an explicit system model. The theoretical results are illustrated through simulations.

eess.SY↗

arXiv2026

Staying on Spec: Real-Time Monitoring under Uncertainty with a Maritime Case Study

Robotic systems must operate under uncertainty while satisfying complex task and safety specifications. Monitoring such specifications under uncertainty remains challenging, as existing formulations typically require extensive data or explicit uncertainty distributions. In this paper, we propose a real-time monitoring framework that reduces data requirements by leveraging data-driven reachable sets for specification evaluation. We instantiate the framework for maritime navigation, where complex specifications arise from traffic rules. We develop a data-efficient pipeline for constructing reachable sets and derive a monitoring formulation suitable for real-time deployment. Simulation and hardware experiments demonstrate robust monitoring under realistic disturbances, achieving improved risk detection compared to state-of-the-art metrics.

cs.RO↗

arXiv2026

Learning-enabled Parameter Synthesis for Nonlinear Systems from Signal Temporal Logic

Signal Temporal Logic (STL) is increasingly used to describe interpretable objectives and constraints for optimal control and learning methods, especially when no target time series data is available. In this work, we propose to synthesize parameters for nonlinear systems that robustly satisfy continuous-time STL specifications for uncertain initial conditions. To this end, we use gradient-based optimization along with set-based reachability verification to efficiently learn in high-dimensional parameter spaces while providing provable satisfaction guarantees for the optimized parameters. We demonstrate the effectiveness and scalability of our method on three systems with up to 18 parameter dimensions.

eess.SY↗

arXiv2026

Any-Body Guard: Universal Safeguarding for Manipulation Policies via Action Masking

Ensuring safety of learning-enabled robotic manipulation across diverse embodiments and tasks still requires significant manual engineering. Existing approaches typically rely on heuristically designed fallback controllers or complex forward invariance assessments. These methods are often too conservative for task success, too computationally expensive for real-time execution, too heuristic to provide useful safety guarantees, or too engineering-heavy to transfer between setups. In this paper, we propose a universal safeguarding approach, X-Safe, which reasons directly in the robot's configuration space to provide formal probabilistic guarantees for collision avoidance. By operating in the configuration space, our method transfers across embodiments while relying solely on an object-based, quasi-static scene representation and a forward kinematics model of the robotic manipulator. Thus, X-Safe provides useful formal safety guarantees without requiring additional data, or engineering effort for different embodiments or scenes. We demonstrate X-Safe for diverse embodiments and policies, both in simulation and on hardware. We observe less degradation in task performance compared to state-of-the-art safeguarding, no collisions on hardware experiments, and empirically corroborate our formal guarantees.

cs.RO↗

arXiv2026

Hierarchical Control for Continuous-time Systems via General Approximate Alternating Simulation Relations

This paper introduces a general approximate alternating simulation relation (\emph{$\varepsilon$-gAAS relation}) for continuous-time systems, which relaxes existing simulation relations to tolerate larger mismatches between abstract and concrete models. The definition of gAAS for continuous-time systems is first proposed, and its properties are investigated. Then, a control refinement method is developed to enable hierarchical control for the gAAS relation. Finally, case studies demonstrate the effectiveness of the proposed approach, highlighting its advantages over existing methods.

eess.SY↗

arXiv2026

Multi-Step Gaussian Process Propagation for Adaptive Path Planning

Efficient and robust path planning hinges on combining all accessible information sources. In particular, the task of path planning for robotic environmental exploration and monitoring depends highly on the current belief of the world. To capture the uncertainty in the belief, we present a Gaussian process based path planning method that adapts to multi-modal environmental sensing data and incorporates state and input constraints. To solve the path planning problem, we optimize over future waypoints in a receding horizon fashion, and our cost is thus a function of the Gaussian process posterior over all these waypoints. We demonstrate this method, dubbed OLAhGP, on an autonomous surface vessel using oceanic algal bloom data from both a high-fidelity model and in-situ sensing data in a monitoring scenario. Our simulated and experimental results demonstrate significant improvement over existing methods. With the same number of samples, our method generates more informative paths and achieves greater accuracy in identifying algal blooms in chlorophyll a rich waters, measured with respect to total misclassification probability and binary misclassification rate over the domain of interest.

cs.RO↗

arXiv2026

Target Mirror Descent: A Unifying Framework for Solving Monotone Variational Inequalities

It is well known that mirror descent may diverge or cycle on merely monotone variational inequalities. In this paper, we propose \emph{Target Mirror Descent} (TMD), a unified framework that stabilizes monotone flows via a target point correction mechanism in the dual update. By appropriate design choices, TMD recovers the proximal point algorithm, extragradient methods, splitting methods, Brown-von Neumann-Nash dynamics, forward-backward-forward dynamics, and discounted mirror descent as special cases. Thus, we establish a unified perspective on these landmark algorithms and their convergence. Beyond unification, we leverage the TMD framework to correct an equilibrium misalignment in discounted mirror descent and to generalize its higher-order extension beyond interior solutions. Moreover, a key structural feature of TMD is the explicit decoupling of the mirror map from the target determination, which enables \emph{geometric ensembles}: multiple algorithms solve the same problem in parallel using distinct mirror maps, while sharing a common dual update. We show that such an ensemble rigorously reduces to a single TMD with a synthesized mirror map, and thus inherits these convergence guarantees.

math.OC↗

arXiv2026

Importance Sampling for Statistical Certification of Viable Initial Sets

We study the problem of statistically certifying viable initial sets (VISs)---sets of initial conditions whose trajectories satisfy a given control specification. While VISs can be obtained from model-based methods, these methods typically rely on simplified models. We propose a simulation-based framework to certify VISs by estimating the probability of specification violations under a high-fidelity or black-box model. Since detecting these violations may be challenging due to their scarcity, we propose a sample-efficient framework that leverages importance sampling to target high-risk regions. We derive an empirical Bernstein inequality for weighted random variables, enabling finite-sample guarantees for importance sampling estimators. We demonstrate the proposed approach on two systems and show improved convergence of the resulting bounds on an adaptive cruise control benchmark.

eess.SY↗

arXiv2026

Probably Approximately Correct (PAC) Guarantees for Data-Driven Reachability Analysis: A Theoretical and Empirical Comparison

Reachability analysis evaluates system safety, by identifying the set of states a system may evolve within over a finite time horizon. In contrast to model-based reachability analysis, data-driven reachability analysis estimates reachable sets and derives probabilistic guarantees directly from data. Several popular techniques for validating reachable sets -- conformal prediction, scenario optimization, and the holdout method -- admit similar Probably Approximately Correct (PAC) guarantees. We establish a formal connection between these PAC bounds and present an empirical case study on reachable sets to illustrate the computational and sample trade-offs associated with these methods. We argue that despite the formal relationship between these techniques, subtle differences arise in both the interpretation of guarantees and the parameterization. As a result, these methods are not generally interchangeable. We conclude with practical advice on the usage of these methods.

eess.SY↗

arXiv2026

Learning Neural Network Controllers with Certified Robust Performance via Adversarial Training

Neural network (NN) controllers achieve strong empirical performance on nonlinear dynamical systems, yet deploying them in safety-critical settings requires robustness to disturbances and uncertainty. We present a method for jointly synthesizing NN controllers and dissipativity certificates that formally guarantee robust closed-loop performance using adversarial training, in which we use counterexamples to the robust dissipativity condition to guide training. Verification is done post-training using alpha,beta-CROWN, a branch-and-bound-based method that enables direct analysis of the nonlinear dynamical system. The proposed method uses quadratic constraints (QCs) only for characterization of non-parametric uncertainties. The method is tested in numerical experiments on maximizing the volume of the set on which a system is certified to be robustly dissipative. Our method certifies regions up to 78 times larger than the region certified by a linear matrix inequality-based approach that we derive for comparison.

eess.SY↗

arXiv2026

Polynomial Constraints for Robustness Analysis of Nonlinear Systems

This paper presents a framework for abstracting uncertain or non-polynomial components of dynamical systems using polynomial constraints. This enables the application of polynomial-based analysis tools, such as sum-of-squares programming, to a broader class of non-polynomial systems. A numerical method for constructing these constraints is proposed. The relationship between polynomial constraints and existing integral quadratic constraints (IQCs) is investigated, providing transformations of IQCs into polynomial constraints. The effectiveness of polynomial constraints in characterizing nonlinearities is validated via numerical examples to compute inner estimates of the region of attraction for two systems.

eess.SY↗

arXiv2025

Congestion Reduction in EV Charger Placement Using Traffic Equilibrium Models

Growing EV adoption can worsen traffic conditions if chargers are sited without regard to their impact on congestion. We study how to strategically place EV chargers to reduce congestion using two equilibrium models: one based on congestion games and one based on an atomic queueing simulation. We apply both models within a scalable greedy station-placement algorithm. Experiments show that this greedy scheme yields optimal or near-optimal congestion outcomes in realistic networks, even though global optimality is not guaranteed as we show with a counterexample. We also show that the queueing-based approach yields more realistic results than the congestion-game model, and we present a unified methodology that calibrates congestion delays from queue simulation and solves equilibrium in link-space.

eess.SY↗

arXiv2025

pacSTL: PAC-Bounded Signal Temporal Logic from Data-Driven Reachability Analysis

Signal Temporal Logic (STL) is an expressive language for specifying behaviors of dynamical systems from continuous signals. However, a limitation of standard STL is its inherently deterministic semantics, which prevents it from accommodating uncertainty. Existing approaches to overcome this limitation are computationally costly and limit real-time capability, requiring repeated trajectory sampling or redesign of probability distributions over atomic propositions whenever the atomic propositions or specifications change. We introduce pacSTL, a framework that combines Probably Approximately Correct (PAC)-bounded reachable set predictions with an interval extension of STL. pacSTL computes lower and upper bounds on atomic robustness values by solving optimization problems over PAC-bounded reachable sets and propagates the bounds through the temporal logic operators. The resulting evaluation yields a PAC-bounded robustness interval at the specification level. We demonstrate the efficiency and relevance of pacSTL by verifying a quadrotor flight scenario and runtime monitoring a maritime navigation encounter.

cs.LO↗

arXiv2025

Falsification-driven reinforcement learning for maritime motion planning

Compliance with maritime traffic rules is essential for the safe operation of autonomous vessels, yet training reinforcement learning (RL) agents to adhere to them is challenging. The behavior of RL agents is shaped by the training scenarios they encounter, but creating scenarios that capture the complexity of maritime navigation is non-trivial, and real-world data alone is insufficient. To address this, we propose a falsification-driven RL approach that generates adversarial training scenarios in which the vessel under test violates maritime traffic rules, which are expressed as signal temporal logic specifications. Our experiments on open-sea navigation with two vessels demonstrate that the proposed approach provides more relevant training scenarios and achieves more consistent rule compliance.

eess.SY↗

arXiv2025

Hierarchical Decision-Making in Population Games

This paper introduces a hierarchical framework for population games, where individuals delegate decision-making to proxies that act within their own strategic interests. This framework extends classical population games, where individuals are assumed to make decisions directly, to capture various real-world scenarios involving multiple decision layers. We establish equilibrium properties and provide convergence results for the proposed hierarchical structure. Additionally, based on these results, we develop a systematic approach to analyze population games with general convex constraints, without requiring individuals to have full knowledge of the constraints as in existing methods. We present a navigation application with capacity constraints as a case study.

eess.SY↗

arXiv2025

STL-based Optimization of Biomolecular Neural Networks for Regression and Control

Biomolecular Neural Networks (BNNs), artificial neural networks with biologically synthesizable architectures, achieve universal function approximation capabilities beyond simple biological circuits. However, training BNNs remains challenging due to the lack of target data. To address this, we propose leveraging Signal Temporal Logic (STL) specifications to define training objectives for BNNs. We build on the quantitative semantics of STL, enabling gradient-based optimization of the BNN weights, and introduce a learning algorithm that enables BNNs to perform regression and control tasks in biological systems. Specifically, we investigate two regression problems in which we train BNNs to act as reporters of dysregulated states, and a feedback control problem in which we train the BNN in closed-loop with a chronic disease model, learning to reduce inflammation while avoiding adverse responses to external infections. Our numerical experiments demonstrate that STL-based learning can solve the investigated regression and control tasks efficiently.

cs.LG↗

arXiv2025

Set Invariance with Probability One for Controlled Diffusion: Score-based Approach

Given a controlled diffusion and a connected, bounded, Lipschitz set, when is it possible to guarantee controlled set invariance with probability one? In this work, we answer this question by deriving the necessary and sufficient conditions for the same in terms of gradients of certain log-likelihoods -- a.k.a. score vector fields -- for two cases: given finite time horizon and infinite time horizon. The deduced conditions comprise a score-based test that provably certifies or falsifies the existence of Markovian controllers for given controlled set invariance problem data. Our results are constructive in the sense when the problem data passes the proposed test, we characterize all controllers guaranteeing the desired set invariance. When the problem data fails the proposed test, there does not exist a controller that can accomplish the desired set invariance with probability one. The computation in the proposed tests involve solving certain Dirichlet boundary value problems, and in the finite horizon case, can also account for additional constraint of hitting a target subset at the terminal time. We illustrate the results using several semi-analytical and numerical examples.

math.OC↗

arXiv2025

On Exact Solutions to the Linear Bellman Equation

This paper presents sufficient conditions for optimal control of systems with dynamics given by a linear operator, in order to obtain an explicit solution to the Bellman equation that can be calculated in a distributed fashion. Further, the class of Linearly Solvable MDP is reformulated as a continuous-state optimal control problem. It is shown that this class naturally satisfies the conditions for explicit solution of the Bellman equation, motivating the extension of previous results to semilinear dynamics to account for input nonlinearities. The applicability of the given conditions is illustrated in scenarios with linear and quadratic cost, corresponding to the Stochastic Shortest Path and Linear-Quadratic Regulator problems.

math.OC↗