BZPEERPapers, people, evidence and research paths
Menu

Discover

SearchFind papers, people, topics, institutions and opportunities from one place.GraphSee how papers, authors, topics and evidence connect.

Research tools

HomeContinue from the papers, people and topics that matter now.CollectionsTurn saved papers into reading lists, evidence maps and shareable context.ResearchReconstruct the path that led you from search to paper to question.CollaborationMove from a paper, topic or expert request into a focused thread.PublishCreate full-text research articles with metadata, formulas and versions.

Network

ExpertsFind specialists whose work and reviews explain why they can help.CommunitiesJoin research groups organized around papers, topics and shared evidence.

Opportunities

ListingsBrowse roles, calls and collaborations connected to real research context.

Account

Log inReturn to your saved papers, graph views and active threads.Create accountStart saving papers, building a research trail and joining teams.
Log inCreate account

Source author record

Paulo Tabuada

Paulo Tabuada appears in the imported research catalog. Authorship, coauthor and topic links are available while profile ownership is still unclaimed.

ResearcherUnclaimed source record
math.OCSystems and ControlCryptography and SecurityInformation Theorymath.ITeess.SYLogic in Computer ScienceComputational ComplexityFormal Languages and Automata TheoryComputer Science and Game Theoryeess.SPMachine Learningmath.DSNetworking and Internet ArchitectureRobotics

Catalog footprint

What is connected

31works
15topics
4close collaborators

Actions

Connect this record

Log in to claim
Open graphBrowse works

Research graph

See the researcher in context

Open full explorer

Inspect adjacent papers, topics, institutions and collaborators without losing the researcher page.

Building this map preview

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

Published work

31 published item(s)

preprint2022arXiv

Controlled invariant sets: implicit closed-form representations and applications

We revisit the problem of computing (robust) controlled invariant sets for discrete-time linear systems. Departing from previous approaches, we consider implicit, rather than explicit, representations for controlled invariant sets. Moreover, by considering such representations in the space of states and finite input sequences we obtain closed-form expressions for controlled invariant sets. An immediate advantage is the ability to handle high-dimensional systems since the closed-form expression is computed in a single step rather than iteratively. To validate the proposed method, we present thorough case studies illustrating that in safety-critical scenarios the implicit representation suffices in place of the explicit invariant set. The proposed method is complete in the absence of disturbances, and we provide a weak completeness result when disturbances are present.

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

Dirty derivatives for output feedback stabilization

Dirty derivatives are routinely used in industrial settings, particularly in the implementation of the derivative term in PID control, and are especially appealing due to their noise-attenuation and model-free characteristics. In this paper, we provide a Lyapunov-based proof for the stability of linear time-invariant control systems in controller canonical form when utilizing dirty derivatives in place of observers for the purpose of output feedback. This is, to the best of the authors' knowledge, the first time that stability proofs are provided for the use of dirty derivatives in lieu of derivatives of different orders. In the spirit of adaptive control, we also show how dirty derivatives can be used for output feedback control when the control gain is unknown.

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

From LTL to rLTL Monitoring: Improved Monitorability through Robust Semantics

Runtime monitoring is commonly used to detect the violation of desired properties in safety critical cyber-physical systems by observing its executions. Bauer et al. introduced an influential framework for monitoring Linear Temporal Logic (LTL) properties based on a three-valued semantics: the formula is already satisfied by the given prefix, it is already violated, or it is still undetermined, i.e., it can still be satisfied and violated by appropriate extensions. However, a wide range of formulas are not monitorable under this approach, meaning that they have a prefix for which satisfaction and violation will always remain undetermined no matter how it is extended. In particular, Bauer et al. report that 44% of the formulas they consider in their experiments fall into this category. Recently, a robust semantics for LTL was introduced to capture different degrees by which a property can be violated. In this paper we introduce a robust semantics for finite strings and show its potential in monitoring: every formula considered by Bauer et al. is monitorable under our approach. Furthermore, we discuss which properties that come naturally in LTL monitoring - such as the realizability of all truth values - can be transferred to the robust setting. Lastly, we show that LTL formulas with robust semantics can be monitored by deterministic automata and report on a prototype implementation.

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

