Showing 1–50 of 51 results for author: Smolka, S

KATch: A Fast Symbolic Verifier for NetKAT

Authors: Mark Moeller, Jules Jacobs, Olivier Savary Belanger, David Darais, Cole Schlesinger, Steffen Smolka, Nate Foster, Alexandra Silva

Abstract: We develop new data structures and algorithms for checking verification queries in NetKAT, a domain-specific language for specifying the behavior of network data planes. Our results extend the techniques obtained in prior work on symbolic automata and provide a framework for building efficient and scalable verification tools. We present KATch, an implementation of these ideas in Scala, featuring a… ▽ More We develop new data structures and algorithms for checking verification queries in NetKAT, a domain-specific language for specifying the behavior of network data planes. Our results extend the techniques obtained in prior work on symbolic automata and provide a framework for building efficient and scalable verification tools. We present KATch, an implementation of these ideas in Scala, featuring an extended set of NetKAT operators that are useful for expressing network-wide specifications, and a verification engine that constructs a bisimulation or generates a counter-example showing that none exists. We evaluate the performance of our implementation on real-world and synthetic benchmarks, verifying properties such as reachability and slice isolation, typically returning a result in well under a second, which is orders of magnitude faster than previous approaches. Our advancements underscore NetKAT's potential as a practical, declarative language for network specification and verification. △ Less

Submitted 21 June, 2024; v1 submitted 6 April, 2024; originally announced April 2024.

Fuzz on the Beach: Fuzzing Solana Smart Contracts

Authors: Sven Smolka, Jens-Rene Giesen, Pascal Winkler, Oussama Draissi, Lucas Davi, Ghassan Karame, Klaus Pohl

Abstract: Solana has quickly emerged as a popular platform for building decentralized applications (DApps), such as marketplaces for non-fungible tokens (NFTs). A key reason for its success are Solana's low transaction fees and high performance, which is achieved in part due to its stateless programming model. Although the literature features extensive tooling support for smart contract security, current so… ▽ More Solana has quickly emerged as a popular platform for building decentralized applications (DApps), such as marketplaces for non-fungible tokens (NFTs). A key reason for its success are Solana's low transaction fees and high performance, which is achieved in part due to its stateless programming model. Although the literature features extensive tooling support for smart contract security, current solutions are largely tailored for the Ethereum Virtual Machine. Unfortunately, the very stateless nature of Solana's execution environment introduces novel attack patterns specific to Solana requiring a rethinking for building vulnerability analysis methods. In this paper, we address this gap and propose FuzzDelSol, the first binary-only coverage-guided fuzzing architecture for Solana smart contracts. FuzzDelSol faithfully models runtime specifics such as smart contract interactions. Moreover, since source code is not available for the large majority of Solana contracts, FuzzDelSol operates on the contract's binary code. Hence, due to the lack of semantic information, we carefully extracted low-level program and state information to develop a diverse set of bug oracles covering all major bug classes in Solana. Our extensive evaluation on 6049 smart contracts shows that FuzzDelSol's bug oracles find bugs with a high precision and recall. To the best of our knowledge, this is the largest evaluation of the security landscape on the Solana mainnet. △ Less

Submitted 4 October, 2023; v1 submitted 6 September, 2023; originally announced September 2023.

Comments: This paper will appear on the ACM CCS 2023 in November 2023

An STL-based Approach to Resilient Control for Cyber-Physical Systems

Authors: Hongkai Chen, Scott A. Smolka, Nicola Paoletti, Shan Lin

Abstract: We present ResilienC, a framework for resilient control of Cyber-Physical Systems subject to STL-based requirements. ResilienC utilizes a recently developed formalism for specifying CPS resiliency in terms of sets of $(\mathit{rec},\mathit{dur})$ real-valued pairs, where $\mathit{rec}$ represents the system's capability to rapidly recover from a property violation (recoverability), and… ▽ More We present ResilienC, a framework for resilient control of Cyber-Physical Systems subject to STL-based requirements. ResilienC utilizes a recently developed formalism for specifying CPS resiliency in terms of sets of $(\mathit{rec},\mathit{dur})$ real-valued pairs, where $\mathit{rec}$ represents the system's capability to rapidly recover from a property violation (recoverability), and $\mathit{dur}$ is reflective of its ability to avoid violations post-recovery (durability). We define the resilient STL control problem as one of multi-objective optimization, where the recoverability and durability of the desired STL specification are maximized. When neither objective is prioritized over the other, the solution to the problem is a set of Pareto-optimal system trajectories. We present a precise solution method to the resilient STL control problem using a mixed-integer linear programming encoding and an a posteriori $ε$-constraint approach for efficiently retrieving the complete set of optimally resilient solutions. In ResilienC, at each time-step, the optimal control action selected from the set of Pareto-optimal solutions by a Decision Maker strategy realizes a form of Model Predictive Control. We demonstrate the practical utility of the ResilienC framework on two significant case studies: autonomous vehicle lane kee** and deadline-driven, multi-region package delivery. △ Less

Submitted 4 November, 2022; originally announced November 2022.

Comments: 11 pages, 6 figures

UMLsec4Edge: Extending UMLsec to model data-protection-compliant edge computing systems

Authors: Sven Smolka, Jan Laufer, Zoltán Ádám Mann, Klaus Pohl

Abstract: Edge computing enables the processing of data - frequently personal data - at the edge of the network. For personal data, legislation such as the European General Data Protection Regulation requires data protection by design. Hence, data protection has to be accounted for in the design of edge computing systems whenever personal data is involved. This leads to specific requirements for modeling th… ▽ More Edge computing enables the processing of data - frequently personal data - at the edge of the network. For personal data, legislation such as the European General Data Protection Regulation requires data protection by design. Hence, data protection has to be accounted for in the design of edge computing systems whenever personal data is involved. This leads to specific requirements for modeling the architecture of edge computing systems, e.g., representation of data and network properties. To the best of our knowledge, no existing modeling language fulfils all these requirements. In our previous work we showed that the commonly used UML profile UMLsec fulfils some of these requirements, and can thus serve as a starting point. The aim of this paper is to create a modeling language which meets all requirements concerning the design of the architecture of edge computing systems accounting for data protection. Thus, we extend UMLsec to satisfy all requirements. We call the resulting UML profile UMLsec4Edge. We follow a systematic approach to develop UMLsec4Edge. We apply UMLsec4Edge to real-world use cases from different domains, and create appropriate deployment diagrams and class diagrams. These diagrams show UMLsec4Edge is capable of meeting the requirements. △ Less

Submitted 17 October, 2022; originally announced October 2022.

Comments: 8 pages, 4 figures, 2 tables, published at the 48th Euromicro Conference Series on Software Engineering and Advanced Applications (SEAA)

An STL-based Formulation of Resilience in Cyber-Physical Systems

Authors: Hongkai Chen, Shan Lin, Scott A. Smolka, Nicola Paoletti

Abstract: Resiliency is the ability to quickly recover from a violation and avoid future violations for as long as possible. Such a property is of fundamental importance for Cyber-Physical Systems (CPS), and yet, to date, there is no widely agreed-upon formal treatment of CPS resiliency. We present an STL-based framework for reasoning about resiliency in CPS in which resiliency has a syntactic characterizat… ▽ More Resiliency is the ability to quickly recover from a violation and avoid future violations for as long as possible. Such a property is of fundamental importance for Cyber-Physical Systems (CPS), and yet, to date, there is no widely agreed-upon formal treatment of CPS resiliency. We present an STL-based framework for reasoning about resiliency in CPS in which resiliency has a syntactic characterization in the form of an STL-based Resiliency Specification (SRS). Given an arbitrary STL formula $\varphi$, time bounds $α$ and $β$, the SRS of $\varphi$, $R_{α,β}(\varphi)$, is the STL formula $\neg\varphi\mathbf{U}_{[0,α]}\mathbf{G}_{[0,β)}\varphi$, specifying that recovery from a violation of $\varphi$ occur within time $α$ (recoverability), and subsequently that $\varphi$ be maintained for duration $β$ (durability). These $R$-expressions, which are atoms in our SRS logic, can be combined using STL operators, allowing one to express composite resiliency specifications, e.g., multiple SRSs must hold simultaneously, or the system must eventually be resilient. We define a quantitative semantics for SRSs in the form of a Resilience Satisfaction Value (ReSV) function $r$ and prove its soundness and completeness w.r.t. STL's Boolean semantics. The $r$-value for $R_{α,β}(\varphi)$ atoms is a singleton set containing a pair quantifying recoverability and durability. The $r$-value for a composite SRS formula results in a set of non-dominated recoverability-durability pairs, given that the ReSVs of subformulas might not be directly comparable (e.g., one subformula has superior durability but worse recoverability than another). To the best of our knowledge, this is the first multi-dimensional quantitative semantics for an STL-based logic. Two case studies demonstrate the practical utility of our approach. △ Less

Submitted 18 July, 2022; v1 submitted 8 May, 2022; originally announced May 2022.

Comments: 16 pages excluding references and appendix (23 pages in total), 6 figures

ACM Class: F.4.1

Multi-Agent Spatial Predictive Control with Application to Drone Flocking (Extended Version)

Authors: Andreas Brandstätter, Scott A. Smolka, Scott D. Stoller, Ashish Tiwari, Radu Grosu

