Showing 1–42 of 42 results for author: Mazo, M

Data-driven Interval MDP for Robust Control Synthesis

Authors: Rudi Coppola, Andrea Peruffo, Licio Romao, Alessandro Abate, Manuel Mazo Jr

Abstract: The abstraction of dynamical systems is a powerful tool that enables the design of feedback controllers using a correct-by-design framework. We investigate a novel scheme to obtain data-driven abstractions of discrete-time stochastic processes in terms of richer discrete stochastic models, whose actions lead to nondeterministic transitions over the space of probability measures. The data-driven co… ▽ More The abstraction of dynamical systems is a powerful tool that enables the design of feedback controllers using a correct-by-design framework. We investigate a novel scheme to obtain data-driven abstractions of discrete-time stochastic processes in terms of richer discrete stochastic models, whose actions lead to nondeterministic transitions over the space of probability measures. The data-driven component of the proposed methodology lies in the fact that we only assume samples from an unknown probability distribution. We also rely on the model of the underlying dynamics to build our abstraction through backward reachability computations. The nondeterminism in the probability space is captured by a collection of Markov Processes, and we identify how this model can improve upon existing abstraction techniques in terms of satisfying temporal properties, such as safety or reach-avoid. The connection between the discrete and the underlying dynamics is made formal through the use of the scenario approach theory. Numerical experiments illustrate the advantages and main limitations of the proposed techniques with respect to existing approaches. △ Less

Submitted 12 April, 2024; originally announced April 2024.

Comments: 6 pages

Data-Driven Abstractions for Control Systems

Authors: Rudi Coppola, Andrea Peruffo, Manuel Mazo Jr

Abstract: At the intersection of dynamical systems, control theory, and formal methods lies the construction of symbolic abstractions: these typically represent simpler, finite-state models whose behaviour mimics the one of an underlying concrete system but are easier to analyse. Building an abstraction usually requires an accurate knowledge of the underlying model: this knowledge may be costly to gather, e… ▽ More At the intersection of dynamical systems, control theory, and formal methods lies the construction of symbolic abstractions: these typically represent simpler, finite-state models whose behaviour mimics the one of an underlying concrete system but are easier to analyse. Building an abstraction usually requires an accurate knowledge of the underlying model: this knowledge may be costly to gather, especially in real-life applications. We aim to bridge this gap by building abstractions based on sampling finite length trajectories. Adding the controller degrees of freedom, we newly define the notion of probabilistic alternating simulation, and provide probably approximately correct (PAC) guarantees that the constructed abstraction includes all behaviours of the concrete system and that it is suitable for control design, for arbitrarily long time horizons, leveraging the scenario theory. Our method is then tested on several numerical benchmarks. △ Less

Submitted 16 February, 2024; originally announced February 2024.

Advanced monitoring of rail breakage in double-track railway lines by means of PCA techniques

Authors: F. Espinosa, J. J. García, A. Hernández, M. Mazo, J. Ureña, J. A. Jiménez, I. Fernández, C. Pérez, J. C. García

Abstract: This work describes a classifier designed to identify rail breakages in double-track railway lines, completing the electronic equipment carried out by authors. The main objective of this proposal is to guarantee the integrity of tracks before the railway traffic starts working. In addition, it facilitates maintenance tasks providing information about possible breakages. The detection of breakages… ▽ More This work describes a classifier designed to identify rail breakages in double-track railway lines, completing the electronic equipment carried out by authors. The main objective of this proposal is to guarantee the integrity of tracks before the railway traffic starts working. In addition, it facilitates maintenance tasks providing information about possible breakages. The detection of breakages is based on the analysis of eight currents provided by the electronic equipment, one per rail, at the ends of the section (emitting and receiving nodes). The imbalance that occurs among the value of these currents implies that there is at least a breakage in the track section under analysis. This analysis is conducted according to three phases. The first one identifies whether there is a breakage, and, in that case, the damaged track is identified. The second phase provides information about which rail is broken (internal, external or both of them) in the previously identified track. Finally, if there is only one breakage, the third phase estimates its most likely zone along the track section. This situation is considered as a classification problem, and solved by means of the Principal Component Analysis technique. This means that a significant number of measurements is required for every breakage pattern (types of breakages) to be considered. Due to the difficulty of having real data, the proposal has been validated using an 8km-long double-track hardware simulator specially designed by the authors, with specific localizations for breakages. △ Less

Submitted 4 February, 2024; originally announced February 2024.

Journal ref: Applied Soft Computing, 2018

Efficient Strategy Synthesis for Switched Stochastic Systems with Distributional Uncertainty

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

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

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

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

Data-driven Abstractions for Verification of Deterministic Systems

Authors: Rudi Coppola, Andrea Peruffo, Manuel Mazo Jr

Abstract: A common technique to verify complex logic specifications for dynamical systems is the construction of symbolic abstractions: simpler, finite-state models whose behaviour mimics the one of the systems of interest. Typically, abstractions are constructed exploiting an accurate knowledge of the underlying model: in real-life applications, this may be a costly assumption. By sampling random $\ell$-st… ▽ More A common technique to verify complex logic specifications for dynamical systems is the construction of symbolic abstractions: simpler, finite-state models whose behaviour mimics the one of the systems of interest. Typically, abstractions are constructed exploiting an accurate knowledge of the underlying model: in real-life applications, this may be a costly assumption. By sampling random $\ell$-step trajectories of an unknown system, we build an abstraction based on the notion of $\ell$-completeness. We newly define the notion of probabilistic behavioural inclusion, and provide probably approximately correct (PAC) guarantees that this abstraction includes all behaviours of the concrete system, for finite and infinite time horizon, leveraging the scenario theory for non convex problems. Our method is then tested on several numerical benchmarks. △ Less

Submitted 29 March, 2023; v1 submitted 3 November, 2022; originally announced November 2022.

Interval Markov Decision Processes with Continuous Action-Spaces

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

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

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

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

Robust Event-Driven Interactions in Cooperative Multi-Agent Learning

Authors: Daniel Jarne Ornia, Manuel Mazo Jr

Abstract: We present an approach to reduce the communication required between agents in a Multi-Agent learning system by exploiting the inherent robustness of the underlying Markov Decision Process. We compute so-called robustness surrogate functions (off-line), that give agents a conservative indication of how far their state measurements can deviate before they need to update other agents in the system. T… ▽ More We present an approach to reduce the communication required between agents in a Multi-Agent learning system by exploiting the inherent robustness of the underlying Markov Decision Process. We compute so-called robustness surrogate functions (off-line), that give agents a conservative indication of how far their state measurements can deviate before they need to update other agents in the system. This results in fully distributed decision functions, enabling agents to decide when it is necessary to update others. We derive bounds on the optimality of the resulting systems in terms of the discounted sum of rewards obtained, and show these bounds are a function of the design parameters. Additionally, we extend the results for the case where the robustness surrogate functions are learned from data, and present experimental results demonstrating a significant reduction in communication events between agents. △ Less

