Search

We introduce a novel approach for the construction of symbolic abstractions - simpler, finite-state models - which mimic the behaviour of a system of interest, and are commonly utilized to verify complex logic specifications. Such abstractions require an exhaustive knowledge of the concrete model, which can be difficult to obtain in real-world applications. To overcome this, we propose to sample finite length trajectories of an unknown system and build an abstraction based on the concept of ℓ -completeness. To this end, we introduce the notion of probabilistic behavioural inclusion. We provide probably approximately correct (PAC) guarantees that such an abstraction, constructed from experimental symbolic trajectories of finite length, includes all behaviours of the concrete system, for both finite and infinite time horizon. Finally, our method is displayed with numerical examples., Green Open Access added to TU Delft Institutional Repository 'You share, we take care!' - Taverne project https://www.openaccess.nl/en/you-share-we-take-care Otherwise as indicated in the copyright section: the publisher is the copyright holder of this work and the author uses the Dutch legislation to make this work public., Team Manuel Mazo Jr

Event-triggered control (ETC) is claimed to provide significant 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, by looking at the map dictating the evolution of states sampled, 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., Green Open Access added to TU Delft Institutional Repository 'You share, we take care!' - Taverne project https://www.openaccess.nl/en/you-share-we-take-care Otherwise as indicated in the copyright section: the publisher is the copyright holder of this work and the author uses the Dutch legislation to make this work public., Team Tamas Keviczky, Team Manuel Mazo Jr

Green Open Access added to TU Delft Institutional Repository ‘You share, we take care!’ – Taverne project https://www.openaccess.nl/en/you-share-we-take-care Otherwise as indicated in the copyright section: the publisher is the copyright holder of this work and the author uses the Dutch legislation to make this work public., Team Manuel Mazo Jr

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 |Q| max problems, where |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 A is a polytope, synthesis over a discrete-action IMDP, where the actions are the vertices of 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., Team Manuel Mazo Jr, Team Luca Laurenti

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 behavior of linear time-invariant (LTI) ETC systems with quadratic triggering functions. Offering an infinite-horizon look to ETC systems' sampling patterns, 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: 1) the state space is partitioned into regions; 2) for each region, an interval is determined, containing all intersampling times of points in the region; and 3) 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 nondeterminism. Simulations showcase our developments., Green Open Access added to TU Delft Institutional Repository 'You share, we take care!' - Taverne project https://www.openaccess.nl/en/you-share-we-take-care Otherwise as indicated in the copyright section: the publisher is the copyright holder of this work and the author uses the Dutch legislation to make this work public., Team Manuel Mazo Jr

We present a biologically inspired design for swarm foraging based on ant’s pheromone deployment, where the swarm is assumed to have very restricted capabilities. The robots do not require global or relative position measurements and the swarm is fully decentralized and needs no infrastructure in place. Additionally, the system only requires one-hop communication over the robot network, we do not make any assumptions about the connectivity of the communication graph and the transmission of information and computation is scalable versus the number of agents. This is done by letting the agents in the swarm act as foragers or as guiding agents (beacons). We present experimental results computed for a swarm of Elisa-3 robots on a simulator, and show how the swarm self-organizes to solve a foraging problem over an unknown environment, converging to trajectories around the shortest path, and test the approach on a real swarm of Elisa-3 robots. At last, we discuss the limitations of such a system and propose how the foraging efficiency can be increased., Team Luca Laurenti, Team Manuel Mazo Jr, Learning & Autonomous Control

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., Green Open Access added to TU Delft Institutional Repository 'You share, we take care!' - Taverne project https://www.openaccess.nl/en/you-share-we-take-care Otherwise as indicated in the copyright section: the publisher is the copyright holder of this work and the author uses the Dutch legislation to make this work public., Team Tamas Keviczky, Team Manuel Mazo Jr

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., Team Manuel Mazo Jr.

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 article.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., Team Manuel Mazo Jr.

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., Team Manuel Mazo Jr., Team Tamas Keviczky

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., Team Tamas Keviczky, Team Manuel Mazo Jr.