Abstract: We introduce the novel concept of Spatial Predictive Control (SPC) to solve the following problem: given a collection of agents (e.g., drones) with positional low-level controllers (LLCs) and a mission-specific distributed cost function, how can a distributed controller achieve and maintain cost-function minimization without a plant model and only positional observations of the environment? Our fu… ▽ More We introduce the novel concept of Spatial Predictive Control (SPC) to solve the following problem: given a collection of agents (e.g., drones) with positional low-level controllers (LLCs) and a mission-specific distributed cost function, how can a distributed controller achieve and maintain cost-function minimization without a plant model and only positional observations of the environment? Our fully distributed SPC controller is based strictly on the position of the agent itself and on those of its neighboring agents. This information is used in every time-step to compute the gradient of the cost function and to perform a spatial look-ahead to predict the best next target position for the LLC. Using a high-fidelity simulation environment, we show that SPC outperforms the most closely related class of controllers, Potential Field Controllers, on the drone flocking problem. We also show that SPC is able to cope with a potential sim-to-real transfer gap by demonstrating its performance on real hardware, namely our implementation of flocking using nine Crazyflie 2.1 drones. △ Less

Submitted 31 March, 2022; originally announced March 2022.

A Barrier Certificate-based Simplex Architecture with Application to Microgrids

Authors: Amol Damare, Shouvik Roy, Scott A. Smolka, Scott D. Stoller

Abstract: We present Barrier Certificate-based Simplex (BC-Simplex), a new, provably correct design for runtime assurance of continuous dynamical systems. BC-Simplex is centered around the Simplex Control Architecture, which consists of a high-performance advanced controller which is not guaranteed to maintain safety of the plant, a verified-safe baseline controller, and a decision module that switches cont… ▽ More We present Barrier Certificate-based Simplex (BC-Simplex), a new, provably correct design for runtime assurance of continuous dynamical systems. BC-Simplex is centered around the Simplex Control Architecture, which consists of a high-performance advanced controller which is not guaranteed to maintain safety of the plant, a verified-safe baseline controller, and a decision module that switches control of the plant between the two controllers to ensure safety without sacrificing performance. In BC-Simplex, Barrier certificates are used to prove that the baseline controller ensures safety. Furthermore, BC-Simplex features a new automated method for deriving, from the barrier certificate, the conditions for switching between the controllers. Our method is based on the Taylor expansion of the barrier certificate and yields computationally inexpensive switching conditions. We consider a significant application of BC-Simplex to a microgrid featuring an advanced controller in the form of a neural network trained using reinforcement learning. The microgrid is modeled in RTDS, an industry-standard high-fidelity, real-time power systems simulator. Our results demonstrate that BC-Simplex can automatically derive switching conditions for complex systems, the switching conditions are not overly conservative, and BC-Simplex ensures safety even in the presence of adversarial attacks on the neural controller. △ Less

Submitted 2 June, 2022; v1 submitted 19 February, 2022; originally announced February 2022.

GoTube: Scalable Stochastic Verification of Continuous-Depth Models

Authors: Sophie Gruenbacher, Mathias Lechner, Ramin Hasani, Daniela Rus, Thomas A. Henzinger, Scott Smolka, Radu Grosu

Abstract: We introduce a new stochastic verification algorithm that formally quantifies the behavioral robustness of any time-continuous process formulated as a continuous-depth model. Our algorithm solves a set of global optimization (Go) problems over a given time horizon to construct a tight enclosure (Tube) of the set of all process executions starting from a ball of initial states. We call our algorith… ▽ More We introduce a new stochastic verification algorithm that formally quantifies the behavioral robustness of any time-continuous process formulated as a continuous-depth model. Our algorithm solves a set of global optimization (Go) problems over a given time horizon to construct a tight enclosure (Tube) of the set of all process executions starting from a ball of initial states. We call our algorithm GoTube. Through its construction, GoTube ensures that the bounding tube is conservative up to a desired probability and up to a desired tightness. GoTube is implemented in JAX and optimized to scale to complex continuous-depth neural network models. Compared to advanced reachability analysis tools for time-continuous neural networks, GoTube does not accumulate overapproximation errors between time steps and avoids the infamous wrap** effect inherent in symbolic techniques. We show that GoTube substantially outperforms state-of-the-art verification tools in terms of the size of the initial ball, speed, time-horizon, task completion, and scalability on a large set of experiments. GoTube is stable and sets the state-of-the-art in terms of its ability to scale to time horizons well beyond what has been previously possible. △ Less

Submitted 2 December, 2021; v1 submitted 18 July, 2021; originally announced July 2021.

Comments: Accepted to the Thirty-Sixth AAAI Conference on Artificial Intelligence (AAAI-22)

The Black-Box Simplex Architecture for Runtime Assurance of Autonomous CPS

Authors: Usama Mehmood, Sanaz Sheikhi, Stanley Bak, Scott A. Smolka, Scott D. Stoller

Abstract: The Simplex Architecture is a runtime assurance framework where control authority may switch from an unverified and potentially unsafe advanced controller to a backup baseline controller in order to maintain the safety of an autonomous cyber-physical system. In this work, we show that runtime checks can replace the requirement to statically verify safety of the baseline controller. This is importa… ▽ More The Simplex Architecture is a runtime assurance framework where control authority may switch from an unverified and potentially unsafe advanced controller to a backup baseline controller in order to maintain the safety of an autonomous cyber-physical system. In this work, we show that runtime checks can replace the requirement to statically verify safety of the baseline controller. This is important as there are many powerful control techniques, such as model-predictive control and neural network controllers, that work well in practice but are difficult to statically verify. Since the method does not use internal information about the advanced or baseline controller, we call the approach the Black-Box Simplex Architecture. We prove the architecture is safe and present two case studies where (i) model-predictive control provides safe multi-robot coordination, and (ii) neural networks provably prevent collisions in groups of F-16 aircraft, despite the controllers occasionally outputting unsafe commands. △ Less

Submitted 31 May, 2022; v1 submitted 24 February, 2021; originally announced February 2021.

Journal ref: NASA Formal Methods (2022) 231-250

A Distributed Simplex Architecture for Multi-Agent Systems

Authors: Usama Mehmood, Scott D. Stoller, Radu Grosu, Shouvik Roy, Amol Damare, Scott A. Smolka

Abstract: We present Distributed Simplex Architecture (DSA), a new runtime assurance technique that provides safety guarantees for multi-agent systems (MASs). DSA is inspired by the Simplex control architecture of Sha et al., but with some significant differences. The traditional Simplex approach is limited to single-agent systems or a MAS with a centralized control scheme. DSA addresses this limitation by… ▽ More We present Distributed Simplex Architecture (DSA), a new runtime assurance technique that provides safety guarantees for multi-agent systems (MASs). DSA is inspired by the Simplex control architecture of Sha et al., but with some significant differences. The traditional Simplex approach is limited to single-agent systems or a MAS with a centralized control scheme. DSA addresses this limitation by extending the scope of Simplex to include MASs under distributed control. In DSA, each agent has a local instance of traditional Simplex such that the preservation of safety in the local instances implies safety for the entire MAS. We provide a proof of safety for DSA, and present experimental results for several case studies, including flocking with collision avoidance, safe navigation of ground rovers through way-points, and the safe operation of a microgrid. △ Less

Submitted 18 December, 2020; originally announced December 2020.

On The Verification of Neural ODEs with Stochastic Guarantees

Authors: Sophie Gruenbacher, Ramin Hasani, Mathias Lechner, Jacek Cyranka, Scott A. Smolka, Radu Grosu

Abstract: We show that Neural ODEs, an emerging class of time-continuous neural networks, can be verified by solving a set of global-optimization problems. For this purpose, we introduce Stochastic Lagrangian Reachability (SLR), an abstraction-based technique for constructing a tight Reachtube (an over-approximation of the set of reachable states over a given time-horizon), and provide stochastic guarantees… ▽ More We show that Neural ODEs, an emerging class of time-continuous neural networks, can be verified by solving a set of global-optimization problems. For this purpose, we introduce Stochastic Lagrangian Reachability (SLR), an abstraction-based technique for constructing a tight Reachtube (an over-approximation of the set of reachable states over a given time-horizon), and provide stochastic guarantees in the form of confidence intervals for the Reachtube bounds. SLR inherently avoids the infamous wrap** effect (accumulation of over-approximation errors) by performing local optimization steps to expand safe regions instead of repeatedly forward-propagating them as is done by deterministic reachability methods. To enable fast local optimizations, we introduce a novel forward-mode adjoint sensitivity method to compute gradients without the need for backpropagation. Finally, we establish asymptotic and non-asymptotic convergence rates for SLR. △ Less

Submitted 16 December, 2020; originally announced December 2020.

Comments: 12 pages, 2 figures

Journal ref: Proceedings of the AAAI Conference on Artificial Intelligence, 35(13), 2021, pages 11525-11535

Lagrangian Reachtubes: The Next Generation

Authors: Sophie Gruenbacher, Jacek Cyranka, Mathias Lechner, Md. Ariful Islam, Scott A. Smolka, Radu Grosu

Abstract: We introduce LRT-NG, a set of techniques and an associated toolset that computes a reachtube (an over-approximation of the set of reachable states over a given time horizon) of a nonlinear dynamical system. LRT-NG significantly advances the state-of-the-art Langrangian Reachability and its associated tool LRT. From a theoretical perspective, LRT-NG is superior to LRT in three ways. First, it uses… ▽ More We introduce LRT-NG, a set of techniques and an associated toolset that computes a reachtube (an over-approximation of the set of reachable states over a given time horizon) of a nonlinear dynamical system. LRT-NG significantly advances the state-of-the-art Langrangian Reachability and its associated tool LRT. From a theoretical perspective, LRT-NG is superior to LRT in three ways. First, it uses for the first time an analytically computed metric for the propagated ball which is proven to minimize the ball's volume. We emphasize that the metric computation is the centerpiece of all bloating-based techniques. Secondly, it computes the next reachset as the intersection of two balls: one based on the Cartesian metric and the other on the new metric. While the two metrics were previously considered opposing approaches, their joint use considerably tightens the reachtubes. Thirdly, it avoids the "wrap** effect" associated with the validated integration of the center of the reachset, by optimally absorbing the interval approximation in the radius of the next ball. From a tool-development perspective, LRT-NG is superior to LRT in two ways. First, it is a standalone tool that no longer relies on CAPD. This required the implementation of the Lohner method and a Runge-Kutta time-propagation method. Secondly, it has an improved interface, allowing the input model and initial conditions to be provided as external input files. Our experiments on a comprehensive set of benchmarks, including two Neural ODEs, demonstrates LRT-NG's superior performance compared to LRT, CAPD, and Flow*. △ Less

