BZPEERReading, trust and collaboration for research
Menu

Discover

GraphFollow connections around a paper, topic or saved view.

Workspaces

HomePick up where your research flow left off.InboxHandle requests, replies and notifications from one place.CollectionsCurate reading lists, evidence sets and shareable dossiers.ResearchSee your private provenance graph, trail and imports.CollaborationMove from discovery into focused discussion rooms.PublishDraft, preview and publish full-text research articles.

Network

ExpertsFind specialists worth following or asking for help.CommunitiesJoin research circles organized around shared work.PartnersSee external organizations active around the same topics.

Opportunities

ListingsBrowse roles, calls and collaborations with clearer fit signals.

Account

Log inReturn to your reading and collaboration workspace.Create accountStart saving work, following people and joining teams.
Log inCreate account

Researcher profile

Sadegh Soudjani

Sadegh Soudjani contributes to research discovery and scholarly infrastructure.

ResearcherAffiliation not importedOpen to collaborate
eess.SYSystems and ControlMachine LearningArtificial IntelligenceLogic in Computer Sciencemath.OCFormal Languages and Automata Theorymath.LOmath.PRNeural and Evolutionary Computingquant-ph

Trust snapshot

Quick read

Trust 21 - EmergingVerification L1Unclaimed author
21works
0followers
11topics
4close collaborators

Actions

Decide how to stay connected

Follow researcher0

Identity and collaboration

How to connect with this researcher

Claiming links this public author record to a researcher profile and unlocks direct collaboration workflows.

Log in to claim

Direct collaboration

Open a focused conversation when the fit is right

Claim this author entity first to unlock direct invitations.

Research graph

See the researcher in context

Open full explorer

Inspect adjacent work, topics, institutions and collaborators without jumping out to a separate graph page.

Building this graph slice

BZPEER is loading the nearby papers, people, topics and institutions for this page.

Published work

21 published item(s)

preprint2026arXiv

Kernel-Based Learning of Safety Barriers

The rapid integration of AI algorithms in safety-critical applications such as autonomous driving and healthcare is raising significant concerns about the ability to meet stringent safety standards. Traditional tools for formal safety verification struggle with the black-box nature of AI-driven systems and lack the flexibility needed to scale to the complexity of real-world applications. In this paper, we present a data-driven approach for safety verification and synthesis of black-box systems with discrete-time stochastic dynamics. We employ the concept of control barrier certificates, which can guarantee safety of the system, and learn the certificate directly from a set of system trajectories. We use conditional mean embeddings to embed data from the system into a reproducing kernel Hilbert space (RKHS) and construct an RKHS ambiguity set that can be inflated to robustify the result to out-of-distribution behavior. We provide the theoretical results on how to apply the approach to general classes of temporal logic specifications beyond safety. For the data-driven computation of safety barriers, we leverage a finite Fourier expansion to cast a typically intractable semi-infinite optimization problem as a linear program. The resulting spectral barrier allows us to leverage the fast Fourier transform to generate the relaxed problem efficiently, offering a scalable yet distributionally robust framework for verifying safety. Our work moves beyond restrictive assumptions on system dynamics and uncertainty, as demonstrated on two case studies including a black-box system with a neural network controller.

0 citations0 reviewsNo code linkedOpen access
preprint2026arXiv

Policy Synthesis for Interval MDPs via Polyhedral Lyapunov Functions

Decision-making under uncertainty is central to many safety-critical applications, where decisions must be guided by probabilistic modeling formalisms. This paper introduces a novel approach to policy synthesis in multi-objective interval Markov decision processes using polyhedral Lyapunov functions. Unlike previous Lyapunov-based methods that mainly rely on quadratic functions, our method utilizes polyhedral functions to enhance accuracy in managing uncertainties within value iteration of dynamic programming. We reformulate the value iteration algorithm as a switched affine system with interval uncertainties and apply control-theoretic stability principles to synthesize policies that guide the system toward a desired target set. By constructing an invariant set of attraction, we ensure that the synthesized policies provide convergence guarantees while minimizing the impact of transition uncertainty in the underlying model. Our methodology removes the need for computationally intensive Pareto curve computations by directly determining a policy that brings objectives within a specified range of their target values. We validate our approach through numerical case studies, including a recycling robot and an electric vehicle battery, demonstrating its effectiveness in achieving policy synthesis under uncertainty.

0 citations0 reviewsNo code linkedOpen access
preprint2026arXiv