We present an approach to reduce the communication of information needed on a Distributed Q-Learning system inspired by Event Triggered Control (ETC) techniques. We consider a baseline scenario of a Distributed Q-Learning problem on a Markov Decision Process (MDP). Following an event-based approach, N agents sharing a value function explore the MDP and compute a trajectory-dependent triggering signal which they use distributedly to decide when to communicate information to a central learner in charge of computing updates on the action-value function. These decision functions form an Event Based distributed Q learning system (EBd-Q), and we derive convergence guarantees resulting from the reduction of communication. We then apply the proposed algorithm to a cooperative path planning problem, and show how the agents are able to learn optimal trajectories communicating a fraction of the information. Additionally, we discuss what effects (desired and undesired) these event-based approaches have on the learning processes studied, and how they can be applied to more complex multi-agent systems., Green Open Access added to TU Delft Institutional Repository 'You share, we take care!' - Taverne project https://www.openaccess.nl/en/you-share-we-take-care Otherwise as indicated in the copyright section: the publisher is the copyright holder of this work and the author uses the Dutch legislation to make this work public., Team Manuel Mazo Jr

We present an approach to safely reduce the communication required between agents in a Multi-Agent Reinforcement Learning system by exploiting the inherent robustness of the underlying Markov Decision Process. We compute robustness certificate 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 with new measurements. This results in fully distributed decision functions, enabling agents to decide when it is necessary to communicate state variables. 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., Green Open Access added to TU Delft Institutional Repository 'You share, we take care!' - Taverne project https://www.openaccess.nl/en/you-share-we-take-care Otherwise as indicated in the copyright section: the publisher is the copyright holder of this work and the author uses the Dutch legislation to make this work public., Team Manuel Mazo Jr

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 optimisation to multiclass SVM algorithms in order to construct a PAC map between the concrete state-space and the inter-sample times. We then build a traffic model applying an l-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., Green Open Access added to TU Delft Institutional Repository 'You share, we take care!' - Taverne project https://www.openaccess.nl/en/you-share-we-take-care Otherwise as indicated in the copyright section: the publisher is the copyright holder of this work and the author uses the Dutch legislation to make this work public., Team Manuel Mazo Jr

Collaborative multiagent 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 multiagent system solving collaborative foraging. We show how mean field techniques can be used to re-formulate such a stochastic multiagent problem into a deterministic autonomous system. This de-couples agent dynamics, enabling the computation of limit behaviors 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 multiagent system, which have impact on more general collaborative stochastic problems., Green Open Access added to TU Delft Institutional Repository 'You share, we take care!' - Taverne project https://www.openaccess.nl/en/you-share-we-take-care Otherwise as indicated in the copyright section: the publisher is the copyright holder of this work and the author uses the Dutch legislation to make this work public., Team Manuel Mazo Jr

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., Team Tamas Keviczky, Team Manuel Mazo Jr

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., Team Manuel Mazo Jr, Team Tamas Keviczky

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., Team Manuel Mazo Jr

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 article.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., Team Manuel Mazo Jr