Submitted 7 September, 2022; v1 submitted 7 April, 2022; originally announced April 2022.

Journal ref: Formal Modeling and Analysis of Timed Systems. FORMATS 2022. Lecture Notes in Computer Science, vol 13465. Springer, Cham

Data-driven Abstractions with Probabilistic Guarantees for Linear PETC Systems

Authors: Andrea Peruffo, Manuel Mazo Jr

Abstract: We employ the scenario approach to compute probably approximately correct (PAC) bounds on the average inter-sample time (AIST) generated by an unknown PETC system, based on a finite number of samples. We extend the scenario approach to multiclass SVM algorithms in order to construct a PAC map between the concrete, unknown state-space and the inter-sample times. We then build a traffic model applyi… ▽ More We employ the scenario approach to compute probably approximately correct (PAC) bounds on the average inter-sample time (AIST) generated by an unknown PETC system, based on a finite number of samples. We extend the scenario approach to multiclass SVM algorithms in order to construct a PAC map between the concrete, unknown state-space and the inter-sample times. We then build a traffic model applying an $\ell$-complete relation and find, in the underlying graph, the cycles of minimum and maximum average weight: these provide lower and upper bounds on the AIST. Numerical benchmarks show the practical applicability of our method, which is compared against model-based state-of-the-art tools. △ Less

Submitted 10 March, 2022; originally announced March 2022.

Comments: 6 pages

A Simpler Alternative: Minimizing Transition Systems Modulo Alternating Simulation Equivalence

Authors: Gabriel de Albuquerque Gleizer, Khushraj Nanik Madnani, Manuel Mazo Jr

Abstract: This paper studies the reduction (abstraction) of finite-state transition systems for control synthesis problems. We revisit the notion of alternating simulation equivalence (ASE), a more relaxed condition than alternating bisimulations, to relate systems and their abstractions. As with alternating bisimulations, ASE preserves the property that the existence of a controller for the abstraction is… ▽ More This paper studies the reduction (abstraction) of finite-state transition systems for control synthesis problems. We revisit the notion of alternating simulation equivalence (ASE), a more relaxed condition than alternating bisimulations, to relate systems and their abstractions. As with alternating bisimulations, ASE preserves the property that the existence of a controller for the abstraction is necessary and sufficient for a controller to exist for the original system. Moreover, being a less stringent condition, ASE can reduce systems further to produce smaller abstractions. We provide an algorithm that produces minimal AS equivalent abstractions. The theoretical results are then applied to obtain (un)schedulability certificates of periodic event-triggered control systems sharing a communication channel. A numerical example illustrates the results. △ Less

Submitted 3 March, 2022; originally announced March 2022.

Comments: Accepted at HSCC'22

ETCetera: beyond Event-Triggered Control

Authors: Giannis Delimpaltadakis, Gabriel de A. Gleizer, Ivo van Straalen, Manuel Mazo Jr

Abstract: We present ETCetera, a Python library developed for the analysis and synthesis of the sampling behaviour of event triggered control (ETC) systems. In particular, the tool constructs abstractions of the sampling behaviour of given ETC systems, in the form of timed automata (TA) or finite-state transition systems (FSTSs). When the abstraction is an FSTS, ETCetera provides diverse manipulation tools… ▽ More We present ETCetera, a Python library developed for the analysis and synthesis of the sampling behaviour of event triggered control (ETC) systems. In particular, the tool constructs abstractions of the sampling behaviour of given ETC systems, in the form of timed automata (TA) or finite-state transition systems (FSTSs). When the abstraction is an FSTS, ETCetera provides diverse manipulation tools for analysis of ETC's sampling performance, synthesis of communication traffic schedulers (when networks shared by multiple ETC loops are considered), and optimization of sampling strategies. Additionally, the TA models may be exported to UPPAAL for analysis and synthesis of schedulers. Several examples of the tool's application for analysis and synthesis problems with different types of dynamics and event-triggered implementations are provided. △ Less

Submitted 10 March, 2022; v1 submitted 3 March, 2022; originally announced March 2022.

Comments: To be presented at the 25th ACM International Conference on Hybrid Systems: Computation and Control 2022 (HSCC 2022)

Formal Analysis of the Sampling Behaviour of Stochastic Event-Triggered Control

Authors: Giannis Delimpaltadakis, Luca Laurenti, Manuel Mazo Jr

Abstract: Analyzing Event-Triggered Control's (ETC) sampling behaviour is of paramount importance, as it enables formal assessment of its sampling performance and prediction of its sampling patterns. In this work, we formally analyze the sampling behaviour of stochastic linear periodic ETC (PETC) systems by computing bounds on associated metrics. Specifically, we consider functions over sequences of state m… ▽ More Analyzing Event-Triggered Control's (ETC) sampling behaviour is of paramount importance, as it enables formal assessment of its sampling performance and prediction of its sampling patterns. In this work, we formally analyze the sampling behaviour of stochastic linear periodic ETC (PETC) systems by computing bounds on associated metrics. Specifically, we consider functions over sequences of state measurements and intersampling times that can be expressed as average, multiplicative or cumulative rewards, and introduce their expectations as metrics on PETC's sampling behaviour. We compute bounds on these expectations, by constructing appropriate Interval Markov Chains equipped with suitable reward structures, that abstract stochastic PETC's sampling behaviour. Our results are illustrated on a numerical example, for which we compute bounds on the expected average intersampling time and on the probability of triggering with the maximum possible intersampling time in a finite horizon. △ Less

Submitted 21 February, 2022; originally announced February 2022.

Comments: Under review

Chaos and order in event-triggered control

Authors: Gabriel de Albuquerque Gleizer, Manuel Mazo Jr

Abstract: Event-triggered control (ETC) is claimed to provide enormous reductions in sampling frequency when compared to periodic sampling, but little is formally known about its generated traffic. This work shows that ETC can exhibit very complex, even chaotic traffic, especially when the triggering condition is aggressive in reducing communications. First, we characterize limit traffic patterns by observi… ▽ More Event-triggered control (ETC) is claimed to provide enormous reductions in sampling frequency when compared to periodic sampling, but little is formally known about its generated traffic. This work shows that ETC can exhibit very complex, even chaotic traffic, especially when the triggering condition is aggressive in reducing communications. First, we characterize limit traffic patterns by observing invariant lines and planes through the origin, as well as their attractivity. Then, we present abstraction-based methods to compute limit metrics, such as limit average and limit inferior inter-sample time (IST) of periodic ETC (PETC), with considerations to the robustness of such metrics, as well as measuring the emergence of chaos. The methodology and tools allow us to find ETC examples that provably outperform periodic sampling in terms of average IST. In particular for PETC, we prove that this requires aperiodic or chaotic traffic. △ Less

