Waga, Masaki(Graduate School of Informatics, Department of Informatics) | Activity Database on Education and Research, Kyoto University

Waga, Masaki

Graduate School of Informatics, Department of Informatics Assistant Professor

Last Updated :2025/05/12

Basic Information

Faculty

工学部

Academic Degree

(The University of Tokyo)

(The Graduate University for Advanced Studies, SOKENDAI)

Academic Resume (Graduate Schools)

The Graduate University for Advanced Studies, SOKENDAI, 複合科学研究科情報学専攻博士課程（３年次編入）, 修了

The University of Tokyo, 大学院情報理工学系研究科コンピュータ科学専攻修士課程, 修了

Academic Resume (Undergraduate School/Majors)

東京大学, 理学部情報科学科, 卒業

High School

High School
開成高校

Research History

From Sep. 2023, To Sep. 2023
University Sorbonne Paris Nord, LIPN, Visiting academic fellow/professor

From Apr. 2021, To Present
National Institute of Informatics, Visiting Assistant Professor

From Oct. 2020, To Present
Kyoto University, Graduate School of Informatics, Assistant Professor

From Apr. 2018, To Sep. 2020
Japan Society for the Promotion of Science, Research Fellow (DC1)

From Apr. 2017, To Sep. 2020
National Institute of Informatics, アーキテクチャ科学研究系, Research Assistant

Language of Instruction

English

Japanese

ID,URL

ORCID ID
0000-0001-9360-7490
J-Global ID
202001014513731091
Researcher number
00899007
External link
https://www.fos.kuis.kyoto-u.ac.jp/~mwaga/

researchmap URL

https://researchmap.jp/mwaga

Last Updated :2025/05/12

Research

Research Topics, Overview of the research

Research Topics
Formal Verification

Research Interests

formal verification

automata learning

runtime verification

model checking

timed automata

Research Areas

Informatics, Software

Papers

Temporal Logic Formalisation of ISO 34502 Critical Scenarios: Modular Construction with the RSS Safety Distance.
Jesse Reimann; Nico Mansion; James Haydon; Benjamin Bray; Agnishom Chattopadhyay; Sota Sato 0001; Masaki Waga; Étienne André; Ichiro Hasuo; Naoki Ueda; Yosuke Yokoyama
CoRR, 2024

Data for "Exemplifying parametric timed specifications over signals with bounded behavior".
Étienne André; Masaki Waga; Natsuki Urabe; Ichiro Hasuo
Mar. 2022

Data for "Exemplifying parametric timed specifications over signals with bounded behavior".
Étienne André; Masaki Waga; Natsuki Urabe; Ichiro Hasuo
Jan. 2022

Oblivious Monitoring for Discrete-Time STL via Fully Homomorphic Encryption.
Masaki Waga; Kotaro Matsuoka; Takashi Suwa; Naoki Matsumoto; Ryotaro Banno; Song Bian 0001; Kohei Suenaga
Runtime Verification - 24th International Conference(RV), 2024

Hyper Parametric Timed CTL
Masaki Waga; Étienne André
IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, Nov. 2024

Learning Weighted Finite Automata over the Max-Plus Semiring and its Termination.
Takamasa Okudono; Masaki Waga; Taro Sekiyama; Ichiro Hasuo
CoRR, 2024

Oblivious Monitoring for Discrete-Time STL via Fully Homomorphic Encryption.
Masaki Waga; Kotaro Matsuoka; Takashi Suwa; Naoki Matsumoto; Ryotaro Banno; Song Bian 0001; Kohei Suenaga
CoRR, 2024

Temporal Logic Formalisation of ISO 34502 Critical Scenarios: Modular Construction with the RSS Safety Distance.
Jesse Reimann; Nico Mansion; James Haydon; Benjamin Bray; Agnishom Chattopadhyay; Sota Sato 0001; Masaki Waga; Étienne André; Ichiro Hasuo; Naoki Ueda; Yosuke Yokoyama
SAC, 2024
Access this paper :