Learning to control from expert demonstrations

In this paper, we revisit the problem of learning a stabilizing controller from a finite number of demonstrations by an expert. By first focusing on feedback linearizable systems, we show how to combine expert demonstrations into a stabilizing controller, provided that demonstrations are sufficiently long and there are at least $n+1$ of them, where $n$ is the number of states of the system being controlled. When we have more than $n+1$ demonstrations, we discuss how to optimally choose the best $n+1$ demonstrations to construct the stabilizing controller. We then extend these results to a class of systems that can be embedded into a higher-dimensional system containing a chain of integrators. The feasibility of the proposed algorithm is demonstrated by applying it on a CrazyFlie 2.0 quadrotor.

0 citations0 reviewsNo code linkedOpen access
preprint2021arXiv

Being correct is not enough: efficient verification using robust linear temporal logic

While most approaches in formal methods address system correctness, ensuring robustness has remained a challenge. In this paper we present and study the logic rLTL which provides a means to formally reason about both correctness and robustness in system design. Furthermore, we identify a large fragment of rLTL for which the verification problem can be efficiently solved, i.e., verification can be done by using an automaton, recognizing the behaviors described by the rLTL formula $φ$, of size at most $\mathcal{O} \left( 3^{ |φ|} \right)$, where $|φ|$ is the length of $φ$. This result improves upon the previously known bound of $\mathcal{O}\left(5^{|φ|} \right)$ for rLTL verification and is closer to the LTL bound of $\mathcal{O}\left( 2^{|φ|} \right)$. The usefulness of this fragment is demonstrated by a number of case studies showing its practical significance in terms of expressiveness, the ability to describe robustness, and the fine-grained information that rLTL brings to the process of system verification. Moreover, these advantages come at a low computational overhead with respect to LTL verification.

0 citations0 reviewsNo code linkedOpen access
preprint2021arXiv

Sampled-Data Stabilization with Control Lyapunov Functions via Quadratically Constrained Quadratic Programs

Controller design for nonlinear systems with Control Lyapunov Function (CLF) based quadratic programs has recently been successfully applied to a diverse set of difficult control tasks. These existing formulations do not address the gap between design with continuous time models and the discrete time sampled implementation of the resulting controllers, often leading to poor performance on hardware platforms. We propose an approach to close this gap by synthesizing sampled-data counterparts to these CLF-based controllers, specified as quadratically constrained quadratic programs (QCQPs). Assuming feedback linearizability and stable zero-dynamics of a system's continuous time model, we derive practical stability guarantees for the resulting sampled-data system. We demonstrate improved performance of the proposed approach over continuous time counterparts in simulation.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

Distortion based Light-weight Security for Cyber-Physical Systems

In Cyber-Physical Systems (CPS), inference based on communicated data is of critical significance as it can be used to manipulate or damage the control operations by adversaries. This calls for efficient mechanisms for secure transmission of data since control systems are becoming increasingly distributed over larger geographical areas. Distortion based security, recently proposed as one candidate for secure transmissions in CPS, is not only more appropriate for these applications but also quite frugal in terms of prior requirements on shared keys. In this paper, we propose distortion-based metrics to protect CPS communication and show that it is possible to confuse adversaries with just a few bits of pre-shared keys. In particular, we will show that a linear dynamical system can communicate its state in a manner that prevents an eavesdropper from accurately learning the state.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

Privacy Against Adversarial Classification in Cyber-Physical Systems

For a class of Cyber-Physical Systems (CPSs), we address the problem of performing computations over the cloud without revealing private information about the structure and operation of the system. We model CPSs as a collection of input-output dynamical systems (the system operation modes). Depending on the mode the system is operating on, the output trajectory is generated by one of these systems in response to driving inputs. Output measurements and driving inputs are sent to the cloud for processing purposes. We capture this "processing" through some function (of the input-output trajectory) that we require the cloud to compute accurately - referred here as the trajectory utility. However, for privacy reasons, we would like to keep the mode private, i.e., we do not want the cloud to correctly identify what mode of the CPS produced a given trajectory. To this end, we distort trajectories before transmission and send the corrupted data to the cloud. We provide mathematical tools (based on output-regulation techniques) to properly design distorting mechanisms so that: 1) the original and distorted trajectories lead to the same utility; and the distorted data leads the cloud to misclassify the mode.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