Metric Temporal Logic (MTL) and Timed Propositional Temporal Logic (TPTL) are prominent real-time extensions of Linear Temporal Logic (LTL). In general, the satisfiability checking problem for these extensions is undecidable when both the future U and the past S modalities are used. In a classical result, the satisfiability checking for MITL[U,S], a non-punctual fragment of MTL[U,S], is shown to be decidable with EXPSPACE complete complexity. Given that this notion of non-punctuality does not recover decidability in the case of TPTL[U,S], we propose a generalization of non-punctuality called non-adjacency for TPTL[U,S], and focus on its 1-variable fragment, 1-TPTL[U,S]. While non-adjacent 1-TPTL[U,S] appears to be a very small fragment, it is strictly more expressive than MITL. As our main result, we show that the satisfiability checking problem for non-adjacent 1-TPTL[U,S] is decidable with EXPSPACE complete complexity., Green Open Access added to TU Delft Institutional Repository 'You share, we take care!' - Taverne project https://www.openaccess.nl/en/you-share-we-take-care Otherwise as indicated in the copyright section: the publisher is the copyright holder of this work and the author uses the Dutch legislation to make this work public., Team Manuel Mazo Jr.

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., Green Open Access added to TU Delft Institutional Repository 'You share, we take care!' - Taverne project https://www.openaccess.nl/en/you-share-we-take-care Otherwise as indicated in the copyright section: the publisher is the copyright holder of this work and the author uses the Dutch legislation to make this work public., Team Tamas Keviczky

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., Team Manuel Mazo Jr.

In this article, 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 interevent 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 interevent times, we use approximations of isochronous manifolds, a notion first introduced in Anta and Tabuada (2012). This article addresses some theoretical issues of Anta and Tabuada (2012) 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 is demonstrated through simulation examples., Green Open Access added to TU Delft Institutional Repository 'You share, we take care!' - Taverne project https://www.openaccess.nl/en/you-share-we-take-care Otherwise as indicated in the copyright section: the publisher is the copyright holder of this work and the author uses the Dutch legislation to make this work public., Team Tamas Keviczky

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 equipping 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., Green Open Access added to TU Delft Institutional Repository 'You share, we take care!' - Taverne project https://www.openaccess.nl/en/you-share-we-take-care Otherwise as indicated in the copyright section: the publisher is the copyright holder of this work and the author uses the Dutch legislation to make this work public., Team Manuel Mazo Jr., Team Luca Laurenti

Self-triggered control (STC) is a sample-and-hold control method aimed at reducing communications in networked-control systems; however, existing STC mechanisms often maximize how late the next sample is, thus not optimizing sampling performance 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, while also allowing earlier samples. These early triggers constitute controllable actions of the abstraction, for which an AIST-maximizing strategy can be obtained by solving a mean-payoff game. We provide optimality bounds, and how to further improve them through abstraction refinement techniques., Green Open Access added to TU Delft Institutional Repository 'You share, we take care!' - Taverne project https://www.openaccess.nl/en/you-share-we-take-care Otherwise as indicated in the copyright section: the publisher is the copyright holder of this work and the author uses the Dutch legislation to make this work public., Team Manuel Mazo Jr.

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 equipping 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., Green Open Access added to TU Delft Institutional Repository 'You share, we take care!' - Taverne project https://www.openaccess.nl/en/you-share-we-take-care Otherwise as indicated in the copyright section: the publisher is the copyright holder of this work and the author uses the Dutch legislation to make this work public., Team Manuel Mazo Jr, Team Luca Laurenti

Self-triggered control (STC) is a sample-and-hold control method aimed at reducing communications in networked-control systems; however, existing STC mechanisms often maximize how late the next sample is, thus not optimizing sampling performance 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, while also allowing earlier samples. These early triggers constitute controllable actions of the abstraction, for which an AIST-maximizing strategy can be obtained by solving a mean-payoff game. We provide optimality bounds, and how to further improve them through abstraction refinement techniques., Green Open Access added to TU Delft Institutional Repository 'You share, we take care!' - Taverne project https://www.openaccess.nl/en/you-share-we-take-care Otherwise as indicated in the copyright section: the publisher is the copyright holder of this work and the author uses the Dutch legislation to make this work public., Team Manuel Mazo Jr

