@inproceedings{e967a276536e41d1a098c19bccf9693b,
title = "Signal Sampling and Optimisation Under Symbolic Timed Automata Constraints",
abstract = "We consider the problem of generating input signals for validation of cyber-physical systems. The class of signals that we are interested in is subject to complex constraints in both time and value domains, which are captured by Symbolic Timed Automata (STA). We propose a method for uniform sampling of traces recognised by STA. The proposed procedure is general and works for arbitrary alphabets equipped with a probability space and a computable measure. We devise a concrete method for linear alphabets. We then show how this method can be used to enhance falsification based on both sampling and optimisation. The results are validated on the case study of an artificial pancreas.",
author = "Beno{\^i}t Barbot and Nicolas Basset and Thao Dang and Alexandre Donz{\'e} and Marco Esposito and Dejan Nickovic",
year = "2025",
doi = "10.1007/978-3-032-05792-1\_6",
language = "English",
isbn = "978-3-032-05791-4",
volume = "16143",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "95--114",
editor = "Pavithra Prabhakar and Andrea Vandin",
booktitle = "Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems - Second International Joint Conference, QEST+FORMATS 2025, Aarhus, Denmark, August 26-28, 2025, Proceedings",
address = "Germany",
}