Other formats:
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 and Ivana ČERNÁ. Timed Automata Relaxation for Reachability. 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, p.~291-310. ISBN~978-3-030-72015-5. Available from: https://dx.doi.org/10.1007/978-3-030-72016-2\_{}16.
|