Rapid Top-Down Synthesis of Large-Scale IoT Networks

Advances in optimization and constraint satisfaction techniques, together with the availability of elastic computing resources, have spurred interest in large-scale network verification and synthesis. Motivated by this, we consider the top-down synthesis of ad-hoc IoT networks for disaster response and search and rescue operations. This synthesis problem must satisfy complex and competing constraints: sensor coverage, line-of-sight visibility, and network connectivity. The central challenge in our synthesis problem is quickly scaling to large regions while producing cost-effective solutions. We explore two qualitatively different representations of the synthesis problems satisfiability modulo convex optimization (SMC), and mixed-integer linear programming (MILP). The former is more expressive, for our problem, than the latter, but is less well-suited for solving optimization problems like ours. We show how to express our network synthesis in these frameworks, and, to scale to problem sizes beyond what these frameworks are capable of, develop a hierarchical synthesis technique that independently synthesizes networks in sub-regions of the deployment area, then combines these. We find that, while MILP outperforms SMC in some settings for smaller problem sizes, the fact that SMC's expressivity matches our problem ensures that it uniformly generates better quality solutions at larger problem sizes.

0 citations0 reviewsNo code linkedOpen access
preprint2016arXiv

Dynamics-Based Reactive Synthesis and Automated Revisions for High-Level Robot Control

The aim of this work is to address issues where formal specifications cannot be realized on a given dynamical system subjected to a changing environment. Such failures occur whenever the dynamics of the system restrict the robot in such a way that the environment may prevent the robot from progressing safely to its goals. We provide a framework that automatically synthesizes revisions to such specifications that restrict the assumed behaviors of the environment and the behaviors of the system. We provide a means for explaining such modifications to the user in a concise, easy-to-understand manner. Integral to the framework is a new algorithm for synthesizing controllers for reactive specifications that include a discrete representation of the robot's dynamics. The new approach is demonstrated with a complex task implemented using a unicycle model.

0 citations0 reviewsNo code linkedOpen access
preprint2016arXiv

Mode-Target Games: Reactive Synthesis for Control Applications

In this paper we introduce a class of Linear Temporal Logic (LTL) specifications for which the problem of synthesizing controllers can be solved in polynomial time. The new class of specifications is an LTL fragment that we term Mode-Target (MT) and is inspired by numerous control applications where there are modes and corresponding (possibly multiple) targets for each mode. We formulate the problem of synthesizing a controller enforcing an MT specification as a game and provide an algorithm that requires $O(\sum_i t_i n^2)$ symbolic steps, where $n$ is the number of states in the game graph, and $t_i$ is the number of targets corresponding to mode $i$.

0 citations0 reviewsNo code linkedOpen access
preprint2016arXiv

Robustness of Control Barrier Functions for Safety Critical Control

Barrier functions (also called certificates) have been an important tool for the verification of hybrid systems, and have also played important roles in optimization and multi-objective control. The extension of a barrier function to a controlled system results in a control barrier function. This can be thought of as being analogous to how Sontag extended Lyapunov functions to control Lyapunov functions in order to enable controller synthesis for stabilization tasks. A control barrier function enables controller synthesis for safety requirements specified by forward invariance of a set using a Lyapunov-like condition. This paper develops several important extensions to the notion of a control barrier function. The first involves robustness under perturbations to the vector field defining the system. Input-to-State stability conditions are given that provide for forward invariance, when disturbances are present, of a "relaxation" of set rendered invariant without disturbances. A control barrier function can be combined with a control Lyapunov function in a quadratic program to achieve a control objective subject to safety guarantees. The second result of the paper gives conditions for the control law obtained by solving the quadratic program to be Lipschitz continuous and therefore to gives rise to well-defined solutions of the resulting closed-loop system.

