Masaki Waga (和賀 正樹)

Research Interests

• Lightweight verification of black-box systems including cyber-physical systems and machine learning-based systems
• In particular, monitoring of real-time systems with timed automata
• Some related problems, e.g., falsification, runtime enforcement, and specification learning

Publications and Theses

• Kengo Irie, Masaki Waga, Kohei SuenagaActive Learning of Symbolic Mealy Automata. To appear in TCS, 2026, Elsevier.
  This paper is an extension of the article with the same title published in the proceedings of ICTAC 2025.
• Masaki Waga, Kotaro Matsuoka, Takashi SuwaArithHomFA: A toolkit for oblivious online STL monitoring.SCICO, vol. 254, issue 103539, pp. 1-4, 2026, Elsevier.
  [Elsevier]
• Kazuki Kinoshita, Masaki WagaLearning Alternating Real-Time Automata. To appear in Proc. QEST+FORMATS 2026, Springer.
  [extended version at arXiv]
• Niklas Kochdumper, Chiao Hsieh, Hadi Dayekh, Thao Dang, Masaki Waga, Kohei SuenagaEvaluating Hybrid Automata Learning Tools Based on Their Success in Formal Verification. To appear in Proc. MED 2026.
• Masataka Yoneda, Yusuke Matsushita, Go Kamoda, Kohei Suenaga, Takuya Akiba, Masaki Waga, Sho YokoiA Fast and Soft Pattern Matcher for Trillion-Scale Corpus. To appear in Proc. ICML 2026.
  [extended version at arXiv]
• Kengo Irie, Masaki Waga, Kohei SuenagaActive Learning of Symbolic Mealy Automata. Proc. ICTAC 2025, LNCS 16237, pp. 319-337, Springer.
  [Springer | extended version at arXiv]
• Daichi Aiba, Masaki Waga, Hiroya Fujinami, Koko Muroya, Shuntaro Ouchi, Naoki Ueda, Yosuke Yokoyama, Yuta Wada, Ichiro HasuoA Variety of Request-Response Specifications. Proc. ICTAC 2025, LNCS 16237, pp. 239-257, Springer.
  [Springer | extended version at arXiv]
• Hiroya Fujinami, Masaki Waga, Jie An, Kohei Suenaga, Nayuta Yanagisawa, Hiroki Iseri, Ichiro HasuoComponentwise Automata Learning for System Integration. Proc. ATVA 2025, LNCS 16145, pp. 3-26, Springer.
  [Springer | extended version at arXiv]
• Masaki Waga, Étienne AndréHyper pattern matching. Proc. RV 2025, pp. 397-416, Springer.
  [Springer | extended version at arXiv]
• Tsubasa Matsumoto, Kazuki Watanabe, Kohei Suenaga, Masaki WagaEfficient Black-Box Checking with Specification-Guided Abstraction.TECS, vol. 24, issue 5s, pp. 137:1-137:26, 2025, ACM.
  This paper was accepted at EMSOFT 2025.
  [ACM]
• Song Bian, Zian Zhao, Ruiyu Shen, Zhou Zhang, Ran Mao, Dawei Li, Yizhong Liu, Masaki Waga, Kohei Suenaga, Zhenyu Guan, Jiafeng Hua, Yier Jin, Jianwei LiuCHLOE: Loop Transformation over Fully Homomorphic Encryption via Multi-Level Vectorization and Control-Path Reduction. Proc. SP 2025, pp. 2395-2413.
  [IEEE | extended version at Cryptology ePrint Archive]
• Chiao Hsieh, Masaki Waga, Kohei SuenagaCertifying Lyapunov Stability of Black-Box Nonlinear Systems via Counterexample Guided Synthesis. Proc. HSCC 2025, pp. 8:1-8:11, ACM.
  [ACM | extended version at arXiv]
• Hiroyuki Deguchi, Go Kamoda, Yusuke Matsushita, Chihiro Taguchi, Kohei Suenaga, Masaki Waga, Sho YokoiA Soft and Fast Pattern Matcher for Billion-Scale Corpus Searches. Proc. ICLR 2025.
  [OpenReview.net | extended version at arXiv]
