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

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}

}

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

}

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

}