Submitted 14 December, 2020; originally announced December 2020.

Comments: 12 pages, 14 figures

Journal ref: Proceedings of the 59th IEEE Conference on Decision and Control (CDC), 2020, pages 1556-1563

Learning Distributed Controllers for V-Formation

Authors: Shouvik Roy, Usama Mehmood, Radu Grosu, Scott A. Smolka, Scott D. Stoller, Ashish Tiwari

Abstract: We show how a high-performing, fully distributed and symmetric neural V-formation controller can be synthesized from a Centralized MPC (Model Predictive Control) controller using Deep Learning. This result is significant as we also establish that under very reasonable conditions, it is impossible to achieve V-formation using a deterministic, distributed, and symmetric controller. The learning proc… ▽ More We show how a high-performing, fully distributed and symmetric neural V-formation controller can be synthesized from a Centralized MPC (Model Predictive Control) controller using Deep Learning. This result is significant as we also establish that under very reasonable conditions, it is impossible to achieve V-formation using a deterministic, distributed, and symmetric controller. The learning process we use for the neural V-formation controller is significantly enhanced by CEGkR, a Counterexample-Guided k-fold Retraining technique we introduce, which extends prior work in this direction in important ways. Our experimental results show that our neural V-formation controller generalizes to a significantly larger number of agents than for which it was trained (from 7 to 15), and exhibits substantial speedup over the MPC-based controller. We use a form of statistical model checking to compute confidence intervals for our neural V-formation controller's convergence rate and time to convergence. △ Less

Submitted 31 May, 2020; originally announced June 2020.

MPC-guided Imitation Learning of Neural Network Policies for the Artificial Pancreas

Authors: Hongkai Chen, Nicola Paoletti, Scott A. Smolka, Shan Lin

Abstract: Even though model predictive control (MPC) is currently the main algorithm for insulin control in the artificial pancreas (AP), it usually requires complex online optimizations, which are infeasible for resource-constrained medical devices. MPC also typically relies on state estimation, an error-prone process. In this paper, we introduce a novel approach to AP control that uses Imitation Learning… ▽ More Even though model predictive control (MPC) is currently the main algorithm for insulin control in the artificial pancreas (AP), it usually requires complex online optimizations, which are infeasible for resource-constrained medical devices. MPC also typically relies on state estimation, an error-prone process. In this paper, we introduce a novel approach to AP control that uses Imitation Learning to synthesize neural-network insulin policies from MPC-computed demonstrations. Such policies are computationally efficient and, by instrumenting MPC at training time with full state information, they can directly map measurements into optimal therapy decisions, thus bypassing state estimation. We apply Bayesian inference via Monte Carlo Dropout to learn policies, which allows us to quantify prediction uncertainty and thereby derive safer therapy decisions. We show that our control policies trained under a specific patient model readily generalize (in terms of model parameters and disturbance distributions) to patient cohorts, consistently outperforming traditional MPC with state estimation. △ Less

Submitted 2 March, 2020; originally announced March 2020.

V-Formation via Model Predictive Control

Authors: Radu Grosu, Anna Lukina, Scott A. Smolka, Ashish Tiwari, Vasudha Varadarajan, Xingfang Wang

Abstract: We present recent results that demonstrate the power of viewing the problem of V-formation in a flock of birds as one of Model Predictive Control (MPC). The V-formation-MPC marriage can be understood in terms of the problem of synthesizing an optimal plan for a continuous-space and continuous-time Markov decision process (MDP), where the goal is to reach a target state that minimizes a given cost… ▽ More We present recent results that demonstrate the power of viewing the problem of V-formation in a flock of birds as one of Model Predictive Control (MPC). The V-formation-MPC marriage can be understood in terms of the problem of synthesizing an optimal plan for a continuous-space and continuous-time Markov decision process (MDP), where the goal is to reach a target state that minimizes a given cost function. First, we consider ARES, an approximation algorithm for generating optimal plans (action sequences) that take an initial state of an MDP to a state whose cost is below a specified (convergence) threshold. ARES uses Particle Swarm Optimization, with adaptive sizing for both the receding horizon and the particle swarm. Inspired by Importance Splitting, the length of the horizon and the number of particles are chosen such that at least one particle reaches a next-level state. ARES can alternatively be viewed as a model-predictive control (MPC) algorithm that utilizes an adaptive receding horizon, aka Adaptive MPC (AMPC). We next present Distributed AMPC (DAMPC), a distributed version of AMPC that works with local neighborhoods. We introduce adaptive neighborhood resizing, whereby the neighborhood size is determined by the cost-based Lyapunov function evaluated over a global system state. Our experiments show that DAMPC can perform almost as well as centralized AMPC, while using only local information and a form of distributed consensus in each time step. Finally, inspired by security attacks on cyber-physical systems, we introduce controller-attacker games (CAG), where two players, a controller and an attacker, have antagonistic objectives. We formulate a special case of CAG called V-formation games, where the attacker's goal is to prevent the controller from attaining V-formation. We demonstrate how adaptation in the design of the controller helps in overcoming certain attacks. △ Less

Submitted 19 February, 2020; originally announced February 2020.

Comments: arXiv admin note: text overlap with arXiv:1612.07059, arXiv:1805.07929, arXiv:1702.00290

Neural Flocking: MPC-based Supervised Learning of Flocking Controllers

Authors: Shouvik Roy, Usama Mehmood, Radu Grosu, Scott A. Smolka, Scott D. Stoller, Ashish Tiwari

Abstract: We show how a distributed flocking controller can be synthesized using deep learning from a centralized controller which generates the trajectories of the flock. Our approach is based on supervised learning, with the centralized controller providing the training data to the learning agent, i.e., the synthesized distributed controller. We use Model Predictive Control (MPC) for the centralized contr… ▽ More We show how a distributed flocking controller can be synthesized using deep learning from a centralized controller which generates the trajectories of the flock. Our approach is based on supervised learning, with the centralized controller providing the training data to the learning agent, i.e., the synthesized distributed controller. We use Model Predictive Control (MPC) for the centralized controller, an approach that has been successfully demonstrated on flocking problems. MPC-based flocking controllers are high-performing but also computationally expensive. By learning a symmetric distributed neural flocking controller from a centralized MPC-based flocking controller, we achieve the best of both worlds: the neural controllers have high performance (on par with the MPC controllers) and high efficiency. Our experimental results demonstrate the sophisticated nature of the distributed controllers we learn. In particular, the neural controllers are capable of achieving myriad flocking-oriented control objectives, including flocking formation, collision avoidance, obstacle avoidance, predator avoidance, and target seeking. Moreover, they generalize the behavior seen in the training data in order to achieve these objectives in a significantly broader range of scenarios. △ Less

Submitted 17 January, 2020; v1 submitted 26 August, 2019; originally announced August 2019.

Comments: This is an updated version of our previous submission. The updated version includes an additional section of experiments using quadrotors

Neural Simplex Architecture

Authors: Dung T. Phan, Radu Grosu, Nils Jansen, Nicola Paoletti, Scott A. Smolka, Scott D. Stoller

Abstract: We present the Neural Simplex Architecture (NSA), a new approach to runtime assurance that provides safety guarantees for neural controllers (obtained e.g. using reinforcement learning) of autonomous and other complex systems without unduly sacrificing performance. NSA is inspired by the Simplex control architecture of Sha et al., but with some significant differences. In the traditional approach,… ▽ More We present the Neural Simplex Architecture (NSA), a new approach to runtime assurance that provides safety guarantees for neural controllers (obtained e.g. using reinforcement learning) of autonomous and other complex systems without unduly sacrificing performance. NSA is inspired by the Simplex control architecture of Sha et al., but with some significant differences. In the traditional approach, the advanced controller (AC) is treated as a black box; when the decision module switches control to the baseline controller (BC), the BC remains in control forever. There is relatively little work on switching control back to the AC, and there are no techniques for correcting the AC's behavior after it generates a potentially unsafe control input that causes a failover to the BC. Our NSA addresses both of these limitations. NSA not only provides safety assurances in the presence of a possibly unsafe neural controller, but can also improve the safety of such a controller in an online setting via retraining, without overly degrading its performance. To demonstrate NSA's benefits, we have conducted several significant case studies in the continuous control domain. These include a target-seeking ground rover navigating an obstacle field, and a neural controller for an artificial pancreas system. △ Less

Submitted 24 March, 2020; v1 submitted 1 August, 2019; originally announced August 2019.

Comments: 12th NASA Formal Methods Symposium (NFM 2020)

Guarded Kleene Algebra with Tests: Verification of Uninterpreted Programs in Nearly Linear Time

Authors: Steffen Smolka, Nate Foster, Justin Hsu, Tobias Kappé, Dexter Kozen, Alexandra Silva

Abstract: Guarded Kleene Algebra with Tests (GKAT) is a variation on Kleene Algebra with Tests (KAT) that arises by restricting the union ($+$) and iteration ($*$) operations from KAT to predicate-guarded versions. We develop the (co)algebraic theory of GKAT and show how it can be efficiently used to reason about imperative programs. In contrast to KAT, whose equational theory is PSPACE-complete, we show th… ▽ More Guarded Kleene Algebra with Tests (GKAT) is a variation on Kleene Algebra with Tests (KAT) that arises by restricting the union ($+$) and iteration ($*$) operations from KAT to predicate-guarded versions. We develop the (co)algebraic theory of GKAT and show how it can be efficiently used to reason about imperative programs. In contrast to KAT, whose equational theory is PSPACE-complete, we show that the equational theory of GKAT is (almost) linear time. We also provide a full Kleene theorem and prove completeness for an analogue of Salomaa's axiomatization of Kleene Algebra. △ Less