Safety Certification is Classification

The goal of this paper is certifying safety of dynamical systems subject to uncertainty. Existing approaches use trajectory data to estimate transition probabilities, and compute safety probabilities recursively via dynamic programming (DP). This recursion may lead to compounding errors in the certified safety probability, thus collapsing to a vacuous lower bound for growing horizons $T$. We propose a kernel embedding framework that treats safety certification as a classification problem on trajectory data, directly estimating the $T$-step safety probability without recursion. We show that the framework subsumes well-established approaches from the literature (e.g., barrier certificates, robust Markov models) as special cases, and allows us to go beyond their limitations. As the main consequence, it bypasses compounding error across the horizon and enables certification for systems with non-Markovian dynamics. We demonstrate that direct estimators remain stable independent of the certification horizon and in the non-Markovian setting, whilst DP-based certificates silently go unsound -- confirmed in simulation on a neural-controlled quadrotor.

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

Automated Verification and Synthesis of Stochastic Hybrid Systems: A Survey

Stochastic hybrid systems have received significant attentions as a relevant modelling framework describing many systems, from engineering to the life sciences: they enable the study of numerous applications, including transportation networks, biological systems and chemical reaction networks, smart energy and power grids, and beyond. Automated verification and policy synthesis for stochastic hybrid systems can be inherently challenging: this is due to the heterogeneity of their dynamics (presence of continuous and discrete components), the presence of uncertainty, and in some applications the large dimension of state and input sets. Over the past few years, a few hundred articles have investigated these models, and developed diverse and powerful approaches to mitigate difficulties encountered in the analysis and synthesis of such complex stochastic systems. In this survey, we overview the most recent results in the literature and discuss different approaches, including (in)finite abstractions, verification and synthesis for temporal logic specifications, stochastic similarity relations, (control) barrier certificates, compositional techniques, and a selection of results on continuous-time stochastic systems; we finally survey recently developed software tools that implement the discussed approaches. Throughout the manuscript we discuss a few open topics to be considered as potential future research directions: we hope that this survey will guide younger researchers through a comprehensive understanding of the various challenges, tools, and solutions in this enticing and rich scientific area.

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

Compositional Construction of Control Barrier Functions for Continuous-Time Stochastic Hybrid Systems

In this work, we propose a compositional framework for the construction of control barrier functions for networks of continuous-time stochastic hybrid systems enforcing complex logic specifications expressed by finite-state automata. The proposed scheme is based on a notion of so-called pseudo-barrier functions computed for subsystems, by employing which one can synthesize hybrid controllers for interconnected systems enforcing complex specifications over a finite-time horizon. Particularly, we first leverage sufficient small-gain type conditions to compositionally construct control barrier functions for interconnected systems based on the corresponding pseudo-barrier functions computed for subsystems. Then, using the constructed control barrier functions, we provide probabilistic guarantees on the satisfaction of given complex specifications in a bounded time horizon. In this respect, we decompose the given complex specification to simpler reachability tasks based on automata representing the complements of original finite-state automata. We then provide systematic approaches to solve those simpler reachability tasks by computing corresponding pseudo-barrier functions. Two different systematic techniques are provided based on (i) the sum-of-squares (SOS) optimization program and (ii) counter-example guided inductive synthesis (CEGIS) to search for pseudo-barrier functions of subsystems while synthesizing local controllers. We demonstrate the effectiveness of our proposed results by applying them to a fully-interconnected Kuramoto network of 100 nonlinear oscillators with Markovian switching signals.

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

Compositional Reinforcement Learning for Discrete-Time Stochastic Control Systems

We propose a compositional approach to synthesize policies for networks of continuous-space stochastic control systems with unknown dynamics using model-free reinforcement learning (RL). The approach is based on implicitly abstracting each subsystem in the network with a finite Markov decision process with unknown transition probabilities, synthesizing a strategy for each abstract model in an assume-guarantee fashion using RL, and then mapping the results back over the original network with approximate optimality guarantees. We provide lower bounds on the satisfaction probability of the overall network based on those over individual subsystems. A key contribution is to leverage the convergence results for adversarial RL (minimax Q-learning) on finite stochastic arenas to provide control strategies maximizing the probability of satisfaction over the network of continuous-space systems. We consider finite-horizon properties expressed in the syntactically co-safe fragment of linear temporal logic. These properties can readily be converted into automata-based reward functions, providing scalar reward signals suitable for RL. Since such reward functions are often sparse, we supply a potential-based reward shaping technique to accelerate learning by producing dense rewards. The effectiveness of the proposed approaches is demonstrated via two physical benchmarks including regulation of a room temperature network and control of a road traffic network.

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

