Timed Automata Relaxation for Reachability

Investor logo

Warning

This publication doesn't include Faculty of Arts. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

BENDÍK Jaroslav SENCAN Ahmet GOL Ebru Aydin ČERNÁ Ivana

Year of publication 2021
Type Article in Proceedings
Conference 27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'21)
MU Faculty or unit

Faculty of Informatics

Citation
Web https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7979188/
Doi http://dx.doi.org/10.1007/978-3-030-72016-2_16
Keywords Timed Automata - Reachability - Relaxation of Constraints
Description 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.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.