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

• Masaki Waga, Étienne AndréHyper parametric timed CTL.TCAD, vol. 43, issue 11, 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, 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, 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, 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, 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, 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.

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

• 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 CharacterizationFORMATS 2023, Antwerp, Belgium, 21st September 2023. [slide]
• 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, 6 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

• 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

• 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: HSCC 2025. SPIN 2025. RV 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.
• Track Chair (FORMATS) of QEST+FORMATS 2024.
• Local Organization Chair of ATVA 2024.

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, 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

• 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