Showing 1–31 of 31 results for author: Lahijanian, M

On Polynomial Stochastic Barrier Functions: Bernstein Versus Sum-of-Squares

Authors: Peter Amorese, Morteza Lahijanian

Abstract: Stochastic Barrier Functions (SBFs) certify the safety of stochastic systems by formulating a functional optimization problem, which state-of-the-art methods solve using Sum-of-Squares (SoS) polynomials. This work focuses on polynomial SBFs and introduces a new formulation based on Bernstein polynomials and provides a comparative analysis of its theoretical and empirical performance against SoS me… ▽ More Stochastic Barrier Functions (SBFs) certify the safety of stochastic systems by formulating a functional optimization problem, which state-of-the-art methods solve using Sum-of-Squares (SoS) polynomials. This work focuses on polynomial SBFs and introduces a new formulation based on Bernstein polynomials and provides a comparative analysis of its theoretical and empirical performance against SoS methods. We show that the Bernstein formulation leads to a linear program (LP), in contrast to the semi-definite program (SDP) required for SoS, and that its relaxations exhibit favorable theoretical convergence properties. However, our empirical results reveal that the Bernstein approach struggles to match SoS in practical performance, exposing an intriguing gap between theoretical advantages and real-world feasibility. △ Less

Submitted 10 June, 2025; originally announced June 2025.

Comments: To appear in IEEE Control Systems Letters (L-CSS) 2025

Falsification of Autonomous Systems in Rich Environments

Authors: Khen Elimelech, Morteza Lahijanian, Lydia E. Kavraki, Moshe Y. Vardi

Abstract: Validating the behavior of autonomous Cyber-Physical Systems (CPS) and Artificial Intelligence (AI) agents, which rely on automated controllers, is an objective of great importance. In recent years, Neural-Network (NN) controllers have been demonstrating great promise. Unfortunately, such learned controllers are often not certified and can cause the system to suffer from unpredictable or unsafe be… ▽ More Validating the behavior of autonomous Cyber-Physical Systems (CPS) and Artificial Intelligence (AI) agents, which rely on automated controllers, is an objective of great importance. In recent years, Neural-Network (NN) controllers have been demonstrating great promise. Unfortunately, such learned controllers are often not certified and can cause the system to suffer from unpredictable or unsafe behavior. To mitigate this issue, a great effort has been dedicated to automated verification of systems. Specifically, works in the category of ``black-box testing'' rely on repeated system simulations to find a falsifying counterexample of a system run that violates a specification. As running high-fidelity simulations is computationally demanding, the goal of falsification approaches is to minimize the simulation effort (NN inference queries) needed to return a falsifying example. This often proves to be a great challenge, especially when the tested controller is well-trained. This work contributes a novel falsification approach for autonomous systems under formal specification operating in uncertain environments. We are especially interested in CPS operating in rich, semantically-defined, open environments, which yield high-dimensional, simulation-dependent sensor observations. Our approach introduces a novel reformulation of the falsification problem as the problem of planning a trajectory for a ``meta-system,'' which wraps and encapsulates the examined system; we call this approach: meta-planning. This formulation can be solved with standard sampling-based motion-planning techniques (like RRT) and can gradually integrate domain knowledge to improve the search. We support the suggested approach with an experimental study on falsification of an obstacle-avoiding autonomous car with a NN controller, where meta-planning demonstrates superior performance over alternative approaches. △ Less

Submitted 23 December, 2024; originally announced December 2024.

Temporal Logic Control for Nonlinear Stochastic Systems Under Unknown Disturbances

Authors: Ibon Gracia, Luca Laurenti, Manuel Mazo Jr., Alessandro Abate, Morteza Lahijanian

Abstract: In this paper, we present a novel framework to synthesize robust strategies for discrete-time nonlinear systems with random disturbances that are unknown, against temporal logic specifications. The proposed framework is data-driven and abstraction-based: leveraging observations of the system, our approach learns a high-confidence abstraction of the system in the form of an uncertain Markov decisio… ▽ More In this paper, we present a novel framework to synthesize robust strategies for discrete-time nonlinear systems with random disturbances that are unknown, against temporal logic specifications. The proposed framework is data-driven and abstraction-based: leveraging observations of the system, our approach learns a high-confidence abstraction of the system in the form of an uncertain Markov decision process (UMDP). The uncertainty in the resulting UMDP is used to formally account for both the error in abstracting the system and for the uncertainty coming from the data. Critically, we show that for any given state-action pair in the resulting UMDP, the uncertainty in the transition probabilities can be represented as a convex polytope obtained by a two-layer state discretization and concentration inequalities. This allows us to obtain tighter uncertainty estimates compared to existing approaches, and guarantees efficiency, as we tailor a synthesis algorithm exploiting the structure of this UMDP. We empirically validate our approach on several case studies, showing substantially improved performance compared to the state-of-the-art. △ Less

Submitted 27 April, 2025; v1 submitted 15 December, 2024; originally announced December 2024.

Learning-Based Shielding for Safe Autonomy under Unknown Dynamics

Authors: Robert Reed, Morteza Lahijanian

Abstract: Shielding is a common method used to guarantee the safety of a system under a black-box controller, such as a neural network controller from deep reinforcement learning (DRL), with simpler, verified controllers. Existing shielding methods rely on formal verification through Markov Decision Processes (MDPs), assuming either known or finite-state models, which limits their applicability to DRL setti… ▽ More Shielding is a common method used to guarantee the safety of a system under a black-box controller, such as a neural network controller from deep reinforcement learning (DRL), with simpler, verified controllers. Existing shielding methods rely on formal verification through Markov Decision Processes (MDPs), assuming either known or finite-state models, which limits their applicability to DRL settings with unknown, continuous-state systems. This paper addresses these limitations by proposing a data-driven shielding methodology that guarantees safety for unknown systems under black-box controllers. The approach leverages Deep Kernel Learning to model the systems' one-step evolution with uncertainty quantification and constructs a finite-state abstraction as an Interval MDP (IMDP). By focusing on safety properties expressed in safe linear temporal logic (safe LTL), we develop an algorithm that computes the maximally permissive set of safe policies on the IMDP, ensuring avoidance of unsafe states. The algorithms soundness and computational complexity are demonstrated through theoretical proofs and experiments on nonlinear systems, including a high-dimensional autonomous spacecraft scenario. △ Less

