SENTIENT Project

@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},

pubstate = {published},

tppubtype = {inproceedings}

}

@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}

}

@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}

}