TY - GEN
T1 - Timed Automata Learning via SMT Solving
AU - Tappler, Martin
AU - Aichernig, Bernhard K.
AU - Lorber, Florian
N1 - Funding Information:
Acknowledgments. This work has been supported by the “University SAL Labs” initiative of Silicon Austria Labs (SAL) and its Austrian partner universities for applied fundamental research for electronic based systems.
Publisher Copyright:
© 2022, Springer Nature Switzerland AG.
PY - 2022
Y1 - 2022
N2 - Automata learning is a technique for automatically inferring models of existing systems, that enables formal verification of black-box systems. In this paper we propose a way of learning timed automata, extended final state machines that can measure the progress of time. We make use of SMT solving to learn timed automata consistent with the observations in a set of timed traces, which can be gathered via active testing or passive monitoring. By imposing a set of restrictions to the learnt models, we ensure that our solutions are not overly general. The presented SMT encoding of the problem allows for two ways of incremental solving and different search orders. We present a prototype implementation with results from case studies and randomly generated timed automata of varying size and complexity. We perform an extensive evaluation over six SMT solvers, using different theories and exploration strategies, as well as incremental and non-incremental solving.
AB - Automata learning is a technique for automatically inferring models of existing systems, that enables formal verification of black-box systems. In this paper we propose a way of learning timed automata, extended final state machines that can measure the progress of time. We make use of SMT solving to learn timed automata consistent with the observations in a set of timed traces, which can be gathered via active testing or passive monitoring. By imposing a set of restrictions to the learnt models, we ensure that our solutions are not overly general. The presented SMT encoding of the problem allows for two ways of incremental solving and different search orders. We present a prototype implementation with results from case studies and randomly generated timed automata of varying size and complexity. We perform an extensive evaluation over six SMT solvers, using different theories and exploration strategies, as well as incremental and non-incremental solving.
UR - http://www.scopus.com/inward/record.url?scp=85131149860&partnerID=8YFLogxK
U2 - 10.1007/978-3-031-06773-0_26
DO - 10.1007/978-3-031-06773-0_26
M3 - Conference paper
AN - SCOPUS:85131149860
SN - 9783031067723
T3 - Lecture Notes in Computer Science
SP - 489
EP - 507
BT - NASA Formal Methods - 14th International Symposium, NFM 2022, Proceedings
A2 - Deshmukh, Jyotirmoy V.
A2 - Havelund, Klaus
A2 - Perez, Ivan
PB - Springer Science and Business Media Deutschland GmbH
T2 - 14th International Symposium on NASA Formal Methods
Y2 - 24 May 2022 through 27 May 2022
ER -