Submitted 9 February, 2022; v1 submitted 12 January, 2022; originally announced January 2022.

Computing the average inter-sample time of event-triggered control using quantitative automata

Authors: Gabriel de Albuquerque Gleizer, Manuel Mazo Jr

Abstract: Event-triggered control (ETC) is a major recent development in cyber-physical systems due to its capability of reducing resource utilization in networked devices. However, while most of the ETC literature reports simulations indicating massive reductions in the sampling required for control, no method so far has been capable of quantifying these results. In this work, we propose an approach throug… ▽ More Event-triggered control (ETC) is a major recent development in cyber-physical systems due to its capability of reducing resource utilization in networked devices. However, while most of the ETC literature reports simulations indicating massive reductions in the sampling required for control, no method so far has been capable of quantifying these results. In this work, we propose an approach through finite-state abstractions to do formal quantification of the traffic generated by ETC of linear systems, in particular aiming at computing its smallest average inter-sample time (SAIST). The method involves abstracting the traffic model through $l$-complete abstractions, finding the cycle of minimum average length in the graph associated to it, and verifying whether this cycle is an infinitely recurring traffic pattern. The method is proven to be robust to sufficiently small model uncertainties, which allows its application to compute the SAIST of ETC of nonlinear systems. △ Less

Submitted 9 February, 2022; v1 submitted 29 September, 2021; originally announced September 2021.

Comments: Submitted to Nonlinear Analysis: Hybrid Systems v2: fixing plant and controller data of numerical example in Sec. 6.2

Self-Triggered Control for Near-Maximal Average Inter-Sample Time

Authors: Gabriel de Albuquerque Gleizer, Khushraj Madnani, Manuel Mazo Jr

Abstract: Self-triggered control (STC) is a sample-and-hold control method aimed at reducing communications within networked-control systems; however, existing STC mechanisms often maximize how late the next sample is, and as such they do not provide any sampling optimality in the long-term. In this work, we devise a method to construct self-triggered policies that provide near-maximal average inter-sample… ▽ More Self-triggered control (STC) is a sample-and-hold control method aimed at reducing communications within networked-control systems; however, existing STC mechanisms often maximize how late the next sample is, and as such they do not provide any sampling optimality in the long-term. In this work, we devise a method to construct self-triggered policies that provide near-maximal average inter-sample time (AIST) while respecting given control performance constraints. To achieve this, we rely on finite-state abstractions of a reference event-triggered control, in which early triggers are also allowed. These early triggers constitute controllable actions of the abstraction, for which an AIST-maximizing strategy can be computed by solving a mean-payoff game. We provide optimality bounds, and how to further improve them through abstraction refinement techniques. △ Less

Submitted 7 May, 2021; originally announced May 2021.

Comments: Submitted to IEEE CDC '21

Abstracting the Sampling Behaviour of Stochastic Linear Periodic Event-Triggered Control Systems

Authors: Giannis Delimpaltadakis, Luca Laurenti, Manuel Mazo Jr

Abstract: Recently, there have been efforts towards understanding the sampling behaviour of event-triggered control (ETC), for obtaining metrics on its sampling performance and predicting its sampling patterns. Finite-state abstractions, capturing the sampling behaviour of ETC systems, have proven promising in this respect. So far, such abstractions have been constructed for non-stochastic systems. Here, in… ▽ More Recently, there have been efforts towards understanding the sampling behaviour of event-triggered control (ETC), for obtaining metrics on its sampling performance and predicting its sampling patterns. Finite-state abstractions, capturing the sampling behaviour of ETC systems, have proven promising in this respect. So far, such abstractions have been constructed for non-stochastic systems. Here, inspired by this framework, we abstract the sampling behaviour of stochastic narrow-sense linear periodic ETC (PETC) systems via Interval Markov Chains (IMCs). Particularly, we define functions over sequences of state-measurements and interevent times that can be expressed as discounted cumulative sums of rewards, and compute bounds on their expected values by constructing appropriate IMCs and equip** them with suitable rewards. Finally, we argue that our results are extendable to more general forms of functions, thus providing a generic framework to define and study various ETC sampling indicators. △ Less

Submitted 27 September, 2021; v1 submitted 25 March, 2021; originally announced March 2021.

Comments: To appear at the 60th IEEE Conference on Decision and Control (CDC), 2021

Journal ref: 2021 60th IEEE Conference on Decision and Control (CDC), 2021, pp. 1287-1294

Mean Field Behaviour of Collaborative Multi-Agent Foragers

Authors: Daniel Jarne Ornia, Pedro J Zufiria, Manuel Mazo Jr

Abstract: Collaborative multi-agent robotic systems where agents coordinate by modifying a shared environment often result in undesired dynamical couplings that complicate the analysis and experiments when solving a specific problem or task. Simultaneously, biologically-inspired robotics rely on simplifying agents and increasing their number to obtain more efficient solutions to such problems, drawing simil… ▽ More Collaborative multi-agent robotic systems where agents coordinate by modifying a shared environment often result in undesired dynamical couplings that complicate the analysis and experiments when solving a specific problem or task. Simultaneously, biologically-inspired robotics rely on simplifying agents and increasing their number to obtain more efficient solutions to such problems, drawing similarities with natural processes. In this work we focus on the problem of a biologically-inspired multi-agent system solving collaborative foraging. We show how mean field techniques can be used to re-formulate such a stochastic multi-agent problem into a deterministic autonomous system. This de-couples agent dynamics, enabling the computation of limit behaviours and the analysis of optimality guarantees. Furthermore, we analyse how having finite number of agents affects the performance when compared to the mean field limit and we discuss the implications of such limit approximations in this multi-agent system, which have impact on more general collaborative stochastic problems. △ Less

Submitted 9 March, 2022; v1 submitted 13 March, 2021; originally announced March 2021.

Comments: Accepted for Publication in IEEE Transactions on Robotics, available for Early Access on 7 March 2022

Computing the sampling performance of event-triggered control

Authors: Gabriel de Albuquerque Gleizer, Manuel Mazo Jr

Abstract: In the context of networked control systems, event-triggered control (ETC) has emerged as a major topic due to its alleged resource usage reduction capabilities. However, this is mainly supported by numerical simulations, and very little is formally known about the traffic generated by ETC. This work devises a method to estimate, and in some cases to determine exactly, the minimum average inter-sa… ▽ More In the context of networked control systems, event-triggered control (ETC) has emerged as a major topic due to its alleged resource usage reduction capabilities. However, this is mainly supported by numerical simulations, and very little is formally known about the traffic generated by ETC. This work devises a method to estimate, and in some cases to determine exactly, the minimum average inter-sample time (MAIST) generated by periodic event-triggered control (PETC) of linear systems. The method involves abstracting the traffic model using a bisimulation refinement algorithm and finding the cycle of minimum average length in the graph associated to it. This always gives a lower bound to the actual MAIST. Moreover, if this cycle turns out to be related to a periodic solution of the closed-loop PETC system, the performance metric is exact. △ Less