• Masaki Waga, Étienne AndréHyper parametric timed CTL.TCAD, vol. 43, issue 11, pp. 4286-4297, 2024, IEEE.
  This paper was accepted at EMSOFT 2024.
  [ieee | extended version at arXiv]
• Masaki Waga, Kotaro Matsuoka, Takashi Suwa, Naoki Matsumoto, Ryotaro Banno, Song Bian, Kohei SuenagaOblivious Monitoring for Discrete-Time STL via Fully Homomorphic Encryption. Proc. RV 2024, LNCS 15191, pp. 59-69, Springer.
  [Springer | extended version at arXiv]
• Jesse Reimann, Nico Mansion, James Haydon, Benjamin Bray, Agnishom Chattopadhyay, Sota Sato, Masaki Waga, Étienne André, Ichiro Hasuo, Naoki Ueda, Yosuke YokoyamaTemporal Logic Formalisation of ISO 34502 Critical Scenarios: Modular Construction with the RSS Safety Distance Proc. SAC 2024, pp. 186-195, ACM.
  [ACM | extended version at arXiv]
• Amit Gurung, Masaki Waga, Kohei SuenagaLearning nonlinear hybrid automata from input--output time-series data. Proc. ATVA 2023, LNCS 14215, pp. 33-52, Springer.
  [Springer | extended version at arXiv]
• Junya Shijubo, Masaki Waga, Kohei SuenagaProbabilistic Black-Box Checking via Active MDP Learning.TECS, vol. 22, issue 5s, pp. 148:1-148:26, 2023, ACM.
  This paper was accepted at EMSOFT 2023.
  [ACM | extended version at arXiv]
• Masaki WagaActive Learning of Deterministic Timed Automata with Myhill-Nerode Style Characterization. Proc. CAV 2023, LNCS 13964, pp. 3-26, Springer.
  [Springer | extended version at arXiv]
• Masaki Waga, Étienne André, Ichiro HasuoParametric Timed Pattern Matching.TOSEM, vol. 32, issue 1, pp. 10:1-10:35, 2023, ACM.
  This paper is an extension of [AHW18] and [WA19] in the proceedings of ICECCS 2018 and NFM 2019, respectively.
  [ACM]
• Masaki Waga, Étienne André, Ichiro HasuoModel-Bounded Monitoring of Hybrid Systems.TCPS, vol. 6, issue 4, pp. 30:1-30:26, 2022, ACM.
  This paper is an extension of the article with the same title published in the proceedings of ICCPS 2021.
  [ACM]
• Atsushi Kikuchi, Kotaro Uchida, Masaki Waga, Kohei SuenagaBOREx: Bayesian-Optimization-Based Refinement of Saliency Map for Image- and Video-Classification Models. Proc. ACCV 2022, LNCS 13847, pp. 274-290, Springer.
  [Springer | extended version at arXiv]
• Masaki Waga, Ezequiel Castellano, Sasinee Pruekprasert, Stefan Klikovits, Toru Takisaka, Ichiro HasuoDynamic Shielding for Reinforcement Learning in Black-Box Environments. Proc. ATVA 2022, LNCS 13505, pp. 25-41, Springer.
  [Springer | extended version at arXiv] [artifact]
• Ryotaro Banno, Kotaro Matsuoka, Naoki Matsumoto, Song Bian, Masaki Waga, Kohei SuenagaOblivious Online Monitoring for Safety LTL Specification via Fully Homomorphic Encryption. Proc. CAV 2022, LNCS 13371, pp. 447-468, Springer.
  [Springer | extended version at arXiv]
• Étienne André, Masaki Waga, Natsuki Urabe, Ichiro HasuoExemplifying parametric timed specifications over signals with bounded behavior. Proc. NFM 2022, LNCS 13260, pp. 470-488, Springer.
  [Springer | extended version at arXiv]