Metric Temporal Logic (MTL) and Timed Propositional Temporal Logic (TPTL) are prominent real-time extensions of Linear Temporal Logic (LTL). In general, the satisfiability checking problem for these extensions is undecidable when both the future U and the past S modalities are used. In a classical result, the satisfiability checking for MITL[U,S], a non-punctual fragment of MTL[U,S], is shown to be decidable with EXPSPACE complete complexity. Given that this notion of non-punctuality does not recover decidability in the case of TPTL[U,S], we propose a generalization of non-punctuality called non-adjacency for TPTL[U,S], and focus on its 1-variable fragment, 1-TPTL[U,S]. While non-adjacent 1-TPTL[U,S] appears to be a very small fragment, it is strictly more expressive than MITL. As our main result, we show that the satisfiability checking problem for non-adjacent 1-TPTL[U,S] is decidable with EXPSPACE complete complexity., Green Open Access added to TU Delft Institutional Repository 'You share, we take care!' - Taverne project https://www.openaccess.nl/en/you-share-we-take-care Otherwise as indicated in the copyright section: the publisher is the copyright holder of this work and the author uses the Dutch legislation to make this work public., Team Manuel Mazo Jr

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., Green Open Access added to TU Delft Institutional Repository 'You share, we take care!' - Taverne project https://www.openaccess.nl/en/you-share-we-take-care Otherwise as indicated in the copyright section: the publisher is the copyright holder of this work and the author uses the Dutch legislation to make this work public., Team Tamas Keviczky

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., Team Manuel Mazo Jr

In this article, 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 interevent 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 interevent times, we use approximations of isochronous manifolds, a notion first introduced in Anta and Tabuada (2012). This article addresses some theoretical issues of Anta and Tabuada (2012) 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 is demonstrated through simulation examples., Green Open Access added to TU Delft Institutional Repository 'You share, we take care!' - Taverne project https://www.openaccess.nl/en/you-share-we-take-care Otherwise as indicated in the copyright section: the publisher is the copyright holder of this work and the author uses the Dutch legislation to make this work public., Team Tamas Keviczky

In previous work, linear time-invariant eventtriggered 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, Green Open Access added to TU Delft Institutional Repository 'You share, we take care!' - Taverne project https://www.openaccess.nl/en/you-share-we-take-care Otherwise as indicated in the copyright section: the publisher is the copyright holder of this work and the author uses the Dutch legislation to make this work public., Team Tamas Keviczky

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., Green Open Access added to TU Delft Institutional Repository ‘You share, we take care!’ – Taverne project https://www.openaccess.nl/en/you-share-we-take-care Otherwise as indicated in the copyright section: the publisher is the copyright holder of this work and the author uses the Dutch legislation to make this work public., Team Tamas Keviczky

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., Green Open Access added to TU Delft Institutional Repository 'You share, we take care!' - Taverne project https://www.openaccess.nl/en/you-share-we-take-care Otherwise as indicated in the copyright section: the publisher is the copyright holder of this work and the author uses the Dutch legislation to make this work public., Team Tamas Keviczky

Ant Colony algorithms are a set of biologically inspired algorithms used commonly to solve distributed optimization problems. Convergence has been proven in the context of optimization processes, but these proofs are not applicable in the framework of robotic control. In order to use Ant Colony algorithms to control robotic swarms, we present in this work more general results that prove asymptotic convergence of a multi-agent Ant Colony swarm moving in a weighted graph., Green Open Access added to TU Delft Institutional Repository ‘You share, we take care!’ – Taverne project https://www.openaccess.nl/en/you-share-we-take-care Otherwise as indicated in the copyright section: the publisher is the copyright holder of this work and the author uses the Dutch legislation to make this work public., Team Tamas Keviczky

A constructive tool of nonlinear control system design, the method of control Lyapunov functions (CLFs), 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 a 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 dwell times between consecutive events. Furthermore, we prove the existence of self-triggered and periodic event-triggered controllers, providing stabilization with a known convergence rate., Green Open Access added to TU Delft Institutional Repository ‘You share, we take care!’ – Taverne project https://www.openaccess.nl/en/you-share-we-take-care Otherwise as indicated in the copyright section: the publisher is the copyright holder of this work and the author uses the Dutch legislation to make this work public., Team Tamas Keviczky

