和賀正樹(情報学研究科情報学専攻コンピュータ工学講座) | 京都大学教育研究活動データベース

和賀正樹

ワガマサキ

情報学研究科情報学専攻コンピュータ工学講座助教

Last Updated :2025/05/12

基本情報

学部兼担

工学部

学位

修士（情報理工学）(東京大学)

博士（情報学）(総合研究大学院大学)

出身大学院・研究科等

総合研究大学院大学, 複合科学研究科情報学専攻博士課程（３年次編入）, 修了

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

出身学校・専攻等

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

出身高等学校

出身高等学校
開成高校, かいせいこうこう

経歴

自 2023年09月, 至 2023年09月
University Sorbonne Paris Nord, LIPN, Visiting academic fellow/professor

自 2021年04月, 至現在
国立情報学研究所, 客員助教 (研究開発連携)

自 2020年10月, 至現在
京都大学, 大学院情報学研究科, 助教

自 2018年04月, 至 2020年09月
独立行政法人日本学術振興会, 特別研究員 (DC1)

自 2017年04月, 至 2020年09月
国立情報学研究所, アーキテクチャ科学研究系, リサーチアシスタント

使用言語

英語

日本語

ID,URL

ORCID ID
0000-0001-9360-7490
J-Global ID
202001014513731091
研究者番号
00899007
外部リンク
https://www.fos.kuis.kyoto-u.ac.jp/~mwaga/

researchmap URL

https://researchmap.jp/mwaga

Last Updated :2025/05/12

研究

研究テーマ・研究概要

研究テーマ
形式検証手法

研究キーワード

形式手法

オートマトン学習

実行時検証

モデル検査

時間オートマトン

研究分野

情報通信, ソフトウェア

論文

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
2022年03月

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

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, 2024年11月

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年
この論文にアクセスする：

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年, 招待有り

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, 2023年10月

Learning Nonlinear Hybrid Automata from Input-Output Time-Series Data.
Amit Gurung; Masaki Waga; Kohei Suenaga
ATVA (1), 2023年, 査読有り

Efficient Online Timed Pattern Matching by Automata-Based Skipping
Masaki Waga; Ichiro Hasuo; Kohei Suenaga
FORMATS 2017, 2017年, 査読有り

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, 2023年07月, 査読有り, 筆頭著者, 最終著者, 責任著者
この論文にアクセスする：

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, 2022年12月13日, 招待有り

Model-bounded Monitoring of Hybrid Systems
Masaki Waga; Étienne André; Ichiro Hasuo
ACM Transactions on Cyber-Physical Systems, 2022年10月31日, 査読有り, 筆頭著者

Parametric Timed Pattern Matching
Masaki Waga; Étienne André; Ichiro Hasuo
ACM Transactions on Software Engineering and Methodology, 2023年01月31日, 査読有り, 筆頭著者

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, 2022年10月21日, 査読有り, 筆頭著者

Exemplifying parametric timed specifications over signals with bounded behavior.
Étienne André; Masaki Waga; Natsuki Urabe; Ichiro Hasuo
NASA Formal Methods Symposium, 2022年05月20日, 査読有り

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, 2022年08月07日, 査読有り

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, 2021年12月06日

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, 2021年11月10日, 査読有り

Efficient Black-Box Checking via Model Checking with Strengthened Specifications
Junya Shijubo; Masaki Waga; Kohei Suenaga
The 21st International Conference on Runtime Verification, 2021年10月06日, 査読有り

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

Constrained Optimization for Falsification and Conjunctive Synthesis.
Sota Sato; Masaki Waga; Ichiro Hasuo
6th IFAC Conference on Analysis and Design of Hybrid Systems, 2021年09月09日, 査読有り

Model-Bounded Monitoring of Hybrid Systems.
Masaki Waga; Étienne André; Ichiro Hasuo
12th ACM/IEEE International Conference on Cyber-Physical Systems, 2021年05月19日, 査読有り, 筆頭著者, 責任著者

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年, 査読有り

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年, 査読有り

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年, 査読有り

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年, 査読有り