Submitted 7 October, 2024; originally announced October 2024.

Comments: 8 pages, 3 figures

Data-Driven Strategy Synthesis for Stochastic Systems with Unknown Nonlinear Disturbances

Authors: Ibon Gracia, Dimitris Boskos, Luca Laurenti, Morteza Lahijanian

Abstract: In this paper, we introduce a data-driven framework for synthesis of provably-correct controllers for general nonlinear switched systems under complex specifications. The focus is on systems with unknown disturbances whose effects on the dynamics of the system is nonlinear. The specifications are assumed to be given as linear temporal logic over finite traces (LTLf) formulas. Starting from observa… ▽ More In this paper, we introduce a data-driven framework for synthesis of provably-correct controllers for general nonlinear switched systems under complex specifications. The focus is on systems with unknown disturbances whose effects on the dynamics of the system is nonlinear. The specifications are assumed to be given as linear temporal logic over finite traces (LTLf) formulas. Starting from observations of either the disturbance or the state of the system, we first learn an ambiguity set that contains the unknown distribution of the disturbances with a user-defined confidence. Next, we construct a robust Markov decision process (RMDP) as a finite abstraction of the system. By composing the RMDP with the automaton obtained from the LTLf formula and performing optimal robust value iteration on the composed RMDP, we synthesize a strategy that yields a high probability that the uncertain system satisfies the specifications. Our empirical evaluations on systems with a wide variety of disturbances show that the strategies synthesized with our approach lead to high satisfaction probabilities and validate the theoretical guarantees. △ Less

Submitted 14 June, 2024; originally announced June 2024.

Sound Heuristic Search Value Iteration for Undiscounted POMDPs with Reachability Objectives

Authors: Qi Heng Ho, Martin S. Feather, Federico Rossi, Zachary N. Sunberg, Morteza Lahijanian

Abstract: Partially Observable Markov Decision Processes (POMDPs) are powerful models for sequential decision making under transition and observation uncertainties. This paper studies the challenging yet important problem in POMDPs known as the (indefinite-horizon) Maximal Reachability Probability Problem (MRPP), where the goal is to maximize the probability of reaching some target states. This is also a co… ▽ More Partially Observable Markov Decision Processes (POMDPs) are powerful models for sequential decision making under transition and observation uncertainties. This paper studies the challenging yet important problem in POMDPs known as the (indefinite-horizon) Maximal Reachability Probability Problem (MRPP), where the goal is to maximize the probability of reaching some target states. This is also a core problem in model checking with logical specifications and is naturally undiscounted (discount factor is one). Inspired by the success of point-based methods developed for discounted problems, we study their extensions to MRPP. Specifically, we focus on trial-based heuristic search value iteration techniques and present a novel algorithm that leverages the strengths of these techniques for efficient exploration of the belief space (informed search via value bounds) while addressing their drawbacks in handling loops for indefinite-horizon problems. The algorithm produces policies with two-sided bounds on optimal reachability probabilities. We prove convergence to an optimal policy from below under certain conditions. Experimental evaluations on a suite of benchmarks show that our algorithm outperforms existing methods in almost all cases in both probability guarantees and computation time. △ Less

Submitted 4 June, 2024; originally announced June 2024.

Comments: Accepted to the Conference on Uncertainty in Artificial Intelligence (UAI) 2024

Data-Driven Permissible Safe Control with Barrier Certificates

Authors: Rayan Mazouz, John Skovbekk, Frederik Baymler Mathiesen, Eric Frew, Luca Laurenti, Morteza Lahijanian

Abstract: This paper introduces a method of identifying a maximal set of safe strategies from data for stochastic systems with unknown dynamics using barrier certificates. The first step is learning the dynamics of the system via Gaussian process (GP) regression and obtaining probabilistic errors for this estimate. Then, we develop an algorithm for constructing piecewise stochastic barrier functions to find… ▽ More This paper introduces a method of identifying a maximal set of safe strategies from data for stochastic systems with unknown dynamics using barrier certificates. The first step is learning the dynamics of the system via Gaussian process (GP) regression and obtaining probabilistic errors for this estimate. Then, we develop an algorithm for constructing piecewise stochastic barrier functions to find a maximal permissible strategy set using the learned GP model, which is based on sequentially pruning the worst controls until a maximal set is identified. The permissible strategies are guaranteed to maintain probabilistic safety for the true system. This is especially important for learning-enabled systems, because a rich strategy space enables additional data collection and complex behaviors while remaining safe. Case studies on linear and nonlinear systems demonstrate that increasing the size of the dataset for learning the system grows the permissible strategy set. △ Less

Submitted 4 May, 2024; v1 submitted 30 April, 2024; originally announced May 2024.

Uncertainty Propagation in Stochastic Systems via Mixture Models with Error Quantification

Authors: Eduardo Figueiredo, Andrea Patane, Morteza Lahijanian, Luca Laurenti

Abstract: Uncertainty propagation in non-linear dynamical systems has become a key problem in various fields including control theory and machine learning. In this work we focus on discrete-time non-linear stochastic dynamical systems. We present a novel approach to approximate the distribution of the system over a given finite time horizon with a mixture of distributions. The key novelty of our approach is… ▽ More Uncertainty propagation in non-linear dynamical systems has become a key problem in various fields including control theory and machine learning. In this work we focus on discrete-time non-linear stochastic dynamical systems. We present a novel approach to approximate the distribution of the system over a given finite time horizon with a mixture of distributions. The key novelty of our approach is that it not only provides tractable approximations for the distribution of a non-linear stochastic system, but also comes with formal guarantees of correctness. In particular, we consider the total variation (TV) distance to quantify the distance between two distributions and derive an upper bound on the TV between the distribution of the original system and the approximating mixture distribution derived with our framework. We show that in various cases of interest, including in the case of Gaussian noise, the resulting bound can be efficiently computed in closed form. This allows us to quantify the correctness of the approximation and to optimize the parameters of the resulting mixture distribution to minimize such distance. The effectiveness of our approach is illustrated on several benchmarks from the control community. △ Less