Constructing MDP Abstractions Using Data with Formal Guarantees

This paper is concerned with a data-driven technique for constructing finite Markov decision processes (MDPs) as finite abstractions of discrete-time stochastic control systems with unknown dynamics while providing formal closeness guarantees. The proposed scheme is based on notions of stochastic bisimulation functions (SBF) to capture the probabilistic distance between state trajectories of an unknown stochastic system and those of finite MDP. In our proposed setting, we first reformulate corresponding conditions of SBF as a robust convex program (RCP). We then propose a scenario convex program (SCP) associated to the original RCP by collecting a finite number of data from trajectories of the system. We ultimately construct an SBF between the data-driven finite MDP and the unknown stochastic system with a given confidence level by establishing a probabilistic relation between optimal values of the SCP and the RCP. We also propose two different approaches for the construction of finite MDPs from data. We illustrate the efficacy of our results over a nonlinear jet engine compressor with unknown dynamics. We construct a data-driven finite MDP as a suitable substitute of the original system to synthesize controllers maintaining the system in a safe set with some probability of satisfaction and a desirable confidence level.

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

Data-Driven Abstraction-Based Control Synthesis

This paper studies formal synthesis of controllers for continuous-space systems with unknown dynamics to satisfy requirements expressed as linear temporal logic formulas. Formal abstraction-based synthesis schemes rely on a precise mathematical model of the system to build a finite abstract model, which is then used to design a controller. The abstraction-based schemes are not applicable when the dynamics of the system are unknown. We propose a data-driven approach that computes the growth bound of the system using a finite number of trajectories. The growth bound together with the sampled trajectories are then used to construct the abstraction and synthesise a controller. Our approach casts the computation of the growth bound as a robust convex optimisation program (RCP). Since the unknown dynamics appear in the optimisation, we formulate a scenario convex program (SCP) corresponding to the RCP using a finite number of sampled trajectories. We establish a sample complexity result that gives a lower bound for the number of sampled trajectories to guarantee the correctness of the growth bound computed from the SCP with a given confidence. We also provide a sample complexity result for the satisfaction of the specification on the system in closed loop with the designed controller for a given confidence. Our results are founded on estimating a bound on the Lipschitz constant of the system and provide guarantees on satisfaction of both finite and infinite-horizon specifications. We show that our data-driven approach can be readily used as a model-free abstraction refinement scheme by modifying the formulation of the growth bound and providing similar sample complexity results. The performance of our approach is shown on three case studies.

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

Matrix Representation of Arbitrarily Controlled Quantum Gates

Controlled operations allow for the entanglement of quantum registers. In particular, a controlled-$U$ gate allows an operation, $U$, to be applied to the target register and entangle the results to certain values in the control register. This can be generalised by making use of the classical notion of conditional statements, where if a value (or state) satisfies some condition then a sequence of operations can be performed. A method is introduced to represent these generalised controlled operations that are based on classical conditional statements. Throughout examples are given to highlight the use of introduced gates.

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

Safety Barrier Certificates for Stochastic Hybrid Systems

This work is concerned with the safety controller synthesis of stochastic hybrid systems, in which continuous evolutions are described by stochastic differential equations with both Brownian motions and Poisson processes, and instantaneous jumps are governed by stochastic difference equations with additive noises. Our proposed framework leverages the notion of control barrier certificates (CBC), as a discretization-free approach, to synthesize safety controllers for stochastic hybrid systems while providing safety guarantees in finite time horizons. In our proposed scheme, we first provide an augmented framework to characterize each stochastic hybrid system containing continuous evolutions and instantaneous jumps with a unified system covering both scenarios. We then introduce an augmented control barrier certificate (ACBC) for augmented systems and propose sufficient conditions to construct an ACBC based on CBC of original hybrid systems. By utilizing the constructed ACBC, we quantify upper bounds on the probability that the stochastic hybrid system reaches certain unsafe regions in a finite time horizon. The proposed approach is verified over a nonlinear case study.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

A Lyapunov Approach for Time Bounded Reachability of CTMCs and CTMDPs