ARCH-COMP23 Category Report: Falsification.
Claudio Menghi; Paolo Arcaini; Walstan Baptista; Gidon Ernst; Georgios Fainekos; Federico Formica; Sauvik Gon; Tanmay Khandait; Atanu Kundu 0002; Giulia Pedrielli; Jarkko Peltomäki; Ivan Porres; Rajarshi Ray 0001; Masaki Waga; Zhenya Zhang
ARCH, 2023, Invited

Probabilistic Black-Box Checking via Active MDP Learning.
Junya Shijubo; Masaki Waga; Kohei Suenaga
CoRR, 2023

Probabilistic Black-Box Checking via Active MDP Learning.
Junya Shijubo; Masaki Waga; Kohei Suenaga
ACM Transactions on Embedded Computing Systems, Oct. 2023

Learning Nonlinear Hybrid Automata from Input-Output Time-Series Data.
Amit Gurung; Masaki Waga; Kohei Suenaga
ATVA (1), 2023, Peer-reviewed

Efficient Online Timed Pattern Matching by Automata-Based Skipping
Masaki Waga; Ichiro Hasuo; Kohei Suenaga
FORMATS 2017, 2017, Peer-reviewed

Learning nonlinear hybrid automata from input-output time-series data.
Amit Gurung; Masaki Waga; Kohei Suenaga
CoRR, 2023

BOREx: Bayesian-Optimization-Based Refinement of Saliency Map for Image- and Video-Classification Models.
Atsushi Kikuchi; Kotaro Uchida; Masaki Waga; Kohei Suenaga
CoRR, 2022

BOREx: Bayesian-Optimization-Based Refinement of Saliency Map for Image- and Video-Classification Models.
Atsushi Kikuchi; Kotaro Uchida; Masaki Waga; Kohei Suenaga
ACCV (7), 2022

Active Learning of Deterministic Timed Automata with Myhill-Nerode Style Characterization
Masaki Waga
35th International Conference on Computer-Aided Verification, Jul. 2023, Peer-reviewed, Lead author, Last author, Corresponding author
Access this paper :

Dynamic Shielding for Reinforcement Learning in Black-Box Environments.
Masaki Waga; Ezequiel Castellano; Sasinee Pruekprasert; Stefan Klikovits; Toru Takisaka; Ichiro Hasuo
CoRR, 2022

Exemplifying parametric timed specifications over signals with bounded behavior.
Étienne André; Masaki Waga; Natsuki Urabe; Ichiro Hasuo
CoRR, 2022

ARCH-COMP 2022 Category Report: Falsification with Ubounded Resources
Gidon Ernst; Paolo Arcaini; Georgios Fainekos; Federico Formica; Jun Inoue; Tanmay Khandait; Mohammad Mahdi Mahboob; Claudio Menghi; Giulia Pedrielli; Masaki Waga; Yoriyuki Yamagata; Zhenya Zhang
EPiC Series in Computing, 13 Dec. 2022, Invited

Model-bounded Monitoring of Hybrid Systems
Masaki Waga; Étienne André; Ichiro Hasuo
ACM Transactions on Cyber-Physical Systems, 31 Oct. 2022, Peer-reviewed, Lead author

Parametric Timed Pattern Matching
Masaki Waga; Étienne André; Ichiro Hasuo
ACM Transactions on Software Engineering and Methodology, 31 Jan. 2023, Peer-reviewed, Lead author

Dynamic Shielding for Reinforcement Learning in Black-Box Environments.
Masaki Waga; Ezequiel Castellano; Sasinee Pruekprasert; Stefan Klikovits; Toru Takisaka; Ichiro Hasuo
International Symposium on Automated Technology for Verification and Analysis, 21 Oct. 2022, Peer-reviewed, Lead author

Exemplifying parametric timed specifications over signals with bounded behavior.
Étienne André; Masaki Waga; Natsuki Urabe; Ichiro Hasuo
NASA Formal Methods Symposium, 20 May 2022, Peer-reviewed

