Biblio

Found 210 results

Filters: Keyword is UIUC  [Clear All Filters]
2015-12-02
Gul Agha, University of Illinois at Urbana-Champaign.  2013.  Euclidean Model Checking: A Scalable Method for Verifying Quantitative Properties in Probabilistic Systems. 5th International Conference on Algebraic Informatics.

In this lecture, I will focus on an alternate method for addressing the problem of large state spaces. For many purposes, it may not be necessary to consider the global state as a cross-product of the states of individual actors. We take our inspiration from statistical physics where macro properties of a system may be related to the properties of individual molecules using probability distributions on the states of the latter. Consider a simple example. Suppose associated with each state is the amount of energy a node consumes when in that state (such an associated value mapping is called the reward function of the state). Now, if we have a frequency count of the nodes in each state, we can estimate the total energy consumed by the system. This suggests a model where the global state is a vector of probability mass functions (pmfs). In the above example, the size of the vector would be 5, one element for each possible state of a node. Each element of the vector represents the probability that any node is in the particular state corresponding to entry.

This was an invited talk to the 5th International Conference on Algebraic Informatics.

2017-02-09
Mohammad Hossein Manshaei, Isfahan University of Technology, Quanyan Zhu, University of Illinois at Urbana-Champaign, Tansu Alpcan, University of Melbourne, Tamer Başar, University of Illinois at Urbana-Champaign, Jean-Pierre Hubaux, Ecole Polytechnique Federal de Lausanne.  2013.  Game Theory Meets Network Security and Privacy. ACM Computing Surveys. 45(3):06/2013.

This survey provides a structured and comprehensive overview of research on security and privacy in computer and communication networks that use game-theoretic approaches. We present a selected set of works to highlight the application of game theory in addressing different forms of security and privacy problems in computer networks and mobile applications. We organize the presented works in six main categories: security of the physical and MAC layers, security of self-organizing networks, intrusion detection systems, anonymity and privacy, economics of network security, and cryptography. In each category, we identify security problems, players, and game models. We summarize the main results of selected works, such as equilibrium analysis and security mechanism designs. In addition, we provide a discussion on the advantages, drawbacks, and future direction of using game theory in this field. In this survey, our goal is to instill in the reader an enhanced understanding of different research approaches in applying gametheoretic methods to network security. This survey can also help researchers from various fields develop game-theoretic solutions to current and emerging security problems in computer networking.

2015-12-02
Dennis Griffith, University of Illinois at Urbana-Champaign, Elsa Gunter, University of Illinois at Urbana-Champaign.  2013.  LiquidPi: Inferable Dependent Session Types. 5th International NASA Formal Methods (NFM 2013) .

The Pi Calculus is a popular formalism for modeling distributed computation. Session Types extend the Pi Calculus with a static, inferable type system. Dependent Types allow for a more precise characterization of the behavior of programs, but in their full generality are not inferable. In this paper, we present LiquidPi an approach that combines the dependent type inferencing of Liquid Types with Honda’s Session Types to give a more precise automatically derived description of the behavior of distributed programs. These types can be used to describe/enforce safety properties of distributed systems. We present a type system parametric over an underlying functional language with Pi Calculus connectives and give an inference algorithm for it by means of efficient external solvers and a set of dependent qualifier templates.

2017-02-09
Alejandro Domininguez-Garcia, University of Illinois at Urbana-Champaign, Bahman Gharesifard, University of Illinois at Urbana-Champaign, Tamer Başar, University of Illinois at Urbana-Champaign.  2013.  A Price-Based Approach to Control of Networked Distributed Energy Resources.

