Další formáty:
BibTeX
LaTeX
RIS
@inproceedings{1716036,
author = {Bendík, Jaroslav and Sencan, Ahmet and Gol, Ebru Aydin and Černá, Ivana},
address = {Heidelberg},
booktitle = {27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'21)},
doi = {http://dx.doi.org/10.1007/978-3-030-72016-2_16},
edition = {Part I vol. 12651},
editor = {Friso Groote and Kim Guldstrand Larsen},
keywords = {Timed Automata - Reachability - Relaxation of Constraints},
howpublished = {tištěná verze "print"},
language = {eng},
location = {Heidelberg},
isbn = {978-3-030-72015-5},
pages = {291-310},
publisher = {Springer},
title = {Timed Automata Relaxation for Reachability},
url = {https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7979188/},
year = {2021}
}
TY - JOUR
ID - 1716036
AU - Bendík, Jaroslav - Sencan, Ahmet - Gol, Ebru Aydin - Černá, Ivana
PY - 2021
TI - Timed Automata Relaxation for Reachability
PB - Springer
CY - Heidelberg
SN - 9783030720155
KW - Timed Automata - Reachability - Relaxation of Constraints
UR - https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7979188/
N2 - Timed automata (TA) have shown to be a suitable formalism for modeling real-time systems. Moreover, modern model-checking tools allow a designer to check whether a TA complies with the system specification. However, the exact timing constraints of the system are often uncertain during the design phase. Consequently, the designer is able to build a TA with a correct structure, however, the timing constraints need to be tuned to make the TA comply with the specification. In this work, we assume that we are given a TA together with an existential property, such as reachability, that is not satisfied by the TA. We propose a novel concept of a minimal sufficient reduction (MSR) that allows us to identify the minimal set S of timing constraints of the TA that needs to be tuned to meet the specification. Moreover, we employ mixed-integer linear programming to actually find a tuning of S that leads to meeting the specification.
ER -
BENDÍK, Jaroslav, Ahmet SENCAN, Ebru Aydin GOL a Ivana ČERNÁ. Timed Automata Relaxation for Reachability. Online. In Friso Groote and Kim Guldstrand Larsen. \textit{27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'21)}. Part I vol. 12651. Heidelberg: Springer, 2021. s.~291-310. ISBN~978-3-030-72015-5. Dostupné z: https://dx.doi.org/10.1007/978-3-030-72016-2\_{}16. [citováno 2024-04-24]
|
