https://github.com/MasWag/monaa

MONAA: a Tool for Timed
Pattern Matching with
Automata-Based Acceleration
Masaki Waga1, Ichiro Hasuo1, and Kohei Suenaga2
National Institute of Informatics1 and Kyoto University2
10 Apr. 2018, MT-CPS 2018
The authors are supported by ERATO HASUO Metamathematics for Systems Design Project (No. JPMJER1603), JST,
Grants-in-Aid No. 15KT0012, JSPS, and JST PRESTO Grant Number JPMJPR15E5, Japan.

1

M. Waga (NII)

Timed Pattern Matching[Ulus et al., FORMATS’14]

Input• Time-series data (Logs of a car/ a robot)
e.g., The gear of a car is high at 0.1s,highlow at 0.3s,…
high
low low
Timed Words
w=t(Sequence of events with timestamps)
0 0.1

•

0.3

0.5

Real-time spec. (Spec. useful for debugging)e.g., The gear of a car changes too frequently
Timed Automata A =[Alur & Dill, TCS’94]

0.7

high, x < 1

start

Output
•

s0

low

s1

s2

$, x < 1s3

low , x < 1

The intervals where the spec. is satisfied in the data
0A) =too{(t,frequentlyt ) | w|(t,t0inL(A)}e.g., The gearM(w,changes0.3s-0.7s) 2
2

M. Waga (NII)MONAA Overview
Command Line Interface (MONAA)
C++ API (libmonaa)
Command line tool for
timed pattern matching• We can inspect a log• The log is read lazily• online monitor• Text-based I/O•

Execute timed patternmatching in a user’scode• Accelerated by
Skipping•[Waga et al., FORMATS’17]•

3

I/O by function/class
M. Waga (NII)Outline
1. Algorithm in MONAA•Skipping for timed pattern matching[Waga et al., FORMATS’17]

2. Frontend of MONAA•

Command line interface (CLI) / C++ API

3. Experiments
4

M. Waga (NII)Skipping for String Matching
STRONG_STRING
STRINGSTRING
Find “STRING”(pattern)⋮from “STRONG_STRING”(target)
STRING

Brute-Force Search

KMP Search

Match until the
3rd char.

[Knuth+, SIAM J. Comput. ’77]
Table for length 3 partial match

S T R I N G✗ * S T R I N✗ * * S T R I✔ * * * S T R
5

STRONG_STRING
STRINGSTRING
Skip 2 trials!!
STRINGSTRING⋮STRING
M. Waga (NII)Brute-Force Algorithm forTimed Pattern Matching
high, x < 1

Find
from w =1st trial

A = start

s0

low

s1
low , x < 1s3(pattern)

high

low

high

low

0 0.1

0.3

0.5

0.7

1.2 t

s0
<latexit sha1_base64="UWVyB2wrJZ3beswyKti6XLAhHMc=">AAAB6nicbVBNS8NAEJ3Ur1q/oh69LBbBU0lE0GPRi8eK9gPaUDbbTbt0swm7E6GE/gQvHhTx6i/y5r9x2+agrQ8GHu/NMDMvTKUw6HnfTmltfWNzq7xd2dnd2z9wD49aJsk0402WyER3Qmq4FIo3UaDknVRzGoeSt8Px7cxvP3FtRKIecZLyIKZDJSLBKFrpwfS9vlv1at4cZJX4BalCgUbf/eoNEpbFXCGT1Jiu76UY5FSjYJJPK73M8JSyMR3yrqWKxtwE+fzUKTmzyoBEibalkMzV3xM5jY2ZxKHtjCmOzLI3E//zuhlG10EuVJohV2yxKMokwYTM/iYDoTlDObGEMi3srYSNqKYMbToVG4K//PIqaV3UfK/m319W6zdFHGU4gVM4Bx+uoA530IAmMBjCM7zCmyOdF+fd+Vi0lpxi5hj+wPn8AQKOjZo=</latexit>

s1<latexit sha1_base64="74/5ryLy7rv4hfaCJ57+tAHgIZ0=">AAAB6nicbVBNS8NAEJ3Ur1q/oh69LBbBU0lE0GPRi8eK9gPaUDbbTbt0swm7E6GE/gQvHhTx6i/y5r9x2+agrQ8GHu/NMDMvTKUw6HnfTmltfWNzq7xd2dnd2z9wD49aJsk0402WyER3Qmq4FIo3UaDknVRzGoeSt8Px7cxvP3FtRKIecZLyIKZDJSLBKFrpwfT9vlv1at4cZJX4BalCgUbf/eoNEpbFXCGT1Jiu76UY5FSjYJJPK73M8JSyMR3yrqWKxtwE+fzUKTmzyoBEibalkMzV3xM5jY2ZxKHtjCmOzLI3E//zuhlG10EuVJohV2yxKMokwYTM/iYDoTlDObGEMi3srYSNqKYMbToVG4K//PIqaV3UfK/m319W6zdFHGU4gVM4Bx+uoA530IAmMBjCM7zCmyOdF+fd+Vi0lpxi5hj+wPn8AQQSjZs=</latexit>

s2

s1<latexit sha1_base64="Y0GdP2x29WLwKXitorGh3wYlFaw=">AAAB6nicbVBNS8NAEJ3Ur1q/qh69LBbBU0mKUI9FLx4r2g9oQ9lsJ+3SzSbsboQS+hO8eFDEq7/Im//GbZuDtj4YeLw3w8y8IBFcG9f9dgobm1vbO8Xd0t7+weFR+fikreNUMWyxWMSqG1CNgktsGW4EdhOFNAoEdoLJ7dzvPKHSPJaPZpqgH9GR5CFn1FjpQQ9qg3LFrboLkHXi5aQCOZqD8ld/GLM0QmmYoFr3PDcxfkaV4UzgrNRPNSaUTegIe5ZKGqH2s8WpM3JhlSEJY2VLGrJQf09kNNJ6GgW2M6JmrFe9ufif10tNeO1nXCapQcmWi8JUEBOT+d9kyBUyI6aWUKa4vZWwMVWUGZtOyYbgrb68Ttq1qudWvfurSuMmj6MIZ3AOl+BBHRpwB01oAYMRPMMrvDnCeXHenY9la8HJZ07hD5zPHwWWjZw=</latexit><latexit sha1_base64="6LwQF3hT/hjtbKtX2Uutcpnd+1c=">AAAB6nicbVBNS8NAEJ3Ur1q/qh69LBbBU0m0oMeiF48V7Qe0oWy2k3bpZhN2N0IJ/QlePCji1V/kzX/jts1BWx8MPN6bYWZekAiujet+O4W19Y3NreJ2aWd3b/+gfHjU0nGqGDZZLGLVCahGwSU2DTcCO4lCGgUC28H4dua3n1BpHstHM0nQj+hQ8pAzaqz0oPuX/XLFrbpzkFXi5aQCORr98ldvELM0QmmYoFp3PTcxfkaV4UzgtNRLNSaUjekQu5ZKGqH2s/mpU3JmlQEJY2VLGjJXf09kNNJ6EgW2M6JmpJe9mfif101NeO1nXCapQckWi8JUEBOT2d9kwBUyIyaWUKa4vZWwEVWUGZtOyYbgLb+8SloXVc+teve1Sv0mj6MIJ3AK5+DBFdThDhrQBAZDeIZXeHOE8+K8Ox+L1oKTzxzDHzifPwcajZ0=</latexit>

3rd trial$, x < 1lows

2nd trials2

s0<latexit sha1_base64="74/5ryLy7rv4hfaCJ57+tAHgIZ0=">AAAB6nicbVBNS8NAEJ3Ur1q/oh69LBbBU0lE0GPRi8eK9gPaUDbbTbt0swm7E6GE/gQvHhTx6i/y5r9x2+agrQ8GHu/NMDMvTKUw6HnfTmltfWNzq7xd2dnd2z9wD49aJsk0402WyER3Qmq4FIo3UaDknVRzGoeSt8Px7cxvP3FtRKIecZLyIKZDJSLBKFrpwfT9vlv1at4cZJX4BalCgUbf/eoNEpbFXCGT1Jiu76UY5FSjYJJPK73M8JSyMR3yrqWKxtwE+fzUKTmzyoBEibalkMzV3xM5jY2ZxKHtjCmOzLI3E//zuhlG10EuVJohV2yxKMokwYTM/iYDoTlDObGEMi3srYSNqKYMbToVG4K//PIqaV3UfK/m319W6zdFHGU4gVM4Bx+uoA530IAmMBjCM7zCmyOdF+fd+Vi0lpxi5hj+wPn8AQQSjZs=</latexit>

8><t 2 [0, 0.1)
3 ✔ t0 2 (0.3, 0.5]>
:0tt 2 (0, 1)

s2s<latexit sha1_base64="6LwQF3hT/hjtbKtX2Uutcpnd+1c=">AAAB6nicbVBNS8NAEJ3Ur1q/qh69LBbBU0m0oMeiF48V7Qe0oWy2k3bpZhN2N0IJ/QlePCji1V/kzX/jts1BWx8MPN6bYWZekAiujet+O4W19Y3NreJ2aWd3b/+gfHjU0nGqGDZZLGLVCahGwSU2DTcCO4lCGgUC28H4dua3n1BpHstHM0nQj+hQ8pAzaqz0oPuX/XLFrbpzkFXi5aQCORr98ldvELM0QmmYoFp3PTcxfkaV4UzgtNRLNSaUjekQu5ZKGqH2s/mpU3JmlQEJY2VLGjJXf09kNNJ6EgW2M6JmpJe9mfif101NeO1nXCapQckWi8JUEBOT2d9kwBUyIyaWUKa4vZWwEVWUGZtOyYbgLb+8SloXVc+teve1Sv0mj6MIJ3AK5+DBFdThDhrQBAZDeIZXeHOE8+K8Ox+L1oKTzxzDHzifPwcajZ0=</latexit><latexit sha1_base64="UWVyB2wrJZ3beswyKti6XLAhHMc=">AAAB6nicbVBNS8NAEJ3Ur1q/oh69LBbBU0lE0GPRi8eK9gPaUDbbTbt0swm7E6GE/gQvHhTx6i/y5r9x2+agrQ8GHu/NMDMvTKUw6HnfTmltfWNzq7xd2dnd2z9wD49aJsk0402WyER3Qmq4FIo3UaDknVRzGoeSt8Px7cxvP3FtRKIecZLyIKZDJSLBKFrpwfS9vlv1at4cZJX4BalCgUbf/eoNEpbFXCGT1Jiu76UY5FSjYJJPK73M8JSyMR3yrqWKxtwE+fzUKTmzyoBEibalkMzV3xM5jY2ZxKHtjCmOzLI3E//zuhlG10EuVJohV2yxKMokwYTM/iYDoTlDObGEMi3srYSNqKYMbToVG4K//PIqaV3UfK/m319W6zdFHGU4gVM4Bx+uoA530IAmMBjCM7zCmyOdF+fd+Vi0lpxi5hj+wPn8AQKOjZo=</latexit>

s1<latexit sha1_base64="74/5ryLy7rv4hfaCJ57+tAHgIZ0=">AAAB6nicbVBNS8NAEJ3Ur1q/oh69LBbBU0lE0GPRi8eK9gPaUDbbTbt0swm7E6GE/gQvHhTx6i/y5r9x2+agrQ8GHu/NMDMvTKUw6HnfTmltfWNzq7xd2dnd2z9wD49aJsk0402WyER3Qmq4FIo3UaDknVRzGoeSt8Px7cxvP3FtRKIecZLyIKZDJSLBKFrpwfT9vlv1at4cZJX4BalCgUbf/eoNEpbFXCGT1Jiu76UY5FSjYJJPK73M8JSyMR3yrqWKxtwE+fzUKTmzyoBEibalkMzV3xM5jY2ZxKHtjCmOzLI3E//zuhlG10EuVJohV2yxKMokwYTM/iYDoTlDObGEMi3srYSNqKYMbToVG4K//PIqaV3UfK/m319W6zdFHGU4gVM4Bx+uoA530IAmMBjCM7zCmyOdF+fd+Vi0lpxi5hj+wPn8AQQSjZs=</latexit>

s2

s1<latexit sha1_base64="Y0GdP2x29WLwKXitorGh3wYlFaw=">AAAB6nicbVBNS8NAEJ3Ur1q/qh69LBbBU0mKUI9FLx4r2g9oQ9lsJ+3SzSbsboQS+hO8eFDEq7/Im//GbZuDtj4YeLw3w8y8IBFcG9f9dgobm1vbO8Xd0t7+weFR+fikreNUMWyxWMSqG1CNgktsGW4EdhOFNAoEdoLJ7dzvPKHSPJaPZpqgH9GR5CFn1FjpQQ9qg3LFrboLkHXi5aQCOZqD8ld/GLM0QmmYoFr3PDcxfkaV4UzgrNRPNSaUTegIe5ZKGqH2s8WpM3JhlSEJY2VLGrJQf09kNNJ6GgW2M6JmrFe9ufif10tNeO1nXCapQcmWi8JUEBOT+d9kyBUyI6aWUKa4vZWwMVWUGZtOyYbgrb68Ttq1qudWvfurSuMmj6MIZ3AOl+BBHRpwB01oAYMRPMMrvDnCeXHenY9la8HJZ07hD5zPHwWWjZw=</latexit>s<latexit sha1_base64="6LwQF3hT/hjtbKtX2Uutcpnd+1c=">AAAB6nicbVBNS8NAEJ3Ur1q/qh69LBbBU0m0oMeiF48V7Qe0oWy2k3bpZhN2N0IJ/QlePCji1V/kzX/jts1BWx8MPN6bYWZekAiujet+O4W19Y3NreJ2aWd3b/+gfHjU0nGqGDZZLGLVCahGwSU2DTcCO4lCGgUC28H4dua3n1BpHstHM0nQj+hQ8pAzaqz0oPuX/XLFrbpzkFXi5aQCORr98ldvELM0QmmYoFp3PTcxfkaV4UzgtNRLNSaUjekQu5ZKGqH2s/mpU3JmlQEJY2VLGjJXf09kNNJ6EgW2M6JmpJe9mfif101NeO1nXCapQckWi8JUEBOT2d9kwBUyIyaWUKa4vZWwEVWUGZtOyYbgLb+8SloXVc+teve1Sv0mj6MIJ3AK5+DBFdThDhrQBAZDeIZXeHOE8+K8Ox+L1oKTzxzDHzifPwcajZ0=</latexit>

68><t 2 [0, 0.1)
3 ✔ >t0 2 (0.7, 1.1]
:0tt 2 (0, 1)<latexit sha1_base64="8bR93AfLHB56ZwN2tFRPJllD5z8=">AAACNHicbZBBSxtBFMdnY2t1rRr12MvQUIwQlx0pxKPYi+BFwaiQXcLs5CUOmZ1dZt4KYcmH8uIH8SKFHiritZ/BybqH1vTBwJ/f/72Zef8kV9JiGP70GksfPi5/Wln11z6vb2w2t7YvbVYYAT2RqcxcJ9yCkhp6KFHBdW6Ap4mCq2TyY+5f3YKxMtMXOM0hTvlYy5EUHB0aNE+jBMZSl8LdYWc+0khq2g87YcD2osjH3Qq0w6DbYQGLK7SPNeywPT8CPaynB81WGIRV0UXBatEidZ0Nmg/RMBNFChqF4tb2WZhjXHKDUiiY+VFhIediwsfQd1LzFGxcVkvP6DdHhnSUGXc00or+PVHy1NppmrjOlOONfe/N4f+8foGjw7iUOi8QtHh7aFQoihmdJ0iH0oBANXWCCyPdX6m44YYLdDn7LgT2fuVFcXkQMBfx+ffW0XEdxwr5Qr6SNmGkS47ICTkjPSLIHXkkv8mTd+/98p69l7fWhlfP7JB/yvvzCqfNpfo=</latexit>

✗

s0

✗

<latexit sha1_base64="Y0GdP2x29WLwKXitorGh3wYlFaw=">AAAB6nicbVBNS8NAEJ3Ur1q/qh69LBbBU0mKUI9FLx4r2g9oQ9lsJ+3SzSbsboQS+hO8eFDEq7/Im//GbZuDtj4YeLw3w8y8IBFcG9f9dgobm1vbO8Xd0t7+weFR+fikreNUMWyxWMSqG1CNgktsGW4EdhOFNAoEdoLJ7dzvPKHSPJaPZpqgH9GR5CFn1FjpQQ9qg3LFrboLkHXi5aQCOZqD8ld/GLM0QmmYoFr3PDcxfkaV4UzgrNRPNSaUTegIe5ZKGqH2s8WpM3JhlSEJY2VLGrJQf09kNNJ6GgW2M6JmrFe9ufif10tNeO1nXCapQcmWi8JUEBOT+d9kyBUyI6aWUKa4vZWwMVWUGZtOyYbgrb68Ttq1qudWvfurSuMmj6MIZ3AOl+BBHRpwB01oAYMRPMMrvDnCeXHenY9la8HJZ07hD5zPHwWWjZw=</latexit><latexit sha1_base64="LOncgRLuUrE2kiSVscHQHWWjl5g=">AAACNHicbZDLSsQwFIZT79bbqEs3wUFU0KH1gi4H3QhuRnBUmJYhzZwZg2laklNhKPNQbnwQNyK4UMStz2CmduHtQODn+89Jcv4olcKg5z05I6Nj4xOTU9PuzOzc/EJlcenCJJnm0OSJTPRVxAxIoaCJAiVcpRpYHEm4jG6Oh/7lLWgjEnWO/RTCmPWU6ArO0KJ25TSIoCdUzu0dZuAiDYSiLW/Lq/mbQeDiegE2vNquRfthgbaxhFv+phuA6pTT7UrVq3lF0b/CL0WVlNVoVx6CTsKzGBRyyYxp+V6KYc40Ci5h4AaZgZTxG9aDlpWKxWDCvFh6QNcs6dBuou1RSAv6fSJnsTH9OLKdMcNr89sbwv+8VobdwzAXKs0QFP96qJtJigkdJkg7QgNH2beCcS3sXym/ZppxtDm7NgT/98p/xcVOzbcRn+1V60dlHFNkhaySDeKTA1InJ6RBmoSTO/JIXsirc+88O2/O+1friFPOLJMf5Xx8AqYZpfk=</latexit><latexit sha1_base64="UWVyB2wrJZ3beswyKti6XLAhHMc=">AAAB6nicbVBNS8NAEJ3Ur1q/oh69LBbBU0lE0GPRi8eK9gPaUDbbTbt0swm7E6GE/gQvHhTx6i/y5r9x2+agrQ8GHu/NMDMvTKUw6HnfTmltfWNzq7xd2dnd2z9wD49aJsk0402WyER3Qmq4FIo3UaDknVRzGoeSt8Px7cxvP3FtRKIecZLyIKZDJSLBKFrpwfS9vlv1at4cZJX4BalCgUbf/eoNEpbFXCGT1Jiu76UY5FSjYJJPK73M8JSyMR3yrqWKxtwE+fzUKTmzyoBEibalkMzV3xM5jY2ZxKHtjCmOzLI3E//zuhlG10EuVJohV2yxKMokwYTM/iYDoTlDObGEMi3srYSNqKYMbToVG4K//PIqaV3UfK/m319W6zdFHGU4gVM4Bx+uoA530IAmMBjCM7zCmyOdF+fd+Vi0lpxi5hj+wPn8AQKOjZo=</latexit>(target)<latexit sha1_base64="74/5ryLy7rv4hfaCJ57+tAHgIZ0=">AAAB6nicbVBNS8NAEJ3Ur1q/oh69LBbBU0lE0GPRi8eK9gPaUDbbTbt0swm7E6GE/gQvHhTx6i/y5r9x2+agrQ8GHu/NMDMvTKUw6HnfTmltfWNzq7xd2dnd2z9wD49aJsk0402WyER3Qmq4FIo3UaDknVRzGoeSt8Px7cxvP3FtRKIecZLyIKZDJSLBKFrpwfT9vlv1at4cZJX4BalCgUbf/eoNEpbFXCGT1Jiu76UY5FSjYJJPK73M8JSyMR3yrqWKxtwE+fzUKTmzyoBEibalkMzV3xM5jY2ZxKHtjCmOzLI3E//zuhlG10EuVJohV2yxKMokwYTM/iYDoTlDObGEMi3srYSNqKYMbToVG4K//PIqaV3UfK/m319W6zdFHGU4gVM4Bx+uoA530IAmMBjCM7zCmyOdF+fd+Vi0lpxi5hj+wPn8AQQSjZs=</latexit>

8><t 2 [0.3, 0.5)
3 ✔ >t0 2 (0.7, 1.2]
:0
t 2 (0,1)
M.t Waga(NII)<latexit sha1_base64="g8/sGKR0WUuZX9MBYjbUjor1QvE=">AAACNnicbZBBT9swFMcdBhsLbHTjyMWimgCpi5xuEztWcOGCxCQKSE1UOc5Lseo4kf0yqYr6qXbZ59itFw6gadd9BNyQw4A9ydJfv/97tt8/KZW0yNjCW3mxuvby1fprf2Pzzdutzrv3F7aojIChKFRhrhJuQUkNQ5So4Ko0wPNEwWUyPV76l9/BWFnoc5yVEOd8omUmBUeHxp3TKIGJ1LVwd9i5jzSSmo5Y8KnHgi8HUeTjXoP2WXDYC4N+3KCP2MJeeOBHoNN2ftzpsoA1RZ+LsBVd0tbZuPMrSgtR5aBRKG7tKGQlxjU3KIWCuR9VFkoupnwCIyc1z8HGdbP2nH5wJKVZYdzRSBv670TNc2tneeI6c47X9qm3hP/zRhVmX+Na6rJC0OLhoaxSFAu6zJCm0oBANXOCCyPdX6m45oYLdEn7LoTw6crPxUU/CFkQfvvcHRy1cayTHbJL9klIDsmAnJAzMiSC/CALckvuvJ/ejffb+/PQuuK1M9vkUXl/7wGykaZ0</latexit>KMP-Style Algorithm forTimed Pattern Matching
high, x < 1

Find

A = startfrom w =1st trials0

2nd trials1

s2
low , x < 1$, x < 1s3(pattern)

low

high

low

high

low

0 0.1

0.3

0.5

0.7

1.2 t

s0
<latexit sha1_base64="UWVyB2wrJZ3beswyKti6XLAhHMc=">AAAB6nicbVBNS8NAEJ3Ur1q/oh69LBbBU0lE0GPRi8eK9gPaUDbbTbt0swm7E6GE/gQvHhTx6i/y5r9x2+agrQ8GHu/NMDMvTKUw6HnfTmltfWNzq7xd2dnd2z9wD49aJsk0402WyER3Qmq4FIo3UaDknVRzGoeSt8Px7cxvP3FtRKIecZLyIKZDJSLBKFrpwfS9vlv1at4cZJX4BalCgUbf/eoNEpbFXCGT1Jiu76UY5FSjYJJPK73M8JSyMR3yrqWKxtwE+fzUKTmzyoBEibalkMzV3xM5jY2ZxKHtjCmOzLI3E//zuhlG10EuVJohV2yxKMokwYTM/iYDoTlDObGEMi3srYSNqKYMbToVG4K//PIqaV3UfK/m319W6zdFHGU4gVM4Bx+uoA530IAmMBjCM7zCmyOdF+fd+Vi0lpxi5hj+wPn8AQKOjZo=</latexit>

s1<latexit sha1_base64="74/5ryLy7rv4hfaCJ57+tAHgIZ0=">AAAB6nicbVBNS8NAEJ3Ur1q/oh69LBbBU0lE0GPRi8eK9gPaUDbbTbt0swm7E6GE/gQvHhTx6i/y5r9x2+agrQ8GHu/NMDMvTKUw6HnfTmltfWNzq7xd2dnd2z9wD49aJsk0402WyER3Qmq4FIo3UaDknVRzGoeSt8Px7cxvP3FtRKIecZLyIKZDJSLBKFrpwfT9vlv1at4cZJX4BalCgUbf/eoNEpbFXCGT1Jiu76UY5FSjYJJPK73M8JSyMR3yrqWKxtwE+fzUKTmzyoBEibalkMzV3xM5jY2ZxKHtjCmOzLI3E//zuhlG10EuVJohV2yxKMokwYTM/iYDoTlDObGEMi3srYSNqKYMbToVG4K//PIqaV3UfK/m319W6zdFHGU4gVM4Bx+uoA530IAmMBjCM7zCmyOdF+fd+Vi0lpxi5hj+wPn8AQQSjZs=</latexit>

s2

s1<latexit sha1_base64="Y0GdP2x29WLwKXitorGh3wYlFaw=">AAAB6nicbVBNS8NAEJ3Ur1q/qh69LBbBU0mKUI9FLx4r2g9oQ9lsJ+3SzSbsboQS+hO8eFDEq7/Im//GbZuDtj4YeLw3w8y8IBFcG9f9dgobm1vbO8Xd0t7+weFR+fikreNUMWyxWMSqG1CNgktsGW4EdhOFNAoEdoLJ7dzvPKHSPJaPZpqgH9GR5CFn1FjpQQ9qg3LFrboLkHXi5aQCOZqD8ld/GLM0QmmYoFr3PDcxfkaV4UzgrNRPNSaUTegIe5ZKGqH2s8WpM3JhlSEJY2VLGrJQf09kNNJ6GgW2M6JmrFe9ufif10tNeO1nXCapQcmWi8JUEBOT+d9kyBUyI6aWUKa4vZWwMVWUGZtOyYbgrb68Ttq1qudWvfurSuMmj6MIZ3AOl+BBHRpwB01oAYMRPMMrvDnCeXHenY9la8HJZ07hD5zPHwWWjZw=</latexit>s

Skip 1 trial!!

2nd triallow<latexit sha1_base64="6LwQF3hT/hjtbKtX2Uutcpnd+1c=">AAAB6nicbVBNS8NAEJ3Ur1q/qh69LBbBU0m0oMeiF48V7Qe0oWy2k3bpZhN2N0IJ/QlePCji1V/kzX/jts1BWx8MPN6bYWZekAiujet+O4W19Y3NreJ2aWd3b/+gfHjU0nGqGDZZLGLVCahGwSU2DTcCO4lCGgUC28H4dua3n1BpHstHM0nQj+hQ8pAzaqz0oPuX/XLFrbpzkFXi5aQCORr98ldvELM0QmmYoFp3PTcxfkaV4UzgtNRLNSaUjekQu5ZKGqH2s/mpU3JmlQEJY2VLGjJXf09kNNJ6EgW2M6JmpJe9mfif101NeO1nXCapQckWi8JUEBOT2d9kwBUyIyaWUKa4vZWwEVWUGZtOyYbgLb+8SloXVc+teve1Sv0mj6MIJ3AK5+DBFdThDhrQBAZDeIZXeHOE8+K8Ox+L1oKTzxzDHzifPwcajZ0=</latexit>

s0<latexit sha1_base64="74/5ryLy7rv4hfaCJ57+tAHgIZ0=">AAAB6nicbVBNS8NAEJ3Ur1q/oh69LBbBU0lE0GPRi8eK9gPaUDbbTbt0swm7E6GE/gQvHhTx6i/y5r9x2+agrQ8GHu/NMDMvTKUw6HnfTmltfWNzq7xd2dnd2z9wD49aJsk0402WyER3Qmq4FIo3UaDknVRzGoeSt8Px7cxvP3FtRKIecZLyIKZDJSLBKFrpwfT9vlv1at4cZJX4BalCgUbf/eoNEpbFXCGT1Jiu76UY5FSjYJJPK73M8JSyMR3yrqWKxtwE+fzUKTmzyoBEibalkMzV3xM5jY2ZxKHtjCmOzLI3E//zuhlG10EuVJohV2yxKMokwYTM/iYDoTlDObGEMi3srYSNqKYMbToVG4K//PIqaV3UfK/m319W6zdFHGU4gVM4Bx+uoA530IAmMBjCM7zCmyOdF+fd+Vi0lpxi5hj+wPn8AQQSjZs=</latexit>

8><t 2 [0, 0.1)
3 ✔ t0 2 (0.3, 0.5]>
:0tt 2 (0, 1)

s2s<latexit sha1_base64="6LwQF3hT/hjtbKtX2Uutcpnd+1c=">AAAB6nicbVBNS8NAEJ3Ur1q/qh69LBbBU0m0oMeiF48V7Qe0oWy2k3bpZhN2N0IJ/QlePCji1V/kzX/jts1BWx8MPN6bYWZekAiujet+O4W19Y3NreJ2aWd3b/+gfHjU0nGqGDZZLGLVCahGwSU2DTcCO4lCGgUC28H4dua3n1BpHstHM0nQj+hQ8pAzaqz0oPuX/XLFrbpzkFXi5aQCORr98ldvELM0QmmYoFp3PTcxfkaV4UzgtNRLNSaUjekQu5ZKGqH2s/mpU3JmlQEJY2VLGjJXf09kNNJ6EgW2M6JmpJe9mfif101NeO1nXCapQckWi8JUEBOT2d9kwBUyIyaWUKa4vZWwEVWUGZtOyYbgLb+8SloXVc+teve1Sv0mj6MIJ3AK5+DBFdThDhrQBAZDeIZXeHOE8+K8Ox+L1oKTzxzDHzifPwcajZ0=</latexit><latexit sha1_base64="UWVyB2wrJZ3beswyKti6XLAhHMc=">AAAB6nicbVBNS8NAEJ3Ur1q/oh69LBbBU0lE0GPRi8eK9gPaUDbbTbt0swm7E6GE/gQvHhTx6i/y5r9x2+agrQ8GHu/NMDMvTKUw6HnfTmltfWNzq7xd2dnd2z9wD49aJsk0402WyER3Qmq4FIo3UaDknVRzGoeSt8Px7cxvP3FtRKIecZLyIKZDJSLBKFrpwfS9vlv1at4cZJX4BalCgUbf/eoNEpbFXCGT1Jiu76UY5FSjYJJPK73M8JSyMR3yrqWKxtwE+fzUKTmzyoBEibalkMzV3xM5jY2ZxKHtjCmOzLI3E//zuhlG10EuVJohV2yxKMokwYTM/iYDoTlDObGEMi3srYSNqKYMbToVG4K//PIqaV3UfK/m319W6zdFHGU4gVM4Bx+uoA530IAmMBjCM7zCmyOdF+fd+Vi0lpxi5hj+wPn8AQKOjZo=</latexit>

s1<latexit sha1_base64="74/5ryLy7rv4hfaCJ57+tAHgIZ0=">AAAB6nicbVBNS8NAEJ3Ur1q/oh69LBbBU0lE0GPRi8eK9gPaUDbbTbt0swm7E6GE/gQvHhTx6i/y5r9x2+agrQ8GHu/NMDMvTKUw6HnfTmltfWNzq7xd2dnd2z9wD49aJsk0402WyER3Qmq4FIo3UaDknVRzGoeSt8Px7cxvP3FtRKIecZLyIKZDJSLBKFrpwfT9vlv1at4cZJX4BalCgUbf/eoNEpbFXCGT1Jiu76UY5FSjYJJPK73M8JSyMR3yrqWKxtwE+fzUKTmzyoBEibalkMzV3xM5jY2ZxKHtjCmOzLI3E//zuhlG10EuVJohV2yxKMokwYTM/iYDoTlDObGEMi3srYSNqKYMbToVG4K//PIqaV3UfK/m319W6zdFHGU4gVM4Bx+uoA530IAmMBjCM7zCmyOdF+fd+Vi0lpxi5hj+wPn8AQQSjZs=</latexit>

s2

s1<latexit sha1_base64="Y0GdP2x29WLwKXitorGh3wYlFaw=">AAAB6nicbVBNS8NAEJ3Ur1q/qh69LBbBU0mKUI9FLx4r2g9oQ9lsJ+3SzSbsboQS+hO8eFDEq7/Im//GbZuDtj4YeLw3w8y8IBFcG9f9dgobm1vbO8Xd0t7+weFR+fikreNUMWyxWMSqG1CNgktsGW4EdhOFNAoEdoLJ7dzvPKHSPJaPZpqgH9GR5CFn1FjpQQ9qg3LFrboLkHXi5aQCOZqD8ld/GLM0QmmYoFr3PDcxfkaV4UzgrNRPNSaUTegIe5ZKGqH2s8WpM3JhlSEJY2VLGrJQf09kNNJ6GgW2M6JmrFe9ufif10tNeO1nXCapQcmWi8JUEBOT+d9kyBUyI6aWUKa4vZWwMVWUGZtOyYbgrb68Ttq1qudWvfurSuMmj6MIZ3AOl+BBHRpwB01oAYMRPMMrvDnCeXHenY9la8HJZ07hD5zPHwWWjZw=</latexit>s<latexit sha1_base64="6LwQF3hT/hjtbKtX2Uutcpnd+1c=">AAAB6nicbVBNS8NAEJ3Ur1q/qh69LBbBU0m0oMeiF48V7Qe0oWy2k3bpZhN2N0IJ/QlePCji1V/kzX/jts1BWx8MPN6bYWZekAiujet+O4W19Y3NreJ2aWd3b/+gfHjU0nGqGDZZLGLVCahGwSU2DTcCO4lCGgUC28H4dua3n1BpHstHM0nQj+hQ8pAzaqz0oPuX/XLFrbpzkFXi5aQCORr98ldvELM0QmmYoFp3PTcxfkaV4UzgtNRLNSaUjekQu5ZKGqH2s/mpU3JmlQEJY2VLGjJXf09kNNJ6EgW2M6JmpJe9mfif101NeO1nXCapQckWi8JUEBOT2d9kwBUyIyaWUKa4vZWwEVWUGZtOyYbgLb+8SloXVc+teve1Sv0mj6MIJ3AK5+DBFdThDhrQBAZDeIZXeHOE8+K8Ox+L1oKTzxzDHzifPwcajZ0=</latexit>

7

8><t 2 [0, 0.1)
3 ✔ >t0 2 (0.7, 1.1]
:0tt 2 (0, 1)<latexit sha1_base64="8bR93AfLHB56ZwN2tFRPJllD5z8=">AAACNHicbZBBSxtBFMdnY2t1rRr12MvQUIwQlx0pxKPYi+BFwaiQXcLs5CUOmZ1dZt4KYcmH8uIH8SKFHiritZ/BybqH1vTBwJ/f/72Zef8kV9JiGP70GksfPi5/Wln11z6vb2w2t7YvbVYYAT2RqcxcJ9yCkhp6KFHBdW6Ap4mCq2TyY+5f3YKxMtMXOM0hTvlYy5EUHB0aNE+jBMZSl8LdYWc+0khq2g87YcD2osjH3Qq0w6DbYQGLK7SPNeywPT8CPaynB81WGIRV0UXBatEidZ0Nmg/RMBNFChqF4tb2WZhjXHKDUiiY+VFhIediwsfQd1LzFGxcVkvP6DdHhnSUGXc00or+PVHy1NppmrjOlOONfe/N4f+8foGjw7iUOi8QtHh7aFQoihmdJ0iH0oBANXWCCyPdX6m44YYLdDn7LgT2fuVFcXkQMBfx+ffW0XEdxwr5Qr6SNmGkS47ICTkjPSLIHXkkv8mTd+/98p69l7fWhlfP7JB/yvvzCqfNpfo=</latexit>

✗

s0

✗

<latexit sha1_base64="Y0GdP2x29WLwKXitorGh3wYlFaw=">AAAB6nicbVBNS8NAEJ3Ur1q/qh69LBbBU0mKUI9FLx4r2g9oQ9lsJ+3SzSbsboQS+hO8eFDEq7/Im//GbZuDtj4YeLw3w8y8IBFcG9f9dgobm1vbO8Xd0t7+weFR+fikreNUMWyxWMSqG1CNgktsGW4EdhOFNAoEdoLJ7dzvPKHSPJaPZpqgH9GR5CFn1FjpQQ9qg3LFrboLkHXi5aQCOZqD8ld/GLM0QmmYoFr3PDcxfkaV4UzgrNRPNSaUTegIe5ZKGqH2s8WpM3JhlSEJY2VLGrJQf09kNNJ6GgW2M6JmrFe9ufif10tNeO1nXCapQcmWi8JUEBOT+d9kyBUyI6aWUKa4vZWwMVWUGZtOyYbgrb68Ttq1qudWvfurSuMmj6MIZ3AOl+BBHRpwB01oAYMRPMMrvDnCeXHenY9la8HJZ07hD5zPHwWWjZw=</latexit><latexit sha1_base64="LOncgRLuUrE2kiSVscHQHWWjl5g=">AAACNHicbZDLSsQwFIZT79bbqEs3wUFU0KH1gi4H3QhuRnBUmJYhzZwZg2laklNhKPNQbnwQNyK4UMStz2CmduHtQODn+89Jcv4olcKg5z05I6Nj4xOTU9PuzOzc/EJlcenCJJnm0OSJTPRVxAxIoaCJAiVcpRpYHEm4jG6Oh/7lLWgjEnWO/RTCmPWU6ArO0KJ25TSIoCdUzu0dZuAiDYSiLW/Lq/mbQeDiegE2vNquRfthgbaxhFv+phuA6pTT7UrVq3lF0b/CL0WVlNVoVx6CTsKzGBRyyYxp+V6KYc40Ci5h4AaZgZTxG9aDlpWKxWDCvFh6QNcs6dBuou1RSAv6fSJnsTH9OLKdMcNr89sbwv+8VobdwzAXKs0QFP96qJtJigkdJkg7QgNH2beCcS3sXym/ZppxtDm7NgT/98p/xcVOzbcRn+1V60dlHFNkhaySDeKTA1InJ6RBmoSTO/JIXsirc+88O2/O+1friFPOLJMf5Xx8AqYZpfk=</latexit><latexit sha1_base64="UWVyB2wrJZ3beswyKti6XLAhHMc=">AAAB6nicbVBNS8NAEJ3Ur1q/oh69LBbBU0lE0GPRi8eK9gPaUDbbTbt0swm7E6GE/gQvHhTx6i/y5r9x2+agrQ8GHu/NMDMvTKUw6HnfTmltfWNzq7xd2dnd2z9wD49aJsk0402WyER3Qmq4FIo3UaDknVRzGoeSt8Px7cxvP3FtRKIecZLyIKZDJSLBKFrpwfS9vlv1at4cZJX4BalCgUbf/eoNEpbFXCGT1Jiu76UY5FSjYJJPK73M8JSyMR3yrqWKxtwE+fzUKTmzyoBEibalkMzV3xM5jY2ZxKHtjCmOzLI3E//zuhlG10EuVJohV2yxKMokwYTM/iYDoTlDObGEMi3srYSNqKYMbToVG4K//PIqaV3UfK/m319W6zdFHGU4gVM4Bx+uoA530IAmMBjCM7zCmyOdF+fd+Vi0lpxi5hj+wPn8AQKOjZo=</latexit>(target)<latexit sha1_base64="74/5ryLy7rv4hfaCJ57+tAHgIZ0=">AAAB6nicbVBNS8NAEJ3Ur1q/oh69LBbBU0lE0GPRi8eK9gPaUDbbTbt0swm7E6GE/gQvHhTx6i/y5r9x2+agrQ8GHu/NMDMvTKUw6HnfTmltfWNzq7xd2dnd2z9wD49aJsk0402WyER3Qmq4FIo3UaDknVRzGoeSt8Px7cxvP3FtRKIecZLyIKZDJSLBKFrpwfT9vlv1at4cZJX4BalCgUbf/eoNEpbFXCGT1Jiu76UY5FSjYJJPK73M8JSyMR3yrqWKxtwE+fzUKTmzyoBEibalkMzV3xM5jY2ZxKHtjCmOzLI3E//zuhlG10EuVJohV2yxKMokwYTM/iYDoTlDObGEMi3srYSNqKYMbToVG4K//PIqaV3UfK/m319W6zdFHGU4gVM4Bx+uoA530IAmMBjCM7zCmyOdF+fd+Vi0lpxi5hj+wPn8AQQSjZs=</latexit>

8><t 2 [0.3, 0.5)
3 ✔ >t0 2 (0.7, 1.2]
:0
t 2 (0,1)
M.t Waga(NII)<latexit sha1_base64="g8/sGKR0WUuZX9MBYjbUjor1QvE=">AAACNnicbZBBT9swFMcdBhsLbHTjyMWimgCpi5xuEztWcOGCxCQKSE1UOc5Lseo4kf0yqYr6qXbZ59itFw6gadd9BNyQw4A9ydJfv/97tt8/KZW0yNjCW3mxuvby1fprf2Pzzdutzrv3F7aojIChKFRhrhJuQUkNQ5So4Ko0wPNEwWUyPV76l9/BWFnoc5yVEOd8omUmBUeHxp3TKIGJ1LVwd9i5jzSSmo5Y8KnHgi8HUeTjXoP2WXDYC4N+3KCP2MJeeOBHoNN2ftzpsoA1RZ+LsBVd0tbZuPMrSgtR5aBRKG7tKGQlxjU3KIWCuR9VFkoupnwCIyc1z8HGdbP2nH5wJKVZYdzRSBv670TNc2tneeI6c47X9qm3hP/zRhVmX+Na6rJC0OLhoaxSFAu6zJCm0oBANXOCCyPdX6m45oYLdEn7LoTw6crPxUU/CFkQfvvcHRy1cayTHbJL9klIDsmAnJAzMiSC/CALckvuvJ/ejffb+/PQuuK1M9vkUXl/7wGykaZ0</latexit>Problems in Skipping forTimed Pattern Matching• The length of partial match is unbounded.
Timed Pattern Matching
String Matching
Table for length 3 partial match

S T R I N G✗✗✔

We construct foreach length* S T R I N* * S T R I* * * S T R

Infinitely Many
Tables!!

• Infinitely many timestamps
String Matching
Timed Pattern Matching
Length 3 partial matchin string matching

Length 2 partial matchin timed pattern matching
low high

S T R

0
8

t

Infinitely many timestamps
M. Waga (NII)Problems in Skipping forTimed Pattern Matching• The length of partial match is unbounded.
Timed Pattern Matching
String Matching
Table for state s2 partial match
Table for length 3 partial match
S T R I N G✗ * S T R I N✗ * * S T R I

lowConstruct foreach state✔ * * * S T R

high
t

0

✗

low
0

✔

high
low

t
high
t

0

• Infinitely many timestamps
String Matching
Timed Pattern Matching
State s2 partial matchin timed pattern matching

Length 3 partial matchin string matching

S T R

high, x < 1

Represent by atimed automaton

start

s0

low

s1

s2
low , x < 1

9

M. Waga (NII)Problems in Skipping forTimed Pattern Matching•

The length of partial match is unbounded.

Table for length 3 partial match

S T R I N G✗ * S T R I N✗ * * S TR I

Table for state s2 partial match

Construct foreach state

high
t

0

✗

✔ * * * S T R

•

low

low
0

✔

high
low

t
high
t

0

Infinitely many timestamps
State s2 partial matchin timed pattern matching

Length 3 partial matchin string matching

S T R

Represent by atimed automaton

10high, x < 1

start

s0

low

s1

s2
low , x < 1

M. Waga (NII)Skipping for Timed Pattern
Matching

Table for state s2 partial match
high, x < 1
low

s0

start

s1

s2

We want tocompare themlow , x < 1high/x := 0

✗

s 1

start

low

s0

s1

start

s 2

high/x := 0
s 1

low

s2
low , x < 1

low /x := 0high✔

high, x < 1

low /x := 0s0high, x < 1
low

s1

s2
low , x < 1

11

M. Waga (NII)Skipping for Timed Pattern
Matching

Table for state s2 partial match
high, x < 1
low

s0

start

s1

s2

Product

low , x < 1high/x := 0

✗

s 1

start

low

s0

s1

start

s 2

high/x := 0
s 1

low

s2
low , x < 1

low /x := 0high✔

high, x < 1

low /x := 0

Emptiness
Checking

s0high, x < 1
low

s1

s2
low , x < 1

12

M. Waga (NII)Emptiness Checking
by Zone Construction
Labelled by a set of “similar” clock
valuations represented by a zones1$, x > 1

a, x < 1

$

s1
0<x<1

construct an NFA

s3
x>1

a

start

s0

s3

start

s0
x=0
b

b,
x = 1/x := 0

s2

$,
x<1

s2
x=0

$

s3
0<x<1

Thm. (soundness and completeness)
Zone automata maintain state reachability.
13

M. Waga (NII)Outline
1. Algorithm in MONAA•Skipping for timed pattern matching[Waga et al., FORMATS’17]

2. Frontend of MONAA•

Command line interface (CLI) / C++ API

3. Experiments
14

M. Waga (NII)Input of MONAA (CLI)15

M. Waga (NII)Output of MONAA (CLI)16

M. Waga (NII)C++ API (libmonaa)
User’s Program e.g., online runtime verification
C++ API (libmonaa)
Get feedback • Execute timed
pattern matching ina user’s code
Give Logs • Accelerated by
Skipping• I/O by function/class
17

M. Waga (NII)Better Performance bylibmonaa
MONAA
libmonaa

Compilemonaa
TA/TRE
Timed Word

Exec.

Resultlibmonaa (TA is hard-coded)
libmonaaTA

CompileMore optimization!!

MonitorExec.

ResultTimed Word18

M. Waga (NII)Outline
1. Algorithm in MONAA•Skipping for timed pattern matching[Waga et al., FORMATS’17]

2. Frontend of MONAA•

Command line interface (CLI) / C++ API

3. Experiments
19

M. Waga (NII)Comparison with Montre
MONAA

Existing Tool (Montre)[Ulus, CAV’17]• Use timed automata• We can also construct a

TA from a TRE• Accelerated by skipping• Both command line andC++ interface• Use timed regular expression• (online) On-the-fly

construction of a statemachine from TRE• Only command line interface
Our algorithm should work fasterbecause of skipping

M. Waga (NII)Experiments•

Monitoring of a Simulink model of an automatictransmission in a car.

•Model and spec. are from an automotive
benchmark paper [Hoxha et al., ARCH ’15]•

Events: gears: g1,g2,g3,g4
velocity: v >v̅ , v ≤ v̅RPM: ω > ω̅, ω ≤ ω̅21

M. Waga (NII)Experiments
Gear changes from g1 to g4 in 10 sec. and RPMchanges to high enough, but velocity is still low.
g1

g2 , trueg2

g3 , trueg3

g4 , x  10
/x := 0g4

3

g1 , true
start
!

?

!

!, true!, true?

!

g1 , true!, true

g1!

g2 , true22!, trueg2!

g3 , true$, x > 1!, trueg3

g4 , x  10
/x := 0g4

M. Waga (NII)Result of the Comparison

ne interllowing
and lined input,
ng proe timed
y a sysr of deching isbmonaa.
write ag proceplement

Table 1. Execution time (sec.)
Length of
timed word

MONAA
(TRE)

MONAA
(TA)

libmonaa(TA ishard coded)

Montre(online)Montre(offline)

306
127,552
255,750
383,168
508,756
632,484
758,500
894,692
1,011,426

7.03
7.55
8.05
8.54
9.16
9.53
10.05
10.53
11.05

0.80
1.27
1.73
2.21
2.69
3.14
3.60
4.06
4.56

0.20
0.31
0.42
0.53
0.64
0.75
0.85
0.97
1.07

0.13
37.45
75.93
115.88153.71
189.55216.92260.77289.63

0.03
1.56
3.13
4.69
6.21
7.75
9.33
10.88
12.39

Efficient
andTable
2. Memory
usage (kbytes)
Length of
timed word

online

MONAA
(TRE)

Blow up!!

MONAA
(TA)
23

libmonaa(TA ishard coded)

Efficient but
offline only

Montre(offline)

M. Waga (NII)Conclusion•

MONAA can inspect logs with timestamps•

fast (skipping)•

simple (text-based I/O)•

flexible (C++ API)

24

M. Waga (NII)Future Works•

Theoretical Side:••

Investigate other techniques for efficientmonitoring

Practical Side:•

Case study of timed pattern matchinghttps://github.com/MasWag/monaa
25

M. Waga (NII)