0 citations0 reviewsNo code linkedOpen access
preprint2015arXiv

A Satisfiability Modulo Theory Approach to Secure State Reconstruction in Differentially Flat Systems Under Sensor Attacks

We address the problem of estimating the state of a differentially flat system from measurements that may be corrupted by an adversarial attack. In cyber-physical systems, malicious attacks can directly compromise the system's sensors or manipulate the communication between sensors and controllers. We consider attacks that only corrupt a subset of sensor measurements. We show that the possibility of reconstructing the state under such attacks is characterized by a suitable generalization of the notion of s-sparse observability, previously introduced by some of the authors in the linear case. We also extend our previous work on the use of Satisfiability Modulo Theory solvers to estimate the state under sensor attacks to the context of differentially flat systems. The effectiveness of our approach is illustrated on the problem of controlling a quadrotor under sensor attacks.

0 citations0 reviewsNo code linkedOpen access
preprint2015arXiv

Comparing Asynchronous $l$-Complete Approximations and Quotient Based Abstractions

This paper is concerned with a detailed comparison of two different abstraction techniques for the construction of finite state symbolic models for controller synthesis of hybrid systems. Namely, we compare quotient based abstractions (QBA), with different realizations of strongest (asynchronous) $l$-complete approximations (SAlCA) Even though the idea behind their construction is very similar, we show that they are generally incomparable both in terms of behavioral inclusion and similarity relations. We therefore derive necessary and sufficient conditions for QBA to coincide with particular realizations of SAlCA. Depending on the original system, either QBA or SAlCA can be a tighter abstraction.

0 citations0 reviewsNo code linkedOpen access
preprint2015arXiv

Robust Linear Temporal Logic

Although it is widely accepted that every system should be robust, in the sense that "small" violations of environment assumptions should lead to "small" violations of system guarantees, it is less clear how to make this intuitive notion of robustness mathematically precise. In this paper, we address this problem by developing a robust version of Linear Temporal Logic (LTL), which we call robust LTL and denote by rLTL. Formulas in rLTL are syntactically identical to LTL formulas but are endowed with a many-valued semantics that encodes robustness. In particular, the semantics of the rLTL formula $φ\Rightarrow ψ$ is such that a "small" violation of the environment assumption $φ$ is guaranteed to only produce a "small" violation of the system guarantee $ψ$. In addition to introducing rLTL, we study the verification and synthesis problems for this logic: similarly to LTL, we show that both problems are decidable, that the verification problem can be solved in time exponential in the number of subformulas of the rLTL formula at hand, and that the synthesis problem can be solved in doubly exponential time.

0 citations0 reviewsNo code linkedOpen access
preprint2015arXiv

Secure State Estimation against Sensor Attacks in the Presence of Noise

We consider the problem of estimating the state of a noisy linear dynamical system when an unknown subset of sensors is arbitrarily corrupted by an adversary. We propose a secure state estimation algorithm, and derive (optimal) bounds on the achievable state estimation error given an upper bound on the number of attacked sensors. The proposed state estimator involves Kalman filters operating over subsets of sensors to search for a sensor subset which is reliable for state estimation. To further improve the subset search time, we propose Satisfiability Modulo Theory based techniques to exploit the combinatorial nature of searching over sensor subsets. Finally, as a result of independent interest, we give a coding theoretic view of attack detection and state estimation against sensor attacks in a noiseless dynamical system.

0 citations0 reviewsNo code linkedOpen access
preprint2015arXiv

Secure State Estimation For Cyber Physical Systems Under Sensor Attacks: A Satisfiability Modulo Theory Approach

We address the problem of detecting and mitigating the effect of malicious attacks to the sensors of a linear dynamical system. We develop a novel, efficient algorithm that uses a Satisfiability-Modulo-Theory approach to isolate the compromised sensors and estimate the system state despite the presence of the attack, thus harnessing the intrinsic combinatorial complexity of the problem. By leveraging results from formal methods over real numbers, we provide guarantees on the soundness and completeness of our algorithm. We then report simulation results to compare its runtime performance with alternative techniques. Finally, we demonstrate its application to the problem of controlling an unmanned ground vehicle.