We introduce a framework for controlling the energy provided or absorbed by distributed energy resources (DERs) in power distribution networks. In this framework, there is a set of agents referred to as aggregators that interact with the wholesale electricity market, and through some market-clearing mechanism, are requested (and will be compensated for) to provide (or absorb) certain amount of active (or reactive) power over some period of time. In order to fulfill the request, each aggregator interacts with a set of DERs and offers them some price per unit of active (or reactive) power they provide (or absorb); the objective is for the aggregator to design a pricing strategy for incentivizing DERs to change its active (or reactive) power consumption (or production) so as they collectively provide the amount that the aggregator has been asked for. In order to make a decision, each DER uses the price information provided by the aggregator and some estimate of the average active (or reactive) power that neighboring DERs can provide computed through some exchange of information among them; this exchange is described by a connected undirected graph. The focus is on the DER strategic decision-making process, which we cast as a game. In this context, we provide sufficient conditions on the aggregator's pricing strategy under which this game has a unique Nash equilibrium. Then, we propose a distributed iterative algorithm that adheres to the graph that describes the exchange of information between DERs that allows them to seek for this Nash equilibrium. We illustrate our results through several numerical simulations.

Presented as part of the DIMACS Workshop on Energy Infrastructure: Designing for Stability and Resilience, Rutgers University, Piscataway, NJ, February 20-22, 2013

2016-12-15
Timothy Bretl, University of Illinois at Urbana-Champaign, Zoe McCarthy, University of Illinois at Urbana-Champaign.  2013.  Quasi-Static Manipulation of a Kirchhoff Elastic Road Based on Geometric Analysis of Equilibrium Configurations. The International Journal of Robotics Research. 33(1)

Consider a thin, flexible wire of fixed length that is held at each end by a robotic gripper. Any curve traced by this wire when in static equilibrium is a local solution to a geometric optimal control problem, with boundary conditions that vary with the position and orientation of each gripper. We prove that the set of all local solutions to this problem over all possible boundary conditions is a smooth manifold of finite dimension that can be parameterized by a single chart. We show that this chart makes it easy to implement a sampling-based algorithm for quasi-static manipulation planning. We characterize the performance of such an algorithm with experiments in simulation.

Published in The International Journal of Robotics Research

2017-02-08
Samira Tasharofi, University of Illinois at Urbana-Champaign, Peter Dinges, University of Illinois at Urbana-Champaign, Ralph E. Johnson, University of Illinois at Urbana-Champaign.  2013.  Why Do Scala Developers Mix the Actor Model with other Concurrency Models?

Mixing the actor model with other concurrency models in a single program can break the actor abstraction. This increases the chance of creating deadlocks and data races—two mistakes that are hard to make with actors. Furthermore, it prevents the use of many advanced testing, modeling, and verification tools for actors, as these require pure actor programs. This study is the first to point out the phenomenon of mixing concurrency models by Scala developers and to systematically identify the factors leading to it. We studied 15 large, mature, and actively maintained actor programs written in Scala and found that 80% of them mix the actor model with another concurrency model. Consequently, a large part of real-world actor programs does not use actors to their fullest advantage. Inspection of the programs and discussion with the developers reveal two reasons for mixing that can be influenced by researchers and library-builders: weaknesses in the actor library implementations, and shortcomings of the actor model itself.

2017-02-09
Hui Lin, University of Illinois at Urbana-Champaign, Adam Slagell, University of Illinois at Urbana-Champaign, Catello Di Marino, University of Illinois at Urbana-Champaugn, Zbigniew Kalbarczyk, University of Illinois at Urbana-Champaign, Ravishankar K. Iyer, University of Illinois at Urbana-Champaign.  2013.  Adapting Bro into SCADA: Building a Specification-based Instrusion Detection System for the DNP3 Protocol. Eighth Annual Security and Information Intelligence Research Workshop (CSIRRW 2013).

When SCADA systems are exposed to public networks, attackers can more easily penetrate the control systems that operate electrical power grids, water plants, and other critical infrastructures. To detect such attacks, SCADA systems require an intrusion detection technique that can understand the information carried by their usually proprietary network protocols.

To achieve that goal, we propose to attach to SCADA systems a specification-based intrusion detection framework based on Bro [7][8], a runtime network traffic analyzer. We have built a parser in Bro to support DNP3, a network protocol widely used in SCADA systems that operate electrical power grids. This built-in parser provides a clear view of all network events related to SCADA systems. Consequently, security policies to analyze SCADA-specific semantics related to the network events can be accurately defined. As a proof of concept, we specify a protocol validation policy to verify that the semantics of the data extracted from network packets conform to protocol definitions. We performed an experimental evaluation to study the processing capabilities of the proposed intrusion detection framework.