Submitted 1 March, 2021; originally announced March 2021.

Comments: Accepted at HSCC 2021

The Wireless Control Bus: Enabling Efficient Multi-hop Event-Triggered Control with Concurrent Transmissions

Authors: Matteo Trobinger, Gabriel de Albuquerque Gleizer, Timofei Istomin, Manuel Mazo Jr., Amy L. Murphy, Gian Pietro Picco

Abstract: Event-triggered control (ETC) holds the potential to significantly improve the efficiency of wireless networked control systems. Unfortunately, its real-world impact has hitherto been hampered by the lack of a network stack able to transfer its benefits from theory to practice specifically by supporting the latency and reliability requirements of the aperiodic communication ETC induces. This is pr… ▽ More Event-triggered control (ETC) holds the potential to significantly improve the efficiency of wireless networked control systems. Unfortunately, its real-world impact has hitherto been hampered by the lack of a network stack able to transfer its benefits from theory to practice specifically by supporting the latency and reliability requirements of the aperiodic communication ETC induces. This is precisely the contribution of this paper. Our Wireless Control Bus (WCB) exploits carefully orchestrated network-wide floods of concurrent transmissions to minimize overhead during quiescent, steady-state periods, and ensures timely and reliable collection of sensor readings and dissemination of actuation commands when an ETC triggering condition is violated. Using a cyber-physical testbed emulating a water distribution system controlled over a real-world multi-hop wireless network, we show that ETC over WCB achieves the same quality of periodic control at a fraction of the energy costs, therefore unleashing and concretely demonstrating its full potential for the first time. △ Less

Submitted 17 October, 2021; v1 submitted 26 January, 2021; originally announced January 2021.

Comments: To appear in ACM Transactions on Cyber-Physical Systems (TCPS), 28 pages

Abstracting the Traffic of Nonlinear Event-Triggered Control Systems

Authors: Giannis Delimpaltadakis, Manuel Mazo Jr

Abstract: Scheduling communication traffic in networks of event-triggered control (ETC) systems is challenging, as their sampling times are unknown, hindering application of ETC in networks. In previous work, finite-state abstractions were created, capturing the sampling behaviour of LTI ETC systems with quadratic triggering functions. Offering an infinite-horizon look to all sampling patterns of an ETC sys… ▽ More Scheduling communication traffic in networks of event-triggered control (ETC) systems is challenging, as their sampling times are unknown, hindering application of ETC in networks. In previous work, finite-state abstractions were created, capturing the sampling behaviour of LTI ETC systems with quadratic triggering functions. Offering an infinite-horizon look to all sampling patterns of an ETC system, such abstractions can be used for scheduling of ETC traffic. Here we significantly extend this framework, by abstracting perturbed uncertain nonlinear ETC systems with general triggering functions. To construct an ETC system's abstraction: a) the state space is partitioned into regions, b) for each region an interval is determined, containing all intersampling times of points in the region, and c) the abstraction's transitions are determined through reachability analysis. To determine intervals and transitions, we devise algorithms based on reachability analysis. For partitioning, we propose an approach based on isochronous manifolds, resulting into tighter intervals and providing control over them, thus containing the abstraction's non-determinism. Simulations showcase our developments. △ Less

Submitted 15 June, 2021; v1 submitted 23 October, 2020; originally announced October 2020.

Self-Triggered Output-Feedback Control of LTI Systems Subject to Disturbances and Noise

Authors: Gabriel de Albuquerque Gleizer, Manuel Mazo Jr

Abstract: Self-triggered control (STC) and periodic event-triggered control (PETC) are aperiodic sampling techniques aiming at reducing control data communication when compared to periodic sampling. In both techniques, the effects of measurement noise in continuous-time systems with output feedback are unaddressed. In this work we prove that additive noise does not hinder stability of output-feedback PETC o… ▽ More Self-triggered control (STC) and periodic event-triggered control (PETC) are aperiodic sampling techniques aiming at reducing control data communication when compared to periodic sampling. In both techniques, the effects of measurement noise in continuous-time systems with output feedback are unaddressed. In this work we prove that additive noise does not hinder stability of output-feedback PETC of linear time-invariant (LTI) systems. Then we build an STC strategy that estimates PETC's worst-case triggering times. To accomplish this, we use set-based methods, more specifically ellipsoidal sets, which describe uncertainties on state, disturbances and noise. Ellipsoidal reachability is then used to predict worst-case triggering condition violations, ultimately determining the next communication time. The ellipsoidal state estimate is recursively updated using guaranteed state estimation (GSE) methods. The proposed STC is designed to be computationally tractable at the expense of some added conservatism. It is expected to be a practical STC implementation for a broad range of applications. △ Less

Submitted 9 July, 2020; v1 submitted 6 July, 2020; originally announced July 2020.

Comments: Manuscript accepted in Automatica

Formal synthesis of closed-form sampled-data controllers for nonlinear continuous-time systems under STL specifications

Authors: Cees F. Verdier, Niklas Kochdumper, Matthias Althoff, Manuel Mazo Jr

Abstract: We propose a counterexample-guided inductive synthesis framework for the formal synthesis of closed-form sampled-data controllers for nonlinear systems to meet STL specifications over finite-time trajectories. Rather than stating the STL specification for a single initial condition, we consider an (infinite and bounded) set of initial conditions. Candidate solutions are proposed using genetic prog… ▽ More We propose a counterexample-guided inductive synthesis framework for the formal synthesis of closed-form sampled-data controllers for nonlinear systems to meet STL specifications over finite-time trajectories. Rather than stating the STL specification for a single initial condition, we consider an (infinite and bounded) set of initial conditions. Candidate solutions are proposed using genetic programming, which evolves controllers based on a finite number of simulations. Subsequently, the best candidate is verified using reachability analysis; if the candidate solution does not satisfy the specification, an initial condition violating the specification is extracted as a counterexample. Based on this counterexample, candidate solutions are refined until eventually a solution is found (or a user-specified number of iterations is met). The resulting sampled-data controller is expressed as a closed-form expression, enabling both interpretability and the implementation in embedded hardware with limited memory and computation power. The effectiveness of our approach is demonstrated for multiple systems. △ Less

Submitted 20 March, 2021; v1 submitted 7 June, 2020; originally announced June 2020.

Comments: submitted to Automatica