Submitted 13 December, 2019; v1 submitted 12 July, 2019; originally announced July 2019.

Comments: Extended version with appendix

Journal ref: Proc. POPL 2020, pp 61:1-61:28

Scalable Verification of Probabilistic Networks

Authors: Steffen Smolka, Praveen Kumar, David M Kahn, Nate Foster, Justin Hsu, Dexter Kozen, Alexandra Silva

Abstract: This paper presents McNetKAT, a scalable tool for verifying probabilistic network programs. McNetKAT is based on a new semantics for the guarded and history-free fragment of Probabilistic NetKAT in terms of finite-state, absorbing Markov chains. This view allows the semantics of all programs to be computed exactly, enabling construction of an automatic verification tool. Domain-specific optimizati… ▽ More This paper presents McNetKAT, a scalable tool for verifying probabilistic network programs. McNetKAT is based on a new semantics for the guarded and history-free fragment of Probabilistic NetKAT in terms of finite-state, absorbing Markov chains. This view allows the semantics of all programs to be computed exactly, enabling construction of an automatic verification tool. Domain-specific optimizations and a parallelizing backend enable McNetKAT to analyze networks with thousands of nodes, automatically reasoning about general properties such as probabilistic program equivalence and refinement, as well as networking properties such as resilience to failures. We evaluate McNetKAT's scalability using real-world topologies, compare its performance against state-of-the-art tools, and develop an extended case study on a recently proposed data center network design. △ Less

Submitted 17 April, 2019; originally announced April 2019.

Comments: extended version with appendix

Journal ref: In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI '19), June 22-26, 2019, Phoenix, AZ, USA. ACM, New York, NY, USA

Automated Synthesis of Safe Digital Controllers for Sampled-Data Stochastic Nonlinear Systems

Authors: Fedor Shmarov, Sadegh Soudjani, Nicola Paoletti, Ezio Bartocci, Shan Lin, Scott A. Smolka, Paolo Zuliani

Abstract: We present a new method for the automated synthesis of digital controllers with formal safety guarantees for systems with nonlinear dynamics, noisy output measurements, and stochastic disturbances. Our method derives digital controllers such that the corresponding closed-loop system, modeled as a sampled-data stochastic control system, satisfies a safety specification with probability above a give… ▽ More We present a new method for the automated synthesis of digital controllers with formal safety guarantees for systems with nonlinear dynamics, noisy output measurements, and stochastic disturbances. Our method derives digital controllers such that the corresponding closed-loop system, modeled as a sampled-data stochastic control system, satisfies a safety specification with probability above a given threshold. The proposed synthesis method alternates between two steps: generation of a candidate controller pc, and verification of the candidate. pc is found by maximizing a Monte Carlo estimate of the safety probability, and by using a non-validated ODE solver for simulating the system. Such a candidate is therefore sub-optimal but can be generated very rapidly. To rule out unstable candidate controllers, we prove and utilize Lyapunov's indirect method for instability of sampled-data nonlinear systems. In the subsequent verification step, we use a validated solver based on SMT (Satisfiability Modulo Theories) to compute a numerically and statistically valid confidence interval for the safety probability of pc. If the probability so obtained is not above the threshold, we expand the search space for candidates by increasing the controller degree. We evaluate our technique on three case studies: an artificial pancreas model, a powertrain control model, and a quadruple-tank process. △ Less

Submitted 10 January, 2019; originally announced January 2019.

Comments: 12 pages, 4 figures, 4 tables

MSC Class: 68N30

Synthesizing Stealthy Reprogramming Attacks on Cardiac Devices

Authors: Nicola Paoletti, Zhihao Jiang, Md Ariful Islam, Houssam Abbas, Rahul Mangharam, Shan Lin, Zachary Gruber, Scott A. Smolka

Abstract: An Implantable Cardioverter Defibrillator (ICD) is a medical device used for the detection of potentially fatal cardiac arrhythmia and their treatment through the delivery of electrical shocks intended to restore normal heart rhythm. An ICD reprogramming attack seeks to alter the device's parameters to induce unnecessary shocks and, even more egregious, prevent required therapy. In this paper, we… ▽ More An Implantable Cardioverter Defibrillator (ICD) is a medical device used for the detection of potentially fatal cardiac arrhythmia and their treatment through the delivery of electrical shocks intended to restore normal heart rhythm. An ICD reprogramming attack seeks to alter the device's parameters to induce unnecessary shocks and, even more egregious, prevent required therapy. In this paper, we present a formal approach for the synthesis of ICD reprogramming attacks that are both effective, i.e., lead to fundamental changes in the required therapy, and stealthy, i.e., involve minimal changes to the nominal ICD parameters. We focus on the discrimination algorithm underlying Boston Scientific devices (one of the principal ICD manufacturers) and formulate the synthesis problem as one of multi-objective optimization. Our solution technique is based on an Optimization Modulo Theories encoding of the problem and allows us to derive device parameters that are optimal with respect to the effectiveness-stealthiness tradeoff (i.e., lie along the corresponding Pareto front). To the best of our knowledge, our work is the first to derive systematic ICD reprogramming attacks designed to maximize therapy disruption while minimizing detection. To evaluate our technique, we employ an extensive dataset of synthetic EGMs (cardiac signals), each generated with a prescribed arrhythmia, allowing us to synthesize attacks tailored to the victim's cardiac condition. Our approach readily generalizes to unseen signals, representing the unknown EGM of the victim patient. △ Less

Submitted 9 October, 2018; originally announced October 2018.

Tight Continuous-Time Reachtubes for Lagrangian Reachability

Authors: Jacek Cyranka, Md. Ariful Islam, Scott A. Smolka, Sicun Gao, Radu Grosu

Abstract: We introduce continuous Lagrangian reachability (CLRT), a new algorithm for the computation of a tight and continuous-time reachtube for the solution flows of a nonlinear, time-variant dynamical system. CLRT employs finite strain theory to determine the deformation of the solution set from time $t_i$ to time $t_{i+1}$. We have developed simple explicit analytic formulas for the optimal metric for… ▽ More We introduce continuous Lagrangian reachability (CLRT), a new algorithm for the computation of a tight and continuous-time reachtube for the solution flows of a nonlinear, time-variant dynamical system. CLRT employs finite strain theory to determine the deformation of the solution set from time $t_i$ to time $t_{i+1}$. We have developed simple explicit analytic formulas for the optimal metric for this deformation; this is superior to prior work, which used semi-definite programming. CLRT also uses infinitesimal strain theory to derive an optimal time increment $h_i$ between $t_i$ and $t_{i+1}$, nonlinear optimization to minimally bloat (i.e., using a minimal radius) the state set at time $t_i$ such that it includes all the states of the solution flow in the interval $[t_i,t_{i+1}]$. We use $δ$-satisfiability to ensure the correctness of the bloating. Our results on a series of benchmarks show that CLRT performs favorably compared to state-of-the-art tools such as CAPD in terms of the continuous reachtube volumes they compute. △ Less

Submitted 24 September, 2018; v1 submitted 19 September, 2018; originally announced September 2018.

Neural State Classification for Hybrid Systems

Authors: Dung Phan, Nicola Paoletti, Timothy Zhang, Radu Grosu, Scott A. Smolka, Scott D. Stoller

Abstract: We introduce the State Classification Problem (SCP) for hybrid systems, and present Neural State Classification (NSC) as an efficient solution technique. SCP generalizes the model checking problem as it entails classifying each state $s$ of a hybrid automaton as either positive or negative, depending on whether or not $s$ satisfies a given time-bounded reachability specification. This is an intere… ▽ More We introduce the State Classification Problem (SCP) for hybrid systems, and present Neural State Classification (NSC) as an efficient solution technique. SCP generalizes the model checking problem as it entails classifying each state $s$ of a hybrid automaton as either positive or negative, depending on whether or not $s$ satisfies a given time-bounded reachability specification. This is an interesting problem in its own right, which NSC solves using machine-learning techniques, Deep Neural Networks in particular. State classifiers produced by NSC tend to be very efficient (run in constant time and space), but may be subject to classification errors. To quantify and mitigate such errors, our approach comprises: i) techniques for certifying, with statistical guarantees, that an NSC classifier meets given accuracy levels; ii) tuning techniques, including a novel technique based on adversarial sampling, that can virtually eliminate false negatives (positive states classified as negative), thereby making the classifier more conservative. We have applied NSC to six nonlinear hybrid system benchmarks, achieving an accuracy of 99.25% to 99.98%, and a false-negative rate of 0.0033 to 0, which we further reduced to 0.0015 to 0 after tuning the classifier. We believe that this level of accuracy is acceptable in many practical applications, and that these results demonstrate the promise of the NSC approach. △ Less

Submitted 25 July, 2018; originally announced July 2018.

Comments: ATVA2018 extended version

Adaptive Neighborhood Resizing for Stochastic Reachability in Multi-Agent Systems

Authors: Anna Lukina, Ashish Tiwari, Scott A. Smolka, Radu Grosu