Submitted 11 September, 2024; v1 submitted 22 March, 2024; originally announced March 2024.

IntervalMDP.jl: Accelerated Value Iteration for Interval Markov Decision Processes

Authors: Frederik Baymler Mathiesen, Morteza Lahijanian, Luca Laurenti

Abstract: In this paper, we present IntervalMDP.jl, a Julia package for probabilistic analysis of interval Markov Decision Processes (IMDPs). IntervalMDP.jl facilitates the synthesis of optimal strategies and verification of IMDPs against reachability specifications and discounted reward properties. The library supports sparse matrices and is compatible with data formats from common tools for the analysis o… ▽ More In this paper, we present IntervalMDP.jl, a Julia package for probabilistic analysis of interval Markov Decision Processes (IMDPs). IntervalMDP.jl facilitates the synthesis of optimal strategies and verification of IMDPs against reachability specifications and discounted reward properties. The library supports sparse matrices and is compatible with data formats from common tools for the analysis of probabilistic models, such as PRISM. A key feature of IntervalMDP.jl is that it presents both a multi-threaded CPU and a GPU-accelerated implementation of value iteration algorithms for IMDPs. In particular, IntervalMDP.jl takes advantage of the Julia type system and the inherently parallelizable nature of value iteration to improve the efficiency of performing analysis of IMDPs. On a set of examples, we show that IntervalMDP.jl substantially outperforms existing tools for verification and strategy synthesis for IMDPs in both computation time and memory consumption. △ Less

Submitted 29 April, 2024; v1 submitted 8 January, 2024; originally announced January 2024.

A Unifying Perspective for Safety of Stochastic Systems: From Barrier Functions to Finite Abstractions

Authors: Luca Laurenti, Morteza Lahijanian

Abstract: Providing safety guarantees for stochastic dynamical systems is a central problem in various fields, including control theory, machine learning, and robotics. Existing methods either employ Stochastic Barrier Functions (SBFs) or rely on numerical approaches based on finite abstractions. SBFs, analogous to Lyapunov functions, are used to establish (probabilistic) set invariance, whereas abstraction… ▽ More Providing safety guarantees for stochastic dynamical systems is a central problem in various fields, including control theory, machine learning, and robotics. Existing methods either employ Stochastic Barrier Functions (SBFs) or rely on numerical approaches based on finite abstractions. SBFs, analogous to Lyapunov functions, are used to establish (probabilistic) set invariance, whereas abstraction-based approaches approximate the stochastic system with a finite model to compute safety probability bounds. This paper presents a unifying perspective on these seemingly different approaches. Specifically, we show that both methods can be interpreted as approximations of a stochastic dynamic programming problem. This perspective allows us to formally establish the correctness of both techniques, characterize their convergence and optimality properties, and analyze their respective assumptions, advantages, and limitations. Our analysis reveals that, unlike SBFs-based methods, abstraction-based approaches can provide asymptotically optimal safety certificates, albeit at the cost of increased computational effort. △ Less

Submitted 24 May, 2025; v1 submitted 3 October, 2023; originally announced October 2023.

Comments: Submitted to IEEE Transaction on Automatic Control

Formal Abstraction of General Stochastic Systems via Noise Partitioning

Authors: John Skovbekk, Luca Laurenti, Eric Frew, Morteza Lahijanian

Abstract: Verifying the performance of safety-critical, stochastic systems with complex noise distributions is difficult. We introduce a general procedure for the finite abstraction of nonlinear stochastic systems with non-standard (e.g., non-affine, non-symmetric, non-unimodal) noise distributions for verification purposes. The method uses a finite partitioning of the noise domain to construct an interval… ▽ More Verifying the performance of safety-critical, stochastic systems with complex noise distributions is difficult. We introduce a general procedure for the finite abstraction of nonlinear stochastic systems with non-standard (e.g., non-affine, non-symmetric, non-unimodal) noise distributions for verification purposes. The method uses a finite partitioning of the noise domain to construct an interval Markov chain (IMC) abstraction of the system via transition probability intervals. Noise partitioning allows for a general class of distributions and structures, including multiplicative and mixture models, and admits both known and data-driven systems. The partitions required for optimal transition bounds are specified for systems that are monotonic with respect to the noise, and explicit partitions are provided for affine and multiplicative structures. By the soundness of the abstraction procedure, verification on the IMC provides guarantees on the stochastic system against a temporal logic specification. In addition, we present a novel refinement-free algorithm that improves the verification results. Case studies on linear and nonlinear systems with non-Gaussian noise, including a data-driven example, demonstrate the generality and effectiveness of the method without introducing excessive conservatism. △ Less

Submitted 19 September, 2023; originally announced September 2023.

Comments: 6 pages, 6 figures, submitted jointly to IEEE Control Systems Letters and 2024 ACC

Promises of Deep Kernel Learning for Control Synthesis

Authors: Robert Reed, Luca Laurenti, Morteza Lahijanian

Abstract: Deep Kernel Learning (DKL) combines the representational power of neural networks with the uncertainty quantification of Gaussian Processes. Hence, it is potentially a promising tool to learn and control complex dynamical systems. In this work, we develop a scalable abstraction-based framework that enables the use of DKL for control synthesis of stochastic dynamical systems against complex specifi… ▽ More Deep Kernel Learning (DKL) combines the representational power of neural networks with the uncertainty quantification of Gaussian Processes. Hence, it is potentially a promising tool to learn and control complex dynamical systems. In this work, we develop a scalable abstraction-based framework that enables the use of DKL for control synthesis of stochastic dynamical systems against complex specifications. Specifically, we consider temporal logic specifications and create an end-to-end framework that uses DKL to learn an unknown system from data and formally abstracts the DKL model into an Interval Markov Decision Process (IMDP) to perform control synthesis with correctness guarantees. Furthermore, we identify a deep architecture that enables accurate learning and efficient abstraction computation. The effectiveness of our approach is illustrated on various benchmarks, including a 5-D nonlinear stochastic system, showing how control synthesis with DKL can substantially outperform state-of-the-art competitive methods. △ Less