In previous work, linear time-invariant eventtriggered 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, Green Open Access added to TU Delft Institutional Repository 'You share, we take care!' - Taverne project https://www.openaccess.nl/en/you-share-we-take-care Otherwise as indicated in the copyright section: the publisher is the copyright holder of this work and the author uses the Dutch legislation to make this work public., Team Tamas Keviczky

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., Green Open Access added to TU Delft Institutional Repository ‘You share, we take care!’ – Taverne project https://www.openaccess.nl/en/you-share-we-take-care Otherwise as indicated in the copyright section: the publisher is the copyright holder of this work and the author uses the Dutch legislation to make this work public., Team Tamas Keviczky

Ant Colony algorithms are a set of biologically inspired algorithms used commonly to solve distributed optimization problems. Convergence has been proven in the context of optimization processes, but these proofs are not applicable in the framework of robotic control. In order to use Ant Colony algorithms to control robotic swarms, we present in this work more general results that prove asymptotic convergence of a multi-agent Ant Colony swarm moving in a weighted graph., Green Open Access added to TU Delft Institutional Repository ‘You share, we take care!’ – Taverne project https://www.openaccess.nl/en/you-share-we-take-care Otherwise as indicated in the copyright section: the publisher is the copyright holder of this work and the author uses the Dutch legislation to make this work public., Team Tamas Keviczky

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., Green Open Access added to TU Delft Institutional Repository 'You share, we take care!' - Taverne project https://www.openaccess.nl/en/you-share-we-take-care Otherwise as indicated in the copyright section: the publisher is the copyright holder of this work and the author uses the Dutch legislation to make this work public., Team Tamas Keviczky

A constructive tool of nonlinear control system design, the method of control Lyapunov functions (CLFs), 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 a 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 dwell times between consecutive events. Furthermore, we prove the existence of self-triggered and periodic event-triggered controllers, providing stabilization with a known convergence rate., Green Open Access added to TU Delft Institutional Repository ‘You share, we take care!’ – Taverne project https://www.openaccess.nl/en/you-share-we-take-care Otherwise as indicated in the copyright section: the publisher is the copyright holder of this work and the author uses the Dutch legislation to make this work public., Team Tamas Keviczky

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 finite-state similar model of the traffic generated by periodic ETC (PETC), which by construction mitigates the combinatorial explosion that is typical of symbolic models. The model is augmented with early triggering actions that can be used by a scheduler. The complete networked control system is then modeled as a network of timed game automata, for which existing tools can generate strategies that avoids communication conflicts, while keeping early triggers to a minimum. Our proposed model is relatively fast to build and is the first to constitute an exact simulation. Finally, we demonstrate modeling and scheduling for a numerical example., Team Tamas Keviczky

In networked control systems (NCSs), extensive data exchange between plants and controllers leads to an unnecessary usage of communication and computational resources. Aperiodic sample-and-hold methods such as event-triggered control (ETC) can reduce the number of transmissions, allowing more applications to operate within the same network. However, most existing event-triggering mechanisms enforce a Lyapunov function of the continuous-time closed-loop system to be (almost) always decreasing. We propose a relaxed triggering condition for periodic event-triggered control (PETC) based on bounding the Lyapunov function with an exponentially decaying reference function, which reduces the communications while guaranteeing the same decay rate as competing strategies. We provide sufficient global exponential and input-to-state stability conditions for linear time-invariant (LTI) systems under our event-based state feedback, giving explicit performance guarantees in the presence of additive disturbances. Finally, some simulation results illustrate the performance of the proposed control strategy., Green Open Access added to TU Delft Institutional Repository ‘You share, we take care!’ – Taverne project https://www.openaccess.nl/en/you-share-we-take-care Otherwise as indicated in the copyright section: the publisher is the copyright holder of this work and the author uses the Dutch legislation to make this work public., Team Tamas Keviczky