0 citations0 reviewsNo code linkedOpen access
preprint2015arXiv

Secure State Estimation: Optimal Guarantees against Sensor Attacks in the Presence of Noise

Motivated by the need to secure cyber-physical systems against attacks, we consider the problem of estimating the state of a noisy linear dynamical system when a subset of sensors is arbitrarily corrupted by an adversary. We propose a secure state estimation algorithm and derive (optimal) bounds on the achievable state estimation error. In addition, as a result of independent interest, we give a coding theoretic interpretation for prior work on secure state estimation against sensor attacks in a noiseless dynamical system.

0 citations0 reviewsNo code linkedOpen access
preprint2014arXiv

Compositional Transient Stability Analysis of Multi-Machine Power Networks

During the normal operation of a power system all the voltages and currents are sinusoids with a frequency of 60 Hz in America and parts of Asia, or of 50Hz in the rest of the world. Forcing all the currents and voltages to be sinusoids with the right frequency is one of the most important problems in power systems. This problem is known as the transient stability problem in the power systems literature. The classical models used to study transient stability are based on several implicit assumptions that are violated when transients occur. One such assumption is the use of phasors to study transients. While phasors require sinusoidal waveforms to be well defined, there is no guarantee that waveforms will remain sinusoidal during transients. In this paper, we use energy-based models derived from first principles that are not subject to hard-to-justify classical assumptions. In addition to eliminate assumptions that are known not to hold during transient stages, we derive intuitive conditions ensuring the transient stability of power systems with lossy transmission lines. Furthermore, the conditions for transient stability are compositional in the sense that one infers transient stability of a large power system by checking simple conditions for individual generators.

0 citations0 reviewsNo code linkedOpen access
preprint2014arXiv

Event-Triggered State Observers for Sparse Sensor Noise/Attacks

This paper describes two algorithms for state reconstruction from sensor measurements that are corrupted with sparse, but otherwise arbitrary, "noise". These results are motivated by the need to secure cyber-physical systems against a malicious adversary that can arbitrarily corrupt sensor measurements. The first algorithm reconstructs the state from a batch of sensor measurements while the second algorithm is able to incorporate new measurements as they become available, in the spirit of a Luenberger observer. A distinguishing point of these algorithms is the use of event-triggered techniques to improve the computational performance of the proposed algorithms.

0 citations0 reviewsNo code linkedOpen access
preprint2012arXiv

Secure estimation and control for cyber-physical systems under adversarial attacks

The vast majority of today's critical infrastructure is supported by numerous feedback control loops and an attack on these control loops can have disastrous consequences. This is a major concern since modern control systems are becoming large and decentralized and thus more vulnerable to attacks. This paper is concerned with the estimation and control of linear systems when some of the sensors or actuators are corrupted by an attacker. In the first part we look at the estimation problem where we characterize the resilience of a system to attacks and study the possibility of increasing its resilience by a change of parameters. We then propose an efficient algorithm to estimate the state despite the attacks and we characterize its performance. Our approach is inspired from the areas of error-correction over the reals and compressed sensing. In the second part we consider the problem of designing output-feedback controllers that stabilize the system despite attacks. We show that a principle of separation between estimation and control holds and that the design of resilient output feedback controllers can be reduced to the design of resilient state estimators.

0 citations0 reviewsNo code linkedOpen access
preprint2011arXiv

A theory of robust software synthesis

A key property for systems subject to uncertainty in their operating environment is robustness, ensuring that unmodelled, but bounded, disturbances have only a proportionally bounded effect upon the behaviours of the system. Inspired by ideas from robust control and dissipative systems theory, we present a formal definition of robustness and algorithmic tools for the design of optimally robust controllers for omega-regular properties on discrete transition systems. Formally, we define metric automata - automata equipped with a metric on states - and strategies on metric automata which guarantee robustness for omega-regular properties. We present fixed point algorithms to construct optimally robust strategies in polynomial time. In contrast to strategies computed by classical graph theoretic approaches, the strategies computed by our algorithm ensure that the behaviours of the controlled system gracefully degrade under the action of disturbances; the degree of degradation is parameterized by the magnitude of the disturbance. We show an application of our theory to the design of controllers that tolerate infinitely many transient errors provided they occur infrequently enough.

