Learning Symbolic Timed Models from Concrete Timed Data

Simon Dierl; Falk Maria Howar; Sean Kauffman; Martin Kristjansen; Kim Guldstrand Larsen; Florian Lorber; Malte Mauritz

doi:10.1007/978-3-031-33170-1_7

Learning Symbolic Timed Models from Concrete Timed Data

Simon Dierl, Falk Maria Howar, Sean Kauffman^*, Martin Kristjansen, Kim Guldstrand Larsen, Florian Lorber, Malte Mauritz

^*Kontaktforfatter

Publikation: Bidrag til bog/antologi/rapport/konference proceeding › Konferenceartikel i proceeding › Forskning › peer review

1 Citationer (Scopus)

Abstract

We present a technique for learning explainable timed automata from passive observations of a black-box function, such as an
artificial intelligence system. Our method accepts a single, long, timed
word with mixed input and output actions and learns a Mealy machine
with one timer. The primary advantage of our approach is that it constructs a symbolic observation tree from a concrete timed word. This
symbolic tree is then transformed into a human comprehensible automaton. We provide a prototype implementation and evaluate it by learning
the controllers of two systems: a brick-sorter conveyor belt trained with reinforcement learning and a real-world derived smart traffic light controller.
We compare different model generators using our symbolic observation
tree as their input and achieve the best results using k-tails. In our experiments, we learn smaller and simpler automata than existing passive
timed learners while maintaining accuracy.

Originalsprog	Engelsk
Titel	NASA Formal Methods : 15th International Symposium, NFM 2023, Houston, TX, USA, May 16–18, 2023, Proceedings
Redaktører	Kristin Yvonne Rozier, Swarat Chaudhuri
Antal sider	18
Forlag	Springer Science+Business Media
Publikationsdato	16 maj 2023
Sider	104-121
ISBN (Trykt)	978-3-031-33169-5
ISBN (Elektronisk)	978-3-031-33170-1
DOI	https://doi.org/10.1007/978-3-031-33170-1_7
Status	Udgivet - 16 maj 2023
Begivenhed	15th International Symposium on NASA Formal Methods, NFM 2023 - Houston, USA Varighed: 16 maj 2023 → 18 maj 2023

Konference

Konference	15th International Symposium on NASA Formal Methods, NFM 2023
Land/Område	USA
By	Houston
Periode	16/05/2023 → 18/05/2023

Navn	Lecture Notes in Computer Science (LNCS)
Vol/bind	13903 LNCS
ISSN	0302-9743

Bibliografisk note

Funding Information:
This work was supported by the S40S Villum Investigator Grant (37819) from VILLUM FONDEN, the ERC Advanced Grant LASSO, DIREC, and the Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) – 495857894 (STING).

Publisher Copyright:
© 2023, The Author(s), under exclusive license to Springer Nature Switzerland AG.

Adgang til dokumentet

10.1007/978-3-031-33170-1_7

AUB Link

Søg efter materialet i Aalborg Universitetsbiblioteks søgemaskine

S4OS: SCALABLE ANALYSIS OF SAFE, SMALL AND SECURE STRATEGIES FOR CYBER-PHYSICAL SYSTEMS
Larsen, K. G.
Villum Fonden
01/01/2021 → 31/12/2027
Projekter: Projekt › Forskning

Citationsformater

Dierl, S., Howar, F. M., Kauffman, S., Kristjansen, M., Guldstrand Larsen, K., Lorber, F., & Mauritz, M. (2023). Learning Symbolic Timed Models from Concrete Timed Data. I K. Y. Rozier, & S. Chaudhuri (red.), NASA Formal Methods: 15th International Symposium, NFM 2023, Houston, TX, USA, May 16–18, 2023, Proceedings (s. 104-121). Springer Science+Business Media. https://doi.org/10.1007/978-3-031-33170-1_7

Dierl, Simon ; Howar, Falk Maria ; Kauffman, Sean et al. / Learning Symbolic Timed Models from Concrete Timed Data. NASA Formal Methods: 15th International Symposium, NFM 2023, Houston, TX, USA, May 16–18, 2023, Proceedings. red. / Kristin Yvonne Rozier ; Swarat Chaudhuri. Springer Science+Business Media, 2023. s. 104-121 (Lecture Notes in Computer Science (LNCS), Bind 13903 LNCS).