Time bounded reachability is a fundamental problem in model checking continuous-time Markov chains (CTMCs) and Markov decision processes (CTMDPs) for specifications in continuous stochastic logics. It can be computed by numerically solving a characteristic linear dynamical system but the procedure is computationally expensive. We take a control-theoretic approach and propose a reduction technique that finds another dynamical system of lower dimension (number of variables), such that numerically solving the reduced dynamical system provides an approximation to the solution of the original system with guaranteed error bounds. Our technique generalises lumpability (or probabilistic bisimulation) to a quantitative setting. Our main result is a Lyapunov function characterisation of the difference in the trajectories of the two dynamics that depends on the initial mismatch and exponentially decreases over time. In particular, the Lyapunov function enables us to compute an error bound between the two dynamics as well as a convergence rate. Finally, we show that the search for the reduced dynamics can be computed in polynomial time using a Schur decomposition of the transition matrix. This enables us to efficiently solve the reduced dynamical system by computing the exponential of an upper-triangular matrix characterising the reduced dynamics. For CTMDPs, we generalise our approach using piecewise quadratic Lyapunov functions for switched affine dynamical systems. We synthesise a policy for the CTMDP via its reduced-order switched system that guarantees the time bounded reachability probability lies above a threshold. We provide error bounds that depend on the minimum dwell time of the policy. We demonstrate the technique on examples from queueing networks, for which lumpability does not produce any state space reduction but our technique synthesises policies using reduced version of the model.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

AMYTISS: Parallelized Automated Controller Synthesis for Large-Scale Stochastic Systems

In this paper, we propose a software tool, called AMYTISS, implemented in C++/OpenCL, for designing correct-by-construction controllers for large-scale discrete-time stochastic systems. This tool is employed to (i) build finite Markov decision processes (MDPs) as finite abstractions of given original systems, and (ii) synthesize controllers for the constructed finite MDPs satisfying bounded-time high-level properties including safety, reachability and reach-avoid specifications. In AMYTISS, scalable parallel algorithms are designed such that they support the parallel execution within CPUs, GPUs and hardware accelerators (HWAs). Unlike all existing tools for stochastic systems, AMYTISS can utilize high-performance computing (HPC) platforms and cloud-computing services to mitigate the effects of the state-explosion problem, which is always present in analyzing large-scale stochastic systems. We benchmark AMYTISS against the most recent tools in the literature using several physical case studies including robot examples, room temperature and road traffic networks. We also apply our algorithms to a 3-dimensional autonomous vehicle and 7-dimensional nonlinear model of a BMW 320i car by synthesizing an autonomous parking controller.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

Compositional (In)Finite Abstractions for Large-Scale Interconnected Stochastic Systems

This paper is concerned with a compositional approach for constructing both infinite (reduced-order models) and finite abstractions (a.k.a. finite Markov decision processes (MDPs)) of large-scale interconnected discrete-time stochastic systems. The proposed framework is based on the notion of stochastic simulation functions enabling us to employ an abstract system as a substitution of the original one in the controller design process with guaranteed error bounds. In the first part of the paper, we derive sufficient small-gain type conditions for the compositional quantification of the probabilistic distance between the interconnection of stochastic control subsystems and that of their infinite abstractions. We then construct infinite abstractions together with their corresponding stochastic simulation functions for a particular class of discrete-time nonlinear stochastic control systems. In the second part of the paper, we leverage small-gain type conditions for the compositional construction of finite abstractions. We propose an approach to construct finite MDPs as finite abstractions of concrete models or their reduced-order versions satisfying an incremental input-to-state stability property. We demonstrate the effectiveness of the proposed results by applying our approaches to a fully interconnected network of 20 nonlinear subsystems (totally 100 dimensions). We construct finite MDPs from their reduced-order versions (together 20 dimensions) with guaranteed error bounds on their output trajectories. We also apply the proposed results to a temperature regulation in a circular building and construct compositionally a finite abstraction of a network containing 1000 rooms. We employ the constructed finite abstractions as substitutes to compositionally synthesize policies regulating the temperature in each room for a bounded time horizon.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

Compositional Abstraction of Large-Scale Stochastic Systems: A Relaxed Dissipativity Approach