Towards Traffic Bisimulation of Linear Periodic Event-Triggered Controllers

Authors: Gabriel de A. Gleizer, Manuel Mazo Jr

Abstract: We provide a method to construct finite abstractions exactly bisimilar to linear systems under a modified periodic event-triggered control (PETC), when considering as output the inter-event times they generate. Assuming that the initial state lies on a known compact set, these finite-state models can exactly predict all sequences of sampling times until a specified Lyapunov sublevel set is reached… ▽ More We provide a method to construct finite abstractions exactly bisimilar to linear systems under a modified periodic event-triggered control (PETC), when considering as output the inter-event times they generate. Assuming that the initial state lies on a known compact set, these finite-state models can exactly predict all sequences of sampling times until a specified Lyapunov sublevel set is reached. Based on these results, we provide a way to build tight models simulating the traffic of conventional PETC. These models allow computing tight bounds of the PETC average frequency and global exponential stability (GES) decay rate. Our results are demonstrated through a numerical case study. △ Less

Submitted 29 May, 2020; originally announced May 2020.

Comments: Accepted at IEEE Control Systems Letters

Journal ref: IEEE Control Systems Letters, vol. 5, no. 1, pp. 25-30, Jan. 2021

Region-Based Self-Triggered Control for Perturbed and Uncertain Nonlinear Systems

Authors: Giannis Delimpaltadakis, Manuel Mazo Jr

Abstract: In this work, we derive a region-based self-triggered control (STC) scheme for nonlinear systems with bounded disturbances and model uncertainties. The proposed STC scheme is able to guarantee different performance specifications (e.g. stability, boundedness, etc.), depending on the event-triggered control (ETC) triggering function that is chosen to be emulated. To deal with disturbances and uncer… ▽ More In this work, we derive a region-based self-triggered control (STC) scheme for nonlinear systems with bounded disturbances and model uncertainties. The proposed STC scheme is able to guarantee different performance specifications (e.g. stability, boundedness, etc.), depending on the event-triggered control (ETC) triggering function that is chosen to be emulated. To deal with disturbances and uncertainties, we employ differential inclusions (DIs). By introducing ETC/STC notions in the context of DIs, we extend well-known results on ETC/STC to perturbed uncertain systems. Given these results, and adapting tools from our previous work, we derive inner-approximations of isochronous manifolds of perturbed uncertain ETC systems. These approximations dictate a partition of the state-space into regions, each of which is associated to a uniform inter-sampling time. At each sampling time instant, the controller checks to which region the measured state belongs and correspondingly decides the next sampling instant. △ Less

Submitted 11 January, 2021; v1 submitted 1 May, 2020; originally announced May 2020.

Journal ref: IEEE Transactions on Control of Network Systems, vol. 8, no. 2, pp. 757-768, June 2021

Formal controller synthesis for hybrid systems using genetic programming

Authors: Cees F. Verdier, Manuel Mazo Jr

Abstract: This paper proposes a framework for automatic formal controller synthesis for general hybrid systems with a subset of safety and reachability specifications. The framework uses genetic programming to automatically co-synthesize controllers and candidate Lyapunov-like functions. These candidate Lyapunov-like functions are used to formally verify the control specification, and their correctness is p… ▽ More This paper proposes a framework for automatic formal controller synthesis for general hybrid systems with a subset of safety and reachability specifications. The framework uses genetic programming to automatically co-synthesize controllers and candidate Lyapunov-like functions. These candidate Lyapunov-like functions are used to formally verify the control specification, and their correctness is proven using a Satisfiability Modulo Theories solver. The advantages of this approach are: no restriction is made to polynomial systems, the synthesized controllers are expressed as compact expressions, and no explicit solution structure has to be specified beforehand. We demonstrate the effectiveness of the proposed framework in several case studies, including nonpolynomial systems, sampled-data systems, systems with bounded uncertainties, switched systems, and systems with jumps. osed framework in several case studies, including nonpolynomial systems, sampled-data systems, systems with bounded uncertainties, switched systems, and systems with jumps. △ Less

Submitted 15 September, 2020; v1 submitted 31 March, 2020; originally announced March 2020.

Comments: Revised version (9/15/2020)

Traffic Abstractions of Nonlinear Homogeneous Event-Triggered Control Systems

Authors: Giannis Delimpaltadakis, Manuel Mazo Jr

Abstract: In previous work, linear time-invariant event-triggered control (ETC) systems were abstracted to finite-state systems that capture the original systems' sampling behaviour. It was shown that these abstractions can be employed for scheduling of communication traffic in networks of ETC loops. In this paper, we extend this framework to the class of nonlinear homogeneous systems, however adopting a di… ▽ More In previous work, linear time-invariant event-triggered control (ETC) systems were abstracted to finite-state systems that capture the original systems' sampling behaviour. It was shown that these abstractions can be employed for scheduling of communication traffic in networks of ETC loops. In this paper, we extend this framework to the class of nonlinear homogeneous systems, however adopting a different approach in a number of steps. Finally, we discuss how the proposed methodology could be extended to general nonlinear systems. △ Less

Submitted 20 March, 2020; originally announced March 2020.

Journal ref: 2020 59th IEEE Conference on Decision and Control (CDC), 2020, pp. 4991-4998

Scalable Traffic Models for Scheduling of Linear Periodic Event-Triggered Controllers

Authors: Gabriel de Albuquerque Gleizer, Manuel Mazo Jr

Abstract: This paper addresses the problem of modeling and scheduling the transmissions generated by multiple event-triggered control (ETC) loops sharing a network. We present a method to build a symbolic traffic model of periodic ETC (PETC), which by construction provides an exact simulation of such traffic. The model is made in such a way as to avoid the combinatorial explosion that is typical of symbolic… ▽ More This paper addresses the problem of modeling and scheduling the transmissions generated by multiple event-triggered control (ETC) loops sharing a network. We present a method to build a symbolic traffic model of periodic ETC (PETC), which by construction provides an exact simulation of such traffic. The model is made in such a way as to avoid the combinatorial explosion that is typical of symbolic models in many applications. It is augmented with early triggering actions that can be used by a scheduler to mitigate communication conflicts. The complete networked control system is then modeled as a network of timed game automata, for which existing tools can generate a strategy that avoids communication conflicts, while kee** early triggers to a minimum. By construction, our proposed symbolic model is a quotient model of the PETC. It is relatively fast to build, and it generates few to no spurious transitions. We finally demonstrate modeling and scheduling for a numerical example. △ Less

Submitted 12 March, 2021; v1 submitted 17 March, 2020; originally announced March 2020.

Comments: Accepted at the 21st IFAC World Congress (IFAC 2020). Reproducibility note: v4 fixes an issue in the (to-be) published version, where wrong values were reported for the R matrices used in the example LQR controllers. Qualitatively, results are unchanged, but values have been fixed for reproducibility

