-
Oblivious Monitoring for Discrete-Time STL via Fully Homomorphic Encryption
Authors:
Masaki Waga,
Kotaro Matsuoka,
Takashi Suwa,
Naoki Matsumoto,
Ryotaro Banno,
Song Bian,
Kohei Suenaga
Abstract:
When monitoring a cyber-physical system (CPS) from a remote server, kee** the monitored data secret is crucial, particularly when they contain sensitive information, e.g., biological or location data. Recently, Banno et al. (CAV'22) proposed a protocol for online LTL monitoring that keeps data concealed from the server using Fully Homomorphic Encryption (FHE). We build on this protocol to allow…
▽ More
When monitoring a cyber-physical system (CPS) from a remote server, kee** the monitored data secret is crucial, particularly when they contain sensitive information, e.g., biological or location data. Recently, Banno et al. (CAV'22) proposed a protocol for online LTL monitoring that keeps data concealed from the server using Fully Homomorphic Encryption (FHE). We build on this protocol to allow arithmetic operations over encrypted values, e.g., to compute a safety measurement combining distance, velocity, and so forth. Overall, our protocol enables oblivious online monitoring of discrete-time real-valued signals against signal temporal logic (STL) formulas. Our protocol combines two FHE schemes, CKKS and TFHE, leveraging their respective strengths. We employ CKKS to evaluate arithmetic predicates in STL formulas while utilizing TFHE to process them using a DFA derived from the STL formula. We conducted case studies on monitoring blood glucose levels and vehicles' behavior against the Responsibility-Sensitive Safety (RSS) rules. Our results suggest the practical relevance of our protocol.
△ Less
Submitted 26 May, 2024;
originally announced May 2024.
-
Temporal Logic Formalisation of ISO 34502 Critical Scenarios: Modular Construction with the RSS Safety Distance
Authors:
Jesse Reimann,
Nico Mansion,
James Haydon,
Benjamin Bray,
Agnishom Chattopadhyay,
Sota Sato,
Masaki Waga,
Étienne André,
Ichiro Hasuo,
Naoki Ueda,
Yosuke Yokoyama
Abstract:
As the development of autonomous vehicles progresses, efficient safety assurance methods become increasingly necessary. Safety assurance methods such as monitoring and scenario-based testing call for formalisation of driving scenarios. In this paper, we develop a temporal-logic formalisation of an important class of critical scenarios in the ISO standard 34502. We use signal temporal logic (STL) a…
▽ More
As the development of autonomous vehicles progresses, efficient safety assurance methods become increasingly necessary. Safety assurance methods such as monitoring and scenario-based testing call for formalisation of driving scenarios. In this paper, we develop a temporal-logic formalisation of an important class of critical scenarios in the ISO standard 34502. We use signal temporal logic (STL) as a logical formalism. Our formalisation has two main features: 1) modular composition of logical formulas for systematic and comprehensive formalisation (following the compositional methodology of ISO 34502); 2) use of the RSS distance for defining danger. We find our formalisation comes with few parameters to tune thanks to the RSS distance. We experimentally evaluated our formalisation; using its results, we discuss the validity of our formalisation and its stability with respect to the choice of some parameter values.
△ Less
Submitted 27 March, 2024;
originally announced March 2024.
-
Probabilistic Black-Box Checking via Active MDP Learning
Authors:
Junya Shijubo,
Masaki Waga,
Kohei Suenaga
Abstract:
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) technique to address stochastic behavior. Traditional BBC primarily involves iteratively identifying an input that breaches the system's specifications by executing the following three phases: the learning phase to con…
▽ More
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) technique to address stochastic behavior. Traditional BBC primarily involves iteratively identifying an input that breaches the system's specifications by executing the following three phases: the learning phase to construct an automaton approximating the black box's behavior, the synthesis phase to identify a candidate counterexample from the learned automaton, and the validation phase to validate the obtained candidate counterexample and the learned automaton against the original black-box system. Our method, ProbBBC, refines the conventional BBC approach by (1) employing an active Markov Decision Process (MDP) learning method during the learning phase, (2) incorporating probabilistic model checking in the synthesis phase, and (3) applying statistical hypothesis testing in the validation phase. ProbBBC uniquely integrates these techniques rather than merely substituting each method in the traditional BBC; for instance, the statistical hypothesis testing and the MDP learning procedure exchange information regarding the black-box system's observation with one another. The experiment results suggest that ProbBBC outperforms an existing method, especially for systems with limited observation.
△ Less
Submitted 15 July, 2023;
originally announced August 2023.
-
Active Learning of Deterministic Timed Automata with Myhill-Nerode Style Characterization
Authors:
Masaki Waga
Abstract:
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 gi…
▽ More
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.
△ Less
Submitted 28 May, 2023;
originally announced May 2023.
-
Learning nonlinear hybrid automata from input--output time-series data
Authors:
Amit Gurung,
Masaki Waga,
Kohei Suenaga
Abstract:
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 and model understanding is recently recognized. We present an algorithm to learn a nonlinear hybrid automaton (HA) that approximates a black-box hybrid system (HS) from a set of input--output traces generated by the HS.…
▽ More
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 and model understanding is recently recognized. We present an algorithm to learn a nonlinear hybrid automaton (HA) that approximates a black-box hybrid system (HS) from a set of input--output traces generated by the HS. Our method is novel in handling (1) both exogenous and endogenous HS and (2) HA with reset associated with each transition. To our knowledge, ours is the first method that achieves both features. We applied our algorithm to various benchmarks and confirmed its effectiveness.
△ Less
Submitted 27 July, 2023; v1 submitted 10 January, 2023;
originally announced January 2023.
-
BOREx: Bayesian-Optimization--Based Refinement of Saliency Map for Image- and Video-Classification Models
Authors:
Atsushi Kikuchi,
Kotaro Uchida,
Masaki Waga,
Kohei Suenaga
Abstract:
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…
▽ More
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.
△ Less
Submitted 31 October, 2022;
originally announced October 2022.
-
Dynamic Shielding for Reinforcement Learning in Black-Box Environments
Authors:
Masaki Waga,
Ezequiel Castellano,
Sasinee Pruekprasert,
Stefan Klikovits,
Toru Takisaka,
Ichiro Hasuo
Abstract:
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…
▽ More
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.
△ Less
Submitted 27 July, 2022;
originally announced July 2022.
-
Oblivious Online Monitoring for Safety LTL Specification via Fully Homomorphic Encryption
Authors:
Ryotaro Banno,
Kotaro Matsuoka,
Naoki Matsumoto,
Song Bian,
Masaki Waga,
Kohei Suenaga
Abstract:
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 wit…
▽ More
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.
△ Less
Submitted 3 June, 2022;
originally announced June 2022.
-
Exemplifying parametric timed specifications over signals with bounded behavior
Authors:
Étienne André,
Masaki Waga,
Natsuki Urabe,
Ichiro Hasuo
Abstract:
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…
▽ More
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.
△ Less
Submitted 24 March, 2022;
originally announced March 2022.
-
Efficient Black-Box Checking via Model Checking with Strengthened Specifications
Authors:
Junya Shijubo,
Masaki Waga,
Kohei Suenaga
Abstract:
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 i…
▽ More
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.
△ Less
Submitted 10 September, 2021;
originally announced September 2021.
-
Model-bounded monitoring of hybrid systems
Authors:
Masaki Waga,
Étienne André,
Ichiro Hasuo
Abstract:
Monitoring of hybrid systems attracts both scientific and practical attention. However, monitoring algorithms suffer from the methodological difficulty of only observing sampled discrete-time signals, while real behaviors are continuous-time signals. To mitigate this problem of sampling uncertainties, we introduce a model-bounded monitoring scheme, where we use prior knowledge about the target sys…
▽ More
Monitoring of hybrid systems attracts both scientific and practical attention. However, monitoring algorithms suffer from the methodological difficulty of only observing sampled discrete-time signals, while real behaviors are continuous-time signals. To mitigate this problem of sampling uncertainties, we introduce a model-bounded monitoring scheme, where we use prior knowledge about the target system to prune interpolation candidates. Technically, we express such prior knowledge by linear hybrid automata (LHAs) - the LHAs are called bounding models. We introduce a novel notion of monitored language of LHAs, and we reduce the monitoring problem to the membership problem of the monitored language. We present two partial algorithms - one is via reduction to reachability in LHAs and the other is a direct one using polyhedra - and show that these methods, and thus the proposed model-bounded monitoring scheme, are efficient and practically relevant.
△ Less
Submitted 15 February, 2021;
originally announced February 2021.
-
Falsification of Cyber-Physical Systems with Robustness-Guided Black-Box Checking
Authors:
Masaki Waga
Abstract:
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 re…
▽ More
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.
△ Less
Submitted 9 November, 2021; v1 submitted 24 April, 2020;
originally announced May 2020.
-
Genetic Algorithm for the Weight Maximization Problem on Weighted Automata
Authors:
Elena Gutiérrez,
Takamasa Okudono,
Masaki Waga,
Ichiro Hasuo
Abstract:
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 approxim…
▽ More
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.
△ Less
Submitted 11 April, 2020;
originally announced April 2020.
-
Online Quantitative Timed Pattern Matching with Semiring-Valued Weighted Automata
Authors:
Masaki Waga
Abstract:
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 dire…
▽ More
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.
△ Less
Submitted 28 June, 2019;
originally announced June 2019.
-
Symbolic Monitoring against Specifications Parametric in Time and Data
Authors:
Masaki Waga,
Étienne André,
Ichiro Hasuo
Abstract:
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 th…
▽ More
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.
△ Less
Submitted 11 May, 2019;
originally announced May 2019.
-
Weighted Automata Extraction from Recurrent Neural Networks via Regression on State Spaces
Authors:
Takamasa Okudono,
Masaki Waga,
Taro Sekiyama,
Ichiro Hasuo
Abstract:
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…
▽ More
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.
△ Less
Submitted 20 November, 2019; v1 submitted 5 April, 2019;
originally announced April 2019.
-
Online Parametric Timed Pattern Matching with Automata-Based Skip**
Authors:
Masaki Waga,
Étienne André
Abstract:
Timed pattern matching has strong connections with monitoring real-time systems. Given a log and a specification containing timing parameters (that can capture uncertain or unknown constants), parametric timed pattern matching aims at exhibiting for which start and end dates, as well as which parameter valuations, a specification holds on that log. This problem is notably close to robustness. We p…
▽ More
Timed pattern matching has strong connections with monitoring real-time systems. Given a log and a specification containing timing parameters (that can capture uncertain or unknown constants), parametric timed pattern matching aims at exhibiting for which start and end dates, as well as which parameter valuations, a specification holds on that log. This problem is notably close to robustness. We propose here a new framework for parametric timed pattern matching. Not only we dramatically improve the efficiency when compared to a previous method based on parametric timed model checking, but we further propose optimizations based on skip**. Our algorithm is suitable for online monitoring, and experiments show that it is fast enough to be applied at runtime.
△ Less
Submitted 18 March, 2019;
originally announced March 2019.
-
Offline timed pattern matching under uncertainty
Authors:
Étienne André,
Ichiro Hasuo,
Masaki Waga
Abstract:
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…
▽ More
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.
△ Less
Submitted 20 December, 2018;
originally announced December 2018.
-
Moore-Machine Filtering for Timed and Untimed Pattern Matching
Authors:
Masaki Waga,
Ichiro Hasuo
Abstract:
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…
▽ More
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.
△ Less
Submitted 11 July, 2019; v1 submitted 22 October, 2018;
originally announced October 2018.
-
MONAA: A Tool for Timed Pattern Matching with Automata-Based Acceleration
Authors:
Masaki Waga,
Ichiro Hasuo,
Kohei Suenaga
Abstract:
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 skip**. Our experiments demonstrate monaa's performance advantage, especially in online usage.
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 skip**. Our experiments demonstrate monaa's performance advantage, especially in online usage.
△ Less
Submitted 22 October, 2018;
originally announced October 2018.
-
Efficient Online Timed Pattern Matching by Automata-Based Skip**
Authors:
Masaki Waga,
Ichiro Hasuo,
Kohei Suenaga
Abstract:
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…
▽ More
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 skip** 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.
△ Less
Submitted 28 June, 2017;
originally announced June 2017.
-
A Boyer-Moore Type Algorithm for Timed Pattern Matching
Authors:
Masaki Waga,
Takumi Akazaki,
Ichiro Hasuo
Abstract:
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…
▽ More
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.
△ Less
Submitted 30 June, 2016; v1 submitted 23 June, 2016;
originally announced June 2016.