• Sota Sato, Atsuyoshi Saimen, Masaki Waga, Kenji Takao, Ichiro HasuoHybrid System Falsification for Multiple-Constraint Parameter Synthesis: a Gas Turbine Case Study. Proc. FM 2021, LNCS 13047, pp. 313-329, Springer.
  [Springer]
• Junya Shijubo, Masaki Waga, Kohei SuenagaEfficient Black-Box Checking via Model Checking with Strengthened Specifications. Proc. RV 2021, LNCS 12974, pp. 100-120, Springer.
  [Springer | extended version at arXiv]
• Sota Sato, Masaki Waga, Ichiro HasuoConstrained Optimization for Falsification and Conjunctive Synthesis. Proc. ADHS 2021, pp. 217-222, Elsevier.
  [Elsevier | extended version at arXiv]
• Masaki Waga, Étienne André, Ichiro HasuoModel-Bounded Monitoring of Hybrid Systems. Proc. ICCPS 2021, pp. 21-32, ACM.
  [ACM | extended version at arXiv] [artifact]
• Masaki WagaEmpowering Runtime Verification with Polyhedra.Ph.D. Thesis, School of Multidisciplinary Sciences, The Graduate University for Advanced Studies (SOKENDAI), 2020.
  [SOKENDAI]
• Elena Gutiérrez, Takamasa Okudono, Masaki Waga, Ichiro HasuoGenetic algorithm for the weight maximization problem on weighted automata. Proc. GECCO 2020, pp. 699-707, ACM.
  [ACM | extended version at arXiv]
• Masaki WagaFalsification of cyber-physical systems with robustness-guided black-box checking. Proc. HSCC 2020, pp. 11:1-11:13, ACM.
  [ACM | extended version at arXiv]
• Takamasa Okudono, Masaki Waga, Taro Sekiyama, Ichiro HasuoWeighted Automata Extraction from Recurrent Neural Networks via Regression on State Spaces. Proc. AAAI 2020, vol. 34, No. 04, pp. 5306-5314, AAAI Press.
  [AAAI | extended version at arXiv]
• Masaki WagaOnline Quantitative Timed Pattern Matching with Semiring-Valued Weighted Automata. Proc. FORMATS 2019, LNCS 11750, pp. 3-22, Springer.
  [lncs | extended version at arXiv]
• Masaki Waga, Étienne André, Ichiro HasuoSymbolic Monitoring Against Specifications Parametric in Time and Data. Proc. CAV 2019, LNCS 11561, pp. 520-539, Springer.
  [lncs | extended version at arXiv] [artifact]
• Masaki Waga, Étienne AndréOnline Parametric Timed Pattern Matching with Automata-Based Skipping. Proc. NFM 2019, LNCS 11460, pp. 371-389, Springer.
  [lncs | extended version at arXiv]
• Étienne André, Ichiro Hasuo, Masaki WagaOffline Timed Pattern Matching under Uncertainty. Proc. ICECCS 2018, pp. 10-20, IEEE.
  [ieee | author version at arXiv]
• Masaki Waga, Ichiro HasuoMoore-Machine Filtering for Timed and Untimed Pattern Matching.TCAD, vol. 37, issue 11, pp. 2649-2660, 2018, IEEE.
  This paper was accepted at EMSOFT 2018.
  [ieee | extended version at arXiv]
• Masaki Waga, Ichiro Hasuo, Kohei SuenagaMONAA: A Tool for Timed Pattern Matching with Automata-Based Acceleration. Proc. MT@CPSWeek 2018, pp. 14-15, IEEE.
  [ieee | extended version at arXiv]
• Masaki WagaTechniques for Efficient Timed Pattern Matching.Master Thesis, Graduate School of Information Science and Technology, The University of Tokyo, 2018.
• Masaki Waga, Ichiro Hasuo, Kohei SuenagaEfficient Online Timed Pattern Matching by Automata-Based Skipping. Proc. FORMATS 2017, LNCS 10419, pp. 224-243, Springer.
  [lncs | extended version at arXiv]
• Masaki Waga, Takumi Akazaki, Ichiro HasuoA Boyer-Moore Type Algorithm for Timed Pattern Matching. Proc. FORMATS 2016, LNCS 9884, pp. 121-139, Springer.
  [lncs | extended version at arXiv]