Isochronous Partitions for Region-Based Self-Triggered Control

Authors: Giannis Delimpaltadakis, Manuel Mazo Jr

Abstract: In this work, we propose a region-based self-triggered control (STC) scheme for nonlinear systems. The state space is partitioned into a finite number of regions, each of which is associated to a uniform inter-event time. The controller, at each sampling time instant, checks to which region does the current state belong, and correspondingly decides the next sampling time instant. To derive the reg… ▽ More In this work, we propose a region-based self-triggered control (STC) scheme for nonlinear systems. The state space is partitioned into a finite number of regions, each of which is associated to a uniform inter-event time. The controller, at each sampling time instant, checks to which region does the current state belong, and correspondingly decides the next sampling time instant. To derive the regions along with their corresponding inter-event times, we use approximations of isochronous manifolds, a notion firstly introduced in [1]. This work addresses some theoretical issues of [1] and proposes an effective computational approach that generates approximations of isochronous manifolds, thus enabling the region-based STC scheme. The efficiency of both our theoretical results and the proposed algorithm are demonstrated through simulation examples. △ Less

Submitted 2 March, 2022; v1 submitted 18 April, 2019; originally announced April 2019.

Comments: One of the numerical examples contains improved results compared to older versions

Journal ref: IEEE Transactions on Automatic Control, vol. 66, no. 3, pp. 1160-1173, March 2021

Formal Synthesis of Analytic Controllers for Sampled-Data Systems via Genetic Programming

Authors: Cees F. Verdier, Manuel Mazo Jr

Abstract: This paper presents an automatic formal controller synthesis method for nonlinear sampled-data systems with safety and reachability specifications. Fundamentally, the presented method is not restricted to polynomial systems and controllers. We consider periodically switched controllers based on a Control Lyapunov Barrier-like functions. The proposed method utilizes genetic programming to synthesiz… ▽ More This paper presents an automatic formal controller synthesis method for nonlinear sampled-data systems with safety and reachability specifications. Fundamentally, the presented method is not restricted to polynomial systems and controllers. We consider periodically switched controllers based on a Control Lyapunov Barrier-like functions. The proposed method utilizes genetic programming to synthesize these functions as well as the controller modes. Correctness of the controller are subsequently verified by means of a Satisfiability Modulo Theories solver. Effectiveness of the proposed methodology is demonstrated on multiple systems. △ Less

Submitted 6 December, 2018; originally announced December 2018.

Comments: The original version of this article has been accepted to CDC 2018. This version contains minor corrections. Supported by NWO Domain TTW under the CADUSY project \#13852

Lyapunov Event-triggered Stabilization with a Known Convergence Rate

Authors: Anton V. Proskurnikov, Manuel Mazo Jr

Abstract: A constructive tool of nonlinear control systems design, the method of Control Lyapunov Functions (CLF) has found numerous applications in stabilization problems for continuous time, discrete-time and hybrid systems. In this paper, we address the fundamental question: given a CLF, corresponding to the continuous-time controller with some predefined (e.g. exponential) convergence rate, can the same… ▽ More A constructive tool of nonlinear control systems design, the method of Control Lyapunov Functions (CLF) has found numerous applications in stabilization problems for continuous time, discrete-time and hybrid systems. In this paper, we address the fundamental question: given a CLF, corresponding to the continuous-time controller with some predefined (e.g. exponential) convergence rate, can the same convergence rate be provided by an event-triggered controller? Under certain assumptions, we give an affirmative answer to this question and show that the corresponding event-based controllers provide positive dwelltimes between the consecutive events. Furthermore, we prove the existence of self-triggered and periodic event-triggered controllers, providing stabilization with a known convergence rate. △ Less

Submitted 14 July, 2020; v1 submitted 23 March, 2018; originally announced March 2018.

Comments: arXiv admin note: text overlap with arXiv:1802.01025

Optimal Symbolic Controllers Determinization for BDD storage

Authors: Ivan S. Zapreev, Cees Verdier, Manuel Mazo Jr

Abstract: Controller synthesis techniques based on symbolic abstractions appeal by producing correct-by-design controllers, under intricate behavioural constraints. Yet, being relations between abstract states and inputs, such controllers are immense in size, which makes them futile for em- bedded platforms. Control-synthesis tools such as PESSOA, SCOTS, and CoSyMA tackle the problem by storing controllers… ▽ More Controller synthesis techniques based on symbolic abstractions appeal by producing correct-by-design controllers, under intricate behavioural constraints. Yet, being relations between abstract states and inputs, such controllers are immense in size, which makes them futile for em- bedded platforms. Control-synthesis tools such as PESSOA, SCOTS, and CoSyMA tackle the problem by storing controllers as binary decision di- agrams (BDDs). However, due to redundantly kee** multiple inputs per-state, the resulting controllers are still too large. In this work, we first show that choosing an optimal controller determinization is an NP- complete problem. Further, we consider the previously known controller determinization technique and discuss its weaknesses. We suggest several new approaches to the problem, based on greedy algorithms, symbolic regression, and (muli-terminal) BDDs. Finally, we empirically compare the techniques and show that some of the new algorithms can produce up to 85% smaller controllers than those obtained with the previous technique. △ Less

Submitted 20 March, 2018; originally announced March 2018.

Comments: Supported by STW-EW as a part of the CADUSY project #13852. The short version of this article has been accepted to ADHS'2018

Lyapunov Design for Event-Triggered Exponential Stabilization

Authors: Anton V. Proskurnikov, Manuel Mazo Jr

Abstract: Control Lyapunov Functions (CLF) method gives a constructive tool for stabilization of nonlinear systems. To find a CLF, many methods have been proposed in the literature, e.g. backstep** for cascaded systems and sum of squares (SOS) programming for polynomial systems. Dealing with continuous-time systems, the CLF-based controller is also continuous-time, whereas practical implementation on a di… ▽ More Control Lyapunov Functions (CLF) method gives a constructive tool for stabilization of nonlinear systems. To find a CLF, many methods have been proposed in the literature, e.g. backstep** for cascaded systems and sum of squares (SOS) programming for polynomial systems. Dealing with continuous-time systems, the CLF-based controller is also continuous-time, whereas practical implementation on a digital platform requires sampled-time control. In this paper, we show that if the continuous-time controller provides exponential stabilization, then an exponentially stabilizing event-triggered control strategy exists with the convergence rate arbitrarily close to the rate of the continuous-time system. △ Less

Submitted 3 February, 2018; originally announced February 2018.

Comments: accepted by ACM HSCC 2018 conference

Traffic Models of Periodic Event-Triggered Control Systems

Authors: Anqi Fu, Manuel Mazo, Jr

