arXiv subjects

Masaki Waga

Publications and source records attributed to Masaki Waga.

35 records · Page 2Linked to original sources

arXiv2023

Active Learning of Deterministic Timed Automata with Myhill-Nerode Style Characterization

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-Nerode style characterization of recognizable timed languages, which is the class of timed languages recognizable by DTAs. We first characterize the recognizable timed languages with a Nerode-style congruence. Using it, we give an algorithm with a smart teacher answering symbolic membership queries in addition to membership and equivalence queries. With a symbolic membership query, one can ask the membership of a certain set of timed words at one time. We prove that for any recognizable timed language, our learning algorithm returns a DTA recognizing it. We show how to answer a symbolic membership query with finitely many membership queries. We also show that our learning algorithm requires a polynomial number of queries with a smart teacher and an exponential number of queries with a normal teacher. We applied our algorithm to various benchmarks and confirmed its effectiveness with a normal teacher.

cs.FL↗

arXiv2022

BOREx: Bayesian-Optimization--Based Refinement of Saliency Map for Image- and Video-Classification Models

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 proposed for producing heat-map--based explanations for this purpose, including ones based on the white-box approach that uses the internal information of a model (e.g., LRP, Grad-CAM, and Grad-CAM++) and ones based on the black-box approach that does not use any internal information (e.g., LIME, SHAP, and RISE). We propose a new black-box method BOREx (Bayesian Optimization for Refinement of visual model Explanation) to refine a heat map produced by any method. Our observation is that a heat-map--based explanation can be seen as a prior for an explanation method based on Bayesian optimization. Based on this observation, BOREx conducts Gaussian process regression (GPR) to estimate the saliency of each pixel in a given image starting from the one produced by another explanation method. Our experiments statistically demonstrate that the refinement by BOREx improves low-quality heat maps for image- and video-classification results.

cs.CV↗

arXiv2022

Dynamic Shielding for Reinforcement Learning in Black-Box Environments

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 reduce undesired behaviors during learning, most of these techniques require prior system knowledge, and their applicability is limited. This paper aims to reduce undesired behaviors during learning without requiring any prior system knowledge. We propose dynamic shielding: an extension of a model-based safe RL technique called shielding using automata learning. The dynamic shielding technique constructs an approximate system model in parallel with RL using a variant of the RPNI algorithm and suppresses undesired explorations due to the shield constructed from the learned model. Through this combination, potentially unsafe actions can be foreseen before the agent experiences them. Experiments show that our dynamic shield significantly decreases the number of undesired events during training.

cs.LG↗

arXiv2022

Oblivious Online Monitoring for Safety LTL Specification via Fully Homomorphic Encryption

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 sensitive information, and the monitored specification is usually proprietary, both must be kept private from the other end. We propose a protocol to conduct oblivious online monitoring -- online monitoring conducted without revealing the private information of each party to the other -- against a safety LTL specification. In our protocol, we first convert a safety LTL formula into a DFA and conduct online monitoring with the DFA. Based on fully homomorphic encryption (FHE), we propose two online algorithms (Reverse and Block) to run a DFA obliviously. We prove the correctness and security of our entire protocol. We also show the scalability of our algorithms theoretically and empirically. Our case study shows that our algorithms are fast enough to monitor blood glucose levels online, demonstrating our protocol's practical relevance.

cs.CR↗

arXiv2022

Exemplifying parametric timed specifications over signals with bounded behavior

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 constraints and timing parameters, and that can also encode constraints over real-valued signals. That is, given such a specification and given an admissible automaton for each signal, we output concrete runs exemplifying real (or impossible) runs for this specification. Specifically, our method takes as input a specification, and a set of admissible behaviors, all given as a subclass of rectangular hybrid automata, namely timed automata extended with arbitrary clock rates, signal constraints, and timing parameters. Our method then generates concrete runs exemplifying the specification.

cs.FL↗

arXiv2021

Falsification of Cyber-Physical Systems with Robustness-Guided Black-Box Checking

For exhaustive formal verification, industrial-scale cyber-physical systems (CPSs) are often too large and complex, and lightweight alternatives (e.g., monitoring and testing) have attracted the attention of both industrial practitioners and academic researchers. Falsification is one popular testing method of CPSs utilizing stochastic optimization. In state-of-the-art falsification methods, the result of the previous falsification trials is discarded, and we always try to falsify without any prior knowledge. To concisely memorize such prior information on the CPS model and exploit it, we employ Black-box checking (BBC), which is a combination of automata learning and model checking. Moreover, we enhance BBC using the robust semantics of STL formulas, which is the essential gadget in falsification. Our experiment results suggest that our robustness-guided BBC outperforms a state-of-the-art falsification tool.