Oblivious Online Monitoring for Safety LTL Specification via Fully Homomorphic Encryption.
Ryotaro Banno; Kotaro Matsuoka; Naoki Matsumoto; Song Bian; Masaki Waga; Kohei Suenaga
34th International Conference on Computer-Aided Verification, 07 Aug. 2022, Peer-reviewed

ARCH-COMP 2021 Category Report: Falsification with Validation of Results.
Gidon Ernst; Paolo Arcaini; Ismail Bennani; Aniruddh Chandratre; Alexandre Donzé; Georgios Fainekos; Goran Frehse; Khouloud Gaaloul; Jun Inoue 0001; Tanmay Khandait; Logan Mathesen; Claudio Menghi; Giulia Pedrielli; Marc Pouzet; Masaki Waga; Shakiba Yaghoubi; Yoriyuki Yamagata; Zhenya Zhang
ARCH@ADHS, 06 Dec. 2021

Hybrid System Falsification for Multiple-Constraint Parameter Synthesis: a Gas Turbine Case Study.
Sota Sato; Atsuyoshi Saimen; Masaki Waga; Kenji Takao; Ichiro Hasuo
24th International Symposium on Formal Methods, 10 Nov. 2021, Peer-reviewed

Efficient Black-Box Checking via Model Checking with Strengthened Specifications
Junya Shijubo; Masaki Waga; Kohei Suenaga
The 21st International Conference on Runtime Verification, 06 Oct. 2021, Peer-reviewed

完全準同型暗号を用いた秘匿LTLオンラインモニタリング
伴野良太郎; 松岡航太郎; 松本直樹; Bian Song; 和賀正樹; 末永幸平
コンピュータセキュリティシンポジウム 2021 (CSS 2021), 19 Oct. 2021

Constrained Optimization for Falsification and Conjunctive Synthesis.
Sota Sato; Masaki Waga; Ichiro Hasuo
6th IFAC Conference on Analysis and Design of Hybrid Systems, 09 Sep. 2021, Peer-reviewed

Model-Bounded Monitoring of Hybrid Systems.
Masaki Waga; Étienne André; Ichiro Hasuo
12th ACM/IEEE International Conference on Cyber-Physical Systems, 19 May 2021, Peer-reviewed, Lead author, Corresponding author

Falsification of cyber-physical systems with robustness-guided black-box checking.
Masaki Waga
HSCC'20: 23rd ACM International Conference on Hybrid Systems: Computation and Control, 2020, Peer-reviewed

Genetic algorithm for the weight maximization problem on weighted automata.
Elena Gutiérrez; Takamasa Okudono; Masaki Waga; Ichiro Hasuo
GECCO'20: Genetic and Evolutionary Computation Conference, 2020, Peer-reviewed

Weighted Automata Extraction from Recurrent Neural Networks via Regression on State Spaces.
Takamasa Okudono; Masaki Waga; Taro Sekiyama; Ichiro Hasuo
The Thirty-Fourth AAAI Conference on Artificial Intelligence, AAAI 2020, The Thirty-Second Innovative Applications of Artificial Intelligence Conference, IAAI 2020, The Tenth AAAI Symposium on Educational Advances in Artificial Intelligence, EAAI 2020, 2020, Peer-reviewed

Moore-machine filtering for timed and untimed pattern matching: poster abstract.
Masaki Waga; Ichiro Hasuo
Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control, 2019

Online Parametric Timed Pattern Matching with Automata-Based Skipping.
Masaki Waga; Étienne André
NASA Formal Methods - 11th International Symposium, 2019, Peer-reviewed

Online Quantitative Timed Pattern Matching with Semiring-Valued Weighted Automata.
Masaki Waga
Formal Modeling and Analysis of Timed Systems - 17th International Conference, 2019, Peer-reviewed

Symbolic Monitoring Against Specifications Parametric in Time and Data.
Masaki Waga; Étienne André; Ichiro Hasuo
Computer Aided Verification - 31st International Conference, Part I, 2019, Peer-reviewed