In this paper, we propose a compositional approach for the construction of finite abstractions (a.k.a. finite Markov decision processes (MDPs)) for networks of discrete-time stochastic control subsystems that are not necessarily stabilizable. The proposed approach leverages the interconnection topology and a notion of finite-step stochastic storage functions, that describes joint dissipativity-type properties of subsystems and their abstractions, and establishes a finite-step stochastic simulation function as a relation between the network and its abstraction. To this end, we first develop a new type of compositionality conditions which is less conservative than the existing ones. In particular, using a relaxation via a finite-step stochastic simulation function, it is possible to construct finite abstractions such that stabilizability of each subsystem is not necessarily required. We then propose an approach to construct finite MDPs together with their corresponding finite-step storage functions for general discrete-time stochastic control systems satisfying an incremental passivablity property. We also construct finite MDPs for a particular class of nonlinear stochastic control systems. To demonstrate the effectiveness of the proposed results, we apply our results on three different case studies.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

Compositional Construction of Control Barrier Certificates for Large-Scale Stochastic Switched Systems

In this paper, we propose a compositional framework for the construction of control barrier certificates for large-scale stochastic switched systems accepting multiple control barrier certificates with some dwell-time conditions. The proposed scheme is based on a notion of so-called augmented pseudo-barrier certificates computed for each switched subsystem, using which one can compositionally synthesize state-feedback controllers for interconnected systems enforcing safety specifications over a finite-time horizon. In particular, we first leverage sufficient max-type small-gain conditions to compositionally construct augmented control barrier certificates for interconnected systems based on the corresponding augmented pseudo-barrier certificates of subsystems. Then we quantify upper bounds on exit probabilities - the probability that an interconnected system reaches certain unsafe regions - in a finite-time horizon using the constructed augmented barrier certificates. We employ a technique based on a counter-example guided inductive synthesis (CEGIS) approach to search for control barrier certificates of each mode while synthesizing safety controllers providing switching signals. We demonstrate our proposed results by applying them first to a room temperature network containing 1000 rooms. Finally, we apply our techniques to a network of 500 switched subsystems (totally 1000 dimensions) accepting multiple barrier certificates with a dwell-time condition, and provide upper bounds on the probability that the interconnected system reaches some unsafe region in a finite-time horizon.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

Data-Driven Verification under Signal Temporal Logic Constraints

We consider systems under uncertainty whose dynamics are partially unknown. Our aim is to study satisfaction of temporal logic properties by trajectories of such systems. We express these properties as signal temporal logic formulas and check if the probability of satisfying the property is at least a given threshold. Since the dynamics are parameterized and partially unknown, we collect data from the system and employ Bayesian inference techniques to associate a confidence value to the satisfaction of the property. The main novelty of our approach is to combine both data-driven and model-based techniques in order to have a two-layer probabilistic reasoning over the behavior of the system: one layer is related to the stochastic noise inside the system and the next layer is related to the noisy data collected from the system. We provide approximate algorithms for computing the confidence for linear dynamical systems.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

Formal Controller Synthesis for Continuous-Space MDPs via Model-Free Reinforcement Learning

A novel reinforcement learning scheme to synthesize policies for continuous-space Markov decision processes (MDPs) is proposed. This scheme enables one to apply model-free, off-the-shelf reinforcement learning algorithms for finite MDPs to compute optimal strategies for the corresponding continuous-space MDPs without explicitly constructing the finite-state abstraction. The proposed approach is based on abstracting the system with a finite MDP (without constructing it explicitly) with unknown transition probabilities, synthesizing strategies over the abstract MDP, and then mapping the results back over the concrete continuous-space MDP with approximate optimality guarantees. The properties of interest for the system belong to a fragment of linear temporal logic, known as syntactically co-safe linear temporal logic (scLTL), and the synthesis requirement is to maximize the probability of satisfaction within a given bounded time horizon. A key contribution of the paper is to leverage the classical convergence results for reinforcement learning on finite MDPs and provide control strategies maximizing the probability of satisfaction over unknown, continuous-space MDPs while providing probabilistic closeness guarantees. Automata-based reward functions are often sparse; we present a novel potential-based reward shaping technique to produce dense rewards to speed up learning. The effectiveness of the proposed approach is demonstrated by applying it to three physical benchmarks concerning the regulation of a room's temperature, control of a road traffic cell, and of a 7-dimensional nonlinear model of a BMW 320i car.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

Formal Synthesis of Stochastic Systems via Control Barrier Certificates