Submitted 12 March, 2024; v1 submitted 12 September, 2023; originally announced September 2023.

Comments: 9 pages, 4 figures, 3 tables

Sampling-based Reactive Synthesis for Nondeterministic Hybrid Systems

Authors: Qi Heng Ho, Zachary N. Sunberg, Morteza Lahijanian

Abstract: This paper introduces a sampling-based strategy synthesis algorithm for nondeterministic hybrid systems with complex continuous dynamics under temporal and reachability constraints. We model the evolution of the hybrid system as a two-player game, where the nondeterminism is an adversarial player whose objective is to prevent achieving temporal and reachability goals. The aim is to synthesize a wi… ▽ More This paper introduces a sampling-based strategy synthesis algorithm for nondeterministic hybrid systems with complex continuous dynamics under temporal and reachability constraints. We model the evolution of the hybrid system as a two-player game, where the nondeterminism is an adversarial player whose objective is to prevent achieving temporal and reachability goals. The aim is to synthesize a winning strategy -- a reactive (robust) strategy that guarantees the satisfaction of the goals under all possible moves of the adversarial player. Our proposed approach involves growing a (search) game-tree in the hybrid space by combining sampling-based motion planning with a novel bandit-based technique to select and improve on partial strategies. We show that the algorithm is probabilistically complete, i.e., the algorithm will asymptotically almost surely find a winning strategy, if one exists. The case studies and benchmark results show that our algorithm is general and effective, and consistently outperforms state of the art algorithms. △ Less

Submitted 23 December, 2023; v1 submitted 13 April, 2023; originally announced April 2023.

Comments: Published in IEEE Robotics and Automation Letters (RA-L)

Journal ref: IEEE Robotics and Automation Letters, vol. 9, no. 2, pp. 931-938, 2024

Efficient Strategy Synthesis for Switched Stochastic Systems with Distributional Uncertainty

Authors: Ibon Gracia, Dimitris Boskos, Morteza Lahijanian, Luca Laurenti, Manuel Mazo Jr

Abstract: We introduce a framework for the control of discrete-time switched stochastic systems with uncertain distributions. In particular, we consider stochastic dynamics with additive noise whose distribution lies in an ambiguity set of distributions that are $\varepsilon-$close, in the Wasserstein distance sense, to a nominal one. We propose algorithms for the efficient synthesis of distributionally rob… ▽ More We introduce a framework for the control of discrete-time switched stochastic systems with uncertain distributions. In particular, we consider stochastic dynamics with additive noise whose distribution lies in an ambiguity set of distributions that are $\varepsilon-$close, in the Wasserstein distance sense, to a nominal one. We propose algorithms for the efficient synthesis of distributionally robust control strategies that maximize the satisfaction probability of reach-avoid specifications with either a given or an arbitrary (not specified) time horizon, i.e., unbounded-time reachability. The framework consists of two main steps: finite abstraction and control synthesis. First, we construct a finite abstraction of the switched stochastic system as a \emph{robust Markov decision process} (robust MDP) that encompasses both the stochasticity of the system and the uncertainty in the noise distribution. Then, we synthesize a strategy that is robust to the distributional uncertainty on the resulting robust MDP. We employ techniques from optimal transport and stochastic programming to reduce the strategy synthesis problem to a set of linear programs, and propose a tailored and efficient algorithm to solve them. The resulting strategies are correctly refined into switching strategies for the original stochastic system. We illustrate the efficacy of our framework on various case studies comprising both linear and non-linear switched stochastic systems. △ Less

Submitted 17 May, 2024; v1 submitted 29 December, 2022; originally announced December 2022.

Comments: The new version includes a strategy synthesis algorithm for robust MDPs under unbounded-time reachability specifications and an updated set of illustrative case studies

Interval Markov Decision Processes with Continuous Action-Spaces

Authors: Giannis Delimpaltadakis, Morteza Lahijanian, Manuel Mazo Jr., Luca Laurenti

Abstract: Interval Markov Decision Processes (IMDPs) are finite-state uncertain Markov models, where the transition probabilities belong to intervals. Recently, there has been a surge of research on employing IMDPs as abstractions of stochastic systems for control synthesis. However, due to the absence of algorithms for synthesis over IMDPs with continuous action-spaces, the action-space is assumed discrete… ▽ More Interval Markov Decision Processes (IMDPs) are finite-state uncertain Markov models, where the transition probabilities belong to intervals. Recently, there has been a surge of research on employing IMDPs as abstractions of stochastic systems for control synthesis. However, due to the absence of algorithms for synthesis over IMDPs with continuous action-spaces, the action-space is assumed discrete a-priori, which is a restrictive assumption for many applications. Motivated by this, we introduce continuous-action IMDPs (caIMDPs), where the bounds on transition probabilities are functions of the action variables, and study value iteration for maximizing expected cumulative rewards. Specifically, we decompose the max-min problem associated to value iteration to $|\mathcal{Q}|$ max problems, where $|\mathcal{Q}|$ is the number of states of the caIMDP. Then, exploiting the simple form of these max problems, we identify cases where value iteration over caIMDPs can be solved efficiently (e.g., with linear or convex programming). We also gain other interesting insights: e.g., in certain cases where the action set $\mathcal{A}$ is a polytope, synthesis over a discrete-action IMDP, where the actions are the vertices of $\mathcal{A}$, is sufficient for optimality. We demonstrate our results on a numerical example. Finally, we include a short discussion on employing caIMDPs as abstractions for control synthesis. △ Less

Submitted 7 April, 2023; v1 submitted 2 November, 2022; originally announced November 2022.

Comments: This work will be presented at the 26th ACM International Conference on Hybrid Systems Computation and Control (HSCC), 09-12 May, 2023, San Antonio, TX, USA