Moore-Machine Filtering for Timed and Untimed Pattern Matching."
Masaki Waga; Ichiro Hasuo
IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2018, Peer-reviewed

Offline Timed Pattern Matching under Uncertainty.
Étienne André; Ichiro Hasuo; Masaki Waga
23rd International Conference on Engineering of Complex Computer Systems, 2018, Peer-reviewed

MONAA: A Tool for Timed Pattern Matching with Automata-Based Acceleration.
Masaki Waga; Ichiro Hasuo; Kohei Suenaga
3rd Workshop on Monitoring and Testing of Cyber-Physical Systems, 2018, Peer-reviewed

Efficient Online Timed Pattern Matching by Automata-Based Skipping.
Masaki Waga; Ichiro Hasuo; Kohei Suenaga
Formal Modeling and Analysis of Timed Systems - 15th International Conference, 2017, Peer-reviewed

A Boyer-Moore Type Algorithm for Timed Pattern Matching.
Masaki Waga; Takumi Akazaki; Ichiro Hasuo
Formal Modeling and Analysis of Timed Systems - 14th International Conference, 2016, Peer-reviewed, Lead author

Presentations

FalCAuN − CPS Testing with Automata Learning
Masaki Waga
The 24th International Conference on Runtime Verification, 16 Oct. 2024

Oblivious Monitoring for Discrete-Time STL via Fully Homomorphic Encryption
Masaki Waga
The 24th International Conference on Runtime Verification (RV 2024), 15 Oct. 2024

Hyper parametric timed CTL
Masaki Waga
International Conference on Embedded Software (EMSOFT 2024), 02 Oct. 2024

Active Learning of Deterministic Timed Automata with Myhill-Nerode Style Characterization
Masaki Waga
35th International Conference on Computer Aided Verification, 22 Jul. 2023

Active Learning of Deterministic Timed Automata with Myhill-Nerode Style Characterization
Masaki Waga
International Conference on Formal Modeling and Analysis of Timed Systems, 21 Sep. 2023, Invited

信頼されるAI-CPSのためのオートマトン学習によるアプローチ
和賀正樹
人工知能学会第125回人工知能基本問題研究会(SIG-FPAI), 29 Aug. 2023, Invited

Dynamic Shielding for Reinforcement Learning in Black-Box Environments
Masaki Waga
International Symposium on Automated Technology for Verification and Analysis, 26 Oct. 2022

Parametric Timed Pattern Matching.
Masaki Waga
ソフトウェアエンジニアリングシンポジウム 2022 (SES 2022), 06 Sep. 2022, Invited

Model-Bounded Monitoring of Hybrid Systems.
Masaki Waga
12th ACM/IEEE International Conference on Cyber-Physical Systems, 20 May 2021

Model-Bounded Monitoring of Hybrid Systems.
Masaki Waga
6th Workshop on Monitoring and Testing of Cyber-Physical Systems, 18 May 2021

Online Quantitative Timed Pattern Matching with Semiring-Valued Weighted Automata
Masaki Waga
YR-OWLS (Online Worldwide Seminar on Logic and Semantics), 12 May 2021, Invited

物理情報システムに対するブラックボックス検査の構文的仕様強化による最適化
四十坊純也
第 23 回プログラミングおよびプログラミング言語ワークショップ (PPL 2021), 10 Mar. 2021

Symbolic Monitoring against Specifications Parametric in Time and Data
和賀正樹
日本ソフトウェア科学会第 37 回大会, 10 Sep. 2020, Invited

Falsification of cyber-physical systems with robustness-guided black-box checking
Masaki Waga
23rd ACM International Conference on Hybrid Systems: Computation and Control, Apr. 2020

Symbolic Monitoring Against Specifications Parametric in Time and Data
Masaki Waga
5th Workshop on Monitoring and Testing of Cyber-Physical Systems

Industrial Property Rights

US 2023/0333546 A1, Monitoring device and monitoring method
Masaki Waga; Etienne Andre; Ichiro Hasuo