This paper focuses on synthesizing control policies for discrete-time stochastic control systems together with a lower bound on the probability that the systems satisfy the complex temporal properties. The desired properties of the system are expressed as linear temporal logic (LTL) specifications over finite traces. In particular, our approach decomposes the given specification into simpler reachability tasks based on its automata representation. We then propose the use of so-called \emph{control barrier certificate} to solve those simpler reachability tasks along with computing the corresponding controllers and probability bounds. Finally, we combine those controllers to obtain a hybrid control policy solving the considered problem. Under some assumptions, we also provide two systematic approaches for uncountable and finite input sets to search for control barrier certificates. We demonstrate the effectiveness of the proposed approach on a room temperature control and lane-keeping of a vehicle modeled as a four-dimensional single-track kinematic model. We compare our results with the discretization-based methods in the literature.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

On Decidability of Time-bounded Reachability in CTMDPs

We consider the time-bounded reachability problem for continuous-time Markov decision processes. We show that the problem is decidable subject to Schanuel's conjecture. Our decision procedure relies on the structure of optimal policies and the conditional decidability (under Schanuel's conjecture) of the theory of reals extended with exponential and trigonometric functions over bounded domains. We further show that any unconditional decidability result would imply unconditional decidability of the bounded continuous Skolem problem, or equivalently, the problem of checking if an exponential polynomial has a non-tangential zero in a bounded interval. We note that the latter problems are also decidable subject to Schanuel's conjecture but finding unconditional decision procedures remain longstanding open problems.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

Symbolic Controller Synthesis for Büchi Specifications on Stochastic Systems

We consider the policy synthesis problem for continuous-state controlled Markov processes evolving in discrete time, when the specification is given as a Büchi condition (visit a set of states infinitely often). We decompose computation of the maximal probability of satisfying the Büchi condition into two steps. The first step is to compute the maximal qualitative winning set, from where the Büchi condition can be enforced with probability one. The second step is to find the maximal probability of reaching the already computed qualitative winning set. In contrast with finite-state models, we show that such a computation only gives a lower bound on the maximal probability where the gap can be non-zero. In this paper we focus on approximating the qualitative winning set, while pointing out that the existing approaches for unbounded reachability computation can solve the second step. We provide an abstraction-based technique to approximate the qualitative winning set by simultaneously using an over- and under-approximation of the probabilistic transition relation. Since we are interested in qualitative properties, the abstraction is non-probabilistic; instead, the probabilistic transitions are assumed to be under the control of a (fair) adversary. Thus, we reduce the original policy synthesis problem to a Büchi game under a fairness assumption and characterize upper and lower bounds on winning sets as nested fixed point expressions in the $μ$-calculus. This characterization immediately provides a symbolic algorithm scheme. Further, a winning strategy computed on the abstract game can be refined to a policy on the controlled Markov process. We describe a concrete abstraction procedure and demonstrate our algorithm on two case studies.

0 citations0 reviewsNo code linkedOpen access
preprint2019arXiv

Perception-in-the-Loop Adversarial Examples

We present a scalable, black box, perception-in-the-loop technique to find adversarial examples for deep neural network classifiers. Black box means that our procedure only has input-output access to the classifier, and not to the internal structure, parameters, or intermediate confidence values. Perception-in-the-loop means that the notion of proximity between inputs can be directly queried from human participants rather than an arbitrarily chosen metric. Our technique is based on covariance matrix adaptation evolution strategy (CMA-ES), a black box optimization approach. CMA-ES explores the search space iteratively in a black box manner, by generating populations of candidates according to a distribution, choosing the best candidates according to a cost function, and updating the posterior distribution to favor the best candidates. We run CMA-ES using human participants to provide the fitness function, using the insight that the choice of best candidates in CMA-ES can be naturally modeled as a perception task: pick the top $k$ inputs perceptually closest to a fixed input. We empirically demonstrate that finding adversarial examples is feasible using small populations and few iterations. We compare the performance of CMA-ES on the MNIST benchmark with other black-box approaches using $L_p$ norms as a cost function, and show that it performs favorably both in terms of success in finding adversarial examples and in minimizing the distance between the original and the adversarial input. In experiments on the MNIST, CIFAR10, and GTSRB benchmarks, we demonstrate that CMA-ES can find perceptually similar adversarial inputs with a small number of iterations and small population sizes when using perception-in-the-loop. Finally, we show that networks trained specifically to be robust against $L_\infty$ norm can still be susceptible to perceptually similar adversarial examples.

0 citations0 reviewsNo code linkedOpen access