Quantitative Timed Pattern Matching

This is our experimental implementation of Quantitative Timed Pattern Matching. See FORMATS2019.md for the experiments in our FORMATS 2019 paper.

Demo on Google Colab is HERE!!

Usage

Synopsis

qtpm [OPTIONS] -f FILE [FILE]

Options

-h, --help Print a help message.
-q, --quiet Quiet mode. Causes any results to be suppressed.
-V, --version Print the version
-i file, --input file Read a signal from file.
-f file, --automaton file Read a timed automaton from file.
-a, --abs absolute time mode.
--maxmin Use max-min semiring robust semantics (default).
--minplus Use min-plus semiring robust semantics.
--maxplus Use max-plus semiring robust semantics.
--boolean Use boolean semantics.

Installation

This software is tested on Arch Linux and Mac OSX 10.13.5

Requirements

• C++ compiler supporting C++14 and the corresponding libraries.
• Boost (>= 1.59)
• Eigen
• CMake

Instructions

mkdir build
cd build && cmake -DCMAKE_BUILD_TYPE=Release .. && make && make install

Input Format

Signal

A signal is a sequence of the following line.

 time v(x1) v(x2) v(x3) ... v(xn)

How to make compile_commands.json

mkdir build
cd build && cmake -DCMAKE_EXPORT_COMPILE_COMMANDS=ON ..

Reference

• Masaki Waga, Online Quantitative Timed Pattern Matching with Semiring-Valued Weighted Automata, In Proc. FORMATS 2019, LNCS 11750, pp. 3-22 (Best paper awarded). arXiv version