Planning with SiMBA: Motion Planning under Uncertainty for Temporal Goals using Simplified Belief Guides

Authors: Qi Heng Ho, Zachary N. Sunberg, Morteza Lahijanian

Abstract: This paper presents a new multi-layered algorithm for motion planning under motion and sensing uncertainties for Linear Temporal Logic specifications. We propose a technique to guide a sampling-based search tree in the combined task and belief space using trajectories from a simplified model of the system, to make the problem computationally tractable. Our method eliminates the need to construct f… ▽ More This paper presents a new multi-layered algorithm for motion planning under motion and sensing uncertainties for Linear Temporal Logic specifications. We propose a technique to guide a sampling-based search tree in the combined task and belief space using trajectories from a simplified model of the system, to make the problem computationally tractable. Our method eliminates the need to construct fine and accurate finite abstractions. We prove correctness and probabilistic completeness of our algorithm, and illustrate the benefits of our approach on several case studies. Our results show that guidance with a simplified belief space model allows for significant speed-up in planning for complex specifications. △ Less

Submitted 9 April, 2023; v1 submitted 18 October, 2022; originally announced October 2022.

Comments: 8 pages, to appear in the IEEE International Conference on Robotics and Automation (ICRA), 2023

Stochastic Robustness Interval for Motion Planning with Signal Temporal Logic

Authors: Roland B. Ilyes, Qi Heng Ho, Morteza Lahijanian

Abstract: In this work, we present a novel robustness measure for continuous-time stochastic trajectories with respect to Signal Temporal Logic (STL) specifications. We show the soundness of the measure and develop a monitor for reasoning about partial trajectories. Using this monitor, we introduce an STL sampling-based motion planning algorithm for robots under uncertainty. Given a minimum robustness requi… ▽ More In this work, we present a novel robustness measure for continuous-time stochastic trajectories with respect to Signal Temporal Logic (STL) specifications. We show the soundness of the measure and develop a monitor for reasoning about partial trajectories. Using this monitor, we introduce an STL sampling-based motion planning algorithm for robots under uncertainty. Given a minimum robustness requirement, this algorithm finds satisfying motion plans; alternatively, the algorithm also optimizes for the measure. We prove probabilistic completeness and asymptotic optimality, and demonstrate the effectiveness of our approach on several case studies. △ Less

Submitted 28 May, 2023; v1 submitted 10 October, 2022; originally announced October 2022.

Pareto Optimal Strategies for Event-Triggered Estimation

Authors: Anne Theurkauf, Nisar Ahmed, Morteza Lahijanian

Abstract: Although resource-limited networked autonomous systems must be able to efficiently and effectively accomplish tasks, better conservation of resources often results in worse task performance. We specifically address the problem of finding strategies for managing measurement communication costs between agents. A well understood technique for trading off communication costs with estimation accuracy i… ▽ More Although resource-limited networked autonomous systems must be able to efficiently and effectively accomplish tasks, better conservation of resources often results in worse task performance. We specifically address the problem of finding strategies for managing measurement communication costs between agents. A well understood technique for trading off communication costs with estimation accuracy is event triggering (ET), where measurements are only communicated when useful, e.g., when Kalman filter innovations exceed some threshold. In the absence of measurements, agents can use implicit information to achieve results almost as well as when explicit data is always communicated. However, there are no methods for setting this threshold with formal guarantees on task performance. We fill this gap by developing a novel belief space discretization technique to abstract a continuous space dynamics model for ET estimation to a discrete Markov decision process, which scalably accommodates threshold-sensitive ET estimator error covariances. We then apply an existing probabilistic trade-off analysis tool to find the set of all optimal trade-offs between resource consumption and task performance. From this set, an ET threshold selection strategy is extracted. Simulated results show our approach identifies non-trivial trade-offs between performance and energy savings, with only modest computational effort. △ Less

Submitted 4 October, 2022; v1 submitted 18 July, 2022; originally announced July 2022.

Comments: 8 pages, accepted to IEEE Conference on Decision and Control 2022

Automaton-Guided Control Synthesis for Signal Temporal Logic Specifications

Authors: Qi Heng Ho, Roland B. Ilyes, Zachary N. Sunberg, Morteza Lahijanian

Abstract: This paper presents an algorithmic framework for control synthesis of continuous dynamical systems subject to signal temporal logic (STL) specifications. We propose a novel algorithm to obtain a time-partitioned finite automaton from an STL specification, and introduce a multi-layered framework that utilizes this automaton to guide a sampling-based search tree both spatially and temporally. Our ap… ▽ More This paper presents an algorithmic framework for control synthesis of continuous dynamical systems subject to signal temporal logic (STL) specifications. We propose a novel algorithm to obtain a time-partitioned finite automaton from an STL specification, and introduce a multi-layered framework that utilizes this automaton to guide a sampling-based search tree both spatially and temporally. Our approach is able to synthesize a controller for nonlinear dynamics and polynomial predicate functions. We prove the correctness and probabilistic completeness of our algorithm, and illustrate the efficiency and efficacy of our framework on several case studies. Our results show an order of magnitude speedup over the state of the art. △ Less

Submitted 4 October, 2022; v1 submitted 7 July, 2022; originally announced July 2022.

Comments: 8 pages, 3 figures, to appear in CDC 2022

Safety Guarantees for Neural Network Dynamic Systems via Stochastic Barrier Functions

Authors: Rayan Mazouz, Karan Muvvala, Akash Ratheesh, Luca Laurenti, Morteza Lahijanian