• Masaki WagaTimed Pattern Matching with Automata.Bachelor Thesis, School of Science, The University of Tokyo, 2016.

Editorial Work and Edited Volumes

• Jane Hillston, Sadegh Soudjani, Masaki WagaIntroduction to the special issue on timed and stochastic approaches to system evaluation. To appear in Int. J. Softw. Tools Technol. Transfer, 2026, Springer.
  [Editorial introduction to special issue]
  [Springer]
• Jane Hillston, Sadegh Soudjani, Masaki Waga (eds.)Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems: QEST+FORMATS 2024 Proceedings.Lecture Notes in Computer Science 14996, 2024, Springer.
  [Editorial introduction to special issue]
  [Springer]

Tools

• FalCAuN — A tool for FALsification of Cyber-physical systems via AUtomata learNing
• SyMon — A tool for SYmbolic MONitoring
• ParamMONAA — A Tool for Parametric Timed Pattern Matching with Automata-Based Acceleration
• filt - An experimental implementation of Moore machine filter for timed and untimed pattern matching
• MONAA — A Tool for Timed Pattern Matching with Automata-Based Acceleration

Selected Talks

• Hyper pattern matching.PPL 2026, Gamagori, Aichi, 11th March 2026.
• Specification-Based Testing of Cyber-Physical Systems via Black-Box Checking. Invited talk at QuantFormal 2025, Goa, India, 15th December 2025. [slide]
• Active Learning of Symbolic Mealy Automata.ICTAC 2025, Marrakech, Morocco, 27th November 2025. [slide]
• Hyper pattern matching.RV 2025, Graz, Austria, 19th September 2025. [slide]
• Soft Pattern Matching: Toward Runtime Verification of NLP Systems. Invited talk at SAIV 2025, Zagreb, Croatia, 21st July 2025. [slide]
• Hyper Parametric Timed CTL.PPL 2025, Gamagori, Aichi, 6th March 2025.
• Oblivious Monitoring for Discrete-Time STL via Fully Homomorphic EncryptionRV 2024, Istanbul, Türkiye, 15th October 2024. [slide]
• Hyper parametric timed CTLEMSOFT 2024, Raleigh, NC, USA, 2nd October 2024. [slide | poster]
• Active Learning of Deterministic Timed Automata with Myhill-Nerode Style Characterization Invited talk at FORMATS 2023, Antwerp, Belgium, 21st September 2023. [slide]
• 信頼されるAI-CPSのためのオートマトン学習によるアプローチ Invited talk at SIG-FPAI 125, Morioka, Japan, 29th August 2023.
• Active Learning of Deterministic Timed Automata with Myhill-Nerode Style CharacterizationCAV 2023, Paris, France, 22nd July 2023.
• Dynamic Shielding for Reinforcement Learning in Black-Box EnvironmentsATVA 2022, Online, 26th October 2022. [slide | video]
• Parametric Timed Pattern Matching. Invited talk at SES 2022, Tokyo, 6th September 2022. [slide (in Japanese)]
• Model-Bounded Monitoring of Hybrid Systems.ICCPS 2021, Online, 20th May 2021. [slide | video]
• Model-Bounded Monitoring of Hybrid Systems.MT-CPS 2021, Online, 18th May 2021. [slide]
• Online Quantitative Timed Pattern Matching with Semiring-Valued Weighted Automata. Invited talk at YR-OWLS, Online, 12th May 2021. [slide | video]
• Symbolic Monitoring against Specifications Parametric in Time and Data. Invited talk at JSSST 2020, Online, 10th September 2020. [video (in Japanese)]
• Falsification of cyber-physical systems with robustness-guided black-box checkingHSCC 2020, Online, April 2020. [slide | video]
• Symbolic Monitoring Against Specifications Parametric in Time and DataMT-CPS 2020, Online, April 2020. [slide | video]
• オートマトンによる柔軟で高速な実行時監視とログ抽出ERATO MMSD 自動車産業応用セミナーシリーズ 第二回, Online, 17th March 2020.
• Online Quantitative Timed Pattern Matching with Semiring-Valued Weighted AutomataFORMATS 2019, Amsterdam, Netherlands, 27th August 2019. [slide]
• Symbolic Monitoring against Specifications Parametric in Time and DataCAV 2019, New York City, USA, 16th July 2019. [slide]
• Online Parametric Timed Pattern Matching with Automata-Based SkippingNFM 2019, Houston, USA, 7th May 2019. [slide]
• Online Parametric Timed Pattern Matching with Automata-Based SkippingMT-CPS 2019, Montreal, Canada, 15th April 2019. [slide]
• Moore-Machine Filtering for Timed and Untimed Pattern MatchingPPL 2019, 花巻, Japan, 8th March 2019.
• Moore-Machine Filtering for Timed and Untimed Pattern MatchingEMSOFT 2018, Turin, Italy, 2nd October 2018. [slide]
• MONAA — A Tool for Timed Pattern Matching with Automata-Based AccelerationMT-CPS 2018, Porto, Portugal, 10th April 2018. [slide]
• A Boyer-Moore Type Algorithm for Timed Pattern MatchingFORMATS 2016, Quebec, Canada, August 2016. [slide]