2017-02-02
Sabita Maharjan, Quanyan Zhu, University of Illinois at Urbana-Champaign, Yan Zhang, Stein Gjessing, Tamer Başar, University of Illinois at Urbana-Champaign.  2013.  Dependable Demand Response Management in Smart Grid: A Stackelberg Game Approach. IEEE Transactions on Smart Grid. 4(1)

Demand ResponseManagement (DRM) is a key component in the smart grid to effectively reduce power generation costs and user bills. However, it has been an open issue to address the DRM problem in a network of multiple utility companies and consumers where every entity is concerned about maximizing its own benefit. In this paper, we propose a Stackelberg game between utility companies and end-users to maximize the revenue of each utility company and the payoff of each user. We derive analytical results for the Stackelberg equilibrium of the game and prove that a unique solution exists.We develop a distributed algorithm which converges to the equilibrium with only local information available for both utility companies and end-users. Though DRM helps to facilitate the reliability of power supply, the smart grid can be succeptible to privacy and security issues because of communication links between the utility companies and the consumers. We study the impact of an attacker who can manipulate the price information from the utility companies.We also propose a scheme based on the concept of shared reserve power to improve the grid reliability and ensure its dependability.

2017-02-10
Quanyan Zhu, University of Illinois at Urbana-Champaign, Linda Bushnell, University of Washington, Tamer Başar, University of Illinois at Urbana-Champaign.  2013.  Resilient Distributed Control of Multi-agent Cyber-Physical Systems. Workshop on Control of Cyber-Physical Systems.

Abstract. Multi-agent cyber-physical systems (CPSs) are ubiquitous in modern infrastructure systems, including the future smart grid, transportation networks, and public health systems. Security of these systems are critical for normal operation of our society. In this paper, we focus on physical layer resilient control of these systems subject to cyber attacks and malicious behaviors of physical agents. We establish a cross-layer system model for the investigation of cross-layer coupling and performance interdependencies for CPSs. In addition, we study a twosystem synchronization problem in which one is a malicious agent who intends to mislead the entire system behavior through physical layer interactions. Feedback Nash equilibrium is used as the solution concept for the distributed control in the multi-agent system environment. We corroborate our results with numerical examples, which show the performance interdependencies between two CPSs through cyber and physical interactions.

2017-02-02
Joseph Sloan, University of Illinois at Urbana-Champaign, Rakesh Kumar, University of Illinois at Urbana-Champaign, Greg Bronevetsky, Lawrence Livermore National Laboratory.  2013.  An Algorithmic Approach to Error Localization and Partial Recomputation for Low-Overhead Fault Tolerance. 43rd Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN 2013).

The increasing size and complexity of massively parallel systems (e.g. HPC systems) is making it increasingly likely that individual circuits will produce erroneous results. For this reason, novel fault tolerance approaches are increasingly needed. Prior fault tolerance approaches often rely on checkpoint-rollback based schemes. Unfortunately, such schemes are primarily limited to rare error event scenarios as the overheads of such schemes become prohibitive if faults are common. In this paper, we propose a novel approach for algorithmic correction of faulty application outputs. The key insight for this approach is that even under high error scenarios, even if the result of an algorithm is erroneous, most of it is correct. Instead of simply rolling back to the most recent checkpoint and repeating the entire segment of computation, our novel resilience approach uses algorithmic error localization and partial recomputation to efficiently correct the corrupted results. We evaluate our approach in the specific algorithmic scenario of linear algebra operations, focusing on matrix-vector multiplication (MVM) and iterative linear solvers. We develop a novel technique for localizing errors in MVM and show how to achieve partial recomputation within this algorithm, and demonstrate that this approach both improves the performance of the Conjugate Gradient solver in high error scenarios by 3x-4x and increases the probability that it completes successfully by up to 60% with parallel experiments up to 100 nodes.

Andrew Clark, Quanyan Zhu, University of Illinois at Urbana-Champaign, Radha Poovendran, Tamer Başar, University of Illinois at Urbana-Champaign.  2013.  An Impact-Aware Defense against Stuxnet. IFAC American Control Conference (ACC 2013).