Abstract: Neural Networks (NNs) have been successfully employed to represent the state evolution of complex dynamical systems. Such models, referred to as NN dynamic models (NNDMs), use iterative noisy predictions of NN to estimate a distribution of system trajectories over time. Despite their accuracy, safety analysis of NNDMs is known to be a challenging problem and remains largely unexplored. To address… ▽ More Neural Networks (NNs) have been successfully employed to represent the state evolution of complex dynamical systems. Such models, referred to as NN dynamic models (NNDMs), use iterative noisy predictions of NN to estimate a distribution of system trajectories over time. Despite their accuracy, safety analysis of NNDMs is known to be a challenging problem and remains largely unexplored. To address this issue, in this paper, we introduce a method of providing safety guarantees for NNDMs. Our approach is based on stochastic barrier functions, whose relation with safety are analogous to that of Lyapunov functions with stability. We first show a method of synthesizing stochastic barrier functions for NNDMs via a convex optimization problem, which in turn provides a lower bound on the system's safety probability. A key step in our method is the employment of the recent convex approximation results for NNs to find piece-wise linear bounds, which allow the formulation of the barrier function synthesis problem as a sum-of-squares optimization program. If the obtained safety probability is above the desired threshold, the system is certified. Otherwise, we introduce a method of generating controls for the system that robustly maximizes the safety probability in a minimally-invasive manner. We exploit the convexity property of the barrier function to formulate the optimal control synthesis problem as a linear program. Experimental results illustrate the efficacy of the method. Namely, they show that the method can scale to multi-dimensional NNDMs with multiple layers and hundreds of neurons per layer, and that the controller can significantly improve the safety probability. △ Less

Submitted 25 May, 2025; v1 submitted 15 June, 2022; originally announced June 2022.

Formal Control Synthesis for Stochastic Neural Network Dynamic Models

Authors: Steven Adams, Morteza Lahijanian, Luca Laurenti

Abstract: Neural networks (NNs) are emerging as powerful tools to represent the dynamics of control systems with complicated physics or black-box components. Due to complexity of NNs, however, existing methods are unable to synthesize complex behaviors with guarantees for NN dynamic models (NNDMs). This work introduces a control synthesis framework for stochastic NNDMs with performance guarantees. The focus… ▽ More Neural networks (NNs) are emerging as powerful tools to represent the dynamics of control systems with complicated physics or black-box components. Due to complexity of NNs, however, existing methods are unable to synthesize complex behaviors with guarantees for NN dynamic models (NNDMs). This work introduces a control synthesis framework for stochastic NNDMs with performance guarantees. The focus is on specifications expressed in linear temporal logic interpreted over finite traces (LTLf), and the approach is based on finite abstraction. Specifically, we leverage recent techniques for convex relaxation of NNs to formally abstract a NNDM into an interval Markov decision process (IMDP). Then, a strategy that maximizes the probability of satisfying a given specification is synthesized over the IMDP and mapped back to the underlying NNDM. We show that the process of abstracting NNDMs to IMDPs reduces to a set of convex optimization problems, hence guaranteeing efficiency. We also present an adaptive refinement procedure that makes the framework scalable. On several case studies, we illustrate the our framework is able to provide non-trivial guarantees of correctness for NNDMs with architectures of up to 5 hidden layers and hundreds of neurons per layer. △ Less

Submitted 21 March, 2022; v1 submitted 11 March, 2022; originally announced March 2022.

Gaussian Belief Trees for Chance Constrained Asymptotically Optimal Motion Planning

Authors: Qi Heng Ho, Zachary N. Sunberg, Morteza Lahijanian

Abstract: In this paper, we address the problem of sampling-based motion planning under motion and measurement uncertainty with probabilistic guarantees. We generalize traditional sampling-based tree-based motion planning algorithms for deterministic systems and propose belief-$\mathcal{A}$, a framework that extends any kinodynamical tree-based planner to the belief space for linear (or linearizable) system… ▽ More In this paper, we address the problem of sampling-based motion planning under motion and measurement uncertainty with probabilistic guarantees. We generalize traditional sampling-based tree-based motion planning algorithms for deterministic systems and propose belief-$\mathcal{A}$, a framework that extends any kinodynamical tree-based planner to the belief space for linear (or linearizable) systems. We introduce appropriate sampling techniques and distance metrics for the belief space that preserve the probabilistic completeness and asymptotic optimality properties of the underlying planner. We demonstrate the efficacy of our approach for finding safe low-cost paths efficiently and asymptotically optimally in simulation, for both holonomic and non-holonomic systems. △ Less

Submitted 4 October, 2022; v1 submitted 24 February, 2022; originally announced February 2022.

Comments: 9 pages, 4 figures. In ICRA 2022

Formal Verification of Unknown Dynamical Systems via Gaussian Process Regression

Authors: John Skovbekk, Luca Laurenti, Eric Frew, Morteza Lahijanian

Abstract: Leveraging autonomous systems in safety-critical scenarios requires verifying their behaviors in the presence of uncertainties and black-box components that influence the system dynamics. In this work, we develop a framework for verifying discrete-time dynamical systems with unmodelled dynamics and noisy measurements against temporal logic specifications from an input-output dataset. The verificat… ▽ More Leveraging autonomous systems in safety-critical scenarios requires verifying their behaviors in the presence of uncertainties and black-box components that influence the system dynamics. In this work, we develop a framework for verifying discrete-time dynamical systems with unmodelled dynamics and noisy measurements against temporal logic specifications from an input-output dataset. The verification framework employs Gaussian process (GP) regression to learn the unknown dynamics from the dataset and abstracts the continuous-space system as a finite-state, uncertain Markov decision process (MDP). This abstraction relies on space discretization and transition probability intervals that capture the uncertainty due to the error in GP regression by using reproducible kernel Hilbert space analysis as well as the uncertainty induced by discretization. The framework utilizes existing model checking tools for verification of the uncertain MDP abstraction against a given temporal logic specification. We establish the correctness of extending the verification results on the abstraction created from noisy measurements to the underlying system. We show that the computational complexity of the framework is polynomial in the size of the dataset and discrete abstraction. The complexity analysis illustrates a trade-off between the quality of the verification results and the computational burden to handle larger datasets and finer abstractions. Finally, we demonstrate the efficacy of our learning and verification framework on several case studies with linear, nonlinear, and switched dynamical systems. △ Less

Submitted 16 July, 2024; v1 submitted 31 December, 2021; originally announced January 2022.

Synergistic Offline-Online Control Synthesis via Local Gaussian Process Regression

