37 citations · 164 across the 31 of their papers we have counts for
35 papers
Specification-Guided Path Shortcutting for Efficient Probabilistic Model Checking
Tsubasa Matsumoto, Kazuki Watanabe, Masaki Waga
Given the safety-critical nature of many embedded systems, their safety assurance is essential. Because such systems are typically stochastic, probabilistic model checking is a par…
Learning Alternating Real-Time Automata
Kazuki Kinoshita, Masaki Waga
We present the AL*RTA algorithm for learning alternating real-time automata (ARTAs) using membership and equivalence queries. AL*RTA combines ideas from AL*for learning alternating…
A Case Study on Runtime Verification of a Continuous Deployment Process
Shoma Ansai, Masaki Waga
We report our experience in applying runtime monitoring to a FluxCD-based continuous deployment (CD) process. Our target system consists of GitHub Actions, GitHub Container Registr…
SoftMatcha 2: A Fast and Soft Pattern Matcher for Trillion-Scale Corpora
Masataka Yoneda, Yusuke Matsushita, Go Kamoda +4
We present SoftMatcha 2, an ultra-fast and flexible search algorithm that enables search over trillion-scale natural language corpora in under 0.3 seconds while allowing semantic v…
A Variety of Request-Response Specifications
Daichi Aiba, Masaki Waga, Hiroya Fujinami +6
We find, motivated by real-world applications, that the well-known request-response specification comes with multiple variations, and that these variations should be distinguished.…
Active Learning of Symbolic Mealy Automata
Kengo Irie, Masaki Waga, Kohei Suenaga
We propose -an active learning algorithm that learns symbolic Mealy automata, which support infinite input alphabets and multiple output characters. Each of these two featur…
Componentwise Automata Learning for System Integration (Extended Version)
Hiroya Fujinami, Masaki Waga, Jie An +4
Compositional automata learning is attracting attention as an analysis technique for complex black-box systems. It exploits a target system's internal compositional structure to re…
Hyper pattern matching
Masaki Waga, Étienne André
In runtime verification, pattern matching, which searches for occurrences of a specific pattern within a word, provides more information than a simple violation detection of the mo…
SoftMatcha: A Soft and Fast Pattern Matcher for Billion-Scale Corpus Searches
Hiroyuki Deguchi, Go Kamoda, Yusuke Matsushita +4
Researchers and practitioners in natural language processing and computational linguistics frequently observe and analyze the real language usage in large-scale corpora. For that p…
Certifying Lyapunov Stability of Black-Box Nonlinear Systems via Counterexample Guided Synthesis (Extended Version)
Chiao Hsieh, Masaki Waga, Kohei Suenaga
Finding Lyapunov functions to certify the stability of control systems has been an important topic for verifying safety-critical systems. Most existing methods on finding Lyapunov…
Hyper parametric timed CTL
Masaki Waga, Étienne André
Hyperproperties enable simultaneous reasoning about multiple execution traces of a system and are useful to reason about non-interference, opacity, robustness, fairness, observatio…
Learning Weighted Finite Automata over the Max-Plus Semiring and its Termination
Takamasa Okudono, Masaki Waga, Taro Sekiyama +1
Active learning of finite automata has been vigorously pursued for the purposes of analysis and explanation of black-box systems. In this paper, we study an L*-style learning algor…
Oblivious Monitoring for Discrete-Time STL via Fully Homomorphic Encryption
Masaki Waga, Kotaro Matsuoka, Takashi Suwa +4
When monitoring a cyber-physical system (CPS) from a remote server, keeping the monitored data secret is crucial, particularly when they contain sensitive information, e.g., biolog…
Temporal Logic Formalisation of ISO 34502 Critical Scenarios: Modular Construction with the RSS Safety Distance
Jesse Reimann, Nico Mansion, James Haydon +8
As the development of autonomous vehicles progresses, efficient safety assurance methods become increasingly necessary. Safety assurance methods such as monitoring and scenario-bas…
Probabilistic Black-Box Checking via Active MDP Learning
Junya Shijubo, Masaki Waga, Kohei Suenaga
We introduce a novel methodology for testing stochastic black-box systems, frequently encountered in embedded systems. Our approach enhances the established black-box checking (BBC…
Active Learning of Deterministic Timed Automata with Myhill-Nerode Style Characterization
Masaki Waga
We present an algorithm to learn a deterministic timed automaton (DTA) via membership and equivalence queries. Our algorithm is an extension of the L* algorithm with a Myhill-Nerod…
Learning nonlinear hybrid automata from input--output time-series data
Amit Gurung, Masaki Waga, Kohei Suenaga
Learning an automaton that approximates the behavior of a black-box system is a long-studied problem. Besides its theoretical significance, its application to search-based testing…
BOREx: Bayesian-Optimization--Based Refinement of Saliency Map for Image- and Video-Classification Models
Atsushi Kikuchi, Kotaro Uchida, Masaki Waga +1
Explaining a classification result produced by an image- and video-classification model is one of the important but challenging issues in computer vision. Many methods have been pr…
Dynamic Shielding for Reinforcement Learning in Black-Box Environments
Masaki Waga, Ezequiel Castellano, Sasinee Pruekprasert +3
It is challenging to use reinforcement learning (RL) in cyber-physical systems due to the lack of safety guarantees during learning. Although there have been various proposals to r…
Oblivious Online Monitoring for Safety LTL Specification via Fully Homomorphic Encryption
Ryotaro Banno, Kotaro Matsuoka, Naoki Matsumoto +3
In many Internet of Things (IoT) applications, data sensed by an IoT device are continuously sent to the server and monitored against a specification. Since the data often contain…
Exemplifying parametric timed specifications over signals with bounded behavior
Étienne André, Masaki Waga, Natsuki Urabe +1
Specifying properties can be challenging work. In this paper, we propose an automated approach to exemplify properties given in the form of automata extended with timing constraint…
Efficient Black-Box Checking via Model Checking with Strengthened Specifications
Junya Shijubo, Masaki Waga, Kohei Suenaga
Black-box checking (BBC)} is a testing method for cyber-physical systems (CPSs) as well as software systems. BBC consists of active automata learning and model checking; a Mealy ma…
Model-bounded monitoring of hybrid systems
Masaki Waga, Étienne André, Ichiro Hasuo
Monitoring of hybrid systems attracts both scientific and practical attention. However, monitoring algorithms suffer from the methodological difficulty of only observing sampled di…
Constrained Optimization for Hybrid System Falsification and Application to Conjunctive Synthesis
Sota Sato, Masaki Waga, Ichiro Hasuo
The synthesis problem of a cyber-physical system (CPS) is to find an input signal under which the system's behavior satisfies a given specification. Our setting is that the specifi…