The Stuxnet worm is a sophisticated malware designed to sabotage industrial control systems (ICSs). It exploits vulnerabilities in removable drives, local area communication networks, and programmable logic controllers (PLCs) to penetrate the process control network (PCN) and the control system network (CSN). Stuxnet was successful in penetrating the control system network and sabotaging industrial control processes since the targeted control systems lacked security mechanisms for verifying message integrity and source authentication. In this work, we propose a novel proactive defense system framework, in which commands from the system operator to the PLC are authenticated using a randomized set of cryptographic keys. The framework leverages cryptographic analysis and controland game-theoretic methods to quantify the impact of malicious commands on the performance of the physical plant. We derive the worst-case optimal randomization strategy as a saddle-point equilibrium of a game between an adversary attempting to insert commands and the system operator, and show that the proposed scheme can achieve arbitrarily low adversary success probability for a sufficiently large number of keys. We evaluate our proposed scheme, using a linear-quadratic regulator (LQR) as a case study, through theoretical and numerical analysis.

2017-02-03
Yuan Yuan, Tsinghua University, Quanyan Zhu, University of Illinois at Urbana-Champaign, Fuchun Sun, Tsinghua University, Qinyi Wang, Beihang University, Tamer Başar, University of Illinois at Urbana-Champaign.  2013.  Resilient Control of Cyber-Physical Systems against Denial-of-Service Attacks. 6th International Symposium on Resilient Control Systems.

The integration of control systems with modern information technologies has posed potential security threats for critical infrastructures. The communication channels of the control system are vulnerable to malicious jamming and Denial-of-Service (DoS) attacks, which lead to severe timedelays and degradation of control performances. In this paper, we design resilient controllers for cyber-physical control systems under DoS attacks. We establish a coupled design framework which incorporates the cyber configuration policy of Intrusion Detection Systems (IDSs) and the robust control of dynamical system. We propose design algorithms based on value iteration methods and linear matrix inequalities for computing the optimal cyber security policy and control laws. We illustrate the design principle with an example from power systems. The results are corroborated by numerical examples and simulations.

Stanley Bak, University of Illinois at Urbana-Champaign, Fardin Abdi, University of Illinois at Urbana-Champaign, Zhenqi Huang, University of Illinois at Urbana-Champaign, Marco Caccamo, University of Illinois at Urbana-Champaign.  2013.  Using Run-Time Checking to Provide Safety and Progress for Distributed Cyber-Physical Systems. 2013 IEEE 19th International Conference on Embedded and Real-Time Computing Systems and Applications.

Cyber-physical systems (CPS) may interact and manipulate objects in the physical world, and therefore ideally would have formal guarantees about their behavior. Performing statictime proofs of safety invariants, however, may be intractable for systems with distributed physical-world interactions. This is further complicated when realistic communication models are considered, for which there may not be bounds on message delays, or even that messages will eventually reach their destination. In this work, we address the challenge of proving safety and progress in distributed CPS communicating over an unreliable communication layer. This is done in two parts. First, we show that system safety can be verified by partially relying upon runtime checks, and that dropping messages if the run-time checks fail will maintain safety. Second, we use a notion of compatible action chains to guarantee system progress, despite unbounded message delays.We demonstrate the effectiveness of our approach on a multi-agent vehicle flocking system, and show that the overhead of the proposed run-time checks is not overbearing.

2017-02-10
Quanyan Zhu, University of Illinois at Urbana-Champaign, Tamer Başar, University of Illinois at Urbana-Champaign.  2013.  Game-Theoretic Approach to Feedback-Driven Multi-stage Moving Target Defense. 4th International Conference on Decision and Game Theory for Security (GameSec 2013).