Control systems designed via learning methods, aiming at quasi-optimal solutions, typically lack stability and performance guarantees. We propose a method to construct a near-optimal control law by means of model-based reinforcement learning and subsequently verifying the reachability and safety of the closed-loop control system through an automatically synthesized Lyapunov barrier function. We demonstrate the method on the control of an anti-lock braking system. Here the optimal control synthesis is used to minimize the braking distance, whereas we use verification to show guaranteed convergence to standstill and formally bound the braking distance., Learning & Autonomous Control, Intelligent Vehicles, Team Tamas Keviczky

Periodic event-triggered control (PETC) [13] is a version of event-triggered control that only requires the measurement of the plant output periodically instead of continuously. In this note, 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 linear matrix inequalities. The state transitions among different regions result from computing the reachable state set starting from each region within the computed event time intervals., Green Open Access added to TU Delft Institutional Repository 'You share, we take care!’ – Taverne project https://www.openaccess.nl/en/you-share-we-take-care Otherwise as indicated in the copyright section: the publisher is the copyright holder of this work and the author uses the Dutch legislation to make this work public., Team Tamas Keviczky

In networked control systems (NCSs), extensive data exchange between plants and controllers leads to an unnecessary usage of communication and computational resources. Aperiodic sample-and-hold methods such as event-triggered control (ETC) can reduce the number of transmissions, allowing more applications to operate within the same network. However, most existing event-triggering mechanisms enforce a Lyapunov function of the continuous-time closed-loop system to be (almost) always decreasing. We propose a relaxed triggering condition for periodic event-triggered control (PETC) based on bounding the Lyapunov function with an exponentially decaying reference function, which reduces the communications while guaranteeing the same decay rate as competing strategies. We provide sufficient global exponential and input-to-state stability conditions for linear time-invariant (LTI) systems under our event-based state feedback, giving explicit performance guarantees in the presence of additive disturbances. Finally, some simulation results illustrate the performance of the proposed control strategy., Green Open Access added to TU Delft Institutional Repository ‘You share, we take care!’ – Taverne project https://www.openaccess.nl/en/you-share-we-take-care Otherwise as indicated in the copyright section: the publisher is the copyright holder of this work and the author uses the Dutch legislation to make this work public., Team Tamas Keviczky

Control systems designed via learning methods, aiming at quasi-optimal solutions, typically lack stability and performance guarantees. We propose a method to construct a near-optimal control law by means of model-based reinforcement learning and subsequently verifying the reachability and safety of the closed-loop control system through an automatically synthesized Lyapunov barrier function. We demonstrate the method on the control of an anti-lock braking system. Here the optimal control synthesis is used to minimize the braking distance, whereas we use verification to show guaranteed convergence to standstill and formally bound the braking distance., Learning & Autonomous Control, Intelligent Vehicles, Team Tamas Keviczky

Periodic event-triggered control (PETC) [13] is a version of event-triggered control that only requires the measurement of the plant output periodically instead of continuously. In this note, 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 linear matrix inequalities. The state transitions among different regions result from computing the reachable state set starting from each region within the computed event time intervals., Green Open Access added to TU Delft Institutional Repository 'You share, we take care!’ – Taverne project https://www.openaccess.nl/en/you-share-we-take-care Otherwise as indicated in the copyright section: the publisher is the copyright holder of this work and the author uses the Dutch legislation to make this work public., Team Tamas Keviczky

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. backstepping 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., Green Open Access added to TU Delft Institutional Repository ‘You share, we take care!’ – Taverne project https://www.openaccess.nl/en/you-share-we-take-care Otherwise as indicated in the copyright section: the publisher is the copyright holder of this work and the author uses the Dutch legislation to make this work public., Team Tamas Keviczky

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 embedded platforms. Control-synthesis tools such as PESSOA, SCOTS, and CoSyMA tackle the problem by storing controllers as binary decision diagrams (BDDs). However, due to redundantly keeping 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., Team Tamas Keviczky