Abstract: We present DAMPC, a distributed, adaptive-horizon and adaptive-neighborhood algorithm for solving the stochastic reachability problem in multi-agent systems, in particular flocking modeled as a Markov decision process. At each time step, every agent calls a centralized, adaptive-horizon model-predictive control (AMPC) algorithm to obtain an optimal solution for its local neighborhood. Second, the… ▽ More We present DAMPC, a distributed, adaptive-horizon and adaptive-neighborhood algorithm for solving the stochastic reachability problem in multi-agent systems, in particular flocking modeled as a Markov decision process. At each time step, every agent calls a centralized, adaptive-horizon model-predictive control (AMPC) algorithm to obtain an optimal solution for its local neighborhood. Second, the agents derive the flock-wide optimal solution through a sequence of consensus rounds. Third, the neighborhood is adaptively resized using a flock-wide, cost-based Lyapunov function V. This way DAMPC improves efficiency without compromising convergence. We evaluate DAMPC's performance using statistical model checking. Our results demonstrate that, compared to AMPC, DAMPC achieves considerable speed-up (two-fold in some cases) with only a slightly lower rate of convergence. The smaller average neighborhood size and lookahead horizon demonstrate the benefits of the DAMPC approach for stochastic reachability problems involving any controllable multi-agent system that possesses a cost function. △ Less

Submitted 21 May, 2018; originally announced May 2018.

Comments: submitted to conference ATVA 2018

How to Learn a Model Checker

Authors: Dung Phan, Radu Grosu, Nicola Paoletti, Scott A. Smolka, Scott D. Stoller

Abstract: We show how machine-learning techniques, particularly neural networks, offer a very effective and highly efficient solution to the approximate model-checking problem for continuous and hybrid systems, a solution where the general-purpose model checker is replaced by a model-specific classifier trained by sampling model trajectories. To the best of our knowledge, we are the first to establish this… ▽ More We show how machine-learning techniques, particularly neural networks, offer a very effective and highly efficient solution to the approximate model-checking problem for continuous and hybrid systems, a solution where the general-purpose model checker is replaced by a model-specific classifier trained by sampling model trajectories. To the best of our knowledge, we are the first to establish this link from machine learning to model checking. Our method comprises a pipeline of analysis techniques for estimating and obtaining statistical guarantees on the classifier's prediction performance, as well as tuning techniques to improve such performance. Our experimental evaluation considers the time-bounded reachability problem for three well-established benchmarks in the hybrid systems community. On these examples, we achieve an accuracy of 99.82% to 100% and a false-negative rate (incorrectly predicting that unsafe states are not reachable from a given state) of 0.0007 to 0. We believe that this level of accuracy is acceptable in many practical applications and we show how the approximate model checker can be made more conservative by tuning the classifier through further training and selection of the classification threshold. △ Less

Submitted 5 December, 2017; originally announced December 2017.

Comments: 16 pages, 13 figures, short version submitted to HSCC2018

Declarative vs Rule-based Control for Flocking Dynamics

Authors: Usama Mehmood, Nicola Paoletti, Dung Phan, Radu Grosu, Shan Lin, Scott D. Stoller, Ashish Tiwari, Junxing Yang, Scott A. Smolka

Abstract: The popularity of rule-based flocking models, such as Reynolds' classic flocking model, raises the question of whether more declarative flocking models are possible. This question is motivated by the observation that declarative models are generally simpler and easier to design, understand, and analyze than operational models. We introduce a very simple control law for flocking based on a cost fun… ▽ More The popularity of rule-based flocking models, such as Reynolds' classic flocking model, raises the question of whether more declarative flocking models are possible. This question is motivated by the observation that declarative models are generally simpler and easier to design, understand, and analyze than operational models. We introduce a very simple control law for flocking based on a cost function capturing cohesion (agents want to stay together) and separation (agents do not want to get too close). We refer to it as {\textit declarative flocking} (DF). We use model-predictive control (MPC) to define controllers for DF in centralized and distributed settings. A thorough performance comparison of our declarative flocking with Reynolds' model, and with more recent flocking models that use MPC with a cost function based on lattice structures, demonstrate that DF-MPC yields the best cohesion and least fragmentation, and maintains a surprisingly good level of geometric regularity while still producing natural flock shapes similar to those produced by Reynolds' model. We also show that DF-MPC has high resilience to sensor noise. △ Less

Submitted 27 October, 2017; originally announced October 2017.

Comments: 7 Pages

Automated Synthesis of Safe and Robust PID Controllers for Stochastic Hybrid Systems

Authors: Fedor Shmarov, Nicola Paoletti, Ezio Bartocci, Shan Lin, Scott A. Smolka, Paolo Zuliani

Abstract: We present a new method for the automated synthesis of safe and robust Proportional-Integral-Derivative (PID) controllers for stochastic hybrid systems. Despite their widespread use in industry, no automated method currently exists for deriving a PID controller (or any other type of controller, for that matter) with safety and performance guarantees for such a general class of systems. In particul… ▽ More We present a new method for the automated synthesis of safe and robust Proportional-Integral-Derivative (PID) controllers for stochastic hybrid systems. Despite their widespread use in industry, no automated method currently exists for deriving a PID controller (or any other type of controller, for that matter) with safety and performance guarantees for such a general class of systems. In particular, we consider hybrid systems with nonlinear dynamics (Lipschitz-continuous ordinary differential equations) and random parameters, and we synthesize PID controllers such that the resulting closed-loop systems satisfy safety and performance constraints given as probabilistic bounded reachability properties. Our technique leverages SMT solvers over the reals and nonlinear differential equations to provide formal guarantees that the synthesized controllers satisfy such properties. These controllers are also robust by design since they minimize the probability of reaching an unsafe state in the presence of random disturbances. We apply our approach to the problem of insulin regulation for type 1 diabetes, synthesizing controllers with robust responses to large random meal disturbances, thereby enabling them to maintain blood glucose levels within healthy, safe ranges. △ Less

Submitted 7 September, 2017; v1 submitted 17 July, 2017; originally announced July 2017.

Comments: Extended version of paper accepted at the 13th Haifa Verification Conference

Probabilistic Program Equivalence for NetKAT

Authors: Steffen Smolka, Praveen Kumar, Nate Foster, Justin Hsu, David Kahn, Dexter Kozen, Alexandra Silva

Abstract: We tackle the problem of deciding whether two probabilistic programs are equivalent in Probabilistic NetKAT, a formal language for specifying and reasoning about the behavior of packet-switched networks. We show that the problem is decidable for the history-free fragment of the language by develo** an effective decision procedure based on stochastic matrices. The main challenge lies in reasoning… ▽ More We tackle the problem of deciding whether two probabilistic programs are equivalent in Probabilistic NetKAT, a formal language for specifying and reasoning about the behavior of packet-switched networks. We show that the problem is decidable for the history-free fragment of the language by develo** an effective decision procedure based on stochastic matrices. The main challenge lies in reasoning about iteration, which we address by designing an encoding of the program semantics as a finite-state absorbing Markov chain, whose limiting distribution can be computed exactly. In an extended case study on a real-world data center network, we automatically verify various quantitative properties of interest, including resilience in the presence of failures, by analyzing the Markov chain semantics. △ Less

Submitted 24 March, 2018; v1 submitted 10 July, 2017; originally announced July 2017.

Data-Driven Robust Control for Type 1 Diabetes Under Meal and Exercise Uncertainties

Authors: Nicola Paoletti, Kin Sum Liu, Scott A. Smolka, Shan Lin

Abstract: We present a fully closed-loop design for an artificial pancreas (AP) which regulates the delivery of insulin for the control of Type I diabetes. Our AP controller operates in a fully automated fashion, without requiring any manual interaction (e.g. in the form of meal announcements) with the patient. A major obstacle to achieving closed-loop insulin control is the uncertainty in those aspects of… ▽ More We present a fully closed-loop design for an artificial pancreas (AP) which regulates the delivery of insulin for the control of Type I diabetes. Our AP controller operates in a fully automated fashion, without requiring any manual interaction (e.g. in the form of meal announcements) with the patient. A major obstacle to achieving closed-loop insulin control is the uncertainty in those aspects of a patient's daily behavior that significantly affect blood glucose, especially in relation to meals and physical activity. To handle such uncertainties, we develop a data-driven robust model-predictive control framework, where we capture a wide range of individual meal and exercise patterns using uncertainty sets learned from historical data. These sets are then used in the controller and state estimator to achieve automated, precise, and personalized insulin therapy. We provide an extensive in silico evaluation of our robust AP design, demonstrating the potential of this approach, without explicit meal announcements, to support high carbohydrate disturbances and to regulate glucose levels in large clusters of virtual patients learned from population-wide survey data. △ Less

Submitted 28 September, 2017; v1 submitted 7 July, 2017; originally announced July 2017.

Comments: Extended version of paper accepted at the 15th International Conference on Computational Methods in Systems Biology

Lagrangian Reachabililty

Authors: Jacek Cyranka, Md. Ariful Islam, Greg Byrne, Paul Jones, Scott A. Smolka, Radu Grosu

Abstract: We introduce LRT, a new Lagrangian-based ReachTube computation algorithm that conservatively approximates the set of reachable states of a nonlinear dynamical system. LRT makes use of the Cauchy-Green stretching factor (SF), which is derived from an over-approximation of the gradient of the solution flows. The SF measures the discrepancy between two states propagated by the system solution from tw… ▽ More We introduce LRT, a new Lagrangian-based ReachTube computation algorithm that conservatively approximates the set of reachable states of a nonlinear dynamical system. LRT makes use of the Cauchy-Green stretching factor (SF), which is derived from an over-approximation of the gradient of the solution flows. The SF measures the discrepancy between two states propagated by the system solution from two initial states lying in a well-defined region, thereby allowing LRT to compute a reachtube with a ball-overestimate in a metric where the computed enclosure is as tight as possible. To evaluate its performance, we implemented a prototype of LRT in C++/Matlab, and ran it on a set of well-established benchmarks. Our results show that LRT compares very favorably with respect to the CAPD and Flow* tools. △ Less

Submitted 3 July, 2017; v1 submitted 16 May, 2017; originally announced May 2017.

Comments: Accepted to CAV 2017

A Component-Based Simplex Architecture for High-Assurance Cyber-Physical Systems