Selected Poster Presentations

• SyMon − Symbolic Monitor for Parametric Spec.
  RV 2025, Graz, Austria, 18 October 2025. [poster]
• FalCAuN − CPS Testing with Automata Learning
  RV 2024, Istanbul, Türkiye, 16 October 2024. [poster]
• Symbolic Monitoring against Specifications Parametric in Time and Data
  WINTER FESTA Episode 5, Tokyo, Japan, 26 December 2019. [poster]
• 物理情報システムのモニタリング --「安全、危険」から「どれくらい安全か」へ--
  NII Open House 2019, Tokyo, Japan, 31 May -- 1 June 2019. [poster] (Japanese)
• 時間パターンマッチングによる CPS のモニタリング
  ERATO MMSD Symposium, Tokyo, Japan, 21 May 2019. [poster] (Japanese)
• Real-Time Monitoring Enhanced by Automata-based Skipping
  NII Open House 2018, Tokyo, Japan, 22--23 June 2018. [poster]

Awards

• Outstanding Paper Award (jointly with Masataka Yoneda, Go Kamoda, Yusuke Matsushita, Kohei Suenaga, Takuya Akiba, and Sho Yokoi), NLP2026, March 11, 2026.
• Distinguished paper award (jointly with Hiroya Fujinami, Jie An, Kohei Suenaga, Nayuta Yanagisawa, Hiroki Iseri, and Ichiro Hasuo), ATVA 2025, October, 2025.
• RV 2024 Best Poster and Tool Showcase Award, 21st International Conference on Runtime Verification (RV 2024), October 16, 2024.
• YANS 2024 demonstration award (jointly with Hiroyuki Deguchi, Go Kamoda, Yusuke Matsushita, Kai Keida, and Sho Yokoi), YANS (Young Researcher Association for NLP Studies), September 6, 2024.
• YANS 2024 Recuruit Co., Ltd. award (jointly with Hiroyuki Deguchi, Go Kamoda, Yusuke Matsushita, Kai Keida, and Sho Yokoi), YANS (Young Researcher Association for NLP Studies), September 6, 2024.
• CSS2021/PWS outstanding paper award (jointly with Ryotaro Banno, Kotaro Matsuoka, Naoki Matsumoto, Song Bian, and Kohei Suenaga), CSEC: Computer Security Group, October 28, 2021.
• Dean award, School of Multidisciplinary Sciences, The Graduate University for Advanced Studies (SOKENDAI), September 28, 2020.
• Best student award, National Institute of Informatics, September 26, 2019.
• Oded Maler award for the best paper, FORMATS 2019, August, 2019.
• Best paper award (jointly with Étienne André and Ichiro Hasuo), ICECCS 2018, December, 2018.

Professional Services

