Timed Automata Relaxation for Reachability

BENDÍK, Jaroslav, Ahmet SENCAN, Ebru Aydin GOL and 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, p. 291-310. ISBN 978-3-030-72015-5. Available from: https://dx.doi.org/10.1007/978-3-030-72016-2_16.

Basic information

• Original name: Timed Automata Relaxation for Reachability
• Authors: BENDÍK, Jaroslav (203 Czech Republic, guarantor, belonging to the institution), Ahmet SENCAN, Ebru Aydin GOL (203 Czech Republic) and Ivana ČERNÁ (203 Czech Republic, belonging to the institution).
• Edition: Part I vol. 12651. Heidelberg, 27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'21), p. 291-310, 20 pp. 2021.
• Publisher: Springer

Other information

• Original language: English
• Type of outcome: Proceedings paper
• Field of Study: 10200 1.2 Computer and information sciences
• Confidentiality degree: is not subject to a state or trade secret
• Publication form: printed version "print"
• WWW: URL
• Impact factor: Impact factor: 0.402 in 2005
• RIV identification code: RIV/00216224:14330/21:00120892
• Organization unit: Faculty of Informatics
• ISBN: 978-3-030-72015-5
• ISSN: 0302-9743
• Doi: http://dx.doi.org/10.1007/978-3-030-72016-2_16
• Keywords in English: Timed Automata - Reachability - Relaxation of Constraints
• Tags: core_A, firank_A
• Tags: International impact, Reviewed

Abstract

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.

Links

• EF16_019/0000822, research and development project: Name: Centrum excelence pro kyberkriminalitu, kyberbezpečnost a ochranu kritických informačních infrastruktur