README.md

MONAA --- A Tool for Timed Patten Matching with Automata-Based Acceleration

This is the source code repository for MONAA --- A Tool for Timed Patten Matching with Automata-Based Acceleration.

Demo on Google Colab is available!!

Usage

Synopsis

monaa [OPTIONS] PATTERN [FILE]
monaa [OPTIONS] -e PATTERN [FILE]
monaa [OPTIONS] -f FILE [FILE]

Options

-h, --help Print a help message.
-q, --quiet Quiet mode. Causes any results to be suppressed.
-a, --ascii Ascii mode. (default)
-b, --binary Binary mode.
-V, --version Print the version
-E, --event Event mode (default)
-S, --signal Signal mode
-i file, --input file Read a timed word from file.
-f file, --automaton file Read a timed automaton from file.
-e pattern, --expression pattern Specify a pattern by a timed regular expression.

Installation

MONAA is tested on Arch Linux, Ubuntu (20.04, 22.04, 24.04), and macOS (12 Monterey, 13 Ventura, 14 Sonoma). We also provide a docker image.

Requirements

• C++ compiler supporting C++20 and the corresponding libraries.
• Boost (>= 1.59)
• Eigen
• CMake (>= 3.30)
• Bison (>= 3.0)
• Flex

Instructions

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

Usage of the docker image

Note: Docker support is experimental. It seems this image does not work with Docker Desktop for macOS.

You can use monaa via docker by docker run -it maswag/monaa ... instead of monaa .... The following shows an example.

docker run -v $PWD:/mnt -it maswag/monaa -f /mnt/examples/small.dot -i /mnt/examples/small.txt

Examples

See Getting Started for an example usage.

Syntax of Timed Automata

You can use DOT language to represent a timed automaton. For the timing constraints and other information, you can use the following custom attributes.

	attribute	value	description
vertex	init	0 or 1	init=1 if the state is initial
vertex	match	0 or 1	match=1 if the state is accepting
edge	label	[a-z], [A-Z]	the value represents the event on the transition
edge	reset	a list of integers	the set of variables reset after the transition
edge	guard	a list of inequality constraints	the guard of the transition

Syntax of Timed Regular Expressions

expr : c (An event)
     | ( expr ) (Grouping)
     | expr + (Kleene Plus)
     | expr * (Kleene Star)
     | expr expr (Concatenation)
     | expr | expr (Disjunction)
     | expr & expr (Conjunction)
     | expr % (s,t) | expr % [s,t) | expr % (s,t] | expr % [s,t] | expr % (>s) | expr % (>=s) | expr % (<t) | expr % (<=t) | expr % (=t) (Time Restriction)

Related Tool

• TimeTrace: A web frontend of MONAA
  • GitHub: https://github.com/JonasGLund99/TimeTrace

References

• A Boyer-Moore Type Algorithm for Timed Pattern Matching. Masaki Waga, Takumi Akazaki, and Ichiro Hasuo
• Efficient Online Timed Pattern Matching by Automata-Based Skipping. Masaki Waga, Ichiro Hasuo, and Kohei Suenaga
• MONAA: a Tool for Timed Patten Matching with Automata-Based Acceleration. Masaki Waga, Ichiro Hasuo, and Kohei Suenaga