The static nature of computer networks allows malicious attackers to easily gather useful information about the network using network scanning and packet sniffing. The employment of secure perimeter firewalls and intrusion detection systems cannot fully protect the network from sophisticated attacks. As an alternative to the expensive and imperfect detection of attacks, it is possible to improve network security by manipulating the attack surface of the network in order to create a moving target defense. In this paper, we introduce a proactive defense scheme that dynamically alters the attack surface of the network to make it difficult for attackers to gather system information by increasing complexity and reducing its signatures. We use concepts from systems and control literature to design an optimal and efficient multi-stage defense mechanism based on a feedback information structure. The change of
attack surface involves a reconfiguration cost and a utility gain resulting from risk reduction. We use information- and control-theoretic tools to provide closed-form optimal randomization strategies. The results are corroborated by a case study and several numerical examples.

Navid Aghasadeghi, University of Illinois at Urbana-Champaign, Huihua Zhao, Texas A&M University, Levi J. Hargrove, Northwestern University, Aaron D. Ames, Texas A&M University, Eric J. Perreault, Northwestern University, Timothy Bretl, University of Illinois at Urbana-Champaign.  2013.  Learning Impedance Controller Parameters for Lower-Limb Prostheses. 2013 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS).

Impedance control is a common framework for control of lower-limb prosthetic devices. This approach requires choosing many impedance controller parameters. In this paper, we show how to learn these parameters for lower-limb prostheses by observation of unimpaired human walkers. We validate our approach in simulation of a transfemoral amputee, and we demonstrate the performance of the learned parameters in a preliminary experiment with a lower-limb prosthetic device.

2017-02-03
Hui Lin, University of Illinois at Urbana-Champaign, Adam Slagell, University of Illinois at Urbana-Champaign, Zbigniew Kalbarczyk, University of Illinois at Urbana-Champaign, Peter W. Sauer, University of Illinois at Urbana-Champaign, Ravishankar K. Iyer, University of Illinois at Urbana-Champaign.  2013.  Semantic Security Analysis of SCADA Networks to Detect Malicious Control Commands in Power Grids. First ACM Workshop on Smart Engergy Grid Security.

In the current generation of SCADA (Supervisory Control And Data Acquisition) systems used in power grids, a sophisticated attacker can exploit system vulnerabilities and use a legitimate maliciously crafted command to cause a wide range of system changes that traditional contingency analysis does not consider and remedial action schemes cannot handle. To detect such malicious commands, we propose a semantic analysis framework based on a distributed network of intrusion detection systems (IDSes). The framework combines system knowledge of both cyber and physical infrastructure in power grid to help IDS to estimate execution consequences of control commands, thus to reveal attacker’s malicious intentions. We evaluated the approach on the IEEE 30-bus system. Our experiments demonstrate that: (i) by opening 3 transmission lines, an attacker can avoid detection by the traditional contingency analysis and instantly put the tested 30-bus system into an insecure state and (ii) the semantic analysis provides reliable detection of malicious commands with a small amount of analysis time.

2017-02-02
Quanyan Zhu, University of Illinois at Urbana-Champaign, Andrew Clark, Radha Poovendran, Tamer Başar, University of Illinois at Urbana-Champaign.  2013.  Deployment and Exploitation of Deceptive Honeybots in Social Networks. 52nd Conference on Decision and Control.

As social networking sites such as Facebook and Twitter are becoming increasingly popular, a growing number of malicious attacks, such as phishing and malware, are exploiting them. Among these attacks, social botnets have sophisticated infrastructure that leverages compromised user accounts, known as bots, to automate the creation of new social networking accounts for spamming and malware propagation. Traditional defense mechanisms are often passive and reactive to non-zero-day attacks. In this paper, we adopt a proactive approach for enhancing security in social networks by infiltrating botnets with honeybots. We propose an integrated system named SODEXO which can be interfaced with social networking sites for creating deceptive honeybots and leveraging them for gaining information from botnets. We establish a Stackelberg game framework to capture strategic interactions between honeybots and botnets, and use quantitative methods to understand the tradeoffs of honeybots for their deployment and exploitation in social networks. We design a protection and alert system that integrates both microscopic and macroscopic models of honeybots and optimally determines the security strategies for honeybots. We corroborate the proposed mechanism with extensive simulations and comparisons with passive defenses.