Online Quantitative Timed Pattern Matching with Semiring-Valued Weighted Automata.
Masaki Waga
Formal Modeling and Analysis of Timed Systems - 17th International Conference, 2019年, 査読有り

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

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年, 査読有り

Offline Timed Pattern Matching under Uncertainty.
Étienne André; Ichiro Hasuo; Masaki Waga
23rd International Conference on Engineering of Complex Computer Systems, 2018年, 査読有り

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年, 査読有り

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年, 査読有り

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年, 査読有り, 筆頭著者

講演・口頭発表等

FalCAuN − CPS Testing with Automata Learning
Masaki Waga
The 24th International Conference on Runtime Verification, 2024年10月16日

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

Hyper parametric timed CTL
Masaki Waga
International Conference on Embedded Software (EMSOFT 2024), 2024年10月02日

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

Active Learning of Deterministic Timed Automata with Myhill-Nerode Style Characterization
Masaki Waga
International Conference on Formal Modeling and Analysis of Timed Systems, 2023年09月21日, 招待有り

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

Dynamic Shielding for Reinforcement Learning in Black-Box Environments
Masaki Waga
International Symposium on Automated Technology for Verification and Analysis, 2022年10月26日

Parametric Timed Pattern Matching.
Masaki Waga
ソフトウェアエンジニアリングシンポジウム 2022 (SES 2022), 2022年09月06日, 招待有り

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

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

Online Quantitative Timed Pattern Matching with Semiring-Valued Weighted Automata
Masaki Waga
YR-OWLS (Online Worldwide Seminar on Logic and Semantics), 2021年05月12日, 招待有り

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

Symbolic Monitoring against Specifications Parametric in Time and Data
和賀正樹
日本ソフトウェア科学会第 37 回大会, 2020年09月10日, 招待有り

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

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

産業財産権

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

受賞

2024年10月01日
Best Poster and Tool Showcase Award(国際会議The 24th International Conference on Runtime Verification)

2024年10月01日
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

2019年09月26日
国立情報学研究所, 優秀学生賞

2020年09月28日
総合研究大学院大学, 複合科学研究科長賞

外部資金：科学研究費補助金

オートマトン的技法を用いた、物理情報システムのための軽量形式検証の量的発展
若手研究
小区分60050:ソフトウェア関連
京都大学
和賀正樹
自 2022年04月01日, 至 2025年03月31日, 交付
能動的MDP学習;確率的モデル検査;ブラックボックス検査;準同型暗号;秘匿モニタリング;物理情報システム;軽量形式手法;オートマトン理論;量的検証
https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-22K17873/

外部資金：その他

品質保証と説明の両立による信頼できる AI の構築技術
科学技術振興機構, さきがけ
自 2022年10月01日, 至 2026年03月01日
和賀正樹

近似的数理モデルによる CPS の動的安全機構
科学技術振興機構 (JST) ACT-X
自 2020年11月01日, 至 2022年03月31日
和賀正樹

Last Updated :2025/05/12

教育

担当科目

自 2024年04月01日, 至 2025年03月31日
計算機科学実験及演習２
9022, 後期, 工学部, 2

自 2024年04月01日, 至 2025年03月31日
システム検証論
3666, 後期, 情報学研究科, 2

自 2024年04月01日, 至 2025年03月31日
計算機科学実験及演習３
9084, 前期, 工学部, 4

自 2023年04月01日, 至 2024年03月31日
計算機科学実験及演習２
9022, 後期, 工学部, 2

自 2023年04月01日, 至 2024年03月31日
システム検証論
3666, 後期, 情報学研究科, 2

自 2023年04月01日, 至 2024年03月31日
計算機科学実験及演習３
9084, 前期, 工学部, 4

自 2022年04月01日, 至 2023年03月31日
計算機科学実験及演習３
9084, 前期, 工学部, 4

自 2022年04月01日, 至 2023年03月31日
システム検証論
3666, 後期, 情報学研究科, 2

自 2021年04月, 至 2022年03月
計算機科学実験及演習２（計算機）
後期, 工学部

自 2021年04月, 至 2022年03月
計算機科学実験及演習３（計算機）
前期, 工学部

ページ上部へ戻る