Authors: John Jackson, Luca Laurenti, Eric Frew, Morteza Lahijanian

Abstract: Autonomous systems often have complex and possibly unknown dynamics due to, e.g., black-box components. This leads to unpredictable behaviors and makes control design with performance guarantees a major challenge. This paper presents a data-driven control synthesis framework for such systems subject to linear temporal logic on finite traces (LTLf) specifications. The framework combines a baseline… ▽ More Autonomous systems often have complex and possibly unknown dynamics due to, e.g., black-box components. This leads to unpredictable behaviors and makes control design with performance guarantees a major challenge. This paper presents a data-driven control synthesis framework for such systems subject to linear temporal logic on finite traces (LTLf) specifications. The framework combines a baseline (offline) controller with a novel online controller and refinement procedure that improves the baseline guarantees as new data is collected. The baseline controller is computed offline on an uncertain abstraction constructed using Gaussian process (GP) regression on a given dataset. The offline controller provides a lower bound on the probability of satisfying the LTLf specification, which may be far from optimal due to both discretization and regression errors. The synergy arises from the online controller using the offline abstraction along with the current state and new data to choose the next best action. The online controller may improve the baseline guarantees since it avoids the discretization error and reduces regression error as new data is collected. The new data are also used to refine the abstraction and offline controller using local GP regression, which significantly reduces the computation overhead. Evaluations show the efficacy of the proposed offline-online framework, especially when compared against the offline controller. △ Less

Submitted 8 March, 2022; v1 submitted 11 October, 2021; originally announced October 2021.

Comments: Updated Prop 1 from published version -- To appear in the 60th IEEE Conf on Decision and Control

Strategy Synthesis for Partially-known Switched Stochastic Systems

Authors: John Jackson, Luca Laurenti, Eric Frew, Morteza Lahijanian

Abstract: We present a data-driven framework for strategy synthesis for partially-known switched stochastic systems. The properties of the system are specified using linear temporal logic (LTL) over finite traces (LTLf), which is as expressive as LTL and enables interpretations over finite behaviors. The framework first learns the unknown dynamics via Gaussian process regression. Then, it builds a formal ab… ▽ More We present a data-driven framework for strategy synthesis for partially-known switched stochastic systems. The properties of the system are specified using linear temporal logic (LTL) over finite traces (LTLf), which is as expressive as LTL and enables interpretations over finite behaviors. The framework first learns the unknown dynamics via Gaussian process regression. Then, it builds a formal abstraction of the switched system in terms of an uncertain Markov model, namely an Interval Markov Decision Process (IMDP), by accounting for both the stochastic behavior of the system and the uncertainty in the learning step. Then, we synthesize a strategy on the resulting IMDP that maximizes the satisfaction probability of the LTLf specification and is robust against all the uncertainties in the abstraction. This strategy is then refined into a switching strategy for the original stochastic system. We show that this strategy is near-optimal and provide a bound on its distance (error) to the optimal strategy. We experimentally validate our framework on various case studies, including both linear and non-linear switched stochastic systems. △ Less

Submitted 8 March, 2022; v1 submitted 5 April, 2021; originally announced April 2021.

Comments: Updated Thm 1 and Fig 2 from published version -- 11 pages, to appear in the 2021 Proceedings of the ACM Int. Conf. on Hybrid Systems: Computation and Control (HSCC 2021)

Safety Verification of Unknown Dynamical Systems via Gaussian Process Regression

Authors: John Jackson, Luca Laurenti, Eric Frew, Morteza Lahijanian

Abstract: The deployment of autonomous systems that operate in unstructured environments necessitates algorithms to verify their safety. This can be challenging due to, e.g., black-box components in the control software, or undermodelled dynamics that prevent model-based verification. We present a novel verification framework for an unknown dynamical system from a given set of noisy observations of the dyna… ▽ More The deployment of autonomous systems that operate in unstructured environments necessitates algorithms to verify their safety. This can be challenging due to, e.g., black-box components in the control software, or undermodelled dynamics that prevent model-based verification. We present a novel verification framework for an unknown dynamical system from a given set of noisy observations of the dynamics. Using Gaussian processes trained on this data set, the framework abstracts the system as an uncertain Markov process with discrete states defined over the safe set. The transition bounds of the abstraction are derived from the probabilistic error bounds between the regression and underlying system. An existing approach for verifying safety properties over uncertain Markov processes then generates safety guarantees. We demonstrate the versatility of the framework on several examples, including switched and nonlinear systems. △ Less

Submitted 15 June, 2020; v1 submitted 3 April, 2020; originally announced April 2020.

Comments: 8 pages, LaTeX; typos corrected, references updated, figures updated

Efficiency through Uncertainty: Scalable Formal Synthesis for Stochastic Hybrid Systems

Authors: Nathalie Cauchi, Luca Laurenti, Morteza Lahijanian, Alessandro Abate, Marta Kwiatkowska, Luca Cardelli

Abstract: This work targets the development of an efficient abstraction method for formal analysis and control synthesis of discrete-time stochastic hybrid systems (SHS) with linear dynamics. The focus is on temporal logic specifications, both over finite and infinite time horizons. The framework constructs a finite abstraction as a class of uncertain Markov models known as interval Markov decision process… ▽ More This work targets the development of an efficient abstraction method for formal analysis and control synthesis of discrete-time stochastic hybrid systems (SHS) with linear dynamics. The focus is on temporal logic specifications, both over finite and infinite time horizons. The framework constructs a finite abstraction as a class of uncertain Markov models known as interval Markov decision process (IMDP). Then, a strategy that maximizes the satisfaction probability of the given specification is synthesized over the IMDP and mapped to the underlying SHS. In contrast to existing formal approaches, which are by and large limited to finite-time properties and rely on conservative over-approximations, we show that the exact abstraction error can be computed as a solution of convex optimization problems and can be embedded into the IMDP abstraction. This is later used in the synthesis step over both finite- and infinite-horizon specifications, mitigating the known state-space explosion problem. Our experimental validation of the new approach compared to existing abstraction-based approaches shows: (i) significant (orders of magnitude) reduction of the abstraction error; (ii) marked speed-ups; and (iii) boosted scalability, allowing in particular to verify models with more than 10 continuous variables. △ Less