0 citations0 reviewsNo code linkedOpen access
preprint2011arXiv

A unifying Lyapunov-based framework for the event-triggered control of nonlinear systems

We present a prescriptive framework for the event-triggered control of nonlinear systems. Rather than closing the loop periodically, as traditionally done in digital control, in event-triggered implementations the loop is closed according to a state-dependent criterion. Event-triggered control is especially well suited for embedded systems and networked control systems since it reduces the amount of resources needed for control such as communication bandwidth. By modeling the event-triggered implementations as hybrid systems, we provide Lyapunov-based conditions to guarantee the stability of the resulting closed-loop system and explain how they can be utilized to synthesize event-triggering rules. We illustrate the generality of the approach by showing how it encompasses several existing event-triggering policies and by developing new strategies which further reduce the resources needed for control.

0 citations0 reviewsNo code linkedOpen access
preprint2011arXiv

Decentralized event-triggered control over wireless sensor/actuator networks

In recent years we have witnessed a move of the major industrial automation providers into the wireless domain. While most of these companies already offer wireless products for measurement and monitoring purposes, the ultimate goal is to be able to close feedback loops over wireless networks interconnecting sensors, computation devices, and actuators. In this paper we present a decentralized event-triggered implementation, over sensor/actuator networks, of centralized nonlinear controllers. Event-triggered control has been recently proposed as an alternative to the more traditional periodic execution of control tasks. In a typical event-triggered implementation, the control signals are kept constant until the violation of a condition on the state of the plant triggers the re-computation of the control signals. The possibility of reducing the number of re-computations, and thus of transmissions, while guaranteeing desired levels of performance makes event-triggered control very appealing in the context of sensor/actuator networks. In these systems the communication network is a shared resource and event-triggered implementations of control laws offer a flexible way to reduce network utilization. Moreover reducing the number of times that a feedback control law is executed implies a reduction in transmissions and thus a reduction in energy expenditures of battery powered wireless sensor nodes.

0 citations0 reviewsNo code linkedOpen access
preprint2011arXiv

Event-triggered and self-triggered stabilization of distributed networked control systems

Event-triggered and self-triggered control have recently been proposed as implementation strategies that considerably reduce the resources required for control. Although most of the work so far has focused on closing a single control loop, some researchers have started to investigate how these new implementation strategies can be applied when closing multiple-feedback loops in the presence of physically distributed sensors and actuators. In this paper, we consider a scenario where the distributed sensors, actuators, and controllers communicate via a shared wired channel. We use our recent prescriptive framework for the event-triggered control of nonlinear systems to develop novel policies suitable for the considered distributed scenario. Afterwards, we explain how self-triggering rules can be deduced from the developed event-triggered strategies.

0 citations0 reviewsNo code linkedOpen access
preprint2011arXiv

Exploiting isochrony in self-triggered control

Event-triggered control and self-triggered control have been recently proposed as new implementation paradigms that reduce resource usage for control systems. In self-triggered control, the controller is augmented with the computation of the next time instant at which the feedback control law is to be recomputed. Since these execution instants are obtained as a function of the plant state, we effectively close the loop only when it is required to maintain the desired performance, thereby greatly reducing the resources required for control. In this paper we present a new technique for the computation of the execution instants by exploiting the concept of isochronous manifolds, also introduced in this paper. While our previous results showed how homogeneity can be used to compute the execution instants along some directions in the state space, the concept of isochrony allows us to compute the executions instants along every direction in the state space. Moreover, we also show in this paper how to homogenize smooth control systems thus making our results applicable to any smooth control system. The benefits of the proposed approach with respect to existing techniques are analyzed in two examples.

0 citations0 reviewsNo code linkedOpen access
preprint2011arXiv

Symbolic Approximate Time-Optimal Control