@inproceedings{a7c1ed561e824752a57ad96e77d755ea,

title = "Learning Symbolic Timed Models from Concrete Timed Data",

abstract = "We present a technique for learning explainable timed automata from passive observations of a black-box function, such as an artificial intelligence system. Our method accepts a single, long, timed word with mixed input and output actions and learns a Mealy machine with one timer. The primary advantage of our approach is that it constructs a symbolic observation tree from a concrete timed word. This symbolic tree is then transformed into a human comprehensible automaton. We provide a prototype implementation and evaluate it by learning the controllers of two systems: a brick-sorter conveyor belt trained with reinforcement learning and a real-world derived smart traffic light controller. We compare different model generators using our symbolic observation tree as their input and achieve the best results using k-tails. In our experiments, we learn smaller and simpler automata than existing passive timed learners while maintaining accuracy.",

author = "Simon Dierl and Howar, {Falk Maria} and Sean Kauffman and Martin Kristjansen and {Guldstrand Larsen}, Kim and Florian Lorber and Malte Mauritz",

note = "Publisher Copyright: {\textcopyright} 2023, The Author(s), under exclusive license to Springer Nature Switzerland AG.; 15th International Symposium on NASA Formal Methods, NFM 2023 ; Conference date: 16-05-2023 Through 18-05-2023",

year = "2023",

month = may,

day = "16",

doi = "10.1007/978-3-031-33170-1_7",

language = "English",

isbn = "978-3-031-33169-5",

series = "Lecture Notes in Computer Science (LNCS)",

publisher = "Springer Science+Business Media",

pages = "104--121",

editor = "Rozier, {Kristin Yvonne} and Swarat Chaudhuri",

booktitle = "NASA Formal Methods",

address = "United States",

}

Dierl, S, Howar, FM, Kauffman, S, Kristjansen, M , Guldstrand Larsen, K, Lorber, F & Mauritz, M 2023, Learning Symbolic Timed Models from Concrete Timed Data. i KY Rozier & S Chaudhuri (red), NASA Formal Methods: 15th International Symposium, NFM 2023, Houston, TX, USA, May 16–18, 2023, Proceedings. Springer Science+Business Media, Lecture Notes in Computer Science (LNCS), bind 13903 LNCS, s. 104-121, 15th International Symposium on NASA Formal Methods, NFM 2023, Houston, USA, 16/05/2023. https://doi.org/10.1007/978-3-031-33170-1_7

Learning Symbolic Timed Models from Concrete Timed Data. / Dierl, Simon; Howar, Falk Maria; Kauffman, Sean et al.
NASA Formal Methods: 15th International Symposium, NFM 2023, Houston, TX, USA, May 16–18, 2023, Proceedings. red. / Kristin Yvonne Rozier; Swarat Chaudhuri. Springer Science+Business Media, 2023. s. 104-121 (Lecture Notes in Computer Science (LNCS), Bind 13903 LNCS).

Publikation: Bidrag til bog/antologi/rapport/konference proceeding › Konferenceartikel i proceeding › Forskning › peer review

TY - GEN

T1 - Learning Symbolic Timed Models from Concrete Timed Data

AU - Dierl, Simon

AU - Howar, Falk Maria

AU - Kauffman, Sean

AU - Kristjansen, Martin

AU - Guldstrand Larsen, Kim

AU - Lorber, Florian

AU - Mauritz, Malte

PY - 2023/5/16

Y1 - 2023/5/16

N2 - We present a technique for learning explainable timed automata from passive observations of a black-box function, such as an artificial intelligence system. Our method accepts a single, long, timed word with mixed input and output actions and learns a Mealy machine with one timer. The primary advantage of our approach is that it constructs a symbolic observation tree from a concrete timed word. This symbolic tree is then transformed into a human comprehensible automaton. We provide a prototype implementation and evaluate it by learning the controllers of two systems: a brick-sorter conveyor belt trained with reinforcement learning and a real-world derived smart traffic light controller. We compare different model generators using our symbolic observation tree as their input and achieve the best results using k-tails. In our experiments, we learn smaller and simpler automata than existing passive timed learners while maintaining accuracy.

AB - We present a technique for learning explainable timed automata from passive observations of a black-box function, such as an artificial intelligence system. Our method accepts a single, long, timed word with mixed input and output actions and learns a Mealy machine with one timer. The primary advantage of our approach is that it constructs a symbolic observation tree from a concrete timed word. This symbolic tree is then transformed into a human comprehensible automaton. We provide a prototype implementation and evaluate it by learning the controllers of two systems: a brick-sorter conveyor belt trained with reinforcement learning and a real-world derived smart traffic light controller. We compare different model generators using our symbolic observation tree as their input and achieve the best results using k-tails. In our experiments, we learn smaller and simpler automata than existing passive timed learners while maintaining accuracy.

U2 - 10.1007/978-3-031-33170-1_7

DO - 10.1007/978-3-031-33170-1_7

M3 - Article in proceeding

AN - SCOPUS:85164022605

SN - 978-3-031-33169-5

T3 - Lecture Notes in Computer Science (LNCS)

SP - 104

EP - 121

BT - NASA Formal Methods

A2 - Rozier, Kristin Yvonne

A2 - Chaudhuri, Swarat

PB - Springer Science+Business Media

T2 - 15th International Symposium on NASA Formal Methods, NFM 2023

Y2 - 16 May 2023 through 18 May 2023

ER -

Dierl S, Howar FM, Kauffman S, Kristjansen M , Guldstrand Larsen K, Lorber F et al. Learning Symbolic Timed Models from Concrete Timed Data. I Rozier KY, Chaudhuri S, red., NASA Formal Methods: 15th International Symposium, NFM 2023, Houston, TX, USA, May 16–18, 2023, Proceedings. Springer Science+Business Media. 2023. s. 104-121. (Lecture Notes in Computer Science (LNCS), Bind 13903 LNCS). doi: 10.1007/978-3-031-33170-1_7