Submitted 6 January, 2019; originally announced January 2019.

Multi-objective Robust Strategy Synthesis for Interval Markov Decision Processes

Authors: Ernst Moritz Hahn, Vahid Hashemi, Holger Hermanns, Morteza Lahijanian, Andrea Turrini

Abstract: Interval Markov decision processes (IMDPs) generalise classical MDPs by having interval-valued transition probabilities. They provide a powerful modelling tool for probabilistic systems with an additional variation or uncertainty that prevents the knowledge of the exact transition probabilities. In this paper, we consider the problem of multi-objective robust strategy synthesis for interval MDPs,… ▽ More Interval Markov decision processes (IMDPs) generalise classical MDPs by having interval-valued transition probabilities. They provide a powerful modelling tool for probabilistic systems with an additional variation or uncertainty that prevents the knowledge of the exact transition probabilities. In this paper, we consider the problem of multi-objective robust strategy synthesis for interval MDPs, where the aim is to find a robust strategy that guarantees the satisfaction of multiple properties at the same time in face of the transition probability uncertainty. We first show that this problem is PSPACE-hard. Then, we provide a value iteration-based decision algorithm to approximate the Pareto set of achievable points. We finally demonstrate the practical effectiveness of our proposed approaches by applying them on several case studies using a prototypical tool. △ Less

Submitted 6 July, 2017; v1 submitted 21 June, 2017; originally announced June 2017.

Comments: This article is a full version of a paper accepted to the Conference on Quantitative Evaluation of SysTems (QEST) 2017

ACM Class: D.2.4; F.1.1; G.1.6; G.3

Temporal Logic Motion Control using Actor-Critic Methods

Authors: Xu Chu Ding, Jing Wang, Morteza Lahijanian, Ioannis Ch. Paschalidis, Calin A. Belta

Abstract: In this paper, we consider the problem of deploying a robot from a specification given as a temporal logic statement about some properties satisfied by the regions of a large, partitioned environment. We assume that the robot has noisy sensors and actuators and model its motion through the regions of the environment as a Markov Decision Process (MDP). The robot control problem becomes finding the… ▽ More In this paper, we consider the problem of deploying a robot from a specification given as a temporal logic statement about some properties satisfied by the regions of a large, partitioned environment. We assume that the robot has noisy sensors and actuators and model its motion through the regions of the environment as a Markov Decision Process (MDP). The robot control problem becomes finding the control policy maximizing the probability of satisfying the temporal logic task on the MDP. For a large environment, obtaining transition probabilities for each state-action pair, as well as solving the necessary optimization problem for the optimal policy are usually not computationally feasible. To address these issues, we propose an approximate dynamic programming framework based on a least-square temporal difference learning method of the actor-critic type. This framework operates on sample paths of the robot and optimizes a randomized control policy with respect to a small set of parameters. The transition probabilities are obtained only when needed. Hardware-in-the-loop simulations confirm that convergence of the parameters translates to an approximately optimal policy. △ Less

Submitted 23 February, 2012; v1 submitted 9 February, 2012; originally announced February 2012.

Comments: Technical Report which accompanies an ICRA2012 paper

Least Squares Temporal Difference Actor-Critic Methods with Applications to Robot Motion Control

Authors: Reza Moazzez Estanjini, Xu Chu Ding, Morteza Lahijanian, Jing Wang, Calin A. Belta, Ioannis Ch. Paschalidis

Abstract: We consider the problem of finding a control policy for a Markov Decision Process (MDP) to maximize the probability of reaching some states while avoiding some other states. This problem is motivated by applications in robotics, where such problems naturally arise when probabilistic models of robot motion are required to satisfy temporal logic task specifications. We transform this problem into a… ▽ More We consider the problem of finding a control policy for a Markov Decision Process (MDP) to maximize the probability of reaching some states while avoiding some other states. This problem is motivated by applications in robotics, where such problems naturally arise when probabilistic models of robot motion are required to satisfy temporal logic task specifications. We transform this problem into a Stochastic Shortest Path (SSP) problem and develop a new approximate dynamic programming algorithm to solve it. This algorithm is of the actor-critic type and uses a least-square temporal difference learning method. It operates on sample paths of the system and optimizes the policy within a pre-specified class parameterized by a parsimonious set of parameters. We show its convergence to a policy corresponding to a stationary point in the parameters' space. Simulation results confirm the effectiveness of the proposed solution. △ Less

Submitted 30 August, 2011; v1 submitted 23 August, 2011; originally announced August 2011.

Comments: Technical report accompanying an accepted paper to CDC 2011

Probabilistically Safe Vehicle Control in a Hostile Environment

Authors: Igor Cizelj, Xu Chu Ding, Morteza Lahijanian, Alessandro Pinto, Calin Belta

Abstract: In this paper we present an approach to control a vehicle in a hostile environment with static obstacles and moving adversaries. The vehicle is required to satisfy a mission objective expressed as a temporal logic specification over a set of properties satisfied at regions of a partitioned environment. We model the movements of adversaries in between regions of the environment as Poisson processes… ▽ More In this paper we present an approach to control a vehicle in a hostile environment with static obstacles and moving adversaries. The vehicle is required to satisfy a mission objective expressed as a temporal logic specification over a set of properties satisfied at regions of a partitioned environment. We model the movements of adversaries in between regions of the environment as Poisson processes. Furthermore, we assume that the time it takes for the vehicle to traverse in between two facets of each region is exponentially distributed, and we obtain the rate of this exponential distribution from a simulator of the environment. We capture the motion of the vehicle and the vehicle updates of adversaries distributions as a Markov Decision Process. Using tools in Probabilistic Computational Tree Logic, we find a control strategy for the vehicle that maximizes the probability of accomplishing the mission objective. We demonstrate our approach with illustrative case studies. △ Less

Submitted 24 March, 2011; v1 submitted 21 March, 2011; originally announced March 2011.