Timed Automata Relaxation for Reachability

Logo poskytovatele

Varování

Publikace nespadá pod Filozofickou fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.
Autoři

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

Rok publikování 2021
Druh Článek ve sborníku
Konference 27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'21)
Fakulta / Pracoviště MU

Fakulta informatiky

Citace
www https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7979188/
Doi http://dx.doi.org/10.1007/978-3-030-72016-2_16
Klíčová slova Timed Automata - Reachability - Relaxation of Constraints
Popis 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.
Související projekty:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.