There is an increasing demand for controller design techniques capable of addressing the complex requirements of todays embedded applications. This demand has sparked the interest in symbolic control where lower complexity models of control systems are used to cater for complex specifications given by temporal logics, regular languages, or automata. These specification mechanisms can be regarded as qualitative since they divide the trajectories of the plant into bad trajectories (those that need to be avoided) and good trajectories. However, many applications require also the optimization of quantitative measures of the trajectories retained by the controller, as specified by a cost or utility function. As a first step towards the synthesis of controllers reconciling both qualitative and quantitative specifications, we investigate in this paper the use of symbolic models for time-optimal controller synthesis. We consider systems related by approximate (alternating) simulation relations and show how such relations enable the transfer of time-optimality information between the systems. We then use this insight to synthesize approximately time-optimal controllers for a control system by working with a lower complexity symbolic model. The resulting approximately time-optimal controllers are equipped with upper and lower bounds for the time to reach a target, describing the quality of the controller. The results described in this paper were implemented in the Matlab Toolbox Pessoa which we used to workout several illustrative examples reported in this paper.

0 citations0 reviewsNo code linkedOpen access
preprint2011arXiv

Symbolic models for nonlinear control systems without stability assumptions

Finite-state models of control systems were proposed by several researchers as a convenient mechanism to synthesize controllers enforcing complex specifications. Most techniques for the construction of such symbolic models have two main drawbacks: either they can only be applied to restrictive classes of systems, or they require the exact computation of reachable sets. In this paper, we propose a new abstraction technique that is applicable to any smooth control system as long as we are only interested in its behavior in a compact set. Moreover, the exact computation of reachable sets is not required. The effectiveness of the proposed results is illustrated by synthesizing a controller to steer a vehicle.

0 citations0 reviewsNo code linkedOpen access
preprint2010arXiv

An ISS self-triggered implementation of linear controller

Nowadays control systems are mostly implemented on digital platforms and, increasingly, over shared communication networks. Reducing resources (processor utilization, network bandwidth, etc.) in such implementations increases the potential to run more applications on the same hardware. We present a self-triggered implementation of linear controllers that reduces the amount of controller updates necessary to retain stability of the closed-loop system. Furthermore, we show that the proposed self-triggered implementation is robust against additive disturbances and provide explicit guarantees of performance. The proposed technique exhibits an inherent trade-off between computation and potential savings on actuation.

0 citations0 reviewsNo code linkedOpen access
preprint2010arXiv

Backstepping design for incremental stability

Stability is arguably one of the core concepts upon which our understanding of dynamical and control systems has been built. The related notion of incremental stability, however, has received much less attention until recently, when it was successfully used as a tool for the analysis and design of intrinsic observers, output regulation of nonlinear systems, frequency estimators, synchronization of coupled identical dynamical systems, symbolic models for nonlinear control systems, and bio-molecular systems. However, most of the existing controller design techniques provide controllers enforcing stability rather than incremental stability. Hence, there is a growing need to extend existing methods or develop new ones for the purpose of designing incrementally stabilizing controllers. In this paper, we develop a backstepping design approach for incremental stability. The effectiveness of the proposed method is illustrated by synthesizing a controller rendering a synchronous generator incrementally stable.

0 citations0 reviewsNo code linkedOpen access
preprint2010arXiv

Safety-Guarantee Controller Synthesis for Cyber-Physical Systems

The verification and validation of cyber-physical systems is known to be a difficult problem due to the different modeling abstractions used for control components and for software components. A recent trend to address this difficulty is to reduce the need for verification by adopting correct-by-design methodologies. According to the correct-by-design paradigm, one seeks to automatically synthesize a controller that can be refined into code and that enforces temporal specifications on the cyber-physical system. In this paper we consider an instance of this problem where the specifications are given by a fragment of Linear Temporal Logic (LTL) and the physical environment is described by a smooth differential equation. The contribution of this paper is to show that synthesis for cyber-physical systems is viable by considering a fragment of LTL that is expressive enough to describe interesting properties but simple enough to avoid Safra's construction. We report on two examples illustrating a preliminary implementation of these techniques on the tool PESSOALTL.

0 citations0 reviewsNo code linkedOpen access