Timed Automata Relaxation for Reachability

D 2021

Timed Automata Relaxation for Reachability

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

Základní údaje

Originální název

Timed Automata Relaxation for Reachability

Autoři

BENDÍK, Jaroslav (203 Česká republika, garant, domácí), Ahmet SENCAN, Ebru Aydin GOL (203 Česká republika) a Ivana ČERNÁ (203 Česká republika, domácí)

Vydání

Part I vol. 12651. Heidelberg, 27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'21), od s. 291-310, 20 s. 2021

Nakladatel

Springer

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10200 1.2 Computer and information sciences

Utajení

není předmětem státního či obchodního tajemství

Forma vydání

tištěná verze "print"

Odkazy

URL

Impakt faktor

Impact factor: 0.402 v roce 2005

Kód RIV

RIV/00216224:14330/21:00120892

Organizační jednotka

Fakulta informatiky

ISBN

978-3-030-72015-5

ISSN

DOI

http://dx.doi.org/10.1007/978-3-030-72016-2_16

Klíčová slova anglicky

Timed Automata - Reachability - Relaxation of Constraints

Štítky

core_A, firank_A

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 15. 5. 2024 02:12, RNDr. Pavel Šmerk, Ph.D.

Anotace

V originále

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.

Návaznosti

EF16_019/0000822, projekt VaV

Název: Centrum excelence pro kyberkriminalitu, kyberbezpečnost a ochranu kritických informačních infrastruktur

Citovat

BENDÍK, Jaroslav, Ahmet SENCAN, Ebru Aydin GOL a Ivana ČERNÁ. Timed Automata Relaxation for Reachability. In Friso Groote and Kim Guldstrand Larsen. 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.

@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. 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.

Podrobný výpis o publikaci