Publications
If you can’t find the preprint you’re looking for below, please try on the TU Delft repository, ORCiD, or GoogleScholar via the linked logos above.
2023
1.
Delimpaltadakis, Giannis; Lahijanian, Morteza; Jr., Manuel Mazo; Laurenti, Luca
Interval Markov Decision Processes with Continuous Action-Spaces Proceedings Article
In: Proceedings of the 26th ACM International Conference on Hybrid Systems: Computation and Control, pp. 1–10, 2023.
BibTeX | Tags: Formal methods, SENTIENT, Stochastic
@inproceedings{delimpaltadakis2023interval,
title = {Interval Markov Decision Processes with Continuous Action-Spaces},
author = { Giannis Delimpaltadakis and Morteza Lahijanian and Manuel Mazo Jr. and Luca Laurenti},
year = {2023},
date = {2023-01-01},
urldate = {2023-01-01},
booktitle = {Proceedings of the 26th ACM International Conference on Hybrid Systems: Computation and Control},
pages = {1–10},
keywords = {Formal methods, SENTIENT, Stochastic},
pubstate = {published},
tppubtype = {inproceedings}
}
2.
Krishna, Shankara Narayanan; Madnani, Khushraj; Jr., Manuel Mazo; Pandya, Paritosh
From Non-punctuality to Non-adjacency: A Quest for Decidability of Timed Temporal Logics with Quantifiers Journal Article
In: Formal Aspects of Computing, vol. 35, no. 2, pp. 1–50, 2023.
BibTeX | Tags: Formal methods, SENTIENT
@article{krishna2023non,
title = {From Non-punctuality to Non-adjacency: A Quest for Decidability of Timed Temporal Logics with Quantifiers},
author = { Shankara Narayanan Krishna and Khushraj Madnani and Manuel Mazo Jr. and Paritosh Pandya},
year = {2023},
date = {2023-01-01},
urldate = {2023-01-01},
journal = {Formal Aspects of Computing},
volume = {35},
number = {2},
pages = {1–50},
publisher = {ACM New York, NY},
keywords = {Formal methods, SENTIENT},
pubstate = {published},
tppubtype = {article}
}
3.
Gracia, Ibon; Boskos, Dimitris; Laurenti, Luca; Jr., Manuel Mazo
Distributionally robust strategy synthesis for switched stochastic systems Best Paper Proceedings Article
In: Proceedings of the 26th ACM International Conference on Hybrid Systems: Computation and Control, pp. 1–10, 2023.
BibTeX | Tags: Formal methods, Stochastic
@inproceedings{gracia2023distributionally,
title = {Distributionally robust strategy synthesis for switched stochastic systems},
author = { Ibon Gracia and Dimitris Boskos and Luca Laurenti and Manuel Mazo Jr.},
year = {2023},
date = {2023-01-01},
urldate = {2023-01-01},
booktitle = {Proceedings of the 26th ACM International Conference on Hybrid Systems: Computation and Control},
pages = {1–10},
keywords = {Formal methods, Stochastic},
pubstate = {published},
tppubtype = {inproceedings}
}
4.
Coppola, Rudi; Peruffo, Andrea; Jr., Manuel Mazo
Data-driven abstractions for verification of deterministic systems Journal Article
In: IEEE Control Systems Letters (To appear), 2023.
BibTeX | Tags: Formal methods, Learning
@article{coppola2023data,
title = {Data-driven abstractions for verification of deterministic systems},
author = { Rudi Coppola and Andrea Peruffo and Manuel Mazo Jr.},
year = {2023},
date = {2023-01-01},
urldate = {2023-01-01},
journal = {IEEE Control Systems Letters (To appear)},
keywords = {Formal methods, Learning},
pubstate = {published},
tppubtype = {article}
}
2022
5.
Verdier, Cees Ferdinand; Kochdumper, Niklas; Althoff, Matthias; Jr., Manuel Mazo
Formal synthesis of closed-form sampled-data controllers for nonlinear continuous-time systems under STL specifications Journal Article
In: Automatica, vol. 139, 2022, ISSN: 0005-1098.
Abstract | BibTeX | Tags: CADUSY, Formal methods | Links:
@article{VerdierAlthof22,
title = {Formal synthesis of closed-form sampled-data controllers for nonlinear continuous-time systems under STL specifications},
author = {Cees Ferdinand Verdier and Niklas Kochdumper and Matthias Althoff and Manuel {Mazo Jr.}},
url = {https://www.sciencedirect.com/science/article/pii/S0005109822000292
https://arxiv.org/abs/2006.04260},
doi = {10.1016/j.automatica.2022.110184},
issn = {0005-1098},
year = {2022},
date = {2022-01-01},
urldate = {2022-01-01},
journal = {Automatica},
volume = {139},
publisher = {Elsevier},
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 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.},
keywords = {CADUSY, Formal methods},
pubstate = {published},
tppubtype = {article}
}
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.
6.
Peruffo, Andrea; Jr., Manuel Mazo
Data-driven Abstractions with Probabilistic Guarantees for Linear PETC Systems Journal Article
In: IEEE Control Systems Letters, vol. 7, pp. 115–120, 2022.
BibTeX | Tags: Formal methods, Learning, NCS, SENTIENT
@article{peruffo2022data,
title = {Data-driven Abstractions with Probabilistic Guarantees for Linear PETC Systems},
author = { Andrea Peruffo and Manuel Mazo Jr.},
year = {2022},
date = {2022-01-01},
urldate = {2022-01-01},
journal = {IEEE Control Systems Letters},
volume = {7},
pages = {115–120},
publisher = {IEEE},
keywords = {Formal methods, Learning, NCS, SENTIENT},
pubstate = {published},
tppubtype = {article}
}
7.
de Albuquerque Gleizer, Gabriel; Jr., Manuel Mazo
Chaos and order in event-triggered control Journal Article
In: IEEE Transactions on Automatic Control, pp. 1-16, 2022.
BibTeX | Tags: Formal methods, NCS, SENTIENT | Links:
@article{gleizer2022chaos,
title = {Chaos and order in event-triggered control},
author = { Gabriel de Albuquerque Gleizer and Manuel Mazo Jr.},
doi = {10.1109/TAC.2023.3242334},
year = {2022},
date = {2022-01-01},
urldate = {2022-01-01},
journal = {IEEE Transactions on Automatic Control},
pages = {1-16},
keywords = {Formal methods, NCS, SENTIENT},
pubstate = {published},
tppubtype = {article}
}
8.
Delimpaltadakis, Giannis; Jr., Manuel Mazo
Abstracting the Traffic of Nonlinear Event-Triggered Control Systems Journal Article
In: IEEE Transactions on Automatic Control, 2022.
BibTeX | Tags: Formal methods, NCS, SENTIENT
@article{delimpaltadakis2022abstracting,
title = {Abstracting the Traffic of Nonlinear Event-Triggered Control Systems},
author = { Giannis Delimpaltadakis and Manuel Mazo Jr.},
year = {2022},
date = {2022-01-01},
urldate = {2022-01-01},
journal = {IEEE Transactions on Automatic Control},
publisher = {IEEE},
keywords = {Formal methods, NCS, SENTIENT},
pubstate = {published},
tppubtype = {article}
}
2021
9.
de A. Gleizer, Gabriel; Jr., Manuel Mazo
Computing the sampling performance of event-triggered control Proceedings Article
In: Proceedings of the 24th International Conference on Hybrid Systems (HSCC 2021), Association for Computing Machinery (ACM), United States, 2021, (24th ACM International Conference on Hybrid Systems Computation and Control, HSCC 2021, held as part of the 14th Cyber Physical Systems and Internet-of-Things Week, CPS-IoT Week 2021 ; ).
Abstract | BibTeX | Tags: Formal methods, NCS, SENTIENT | Links:
@inproceedings{GleizerHSCC21,
title = {Computing the sampling performance of event-triggered control},
author = {Gabriel {de A. Gleizer} and Manuel {Mazo Jr.}},
url = {https://research.tudelft.nl/files/90951924/3447928.3456635.pdf
https://arxiv.org/abs/2103.00919
https://dl.acm.org/doi/10.1145/3447928.3456635},
doi = {10.1145/3447928.3456635},
year = {2021},
date = {2021-05-20},
urldate = {2021-05-20},
booktitle = {Proceedings of the 24th International Conference on Hybrid Systems (HSCC 2021)},
publisher = {Association for Computing Machinery (ACM)},
address = {United States},
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-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.},
note = {24th ACM International Conference on Hybrid Systems Computation and Control, HSCC 2021, held as part of the 14th Cyber Physical Systems and Internet-of-Things Week, CPS-IoT Week 2021 ; },
keywords = {Formal methods, NCS, SENTIENT},
pubstate = {published},
tppubtype = {inproceedings}
}
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.
10.
Delimpaltadakis, Giannis; Laurenti, Luca; Jr., Manuel Mazo
Abstracting the Sampling Behaviour of Stochastic Linear Periodic Event-Triggered Control Systems Proceedings Article
In: Proceedings of the 60th IEEE Conference on Decision and Control (CDC 2021), pp. 1287–1294, IEEE, United States, 2021, ISBN: 978-1-6654-3659-5, (60th IEEE Conference on Decision and Control (CDC 2021) ; Conference date: 14-12-2021 Through 17-12-2021).
Abstract | BibTeX | Tags: Formal methods, NCS, SENTIENT, Stochastic | Links:
@inproceedings{DelimpaltadakisCDC21,
title = {Abstracting the Sampling Behaviour of Stochastic Linear Periodic Event-Triggered Control Systems},
author = {Giannis Delimpaltadakis and Luca Laurenti and Manuel {Mazo Jr.}},
url = {https://ieeexplore.ieee.org/document/9683751
https://arxiv.org/abs/2103.13839},
doi = {10.1109/CDC45484.2021.9683751},
isbn = {978-1-6654-3659-5},
year = {2021},
date = {2021-01-01},
urldate = {2021-01-01},
booktitle = {Proceedings of the 60th IEEE Conference on Decision and Control (CDC 2021)},
pages = {1287--1294},
publisher = {IEEE},
address = {United States},
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, 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.},
note = {60th IEEE Conference on Decision and Control (CDC 2021) ; Conference date: 14-12-2021 Through 17-12-2021},
keywords = {Formal methods, NCS, SENTIENT, Stochastic},
pubstate = {published},
tppubtype = {inproceedings}
}
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.
11.
Krishna, Shankara Narayanan; Madnani, Khushraj; Jr., Manuel Mazo; Pandya, Paritosh K.
Generalizing Non-punctuality for Timed Temporal Logic with Freeze Quantifiers Proceedings Article
In: Huisman, Marieke; areanu, Corina Pu; Zhan, Naijun (Ed.): Formal Methods, pp. 182–199, Springer, 2021, ISBN: 978-3-030-90869-0, (24th International Symposium on Formal Methods, FM 2021 ; Conference date: 20-11-2021 Through 26-11-2021).
Abstract | BibTeX | Tags: Formal methods, SENTIENT | Links:
@inproceedings{MadnaniLNCS21,
title = {Generalizing Non-punctuality for Timed Temporal Logic with Freeze Quantifiers},
author = {Shankara Narayanan Krishna and Khushraj Madnani and Manuel {Mazo Jr.} and Paritosh K. Pandya},
editor = {Marieke Huisman and Corina Pu areanu and Naijun Zhan},
url = {https://link.springer.com/chapter/10.1007/978-3-030-90870-6_10
https://arxiv.org/abs/2105.09534},
doi = {10.1007/978-3-030-90870-6_10},
isbn = {978-3-030-90869-0},
year = {2021},
date = {2021-01-01},
urldate = {2021-01-01},
booktitle = {Formal Methods},
pages = {182--199},
publisher = {Springer},
series = {Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)},
abstract = {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.},
note = {24th International Symposium on Formal Methods, FM 2021 ; Conference date: 20-11-2021 Through 26-11-2021},
keywords = {Formal methods, SENTIENT},
pubstate = {published},
tppubtype = {inproceedings}
}
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.
12.
de A. Gleizer, Gabriel; Madnani, K. N.; Jr., Manuel Mazo
Self-Triggered Control for Near-Maximal Average Inter-Sample Time Proceedings Article
In: Proceedings of the 60th IEEE Conference on Decision and Control (CDC 2021), pp. 1308–1313, IEEE, Ünited States, 2021, ISBN: 978-1-6654-3659-5, (60th IEEE Conference on Decision and Control (CDC 2021) ; Conference date: 14-12-2021 Through 17-12-2021).
Abstract | BibTeX | Tags: Formal methods, NCS, SENTIENT | Links:
@inproceedings{GleizerCDC21,
title = {Self-Triggered Control for Near-Maximal Average Inter-Sample Time},
author = {Gabriel de A. Gleizer and K. N. Madnani and Manuel {Mazo Jr.}},
url = {https://arxiv.org/abs/2105.03110
https://ieeexplore.ieee.org/document/9682986},
doi = {10.1109/CDC45484.2021.9682986},
isbn = {978-1-6654-3659-5},
year = {2021},
date = {2021-01-01},
urldate = {2021-01-01},
booktitle = {Proceedings of the 60th IEEE Conference on Decision and Control (CDC 2021)},
pages = {1308--1313},
publisher = {IEEE},
address = {Ünited States},
abstract = {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.},
note = {60th IEEE Conference on Decision and Control (CDC 2021) ; Conference date: 14-12-2021 Through 17-12-2021},
keywords = {Formal methods, NCS, SENTIENT},
pubstate = {published},
tppubtype = {inproceedings}
}
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.
2020
13.
Delimpaltadakis, Giannis; Jr., Manuel Mazo
Traffic Abstractions of Nonlinear Homogeneous Event-Triggered Control Systems Proceedings Article
In: Proceedings of the 59th IEEE Conference on Decision and Control, pp. 4991–4998, IEEE, 2020.
Abstract | BibTeX | Tags: Formal methods, NCS, SENTIENT | Links:
@inproceedings{DelimpCDC20,
title = {Traffic Abstractions of Nonlinear Homogeneous Event-Triggered Control Systems},
author = {Giannis Delimpaltadakis and Manuel {Mazo Jr.}},
url = {https://mmazojr.3me.tudelft.nl/wp-content/uploads/2020/09/final2.pdf
https://research.tudelft.nl/files/87240321/09303968.pdf
https://ieeexplore.ieee.org/document/9303968
https://arxiv.org/abs/2003.09361
},
doi = {10.1109/CDC42340.2020.9303968},
year = {2020},
date = {2020-12-15},
urldate = {2020-12-15},
booktitle = {Proceedings of the 59th IEEE Conference on Decision and Control},
pages = {4991--4998},
publisher = {IEEE},
abstract = {In previous work, linear time-invariant eventtriggered control (ETC) systems were abstracted to finite-state systems that capture the original systems{textquoteright} 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},
keywords = {Formal methods, NCS, SENTIENT},
pubstate = {published},
tppubtype = {inproceedings}
}
In previous work, linear time-invariant eventtriggered control (ETC) systems were abstracted to finite-state systems that capture the original systems{textquoteright} 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
14.
de A. Gleizer, Gabriel; Jr., Manuel Mazo
Self-triggered output-feedback control of LTI systems subject to disturbances and noise. Journal Article
In: Automatica, vol. 120, 2020, ISSN: 0005-1098.
Abstract | BibTeX | Tags: Formal methods, NCS, SENTIENT | Links:
@article{Aut2020Gleizer,
title = {Self-triggered output-feedback control of LTI systems subject to disturbances and noise.},
author = {Gabriel de A. Gleizer and Manuel {Mazo Jr.}},
url = {https://mmazojr.3me.tudelft.nl/wp-content/uploads/2020/09/19-0776_04_MS.pdf
https://research.tudelft.nl/files/81771634/1_s2.0_S0005109820303277_main.pdf
https://www.sciencedirect.com/science/article/pii/S0005109820303277?via%3Dihub
https://arxiv.org/abs/2007.02703},
doi = {10.1016/j.automatica.2020.109129},
issn = {0005-1098},
year = {2020},
date = {2020-10-01},
urldate = {2020-10-01},
journal = {Automatica},
volume = {120},
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 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.},
keywords = {Formal methods, NCS, SENTIENT},
pubstate = {published},
tppubtype = {article}
}
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.
15.
Delimpaltadakis, Giannis; Jr., Manuel Mazo
Region-Based Self-Triggered Control for Perturbed and Uncertain Nonlinear Systems. Online
2020.
BibTeX | Tags: Formal methods, NCS, SENTIENT | Links:
@online{RegionBasedSTC20,
title = {Region-Based Self-Triggered Control for Perturbed and Uncertain Nonlinear Systems.},
author = {Giannis Delimpaltadakis and Manuel {Mazo Jr.}},
url = {https://arxiv.org/abs/2005.00473},
year = {2020},
date = {2020-09-01},
keywords = {Formal methods, NCS, SENTIENT},
pubstate = {published},
tppubtype = {online}
}
16.
de A. Gleizer, Gabriel; Jr., Manuel Mazo
Scalable Traffic Models for Scheduling of Linear Periodic Event-Triggered Controllers. Proceedings Article
In: 21st IFAC World Congress : Automatic Control – Meeting Societal Challenges - Berlin, Germany, pp. 2726-2732, IFAC 2020.
Abstract | BibTeX | Tags: Formal methods, NCS, SENTIENT | Links:
@inproceedings{IFAC20Gleizer,
title = {Scalable Traffic Models for Scheduling of Linear Periodic Event-Triggered Controllers.},
author = {Gabriel de A. Gleizer and Manuel {Mazo Jr.}},
url = {https://research.tudelft.nl/files/93709907/1_s2.0_S2405896320332729_main.pdf
https://arxiv.org/abs/2003.07642},
doi = {10.1016/j.ifacol.2020.12.2525},
year = {2020},
date = {2020-07-13},
urldate = {2020-07-13},
booktitle = {21st IFAC World Congress : Automatic Control – Meeting Societal Challenges - Berlin, Germany},
volume = {53},
number = {2},
pages = {2726-2732},
organization = {IFAC},
series = {IFAC-PapersOnLine},
abstract = {Scalable Traffic Models for Scheduling of Linear Periodic Event-Triggered Controllers",
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.},
keywords = {Formal methods, NCS, SENTIENT},
pubstate = {published},
tppubtype = {inproceedings}
}
Scalable Traffic Models for Scheduling of Linear Periodic Event-Triggered Controllers",
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.
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.
17.
de A. Gleizer, Gabriel; Jr., Manuel Mazo
Towards Traffic Bisimulation of Linear Periodic Event-Triggered Controllers Journal Article
In: IEEE Control Systems Letters, vol. 5, no. 1, pp. 25–30, 2020, ISBN: 2475-1456, (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.).
Abstract | BibTeX | Tags: Formal methods, NCS, SENTIENT | Links:
@article{LCSS20Gleizer,
title = {Towards Traffic Bisimulation of Linear Periodic Event-Triggered Controllers},
author = {Gabriel de A. Gleizer and Manuel {Mazo Jr.}},
url = {https://mmazojr.3me.tudelft.nl/wp-content/uploads/2020/09/20-0377_03_MS.pdf
https://arxiv.org/abs/2005.14504
https://ieeexplore.ieee.org/document/9105095},
doi = {10.1109/LCSYS.2020.2999177},
isbn = {2475-1456},
year = {2020},
date = {2020-06-01},
urldate = {2020-06-01},
journal = {IEEE Control Systems Letters},
volume = {5},
number = {1},
pages = {25--30},
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. 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.},
note = {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.},
keywords = {Formal methods, NCS, SENTIENT},
pubstate = {published},
tppubtype = {article}
}
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.
18.
Delimpaltadakis, Giannis; Jr., Manuel Mazo
Isochronous Partitions for Region-Based Self-Triggered Control Journal Article
In: IEEE Transactions on Automatic Control, pp. 1-1, 2020, ISSN: 1558-2523.
BibTeX | Tags: Formal methods, NCS, SENTIENT | Links:
@article{delimpaltadakis2019isochronousb,
title = {Isochronous Partitions for Region-Based Self-Triggered Control},
author = {Giannis Delimpaltadakis and Manuel {Mazo Jr.}},
url = {https://mmazojr.3me.tudelft.nl/wp-content/uploads/2020/09/final_version_isoc_manifolds.pdf
https://arxiv.org/abs/1904.08788
https://ieeexplore.ieee.org/document/9091336},
doi = {10.1109/TAC.2020.2994020},
issn = {1558-2523},
year = {2020},
date = {2020-05-11},
journal = {IEEE Transactions on Automatic Control},
pages = {1-1},
keywords = {Formal methods, NCS, SENTIENT},
pubstate = {published},
tppubtype = {article}
}
19.
Verdier, Cees F; Jr., Manuel Mazo
Formal Controller Synthesis for Hybrid Systems Using Genetic Programming Online
2020.
BibTeX | Tags: CADUSY, Formal methods | Links:
@online{CeesFormalGP20,
title = {Formal Controller Synthesis for Hybrid Systems Using Genetic Programming},
author = {Cees F Verdier and Manuel {Mazo Jr.}},
url = {https://mmazojr.3me.tudelft.nl/wp-content/uploads/2020/09/Journal_Hybrid_Arxiv_Preprint.pdf
https://arxiv.org/abs/2003.14322},
year = {2020},
date = {2020-03-31},
keywords = {CADUSY, Formal methods},
pubstate = {published},
tppubtype = {online}
}
2019
20.
Verdier, Cees F; Babuska, Robert; Shyrokau, Barys; Jr., Manuel Mazo
Near Optimal Control With Reachability and Safety Guarantees Proceedings Article
In: 5th IFAC Conference on Intelligent Control and Automation Sciences (ICONS), 2019, pp. 230–235, 2019, ISSN: 2405-8963.
BibTeX | Tags: CADUSY, Formal methods | Links:
@inproceedings{ICONS19Cees,
title = {Near Optimal Control With Reachability and Safety Guarantees},
author = {Cees F Verdier and Robert Babuska and Barys Shyrokau and Manuel {Mazo Jr.} },
url = {https://mmazojr.3me.tudelft.nl/wp-content/uploads/2020/09/Near_optimal_control_preprint.pdf
https://www.sciencedirect.com/science/article/pii/S2405896319307761?via%3Dihub
},
doi = {10.1016/j.ifacol.2019.09.146},
issn = {2405-8963},
year = {2019},
date = {2019-10-29},
urldate = {2019-10-29},
booktitle = { 5th IFAC Conference on Intelligent Control and Automation Sciences (ICONS), 2019},
volume = {52},
number = {11},
pages = {230--235},
series = {IFAC-PapersOnLine},
keywords = {CADUSY, Formal methods},
pubstate = {published},
tppubtype = {inproceedings}
}