Abstract: Periodic event-triggered control (PETC) is a version of event-triggered control (ETC) that only requires to measure the plant output periodically instead of continuously. In this work, we present a construction of timing models for these PETC implementations to capture the dynamics of the traffic they generate. In the construction, we employ a two-step approach. We first partition the state space… ▽ More Periodic event-triggered control (PETC) is a version of event-triggered control (ETC) that only requires to measure the plant output periodically instead of continuously. In this work, we present a construction of timing models for these PETC implementations to capture the dynamics of the traffic they generate. In the construction, we employ a two-step approach. We first partition the state space into a finite number of regions. Then in each region, the event-triggering behavior is analyzed with the help of LMIs. The state transitions among different regions result from computing the reachable state set starting from each region within the computed event time intervals. △ Less

Submitted 9 November, 2017; originally announced November 2017.

Decentralized Periodic Event-Triggered Control with Quantization and Asynchronous Communication

Authors: Anqi Fu, Manuel Mazo Jr

Abstract: Asynchronous decentralized event-triggered control (ADETC) is an implementation of controllers characterized by decentralized event generation, asynchronous sampling updates, and dynamic quantization. Combining those elements in ADETC results in a parsimonious transmission of information which makes it suitable for wireless networked implementations. We extend the previous work on ADETC by introdu… ▽ More Asynchronous decentralized event-triggered control (ADETC) is an implementation of controllers characterized by decentralized event generation, asynchronous sampling updates, and dynamic quantization. Combining those elements in ADETC results in a parsimonious transmission of information which makes it suitable for wireless networked implementations. We extend the previous work on ADETC by introducing periodic sampling, denoting our proposal asynchronous decentralized periodic event-triggered control (ADPETC), and study the stability and L2-gain of ADPETC for implementations affected by disturbances. In ADPETC, at each sampling time, quantized measurements from those sensors that triggered a local event are transmitted to a dynamic controller that computes control actions; the quantized control actions are then transmitted to the corresponding actuators only if certain events are also triggered for the corresponding actuator. The developed theory is demonstrated and illustrated via a numerical example. △ Less

Submitted 10 November, 2017; v1 submitted 29 March, 2017; originally announced March 2017.

Simple synchronization protocols for heterogeneous networks: beyond passivity (extended version)

Authors: Anton V. Proskurnikov, Manuel Mazo Jr

Abstract: Synchronization among autonomous agents via local interactions is one of the benchmark problems in multi-agent control. Whereas synchronization algorithms for identical agents have been thoroughly studied, synchronization of heterogeneous networks still remains a challenging problem. The existing algorithms primarily use the internal model principle, assigning to each agent a local copy of some dy… ▽ More Synchronization among autonomous agents via local interactions is one of the benchmark problems in multi-agent control. Whereas synchronization algorithms for identical agents have been thoroughly studied, synchronization of heterogeneous networks still remains a challenging problem. The existing algorithms primarily use the internal model principle, assigning to each agent a local copy of some dynamical system (internal model). Synchronization of heterogeneous agents thus reduces to global synchronization of identical generators and local synchronization between the agents and their internal models. The internal model approach imposes a number of restrictions and leads to sophisticated dynamical (and, in general, nonlinear) controllers. At the same time, passive heterogeneous agents can be synchronized by a very simple linear protocol, which is used for consensus of first-order integrators. A natural question arises whether analogous algorithms are applicable to synchronization of agents that do not satisfy the passivity condition. In this paper, we study the synchronization problem for heterogeneous agents that are not passive but satisfy a weaker input feedforward passivity (IFP) condition. We show that such agents can also be synchronized by a simple linear protocol, provided that the interaction graph is strongly connected and the couplings are sufficiently weak. We demonstrate how stability of cooperative adaptive cruise control algorithms and some microscopic traffic flow models reduce to synchronization of heterogeneous IFP agents. △ Less

Submitted 8 March, 2017; originally announced March 2017.

Comments: accepted to IFAC World Congress

Evaluation of Decentralized Event-Triggered Control Strategies for Cyber-Physical Systems

Authors: Sokratis Kartakis, Anqi Fu, Manuel Mazo Jr., Julie A. McCann

Abstract: Energy constraint long-range wireless sensor/ actuator based solutions are theoretically the perfect choice to support the next generation of city-scale cyber-physical systems. Traditional systems adopt periodic control which increases network congestion and actuations while burdens the energy consumption. Recent control theory studies overcome these problems by introducing aperiodic strategies, s… ▽ More Energy constraint long-range wireless sensor/ actuator based solutions are theoretically the perfect choice to support the next generation of city-scale cyber-physical systems. Traditional systems adopt periodic control which increases network congestion and actuations while burdens the energy consumption. Recent control theory studies overcome these problems by introducing aperiodic strategies, such as event trigger control. In spite of the potential savings, these strategies assume actuator continuous listening while ignoring the sensing energy costs. In this paper, we fill this gap, by enabling sensing and actuator listening duty-cycling and proposing two innovative MAC protocols for three decentralized event trigger control approaches. A laboratory experimental testbed, which emulates a smart water network, was modelled and extended to evaluate the impact of system parameters and the performance of each approach. Experimental results reveal the predominance of the decentralized event-triggered control against the classic periodic control either in terms of communication or actuation by promising significant system lifetime extension. △ Less

Submitted 14 November, 2016; originally announced November 2016.

Scheduling of Event-Triggered Networked Control Systems using Timed Game Automata

Authors: Dieky Adzkiya, Manuel Mazo Jr

Abstract: We discuss the scheduling of a set of networked control systems implemented over a shared communication network. Each control loop is described by a linear-time-invariant (LTI) system with an event-triggered implementation. We assume the network can be used by at most one control loop at any time instant and after each controller update, a pre-defined channel occupancy time elapses before the netw… ▽ More We discuss the scheduling of a set of networked control systems implemented over a shared communication network. Each control loop is described by a linear-time-invariant (LTI) system with an event-triggered implementation. We assume the network can be used by at most one control loop at any time instant and after each controller update, a pre-defined channel occupancy time elapses before the network is available. In our framework we offer the scheduler two options to avoid conflicts: using the event-triggering mechanism, where the scheduler can choose the triggering coefficient; or forcing controller updates at an earlier pre-defined time. Our objective is avoiding communication conflict while guaranteeing stability of all control loops. We formulate the original scheduling problem as a control synthesis problem over a network of timed game automata (NTGA) with a safety objective. The NTGA is obtained by taking the parallel composition of the timed game automata (TGA) associated with the network and with all control loops. The construction of TGA associated with control loops leverages recent results on the abstraction of timing models of event-triggered LTI systems. In our problem, the safety objective is to avoid that update requests from a control loop happen while the network is in use by another task. We showcase the results in some examples. △ Less

Submitted 12 October, 2016; originally announced October 2016.