特願 2024-007664, ブラックボックスシステムのテストのためのコンピュータ実装方法及びコンピュータシステム
Amit Gurung; 和賀正樹; 末永幸平

特開2023-69054, 特願 2021-180647, 情報処理装置、情報処理方法および情報処理プログラム
菊池淳; 和賀正樹; 末永幸平

特願 2020-215603, モニタリング装置及びモニタリング方法
和賀正樹; エティエンヌアンドレ; 蓮尾一郎

US 11537415B2, US 11537415, US 11537415, Information processing apparatus, information processing circuit, information processing system, and information processing method
Masaki Waga; Ichiro Hasuo

特許第7464268号, 特開 2021-170192, 特願 2020-072577, オートマトン生成装置、オートマトン生成方法及びプログラム
和賀正樹

特許第7383273号, 特開 2020-57362, 特願 2019-129643, 情報処理装置、情報処理回路、情報処理システム及び情報処理方法
和賀正樹; 蓮尾一郎

Works

FalCAuN

Awards

01 Oct. 2024
Best Poster and Tool Showcase Award(国際会議The 24th International Conference on Runtime Verification)

01 Oct. 2024
Best Poster and Tool Showcase Award(国際会議The 24th International Conference on Runtime Verification)

2018
ICECCS 2018, Best paper award

2019
FORMATS 2019, Oded Maler award for the best paper

26 Sep. 2019
National Institute of Informatics, Best Student Award

28 Sep. 2020
The Graduate University for Advanced Studies (SOKENDAI), Dean Award, School of Multidisciplinary Sciences

External funds: Kakenhi

オートマトン的技法を用いた、物理情報システムのための軽量形式検証の量的発展
Grant-in-Aid for Early-Career Scientists
Basic Section 60050:Software-related
Kyoto University
和賀正樹
From 01 Apr. 2022, To 31 Mar. 2025, Granted
能動的MDP学習;確率的モデル検査;ブラックボックス検査;準同型暗号;秘匿モニタリング;物理情報システム;軽量形式手法;オートマトン理論;量的検証
https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-22K17873/

External funds: others

品質保証と説明の両立による信頼できる AI の構築技術
科学技術振興機構, PRESTO
From 01 Oct. 2022, To 01 Mar. 2026
Masaki Waga

近似的数理モデルによる CPS の動的安全機構
科学技術振興機構 (JST) ACT-X
From 01 Nov. 2020, To 31 Mar. 2022
和賀正樹

Last Updated :2025/05/12

Education

Teaching subject(s)

From 01 Apr. 2024, To 31 Mar. 2025
Computer Science Laboratory and Exercise 2
9022, Fall, Faculty of Engineering, 2

From 01 Apr. 2024, To 31 Mar. 2025
System Verification
3666, Fall, Graduate School of Informatics, 2

From 01 Apr. 2024, To 31 Mar. 2025
Computer Science Laboratory and Exercise 3
9084, Spring, Faculty of Engineering, 4

From 01 Apr. 2023, To 31 Mar. 2024
Computer Science Laboratory and Exercise 2
9022, Fall, Faculty of Engineering, 2

From 01 Apr. 2023, To 31 Mar. 2024
System Verification
3666, Fall, Graduate School of Informatics, 2

From 01 Apr. 2023, To 31 Mar. 2024
Computer Science Laboratory and Exercise 3
9084, Spring, Faculty of Engineering, 4

From 01 Apr. 2022, To 31 Mar. 2023
Computer Science Laboratory and Exercise 3
9084, Spring, Faculty of Engineering, 4

From 01 Apr. 2022, To 31 Mar. 2023
System Verification
3666, Fall, Graduate School of Informatics, 2

From Apr. 2021, To Mar. 2022
Computer Science Laboratory and Exercise 2
Fall, 工学部

From Apr. 2021, To Mar. 2022
Computer Science Laboratory and Exercise 3
Spring, 工学部

ページ上部へ戻る