cs.LO↗

arXiv2021

Efficient Black-Box Checking via Model Checking with Strengthened Specifications

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 machine is learned from the system under test (SUT), and the learned Mealy machine is verified against a specification using model checking. When the Mealy machine violates the specification, the model checker returns an input witnessing the specification violation of the Mealy machine. We use it to refine the Mealy machine or conclude that the SUT violates the specification. Otherwise, we conduct equivalence testing to find an input witnessing the difference between the Mealy machine and the SUT. In the BBC for CPSs, equivalence testing tends to be time-consuming due to the time for the system execution. In this paper, we enhance the BBC utilizing model checking with strengthened specifications. By model checking with a strengthened specification, we have more chance to obtain an input witnessing the specification violation than model checking with the original specification. The refinement of the Mealy machine with such an input tends to reduce the number of equivalence testing, which improves the efficiency. We conducted experiments with an automotive benchmark. Our experiment results demonstrate the merit of our method.

cs.LO↗

arXiv2021

Constrained Optimization for Hybrid System Falsification and Application to Conjunctive Synthesis

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 specification is a formula of signal temporal logic, and furthermore, that the specification is a conjunction of different and often conflicting requirements. Conjunctive specifications are often challenging for optimization-based falsification -- an established method for CPS analysis that can also be used for synthesis -- since the usual framework (especially how its robust semantics handles Boolean connectives) is not suited for finding delicate trade-offs between different requirements. Our proposed method consists of the combination of optimization-based falsification and constrained optimization. Specifically, we show that the state-of-the-art multiple constraint ranking method can be combined with falsification powered by CMA-ES optimization; its performance advantage is demonstrated in experiments.

eess.SY↗

arXiv2020

Genetic Algorithm for the Weight Maximization Problem on Weighted Automata

The weight maximization problem (WMP) is the problem of finding the word of highest weight on a weighted finite state automaton (WFA). It is an essential question that emerges in many optimization problems in automata theory. Unfortunately, the general problem can be shown to be undecidable, whereas its bounded decisional version is NP-complete. Designing efficient algorithms that produce approximate solutions to the WMP in reasonable time is an appealing research direction that can lead to several new applications including formal verification of systems abstracted as WFAs. In particular, in combination with a recent procedure that translates a recurrent neural network into a weighted automaton, an algorithm for the WMP can be used to analyze and verify the network by exploiting the simpler and more compact automata model. In this work, we propose, implement and evaluate a metaheuristic based on genetic algorithms to approximate solutions to the WMP. We experimentally evaluate its performance on examples from the literature and show its potential on different applications.

cs.NE↗

arXiv2019

Weighted Automata Extraction from Recurrent Neural Networks via Regression on State Spaces

We present a method to extract a weighted finite automaton (WFA) from a recurrent neural network (RNN). Our algorithm is based on the WFA learning algorithm by Balle and Mohri, which is in turn an extension of Angluin's classic \lstar algorithm. Our technical novelty is in the use of \emph{regression} methods for the so-called equivalence queries, thus exploiting the internal state space of an RNN to prioritize counterexample candidates. This way we achieve a quantitative/weighted extension of the recent work by Weiss, Goldberg and Yahav that extracts DFAs. We experimentally evaluate the accuracy, expressivity and efficiency of the extracted WFAs.

cs.LG↗

arXiv2019

Moore-Machine Filtering for Timed and Untimed Pattern Matching

Monitoring is an important body of techniques in runtime verification of real-time, embedded, and cyber-physical systems. Mathematically, the monitoring problem can be formalized as a pattern matching problem against a pattern automaton. Motivated by the needs in embedded applications---especially the limited channel capacity between a sensor unit and a processor that monitors---we pursue the idea of filtering as preprocessing for monitoring. Technically, for a given pattern automaton, we present a construction of a Moore machine that works as a filter. The construction is automata-theoretic, and we find the use of Moore machines particularly suited for embedded applications, not only because their sequential operation is relatively cheap but also because they are amenable to hardware acceleration by dedicated circuits. We prove soundness (i.e., absence of lost matches), too. We work in two settings: in the untimed one, a pattern is an NFA; in the timed one, a pattern is a timed automaton. The extension of our untimed construction to the timed setting is technically involved, but our experiments demonstrate its practical benefits.

cs.FL↗

arXiv2019

Online Quantitative Timed Pattern Matching with Semiring-Valued Weighted Automata