• Program committee member: ICFEM 2026. RV 2026. QEST+FORMATS 2026. EMSOFT 2026. FM 2026 Doctoral Symposium. HSCC/ICCPS 2026. VMCAI 2026. PPL 2026. ICFEM 2025. RV 2025. ATVA 2025. QEST+FORMATS 2025. HSCC 2025. SPIN 2025. RV 2024. PPL 2024. RV 2023. FORMATS 2023 (also chair of special track on "monitoring of cyber-physical systems"). HSCC 2023. RV 2022. AAAI 2021. FORMATS 2020. HSCC Poster/Demo 2021. HSCC Poster/Demo 2020.
• Artifact evaluation committee member: ATVA 2024. CAV 2022. CAV 2021.
• Guest Co-Editor of the STTT Special Issue on Timed and Stochastic Approaches to System Evaluation of International Journal on Software Tools for Technology Transfer (STTT).
• Organization Committee Member of IPSJ PRO2026.
• Artifact Evaluation Co-Chair of FM 2026.
• Track Chair (FORMATS) of QEST+FORMATS 2024.
• Local Organization Chair of ATVA 2024.
• Financial Vice Chair of PPL 2023.
• Financial Chair of PPL 2022.

Teaching Experiences

• Computer Science Laboratory and Exercise 2 (Hardware) (計算機科学実験及演習２ (ハードウェア)), 2023/10--, Kyoto University
• Elementary Course of Experimental Physics (物理学実験), 2022/10--2023/3, Kyoto University
• System Verification (システム検証論) (jointly with Kohei Suenaga and Atsushi Igarashi), 2021/10--, Kyoto University
• Computer Science Laboratory and Exercise 3 (Software) (計算機科学実験及演習３ (ソフトウェア)) (jointly with Kohei Suenaga), 2021/4--, Kyoto University
• Computer Science Laboratory and Exercise 2 (Hardware) (計算機科学実験及演習２ (ハードウェア)), 2020/10--2022/3, Kyoto University
• Teaching assistant for Formal Language Theory (形式言語理論), 2016/10--2017/3, The University of Tokyo
• Teaching assistant for Applied Logic (応用論理), 2016/4--2016/9, The University of Tokyo

Grants

• PRESTO Convergence Research, Grant Number: JPMJCR26X4, Japan Science and Technology Agency (JST), 2026/04-2028/03.
• BOOST, Grant Number: JPMJBY24H8, Japan Science and Technology Agency (JST), 2025/05-2030/04.
• Grant-in-Aid for Scientific Research (A), Grant Number: 25H01113, Japan Society for the Promotion of Science, 2025/04-2030/03.
• PRESTO, Grant Number: JPMJPR22CA, Japan Science and Technology Agency (JST), 2022/10-2026/03.
• Grant-in-Aid for Early-Career Scienticts, Grant Number: 22K17873, Japan Society for the Promotion of Science, 2022/04-2025/03.
• ACT-X, Grant Number: JPMJAX200U, Japan Science and Technology Agency (JST), 2020/11-2023/03.
• Grant-in-Aid for JSPS Fellows, Grant Number: 18J22498, Japan Society for the Promotion of Science, 2018/04-2021/03.
• Travel Grant, REFEC: Research Foundation for the Electrotechnology of Chubu.

Misc

• JST News September 2025: "さきがける科学人― 数学を使ってシステムの安全性を証明する 信頼できるAIを構築する基盤技術を創出" (in Japanese)
• Press release: "ＩＳＯ ３４５０２の自動運転車危険シナリオを数学的に定式化" (in Japanese)
  • "Mathematical Formulation of ISO 34502 Hazardous Scenarios for Automated Driving Systems - Automation and Streamlining of Safety Assurance Tasks Accelerate Social Acceptance of Automated Driving" (in English)
• An article at CNRS web page on our ICECCS 2018 paper (in French)

Contact

Office

Dept. of Communications and Computer Engineering, Graduate School of Informatics, Kyoto University, Yoshida-Honmachi, Sakyo-ku, Kyoto 606-8501, Japan

E-mail address

mwaga [at] fos.kuis.kyoto-u.ac.jp