Authors: Dung Phan, Junxing Yang, Matthew Clark, Radu Grosu, John D. Schierman, Scott A. Smolka, Scott D. Stoller

Abstract: We present Component-Based Simplex Architecture (CBSA), a new framework for assuring the runtime safety of component-based cyber-physical systems (CPSs). CBSA integrates Assume-Guarantee (A-G) reasoning with the core principles of the Simplex control architecture to allow component-based CPSs to run advanced, uncertified controllers while still providing runtime assurance that A-G contracts and gl… ▽ More We present Component-Based Simplex Architecture (CBSA), a new framework for assuring the runtime safety of component-based cyber-physical systems (CPSs). CBSA integrates Assume-Guarantee (A-G) reasoning with the core principles of the Simplex control architecture to allow component-based CPSs to run advanced, uncertified controllers while still providing runtime assurance that A-G contracts and global properties are satisfied. In CBSA, multiple Simplex instances, which can be composed in a nested, serial or parallel manner, coordinate to assure system-wide properties. Combining A-G reasoning and the Simplex architecture is a challenging problem that yields significant benefits. By utilizing A-G contracts, we are able to compositionally determine the switching logic for CBSAs, thereby alleviating the state explosion encountered by other approaches. Another benefit is that we can use A-G proof rules to decompose the proof of system-wide safety assurance into sub-proofs corresponding to the component-based structure of the system architecture. We also introduce the notion of coordinated switching between Simplex instances, a key component of our compositional approach to reasoning about CBSA switching logic. We illustrate our framework with a component-based control system for a ground rover. We formally prove that the CBSA for this system guarantees energy safety (the rover never runs out of power), and collision freedom (the rover never collides with a stationary obstacle). We also consider a CBSA for the rover that guarantees mission completion: all target destinations visited within a prescribed amount of time. △ Less

Submitted 16 April, 2017; originally announced April 2017.

Comments: Extended version of a paper to be presented at ACSD 2017, 12 pages, 3 figures, 1 appendix

Model Checking Cyber-Physical Systems using Particle Swarm Optimization

Authors: Dung Phan, Scott A. Smolka, Radu Grosu, Usama Mehmood, Scott D. Stoller, Junxing Yang

Abstract: We present a novel approach to the problem of model checking cyber-physical systems. We transform the model checking problem to an optimization one by designing an objective function that measures how close a state is to a violation of a property. We use particle swarm optimization (PSO) to effectively search for a state that minimizes the objective function. Such states, if found, are counter-exa… ▽ More We present a novel approach to the problem of model checking cyber-physical systems. We transform the model checking problem to an optimization one by designing an objective function that measures how close a state is to a violation of a property. We use particle swarm optimization (PSO) to effectively search for a state that minimizes the objective function. Such states, if found, are counter-examples describing safe states from which the system can reach an unsafe state in one time step. We illustrate our approach with a controller for the Quickbot ground rover. Our PSO model checker quickly found a bug in the controller that could cause the rover to collide with an obstacle. △ Less

Submitted 3 March, 2017; originally announced March 2017.

Attacking the V: On the Resiliency of Adaptive-Horizon MPC

Authors: Scott A. Smolka, Ashish Tiwari, Lukas Esterle, Anna Lukina, Junxing Yang, Radu Grosu

Abstract: We introduce the concept of a V-formation game between a controller and an attacker, where controller's goal is to maneuver the plant (a simple model of flocking dynamics) into a V-formation, and the goal of the attacker is to prevent the controller from doing so. Controllers in V-formation games utilize a new formulation of model-predictive control we call Adaptive-Horizon MPC (AMPC), giving them… ▽ More We introduce the concept of a V-formation game between a controller and an attacker, where controller's goal is to maneuver the plant (a simple model of flocking dynamics) into a V-formation, and the goal of the attacker is to prevent the controller from doing so. Controllers in V-formation games utilize a new formulation of model-predictive control we call Adaptive-Horizon MPC (AMPC), giving them extraordinary power: we prove that under certain controllability assumptions, an AMPC controller is able to attain V-formation with probability 1. We define several classes of attackers, including those that in one move can remove R birds from the flock, or introduce random displacement into flock dynamics. We consider both naive attackers, whose strategies are purely probabilistic, and AMPC-enabled attackers, putting them on par strategically with the controllers. While an AMPC-enabled controller is expected to win every game with probability 1, in practice, it is resource-constrained: its maximum prediction horizon and the maximum number of game execution steps are fixed. Under these conditions, an attacker has a much better chance of winning a V-formation game. Our extensive performance evaluation of V-formation games uses statistical model checking to estimate the probability an attacker can thwart the controller. Our results show that for the bird-removal game with R = 1, the controller almost always wins (restores the flock to a V-formation). For R = 2, the game outcome critically depends on which two birds are removed. For the displacement game, our results again demonstrate that an intelligent attacker, i.e. one that uses AMPC in this case, significantly outperforms its naive counterpart that randomly executes its attack. △ Less

Submitted 1 February, 2017; originally announced February 2017.

Quantitative Regular Expressions for Arrhythmia Detection Algorithms

Authors: Houssam Abbas, Alena Rodionova, Ezio Bartocci, Scott A. Smolka, Radu Grosu

Abstract: Motivated by the problem of verifying the correctness of arrhythmia-detection algorithms, we present a formalization of these algorithms in the language of Quantitative Regular Expressions. QREs are a flexible formal language for specifying complex numerical queries over data streams, with provable runtime and memory consumption guarantees. The medical-device algorithms of interest include peak de… ▽ More Motivated by the problem of verifying the correctness of arrhythmia-detection algorithms, we present a formalization of these algorithms in the language of Quantitative Regular Expressions. QREs are a flexible formal language for specifying complex numerical queries over data streams, with provable runtime and memory consumption guarantees. The medical-device algorithms of interest include peak detection (where a peak in a cardiac signal indicates a heartbeat) and various discriminators, each of which uses a feature of the cardiac signal to distinguish fatal from non-fatal arrhythmias. Expressing these algorithms' desired output in current temporal logics, and implementing them via monitor synthesis, is cumbersome, error-prone, computationally expensive, and sometimes infeasible. In contrast, we show that a range of peak detectors (in both the time and wavelet domains) and various discriminators at the heart of today's arrhythmia-detection devices are easily expressible in QREs. The fact that one formalism (QREs) is used to describe the desired end-to-end operation of an arrhythmia detector opens the way to formal analysis and rigorous testing of these detectors' correctness and performance. Such analysis could alleviate the regulatory burden on device developers when modifying their algorithms. The performance of the peak-detection QREs is demonstrated by running them on real patient data, on which they yield results on par with those provided by a cardiologist. △ Less

Submitted 24 September, 2017; v1 submitted 22 December, 2016; originally announced December 2016.

Comments: CMSB 2017: 15th Conference on Computational Methods for Systems Biology

ARES: Adaptive Receding-Horizon Synthesis of Optimal Plans

Authors: Anna Lukina, Lukas Esterle, Christian Hirsch, Ezio Bartocci, Junxing Yang, Ashish Tiwari, Scott A. Smolka, Radu Grosu

Abstract: We introduce ARES, an efficient approximation algorithm for generating optimal plans (action sequences) that take an initial state of a Markov Decision Process (MDP) to a state whose cost is below a specified (convergence) threshold. ARES uses Particle Swarm Optimization, with adaptive sizing for both the receding horizon and the particle swarm. Inspired by Importance Splitting, the length of the… ▽ More We introduce ARES, an efficient approximation algorithm for generating optimal plans (action sequences) that take an initial state of a Markov Decision Process (MDP) to a state whose cost is below a specified (convergence) threshold. ARES uses Particle Swarm Optimization, with adaptive sizing for both the receding horizon and the particle swarm. Inspired by Importance Splitting, the length of the horizon and the number of particles are chosen such that at least one particle reaches a next-level state, that is, a state where the cost decreases by a required delta from the previous-level state. The level relation on states and the plans constructed by ARES implicitly define a Lyapunov function and an optimal policy, respectively, both of which could be explicitly generated by applying ARES to all states of the MDP, up to some topological equivalence relation. We also assess the effectiveness of ARES by statistically evaluating its rate of success in generating optimal plans. The ARES algorithm resulted from our desire to clarify if flying in V-formation is a flocking policy that optimizes energy conservation, clear view, and velocity alignment. That is, we were interested to see if one could find optimal plans that bring a flock from an arbitrary initial state to a state exhibiting a single connected V-formation. For flocks with 7 birds, ARES is able to generate a plan that leads to a V-formation in 95% of the 8,000 random initial configurations within 63 seconds, on average. ARES can also be easily customized into a model-predictive controller (MPC) with an adaptive receding horizon and statistical guarantees of convergence. To the best of our knowledge, our adaptive-sizing approach is the first to provide convergence guarantees in receding-horizon techniques. △ Less

Submitted 21 December, 2016; originally announced December 2016.

Comments: submitted to TACAS 2017

Cantor meets Scott: Semantic Foundations for Probabilistic Networks

Authors: Steffen Smolka, Praveen Kumar, Nate Foster, Dexter Kozen, Alexandra Silva

Abstract: ProbNetKAT is a probabilistic extension of NetKAT with a denotational semantics based on Markov kernels. The language is expressive enough to generate continuous distributions, which raises the question of how to compute effectively in the language. This paper gives an new characterization of ProbNetKAT's semantics using domain theory, which provides the foundation needed to build a practical impl… ▽ More ProbNetKAT is a probabilistic extension of NetKAT with a denotational semantics based on Markov kernels. The language is expressive enough to generate continuous distributions, which raises the question of how to compute effectively in the language. This paper gives an new characterization of ProbNetKAT's semantics using domain theory, which provides the foundation needed to build a practical implementation. We show how to use the semantics to approximate the behavior of arbitrary ProbNetKAT programs using distributions with finite support. We develop a prototype implementation and show how to use it to solve a variety of problems including characterizing the expected congestion induced by different routing schemes and reasoning probabilistically about reachability in a network. △ Less