2017-02-03
Bahman Gharesifard, Behrouz Touri, Tamer Başar, University of Illinois at Urbana-Champaign, Cedric Langbort, University of Illinois at Urbana-Champaign.  2013.  Distributed Optimization by Myopic Strategic Interactions and the Price of Heterogeneity. 52nd Conference on Decision and Control.

This paper is concerned with the tradeoffs between low-cost heterogenous designs and optimality. We study a class of constrained myopic strategic games on networks which approximate the solutions to a constrained quadratic optimization problem; the Nash equilibria of these games can be found using best-response dynamical systems, which only use local information. The notion of price of heterogeneity captures the quality of our approximations. This notion relies on the structure and the strength of the interconnections between agents. We study the stability properties of these dynamical systems and demonstrate their complex characteristics, including abundance of equilibria on graphs with high sparsity and heterogeneity. We also introduce the novel notions of social equivalence and social dominance, and show some of their interesting implications, including their correspondence to consensus. Finally, using a classical result of Hirsch [1], we fully characterize the stability of these dynamical systems for the case of star graphs with asymmetric interactions. Various examples illustrate our results.

Miles Johnson, University of Illinois at Urbana-Champaign, Navid Aghasadeghi, University of Illinois at Urbana-Champaign, Timothy Bretl, University of Illinois at Urbana-Champaign.  2013.  Inverse Optimal Control for Deterministic Continuous-time Nonlinear Systems. 52nd Conference on Decision and Control.

Inverse optimal control is the problem of computing a cost function with respect to which observed state and input trajectories are optimal. We present a new method of inverse optimal control based on minimizing the extent to which observed trajectories violate first-order necessary conditions for optimality. We consider continuous-time deterministic optimal control systems with a cost function that is a linear combination of known basis functions. We compare our approach with three prior methods of inverse optimal control. We demonstrate the performance of these methods by performing simulation experiments using a collection of nominal system models. We compare the robustness of these methods by analysing how they perform under perturbations to the system. To this purpose, we consider two scenarios: one in which we exactly know the set of basis functions in the cost function, and another in which the true cost function contains an unknown perturbation. Results from simulation experiments show that our new method is more computationally efficient than prior methods, performs similarly to prior approaches under large perturbations to the system, and better learns the true cost function under small perturbations.

2015-11-17
Zhenqi Huang, University of Illinois at Urbana-Champaign, Sayan Mitra, University of Illinois at Urbana-Champaign, Geir Dullerud, University of Illinois at Urbana-Champaign.  2012.  Differentially Private Iterative Synchronous Consensus. Workshop on Privacy in the Electronic Society (WPES 2012).

The iterative consensus problem requires a set of processes or agents with different initial values, to interact and update their states to eventually converge to a common value. Pro- tocols solving iterative consensus serve as building blocks in a variety of systems where distributed coordination is re- quired for load balancing, data aggregation, sensor fusion, filtering, and synchronization. In this paper, we introduce the private iterative consensus problem where agents are re- quired to converge while protecting the privacy of their ini- tial values from honest but curious adversaries. Protecting the initial states, in many applications, suffice to protect all subsequent states of the individual participants.

We adapt the notion of differential privacy in this setting of iterative computation. Next, we present (i) a server-based and (ii) a completely distributed randomized mechanism for solving differentially private iterative consensus with adver- saries who can observe the messages as well as the internal states of the server and a subset of the clients. Our analysis establishes the tradeoff between privacy and the accuracy.

2017-02-10
Quanyan Zhu, University of Illinois at Urbana-Champaign, Tamer Başar, University of Illinois at Urbana-Champaign.  2012.  Game-Theoretic Methods for Distributed Management of Energy Resources in the Smart Grid.