Comments: 26 pages, 8 figures

Technical Report: Timing Abstraction of Perturbed LTI systems with $\mathcal{L}_2$-based Event-Triggering Mechanism

Authors: Arman Sharifi Kolarijani, Manuel Mazo Jr, Tamas Keviczky

Abstract: In networked control systems, the advent of event-triggering strategies in the sampling process has resulted in the usage reduction of network capacities, such as communication bandwidth. However, the aperiodic nature of sampling periods generated by event-triggering strategies has hindered the schedulability of such networks. In this study, we propose a framework to construct a timed safety autom… ▽ More In networked control systems, the advent of event-triggering strategies in the sampling process has resulted in the usage reduction of network capacities, such as communication bandwidth. However, the aperiodic nature of sampling periods generated by event-triggering strategies has hindered the schedulability of such networks. In this study, we propose a framework to construct a timed safety automaton that captures the sampling behavior of perturbed LTI systems with an $\mathcal{L}_2$-based triggering mechanisms proposed in the Literature. In this framework, the state-space is partitioned into a finite number of convex polyhedral cones, each cone representing a discrete mode in the abstracted automaton. Adopting techniques from stability analysis of retarded systems accompanied with a polytopic embedding of time, LMI conditions to characterize the sampling interval associated with each region are derived. Then, using reachability analysis, the transitions in the abstracted automaton are derived. △ Less

Submitted 12 September, 2016; originally announced September 2016.

Comments: 8 pages, 4 figures, technical report

A Formal Traffic Characterization of LTI Event-triggered Control Systems

Authors: Arman Sharifi Kolarijani, Manuel Mazo Jr

Abstract: Unnecessary communication and computation in the periodic execution of control tasks lead to over-provisioning in hardware design (or underexploitation in hardware utilization) in control applications, such as networked control systems. To address these issues, researchers have proposed a new class of strategies, named event-driven strategies. Despite of their beneficiary effects, matters like tas… ▽ More Unnecessary communication and computation in the periodic execution of control tasks lead to over-provisioning in hardware design (or underexploitation in hardware utilization) in control applications, such as networked control systems. To address these issues, researchers have proposed a new class of strategies, named event-driven strategies. Despite of their beneficiary effects, matters like task scheduling and appropriate dimensioning of communication components have become more complicated with respect to traditional periodic strategies. In this paper, we present a formal approach to derive an abstracted system that captures the sampling behavior of a family of event-triggered strategies for the case of LTI systems. This structure approximately simulates the sampling behavior of the aperiodic control system. Furthermore, the resulting quotient system is equivalent to a timed automaton. In the construction of the abstraction, the state space is confined to a finite number of convex regions, each of which represents a mode in the quotient system. An LMI-based technique is deployed to derive a sampling time interval associated to each region. Finally, reachability analysis is leveraged to find the transitions of the quotient system. △ Less

Submitted 15 June, 2015; v1 submitted 19 March, 2015; originally announced March 2015.

Comments: 10 pages, 7 figures

MSC Class: 93C30; 93C57; 93C10; 93C95

Symbolic Abstractions of Networked Control Systems

Authors: Majid Zamani, Manuel Mazo Jr, Mahmoud Khaled, Alessandro Abate

Abstract: The last decade has witnessed significant attention on networked control systems (NCS) due to their ubiquitous presence in industrial applications, and, in the particular case of wireless NCS, because of their architectural flexibility and low installation and maintenance costs. In wireless NCS the communication between sensors, controllers, and actuators is supported by a communication channel th… ▽ More The last decade has witnessed significant attention on networked control systems (NCS) due to their ubiquitous presence in industrial applications, and, in the particular case of wireless NCS, because of their architectural flexibility and low installation and maintenance costs. In wireless NCS the communication between sensors, controllers, and actuators is supported by a communication channel that is likely to introduce variable communication delays, packet losses, limited bandwidth, and other practical non-idealities leading to numerous technical challenges. Although stability properties of NCS have been investigated extensively in the literature, results for NCS under more complex and general objectives, and in particular results dealing with verification or controller synthesis for logical specifications, are much more limited. This work investigates how to address such complex objectives by constructively deriving symbolic models of NCS, while encompassing the mentioned network non-idealities. The obtained abstracted (symbolic) models can then be employed to synthesize hybrid controllers enforcing rich logical specifications over the concrete NCS models. Examples of such general specifications include properties expressed as formulae in linear temporal logic (LTL) or as automata on infinite strings. We thus provide a general synthesis framework that can be flexibly adapted to a number of NCS setups. We illustrate the effectiveness of the results over some case studies. △ Less

Submitted 21 November, 2016; v1 submitted 24 January, 2014; originally announced January 2014.

Comments: 22 pages, 8 figures, 1 table

MSC Class: 93C57; 93C85; 68M10 ACM Class: D.2.4; B.1.2; C.2.1

Asynchronous Decentralized Event-triggered Control

Authors: Manuel Mazo Jr, Ming Cao

Abstract: In this paper we propose an approach to the implementation of controllers with decentralized strategies triggering controller updates. We consider set-ups with a central node in charge of the computation of the control commands, and a set of not co-located sensors providing measurements to the controller node. The solution we propose does not require measurements from the sensors to be synchronize… ▽ More In this paper we propose an approach to the implementation of controllers with decentralized strategies triggering controller updates. We consider set-ups with a central node in charge of the computation of the control commands, and a set of not co-located sensors providing measurements to the controller node. The solution we propose does not require measurements from the sensors to be synchronized in time. The sensors in our proposal provide measurements in an aperiodic way triggered by local conditions. Furthermore, in the proposed implementation (most of) the communication between nodes requires only the exchange of one bit of information (per controller update), which could aid in reducing transmission delays and as a secondary effect result in fewer transmissions being triggered. △ Less

Submitted 17 May, 2013; v1 submitted 28 June, 2012; originally announced June 2012.

Comments: 17 pages, 2 figures

MSC Class: 93C10; 93C30; 93C57; 93C95

Symbolic Approximate Time-Optimal Control

Authors: Manuel Mazo Jr., Paulo Tabuada

Abstract: 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 a… ▽ More 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. △ Less

Submitted 3 February, 2011; v1 submitted 5 April, 2010; originally announced April 2010.

Comments: 17 pages, 2 figures, journal

MSC Class: 93C10; 93C62; 93C30; 93A30

Decentralized event-triggered control over wireless sensor/actuator networks

Authors: Manuel Mazo Jr., Paulo Tabuada

Abstract: 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 even… ▽ More 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. △ Less

Submitted 3 February, 2011; v1 submitted 3 April, 2010; originally announced April 2010.

Comments: 13 pages, 3 figures, journal submission

MSC Class: 93C10; 93C30; 93C57; 93C95