Submitted 15 December, 2018; v1 submitted 20 July, 2016; originally announced July 2016.

Comments: to appear at POPL 2017, Paris

ACM Class: D.3.1

A survey on unmanned aerial vehicle collision avoidance systems

Authors: Hung Pham, Scott A. Smolka, Scott D. Stoller, Dung Phan, Junxing Yang

Abstract: Collision avoidance is a key factor in enabling the integration of unmanned aerial vehicle into real life use, whether it is in military or civil application. For a long time there have been a large number of works to address this problem; therefore a comparative summary of them would be desirable. This paper presents a survey on the major collision avoidance systems developed in up to date public… ▽ More Collision avoidance is a key factor in enabling the integration of unmanned aerial vehicle into real life use, whether it is in military or civil application. For a long time there have been a large number of works to address this problem; therefore a comparative summary of them would be desirable. This paper presents a survey on the major collision avoidance systems developed in up to date publications. Each collision avoidance system contains two main parts: sensing and detection, and collision avoidance. Based on their characteristics each part is divided into different categories; and those categories are explained, compared and discussed about advantages and disadvantages in this paper. △ Less

Submitted 31 August, 2015; originally announced August 2015.

Comments: This is only a draft

A Fast Compiler for NetKAT

Authors: Steffen Smolka, Spiridon Eliopoulos, Nate Foster, Arjun Guha

Abstract: High-level programming languages play a key role in a growing number of networking platforms, streamlining application development and enabling precise formal reasoning about network behavior. Unfortunately, current compilers only handle "local" programs that specify behavior in terms of hop-by-hop forwarding behavior, or modest extensions such as simple paths. To encode richer "global" behaviors,… ▽ More High-level programming languages play a key role in a growing number of networking platforms, streamlining application development and enabling precise formal reasoning about network behavior. Unfortunately, current compilers only handle "local" programs that specify behavior in terms of hop-by-hop forwarding behavior, or modest extensions such as simple paths. To encode richer "global" behaviors, programmers must add extra state -- something that is tricky to get right and makes programs harder to write and maintain. Making matters worse, existing compilers can take tens of minutes to generate the forwarding state for the network, even on relatively small inputs. This forces programmers to waste time working around performance issues or even revert to using hardware-level APIs. This paper presents a new compiler for the NetKAT language that handles rich features including regular paths and virtual networks, and yet is several orders of magnitude faster than previous compilers. The compiler uses symbolic automata to calculate the extra state needed to implement "global" programs, and an intermediate representation based on binary decision diagrams to dramatically improve performance. We describe the design and implementation of three essential compiler stages: from virtual programs (which specify behavior in terms of virtual topologies) to global programs (which specify network-wide behavior in terms of physical topologies), from global programs to local programs (which specify behavior in terms of single-switch behavior), and from local programs to hardware-level forwarding tables. We present results from experiments on real-world benchmarks that quantify performance in terms of compilation time and forwarding table size. △ Less

Submitted 24 June, 2015; v1 submitted 21 June, 2015; originally announced June 2015.

ACM Class: D.3.4

Journal ref: ACM SIGPLAN Notices - ICFP '15, Volume 50 Issue 9, September 2015, Pages 328-341

Abstract Model Repair

Authors: George Chatzieleftheriou, Borzoo Bonakdarpour, Panagiotis Katsaros, Scott A. Smolka

Abstract: Given a Kripke structure M and CTL formula $\varphi$, where M does not satisfy $\varphi$, the problem of Model Repair is to obtain a new model M' such that M' satisfies $\varphi$. Moreover, the changes made to M to derive M' should be minimum with respect to all such M'. As in model checking, state explosion can make it virtually impossible to carry out model repair on models with infinite or ev… ▽ More Given a Kripke structure M and CTL formula $\varphi$, where M does not satisfy $\varphi$, the problem of Model Repair is to obtain a new model M' such that M' satisfies $\varphi$. Moreover, the changes made to M to derive M' should be minimum with respect to all such M'. As in model checking, state explosion can make it virtually impossible to carry out model repair on models with infinite or even large state spaces. In this paper, we present a framework for model repair that uses abstraction refinement to tackle state explosion. Our framework aims to repair Kripke Structure models based on a Kripke Modal Transition System abstraction and a 3-valued semantics for CTL. We introduce an abstract-model-repair algorithm for which we prove soundness and semi-completeness, and we study its complexity class. Moreover, a prototype implementation is presented to illustrate the practical utility of abstract-model-repair on an Automatic Door Opener system model and a model of the Andrew File System 1 protocol. △ Less

Submitted 16 September, 2015; v1 submitted 19 June, 2015; originally announced June 2015.

Comments: 43 pages

Journal ref: Logical Methods in Computer Science, Volume 11, Issue 3 (September 17, 2015) lmcs:1587

Model Checking as Control: Feedback Control for Statistical Model Checking of Cyber-Physical Systems

Authors: Kenan Kalajdzic, Cyrille Jegourel, Ezio Bartocci, Axel Legay, Scott A. Smolka, Radu Grosu

Abstract: We introduce feedback-control statistical system checking (FC-SSC), a new approach to statistical model checking that exploits principles of feedback-control for the analysis of cyber-physical systems (CPS). FC-SSC uses stochastic system identification to learn a CPS model, importance sampling to estimate the CPS state, and importance splitting to control the CPS so that the probability that the C… ▽ More We introduce feedback-control statistical system checking (FC-SSC), a new approach to statistical model checking that exploits principles of feedback-control for the analysis of cyber-physical systems (CPS). FC-SSC uses stochastic system identification to learn a CPS model, importance sampling to estimate the CPS state, and importance splitting to control the CPS so that the probability that the CPS satisfies a given property can be efficiently inferred. We illustrate the utility of FC-SSC on two example applications, each of which is simple enough to be easily understood, yet complex enough to exhibit all of FC-SCC's features. To the best of our knowledge, FC-SSC is the first statistical system checker to efficiently estimate the probability of rare events in realistic CPS applications or in any complex probabilistic program whose model is either not available, or is infeasible to derive through static-analysis techniques. △ Less

Submitted 12 June, 2015; v1 submitted 24 April, 2015; originally announced April 2015.

Comments: There are somethings to be checked more carefully

Model Checking Tap Withdrawal in C. Elegans

Authors: Md. Ariful Islam, Richard DeFrancisco, Chuchu Fan, Radu Grosu, Sayan Mitra, Scott A. Smolka

Abstract: We present what we believe to be the first formal verification of a biologically realistic (nonlinear ODE) model of a neural circuit in a multicellular organism: Tap Withdrawal (TW) in \emph{C. Elegans}, the common roundworm. TW is a reflexive behavior exhibited by \emph{C. Elegans} in response to vibrating the surface on which it is moving; the neural circuit underlying this response is the subje… ▽ More We present what we believe to be the first formal verification of a biologically realistic (nonlinear ODE) model of a neural circuit in a multicellular organism: Tap Withdrawal (TW) in \emph{C. Elegans}, the common roundworm. TW is a reflexive behavior exhibited by \emph{C. Elegans} in response to vibrating the surface on which it is moving; the neural circuit underlying this response is the subject of this investigation. Specifically, we perform reachability analysis on the TW circuit model of Wicks et al. (1996), which enables us to estimate key circuit parameters. Underlying our approach is the use of Fan and Mitra's recently developed technique for automatically computing local discrepancy (convergence and divergence rates) of general nonlinear systems. We show that the results we obtain are in agreement with the experimental results of Wicks et al. (1995). As opposed to the fixed parameters found in most biological models, which can only produce the predominant behavior, our techniques characterize ranges of parameters that produce (and do not produce) all three observed behaviors: reversal of movement, acceleration, and lack of response. △ Less

Submitted 22 March, 2015; originally announced March 2015.

Nonequilibrium dynamics in an optical transition from a neutral quantum dot to a correlated many-body state

Authors: F. Haupt, S. Smolka, M. Hanl, W. Wüster, J. Miguel-Sanchez, A. Weichselbaum, J. von Delft, A. Imamoglu

Abstract: We investigate the effect of many-body interactions on the optical absorption spectrum of a charge-tunable quantum dot coupled to a degenerate electron gas. A constructive Fano interference between an indirect path, associated with an intra dot exciton generation followed by tunneling, and a direct path, associated with the ionization of a valence-band quantum dot electron, ensures the visibility… ▽ More We investigate the effect of many-body interactions on the optical absorption spectrum of a charge-tunable quantum dot coupled to a degenerate electron gas. A constructive Fano interference between an indirect path, associated with an intra dot exciton generation followed by tunneling, and a direct path, associated with the ionization of a valence-band quantum dot electron, ensures the visibility of the ensuing Fermi-edge singularity despite weak absorption strength. We find good agreement between experiment and renormalization group theory, but only when we generalize the Anderson impurity model to include a static hole and a dynamic dot-electron scattering potential. The latter highlights the fact that an optically active dot acts as a tunable quantum impurity, enabling the investigation of a new dynamic regime of Fermi-edge physics. △ Less

Submitted 4 November, 2013; v1 submitted 5 April, 2013; originally announced April 2013.

Comments: 14 pages, 10 figures

Journal ref: Phys. Rev. B 88, 161304(R) (2013)

Model Checking with Probabilistic Tabled Logic Programming

Authors: Andrey Gorlin, C. R. Ramakrishnan, Scott A. Smolka