Monitoring of a signal plays an essential role in the runtime verification of cyber-physical systems. Qualitative timed pattern matching is one of the mathematical formulations of monitoring, which gives a Boolean verdict for each sub-signal according to the satisfaction of the given specification. There are two orthogonal directions of extension of the qualitative timed pattern matching. One direction on the result is quantitative: what engineers want is often not a qualitative verdict but the quantitative measurement of the satisfaction of the specification. The other direction on the algorithm is online checking: the monitor returns some verdicts before obtaining the entire signal, which enables to monitor a running system. It is desired from application viewpoints. In this paper, we conduct these two extensions, taking an automata-based approach. This is the first quantitative and online timed pattern matching algorithm to the best of our knowledge. More specifically, we employ what we call timed symbolic weighted automata to specify quantitative specifications to be monitored, and we obtain an online algorithm using the shortest distance of a weighted variant of the zone graph and dynamic programming. Moreover, our problem setting is semiring-based and therefore, general. Our experimental results confirm the scalability of our algorithm for specifications with a time-bound.

cs.FL↗

arXiv2019

Symbolic Monitoring against Specifications Parametric in Time and Data

Monitoring consists in deciding whether a log meets a given specification. In this work, we propose an automata-based formalism to monitor logs in the form of actions associated with time stamps and arbitrarily data values over infinite domains. Our formalism uses both timing parameters and data parameters, and is able to output answers symbolic in these parameters and in the log segments where the property is satisfied or violated. We implemented our approach in an ad-hoc prototype SyMon, and experiments show that its high expressive power still allows for efficient online monitoring.

cs.FL↗

arXiv2018

Offline timed pattern matching under uncertainty

Given a log and a specification, timed pattern matching aims at exhibiting for which start and end dates a specification holds on that log. For example, "a given action is always followed by another action before a given deadline". This problem has strong connections with monitoring real-time systems. We address here timed pattern matching in presence of an uncertain specification, i.e., that may contain timing parameters (e.g., the deadline can be uncertain or unknown). That is, we want to know for which start and end dates, and for what values of the deadline, this property holds. Or what is the minimum or maximum deadline (together with the corresponding start and end dates) for which this property holds. We propose here a framework for timed pattern matching based on parametric timed model checking. In contrast to most parametric timed problems, the solution is effectively computable, and we perform experiments using IMITATOR to show the applicability of our approach.

eess.SY↗

arXiv2018

MONAA: A Tool for Timed Pattern Matching with Automata-Based Acceleration

We present monaa, a monitoring tool over a real-time property specified by either a timed automaton or a timed regular expression. It implements a timed pattern matching algorithm that combines 1) features suited for online monitoring, and 2) acceleration by automata-based skipping. Our experiments demonstrate monaa's performance advantage, especially in online usage.

cs.FL↗

arXiv2017

Efficient Online Timed Pattern Matching by Automata-Based Skipping

The timed pattern matching problem is an actively studied topic because of its relevance in monitoring of real-time systems. There one is given a log $w$ and a specification $\mathcal{A}$ (given by a timed word and a timed automaton in this paper), and one wishes to return the set of intervals for which the log $w$, when restricted to the interval, satisfies the specification $\mathcal{A}$. In our previous work we presented an efficient timed pattern matching algorithm: it adopts a skipping mechanism inspired by the classic Boyer--Moore (BM) string matching algorithm. In this work we tackle the problem of online timed pattern matching, towards embedded applications where it is vital to process a vast amount of incoming data in a timely manner. Specifically, we start with the Franek-Jennings-Smyth (FJS) string matching algorithm---a recent variant of the BM algorithm---and extend it to timed pattern matching. Our experiments indicate the efficiency of our FJS-type algorithm in online and offline timed pattern matching.

cs.FL↗

arXiv2016

A Boyer-Moore Type Algorithm for Timed Pattern Matching

The timed pattern matching problem is formulated by Ulus et al. and has been actively studied since, with its evident application in monitoring real-time systems. The problem takes as input a timed word/signal and a timed pattern (specified either by a timed regular expression or by a timed automaton); and it returns the set of those intervals for which the given timed word, when restricted to the interval, matches the given pattern. We contribute a Boyer-Moore type optimization in timed pattern matching, relying on the classic Boyer-Moore string matching algorithm and its extension to (untimed) pattern matching by Watson and Watson. We assess its effect through experiments; for some problem instances our Boyer-Moore type optimization achieves speed-up by two times, indicating its potential in real-world monitoring tasks where data sets tend to be massive.

cs.FL↗