control engineers

Abstract: Ensuring the satisfaction of Signal Temporal Logic (STL) specifications under uncertainty is challenging, as reachability-based monitoring provides guarantees but does not indicate how to restore satisfaction when it becomes indeterminate. A key difficulty is identifying which uncertain components actually affect global satisfaction, especially for nested formulas. This paper introduces a logical dependency tracking framework that propagates uncertainty through the STL structure and captures the causal contribution of reachable sets to satisfaction. By associating markers to uncertain predicates and propagating them via three-valued semantics, we extract in milliseconds a compact Disjunctive Normal Form (DNF) of sufficient constraints, avoiding combinatorial enumeration. As an application, we formulate control correction as a minimum-effort optimization problem. Using zonotopic reachability, the derived constraints are enforced via linear programming, yielding corrections that guarantee STL satisfaction under bounded uncertainty and provide certified probabilistic bounds in the stochastic case. We demonstrate the approach on a nonlinear system with nested STL specifications, showing that dependency tracking enables efficient and formally guaranteed correction. The tracking implementation is available at https://github.com/Antoine-Bst/STL-Three-Valued-Clause-Filtering/.

Abstract: In this paper we derive a Probably Approximately Correct (PAC)-Bayesian error bound for partially observed linear time-invariant (LTI) stochastic dynamical systems in state-space form with inputs and sub-Gaussian noise. Such bounds are widespread in machine learning, and they are useful for characterizing the predictive power of models learned from finitely many data points. The bound derived in this paper relates the expectation of prediction errors with the prediction error generated by the model on the data used for learning. In addition, we show that it can also be used to derive bounds for the parameter estimation error. In turn, this allows us to provide finite-sample error bounds for the prediction error and parameter estimation error for a wide class of system identification algorithms. Furthermore, as LTI systems are a sub-class of recurrent neural networks (RNNs), these error bounds could be a first step towards PAC-Bayesian bounds for RNNs.

Abstract: We propose a new approach for synthesizing large sets of winning strategies in stochastic parity games (2.5-player games) with quantitative objectives. Instead of computing a single, fully specified winning strategy, we introduce Actionable Strategy Certificates (ASCerts) as a local and permissive representation of a large class of system player winning strategies. To this end, we extend known certificates for stochastic invariants to the setting of games. Our certificates prove that synthesized strategies remain within a safe region of the game with probability at least $λ\in [0,1]$. As such, the certificates enhance the trustworthiness of synthesized strategies. The crux of our approach is to reinterpret and leverage the certificates as concise, local, and permissive representation of (possibly infinitely many) strategies. By carefully combining our certificates for stochastic invariants with strategy templates for almost-sure winning, we obtain a novel local representation of quantitatively winning strategies in stochastic parity games. This enables efficient synthesis, adaptation, and runtime strategy extraction, making ASCerts well suited for logical control in uncertain and adversarial environments. We provide a proof-of-concept implementation and demonstrate the potential of applying ASCerts in runtime adaptation on a case study.