Abstract: We present a formulation of the problem of probabilistic model checking as one of query evaluation over probabilistic logic programs. To the best of our knowledge, our formulation is the first of its kind, and it covers a rich class of probabilistic models and probabilistic temporal logics. The inference algorithms of existing probabilistic logic-programming systems are well defined only for queri… ▽ More We present a formulation of the problem of probabilistic model checking as one of query evaluation over probabilistic logic programs. To the best of our knowledge, our formulation is the first of its kind, and it covers a rich class of probabilistic models and probabilistic temporal logics. The inference algorithms of existing probabilistic logic-programming systems are well defined only for queries with a finite number of explanations. This restriction prohibits the encoding of probabilistic model checkers, where explanations correspond to executions of the system being model checked. To overcome this restriction, we propose a more general inference algorithm that uses finite generative structures (similar to automata) to represent families of explanations. The inference algorithm computes the probability of a possibly infinite set of explanations directly from the finite generative structure. We have implemented our inference algorithm in XSB Prolog, and use this implementation to encode probabilistic model checkers for a variety of temporal logics, including PCTL and GPL (which subsumes PCTL*). Our experiment results show that, despite the highly declarative nature of their encodings, the model checkers constructed in this manner are competitive with their native implementations. △ Less

Submitted 20 April, 2012; originally announced April 2012.

Statistical theory of a quantum emitter strongly coupled to Anderson-localized modes

Authors: Henri Thyrrestrup, Stephan Smolka, Luca Sapienza, Peter Lodahl

Abstract: A statistical theory of the coupling between a quantum emitter and Anderson-localized cavity modes is presented based on a dyadic Green's function formalism. The probability of achieving the strong light-matter coupling regime is extracted for an experimentally realistic system composed of InAs quantum dots embedded in a disordered photonic crystal waveguide. We demonstrate that by engineering the… ▽ More A statistical theory of the coupling between a quantum emitter and Anderson-localized cavity modes is presented based on a dyadic Green's function formalism. The probability of achieving the strong light-matter coupling regime is extracted for an experimentally realistic system composed of InAs quantum dots embedded in a disordered photonic crystal waveguide. We demonstrate that by engineering the relevant parameters that define the quality of light confinement, i.e. the light localization length and the loss length, strong coupling between a single quantum dot and an Anderson-localized cavity is within experimental reach. As a consequence of disorder-induced light confinement provides a novel platform for quantum electrodynamics experiments. △ Less

Submitted 23 December, 2011; originally announced December 2011.

Comments: 5 pages, 4 figures

Journal ref: Phys. Rev. Lett. 108, 113901 (2012)

Probing statistical properties of Anderson localization with quantum emitters

Authors: Stephan Smolka, Henri Thyrrestrup, Luca Sapienza, Tau B. Lehmann, Kristian R. Rix, Luis S. Froufe-Pérez, Pedro D. García, Peter Lodahl

Abstract: Wave propagation in disordered media can be strongly modified by multiple scattering and wave interference. Ultimately the so-called Anderson-localized regime is reached when the waves become strongly confined in space. So far, Anderson localization of light has been probed in transmission experiments by measuring the intensity of an external light source after propagation through a disordered med… ▽ More Wave propagation in disordered media can be strongly modified by multiple scattering and wave interference. Ultimately the so-called Anderson-localized regime is reached when the waves become strongly confined in space. So far, Anderson localization of light has been probed in transmission experiments by measuring the intensity of an external light source after propagation through a disordered medium. However, discriminating between Anderson localization and losses in these experiments remains a major challenge. Here we present an alternative approach where we use quantum emitters embedded in disordered photonic crystal waveguides as light sources. Anderson-localized modes are efficiently excited and the analysis of the photoluminescence spectra allows to explore their statistical properties paving a way for controlling Anderson localization in disordered photonic crystals. △ Less

Submitted 30 March, 2011; originally announced March 2011.

Comments: 13 pages, 5 figures

Journal ref: New J. Phys. 13 063044 (2011)

Continuous-wave spatial quantum correlations of light induced by multiple scattering

Authors: Stephan Smolka, Johan R. Ott, Alexander Huck, Ulrik L. Andersen, Peter Lodahl

Abstract: We present theoretical and experimental results on spatial quantum correlations induced by multiple scattering of nonclassical light. A continuous mode quantum theory is derived that enables determining the spatial quantum correlation function from the fluctuations of the total transmittance and reflectance. Utilizing frequency-resolved quantum noise measurements, we observe that the strength of t… ▽ More We present theoretical and experimental results on spatial quantum correlations induced by multiple scattering of nonclassical light. A continuous mode quantum theory is derived that enables determining the spatial quantum correlation function from the fluctuations of the total transmittance and reflectance. Utilizing frequency-resolved quantum noise measurements, we observe that the strength of the spatial quantum correlation function can be controlled by changing the quantum state of an incident bright squeezed-light source. Our results are found to be in excellent agreement with the developed theory and form a basis for future research on, e.g., quantum interference of multiple quantum states in a multiple scattering medium. △ Less

Submitted 11 July, 2012; v1 submitted 4 March, 2011; originally announced March 2011.

Comments: 8 pages, 6 figures

Angular-resolved photon-coincidence measurements in a multiple-scattering medium

Authors: Stephan Smolka, Otto L. Muskens, Ad Lagendijk, Peter Lodahl

Abstract: We present angular-resolved correlation measurements between photons after propagation through a three-dimensional disordered medium. The multiple scattering process induces photon correlations that are directly measured for light sources with different photon statistics. We find that multiple scattered photons between different angular directions with angles much larger than the average speckle w… ▽ More We present angular-resolved correlation measurements between photons after propagation through a three-dimensional disordered medium. The multiple scattering process induces photon correlations that are directly measured for light sources with different photon statistics. We find that multiple scattered photons between different angular directions with angles much larger than the average speckle width are strongly correlated. The time dependence of the angular photon correlation function is investigated and the coherence time of the light source is determined. Our results are found to be in excellent agreement with the continuous mode quantum theory of multiple scattering of light. The presented experimental technique is essential in order to study quantum phenomena in multiple scattering random media such as quantum interference and quantum entanglement of photons. △ Less

Submitted 4 March, 2011; v1 submitted 10 April, 2010; originally announced April 2010.

Comments: 6 pages, 4 figures

Journal ref: Phys. Rev. A 83, 043819 (2011)

Cavity Quantum Electrodynamics with Anderson-localized Modes

Authors: Luca Sapienza, Henri Thyrrestrup, Søren Stobbe, Pedro David Garcia, Stephan Smolka, Peter Lodahl

Abstract: A major challenge in quantum optics and quantum information technology is to enhance the interaction between single photons and single quantum emitters. Highly engineered optical cavities are generally implemented requiring nanoscale fabrication precision. We demonstrate a fundamentally different approach in which disorder is used as a resource rather than a nuisance. We generate strongly confine… ▽ More A major challenge in quantum optics and quantum information technology is to enhance the interaction between single photons and single quantum emitters. Highly engineered optical cavities are generally implemented requiring nanoscale fabrication precision. We demonstrate a fundamentally different approach in which disorder is used as a resource rather than a nuisance. We generate strongly confined Anderson-localized cavity modes by deliberately adding disorder to photonic crystal waveguides. The emission rate of a semiconductor quantum dot embedded in the waveguide is enhanced by a factor of 15 on resonance with the Anderson-localized mode and 94 % of the emitted single-photons couple to the mode. Disordered photonic media thus provide an efficient platform for quantum electrodynamics offering an approach to inherently disorder-robust quantum information devices. △ Less

Submitted 12 March, 2010; originally announced March 2010.

Journal ref: Science 327, 1352 (2010)

Controlling Anderson localization in disordered photonic crystal waveguides

Authors: P. D. Garcia, S. Smolka, S. Stobbe, P. Lodahl

Abstract: We prove Anderson localization in a disordered photonic crystal waveguide by measuring the ensemble-averaged localization length which is controlled by the dispersion of the photonic crystal waveguide. In such structures, the localization length shows a 10-fold variation between the fast- and the slow-light regime and, in the latter case, it becomes shorter than the sample length thus giving ris… ▽ More We prove Anderson localization in a disordered photonic crystal waveguide by measuring the ensemble-averaged localization length which is controlled by the dispersion of the photonic crystal waveguide. In such structures, the localization length shows a 10-fold variation between the fast- and the slow-light regime and, in the latter case, it becomes shorter than the sample length thus giving rise to strongly confined modes. The dispersive behavior of the localization length demonstrates the close relation between Anderson localization and the photon density of states in disordered photonic crystals, which opens a promising route to controlling and exploiting Anderson localization for efficient light confinement. △ Less

Submitted 12 March, 2010; v1 submitted 3 March, 2010; originally announced March 2010.

Comments: 4 pages, 4 figures

Demonstration of Quadrature Squeezed Surface-Plasmons in a Gold Waveguide

Authors: Alexander Huck, Stephan Smolka, Peter Lodahl, Anders S. Soerensen, Alexandra Boltasseva, Jiri Janousek, Ulrik L. Andersen

Abstract: We report on the efficient generation, propagation, and re-emission of squeezed long-range surface-plasmon polaritons (SPPs) in a gold waveguide. Squeezed light is used to excite the non-classical SPPs and the re-emitted quantum state is fully quantum characterized by complete tomographic reconstruction of the density matrix. We find that the plasmon-assisted transmission of non-classical light… ▽ More We report on the efficient generation, propagation, and re-emission of squeezed long-range surface-plasmon polaritons (SPPs) in a gold waveguide. Squeezed light is used to excite the non-classical SPPs and the re-emitted quantum state is fully quantum characterized by complete tomographic reconstruction of the density matrix. We find that the plasmon-assisted transmission of non-classical light in metallic waveguides can be described by a Hamiltonian analogue to a beam splitter. This result is explained theoretically. △ Less

Submitted 26 January, 2009; originally announced January 2009.

Journal ref: Phys. Rev. Lett. 102, 246802 (2009)