The smart grid is an ever-growing complex dynamic system with multiple interleaved layers and a large number of interacting components. In this talk, we discuss how game-theoretic tools can be used as an analytical tool to understand strategic interactions at different layers of the system and between different decision-making entities for distributed management of energy resources. We first investigate the issue of integration of renewable energy resources into the power grid. We establish a game-theoretic framework for modeling the strategic behavior of buses that are connected to renewable energy resources, and study the Nash equilibrium solution of distributed power generation at each bus. Our framework uses a cross-layer approach, taking into account the economic factors as well as system stability issues at the physical layer. In the second part of the talk, we discuss the issue of integration of plug-in electric vehicles (PHEVs) for vehicle-to-grid (V2G) transactions on the smart grid. Electric vehicles will be capable of buying and selling energy from smart parking lots in the future. We propose a multi-resolution and multi-layer stochastic differential game framework to study the dynamic decision-making process among PHEVs. We analyze the stochastic game in a large-population regime and account for the multiple types of interactions in the grid. Using these two settings, we demonstrate that game theory is a versatile tool to address many fundamental and emerging issues in the smart grid.

Presented at the Eighth Annual Carnegie Mellon Conference on the Electricity Industry Data-Driven Sustainable Engergy Systems in Pittsburgh, PA, March 12-14, 2012.

2015-11-23
Minas Charalambides, University of Illinois at Urbana-Champaign, Peter Dinges, University of Illinois at Urbana-Champaign, Gul Agha, University of Illinois at Urbana-Champaign.  2012.  Parameterized Concurrent Multi-Party Session Types. 11th International Workshop on Foundations of Coordination Languages and Self-Adaptive Systems (FOCLASA 2012). 91:16-30.

Session types have been proposed as a means of statically verifying implementations of communication protocols. Although prior work has been successful in verifying some classes of protocols, it does not cope well with parameterized, multi-actor scenarios with inherent asynchrony. For example, the sliding window protocol is inexpressible in previously proposed session type systems. This paper describes System-A, a new typing language which overcomes many of the expressiveness limitations of prior work. System-A explicitly supports asynchrony and parallelism, as well as multiple forms of parameterization. We define System-A and show how it can be used for the static verification of a large class of asynchronous communication protocols.

2016-12-14
Quanyan Zhu, University of Illinois at Urbana-Champaign, Tamer Başar, University of Illinois at Urbana-Champaign.  2012.  A Dynamic Game-Theoretic Approach to Resilient Control System Design for Cascading Failures. International Conference on High Confidence Networked Systems.

The migration of many current critical infrastructures, such as power grids and transportations systems, into open publicnetworks has posed many challenges in control systems. Modern control systems face uncertainties not only from the physical world but also from the cyber space. In this paper, we propose a hybrid game-theoretic approach to investigate the coupling between cyber security policy and robust control design. We study in detail the case of cascading failures in industrial control systems and provide a set of coupled optimality criteria in the linear-quadratic case. This approach can be further extended to more general cases of parallel cascading failures.

2016-12-15
Zoe McCarthy, University of Illinois at Urbana-Champaign, Timothy Bretl, University of Illinois at Urbana-Champaign.  2012.  Mechanics and Manipulation of Planar Elastic Kinematic Chains. IEEE International Conference on Robotics and Automation.

This paper presents a control strategy based on model learning for a self-assembled robotic “swimmer”. The swimmer forms when a liquid suspension of ferro-magnetic micro-particles and a non-magnetic bead are exposed to an alternating magnetic field that is oriented perpendicular to the liquid surface. It can be steered by modulating the frequency of the alternating field. We model the swimmer as a unicycle and learn a mapping from frequency to forward speed and turning rate using locally-weighted projection regression. We apply iterative linear quadratic regulation with a receding horizon to track motion primitives that could be used for path following. Hardware experiments validate our approach.

2017-02-03
Zoe McCarthy, University of Illinois at Urbana-Champaign, Timothy Bretl, University of Illinois at Urbana-Champaign.  2012.  Mechanics and Manipulation of Planar Elastic Kinematic Chains. 2012 IEEE International Conference on Robotics and Automation.

In this paper, we study quasi-static manipulation of a planar kinematic chain with a fixed base in which each joint is a linearly-elastic torsional spring. The shape of this chain when in static equilibrium can be represented as the solution to a discrete-time optimal control problem, with boundary conditions that vary with the position and orientation of the last link. We prove that the set of all solutions to this problem is a smooth manifold that can be parameterized by a single chart. For manipulation planning, we show several advantages of working in this chart instead of in the space of boundary conditions, particularly in the context of a sampling-based planning algorithm. Examples are provided in simulation.