Real-Time Monitoring Enhanced
by Automata-based Skipping
Masaki Waga, SOKENDAI / NII / ERATO MMSD project

Timed Pattern Matching

State of the Art[Ulus+, FORMATS’14]• There is a tool Montre [Ulus, CAV’17]• However it has the following issues.
• The offline algorithm [Ulus+, FORMATS’14] requires huge RAM.
• linear to the size of the log• The online algorithm [Ulus+, TACAS’16] is slow.

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

high

0 0.1 0.2

0.5

0.7 t

Real-time spec. (Spec. useful for debugging)e.g., The gear of a car changes too frequently
Timed Automata A = startOutput•

high low

Our Solution

high, x < 1s0

low /x := 0

[Alur & Dill, TCS’94]

s1s2$, x < 1s3

low , x < 1Idea from string matching• Construct an automata-based algorithm• [Waga+, FORMATS’16]• Enhance the automata-based algorithm by Skipping• [Waga+, FORMATS’16], [Waga+, FORMATS’17]

The intervals where the spec. is satisfied in the datae.g., The gear changes too frequently in 0.2s-0.7s
0M(w, A) = {(t, t ) | w|(t,t0 ) 2 L(A)}
00= {(t, t ) | 0.2  t < 0.5, 0.7 < t }<latexit sha1_base64="Kf+trS32qO6hEDFxdeYvKfPlk20=">AAACYXicbZFNSwMxEIaz63f9WvXoJVjUCqXsFqUeFPy4eFBQsCo0pWTTtAaz2SWZVcu6f9KbFy/+EdO6iFoHEp55Z4Ykb8JECgO+/+a4E5NT0zOzc6X5hcWlZW9l9cbEqWa8yWIZ67uQGi6F4k0QIPldojmNQslvw4fTYf32kWsjYnUNg4S3I9pXoicYBSt1vGcSUbhnVGYXeeWp+p0d5zt46xCTrAJV2N4hkejip5dOkeZEKHxe+dlNckLGJvxaHRPJMeADy3tVuzUswjbJO17Zr/mjwOMQFFBGRVx2vFfSjVkacQVMUmNagZ9AO6MaBJM8L5HU8ISyB9rnLYuKRty0s5FDOd60Shf3Ym2XAjxSf05kNDJmEIW2c/gm87c2FP+rtVLo7bczoZIUuGJfB/VSiSHGQ7txV2jOQA4sUKaFvStm91RTBvZTStaE4O+Tx+GmXgv8WnC1Wz46KeyYRetoA1VQgBroCJ2hS9REDL07k86is+R8uHOu565+tbpOMbOGfoW7/glEpK/P</latexit>

Timed Pattern Matchingwith Skipping

Skipping for
String Matching[Waga+, FORMATS’16], [Waga+, FORMATS’17]

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

high, x < 1A = start

Findfrom w =s0s1s2
low , x < 1$, x < 1(pattern)s3lowhighlowhigh

low

0 0.1

0.3

0.5

0.7

1.2 t

s1s0

1st trial

STRONG_STRING
STRINGSTRING
Skip 2 trials!!
STRINGSTRING⋮STRING

lows2<latexit sha1_base64="74/5ryLy7rv4hfaCJ57+tAHgIZ0=">AAAB6nicbVBNS8NAEJ3Ur1q/oh69LBbBU0lE0GPRi8eK9gPaUDbbTbt0swm7E6GE/gQvHhTx6i/y5r9x2+agrQ8GHu/NMDMvTKUw6HnfTmltfWNzq7xd2dnd2z9wD49aJsk0402WyER3Qmq4FIo3UaDknVRzGoeSt8Px7cxvP3FtRKIecZLyIKZDJSLBKFrpwfT9vlv1at4cZJX4BalCgUbf/eoNEpbFXCGT1Jiu76UY5FSjYJJPK73M8JSyMR3yrqWKxtwE+fzUKTmzyoBEibalkMzV3xM5jY2ZxKHtjCmOzLI3E//zuhlG10EuVJohV2yxKMokwYTM/iYDoTlDObGEMi3srYSNqKYMbToVG4K//PIqaV3UfK/m319W6zdFHGU4gVM4Bx+uoA530IAmMBjCM7zCmyOdF+fd+Vi0lpxi5hj+wPn8AQQSjZs=</latexit><latexit sha1_base64="UWVyB2wrJZ3beswyKti6XLAhHMc=">AAAB6nicbVBNS8NAEJ3Ur1q/oh69LBbBU0lE0GPRi8eK9gPaUDbbTbt0swm7E6GE/gQvHhTx6i/y5r9x2+agrQ8GHu/NMDMvTKUw6HnfTmltfWNzq7xd2dnd2z9wD49aJsk0402WyER3Qmq4FIo3UaDknVRzGoeSt8Px7cxvP3FtRKIecZLyIKZDJSLBKFrpwfS9vlv1at4cZJX4BalCgUbf/eoNEpbFXCGT1Jiu76UY5FSjYJJPK73M8JSyMR3yrqWKxtwE+fzUKTmzyoBEibalkMzV3xM5jY2ZxKHtjCmOzLI3E//zuhlG10EuVJohV2yxKMokwYTM/iYDoTlDObGEMi3srYSNqKYMbToVG4K//PIqaV3UfK/m319W6zdFHGU4gVM4Bx+uoA530IAmMBjCM7zCmyOdF+fd+Vi0lpxi5hj+wPn8AQKOjZo=</latexit>sSkip 1 trial!!

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

2nd trial

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

s2<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)s<latexit sha1_base64="6LwQF3hT/hjtbKtX2Uutcpnd+1c=">AAAB6nicbVBNS8NAEJ3Ur1q/qh69LBbBU0m0oMeiF48V7Qe0oWy2k3bpZhN2N0IJ/QlePCji1V/kzX/jts1BWx8MPN6bYWZekAiujet+O4W19Y3NreJ2aWd3b/+gfHjU0nGqGDZZLGLVCahGwSU2DTcCO4lCGgUC28H4dua3n1BpHstHM0nQj+hQ8pAzaqz0oPuX/XLFrbpzkFXi5aQCORr98ldvELM0QmmYoFp3PTcxfkaV4UzgtNRLNSaUjekQu5ZKGqH2s/mpU3JmlQEJY2VLGjJXf09kNNJ6EgW2M6JmpJe9mfif101NeO1nXCapQckWi8JUEBOT2d9kwBUyIyaWUKa4vZWwEVWUGZtOyYbgLb+8SloXVc+teve1Sv0mj6MIJ3AK5+DBFdThDhrQBAZDeIZXeHOE8+K8Ox+L1oKTzxzDHzifPwcajZ0=</latexit>

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

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>✗2nd trial✗<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><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>s18><t 2 [0.3, 0.5)
t0 2 (0.7, 1.2]
3 ✔ >
:0t
t 2 (0, 1)<latexit sha1_base64="74/5ryLy7rv4hfaCJ57+tAHgIZ0=">AAAB6nicbVBNS8NAEJ3Ur1q/oh69LBbBU0lE0GPRi8eK9gPaUDbbTbt0swm7E6GE/gQvHhTx6i/y5r9x2+agrQ8GHu/NMDMvTKUw6HnfTmltfWNzq7xd2dnd2z9wD49aJsk0402WyER3Qmq4FIo3UaDknVRzGoeSt8Px7cxvP3FtRKIecZLyIKZDJSLBKFrpwfT9vlv1at4cZJX4BalCgUbf/eoNEpbFXCGT1Jiu76UY5FSjYJJPK73M8JSyMR3yrqWKxtwE+fzUKTmzyoBEibalkMzV3xM5jY2ZxKHtjCmOzLI3E//zuhlG10EuVJohV2yxKMokwYTM/iYDoTlDObGEMi3srYSNqKYMbToVG4K//PIqaV3UfK/m319W6zdFHGU4gVM4Bx+uoA530IAmMBjCM7zCmyOdF+fd+Vi0lpxi5hj+wPn8AQQSjZs=</latexit>

Adaptation for Timed Pattern Matching• The length of partial match is unbounded.
Timed Pattern Matching
String Matching✗ * S T R I N✗ * * S T R I✔ * * * S T R

Infinitely ManyTables!!
We construct for each length

lowhigh, x < 1✗lowlow

S T RLength 2 partial matchin timed pattern matching
low high0tZone Construction
s2high/x := 0thigh

✗s 1

start

t0

high, x < 1
lows0

s1

✔ starts 2

high/x := 0s 1

lows2
start

low , x < 1

low /x := 0high

Emptiness
Checking

Product

low , x < 1• Infinitely many timestamps
String Matching
Timed Pattern MatchingRepresent by a timed automaton
Length 3 partial matchin string matching

s1t
high0

✔

lows0

start

high0<latexit sha1_base64="g8/sGKR0WUuZX9MBYjbUjor1QvE=">AAACNnicbZBBT9swFMcdBhsLbHTjyMWimgCpi5xuEztWcOGCxCQKSE1UOc5Lseo4kf0yqYr6qXbZ59itFw6gadd9BNyQw4A9ydJfv/97tt8/KZW0yNjCW3mxuvby1fprf2Pzzdutzrv3F7aojIChKFRhrhJuQUkNQ5So4Ko0wPNEwWUyPV76l9/BWFnoc5yVEOd8omUmBUeHxp3TKIGJ1LVwd9i5jzSSmo5Y8KnHgi8HUeTjXoP2WXDYC4N+3KCP2MJeeOBHoNN2ftzpsoA1RZ+LsBVd0tbZuPMrSgtR5aBRKG7tKGQlxjU3KIWCuR9VFkoupnwCIyc1z8HGdbP2nH5wJKVZYdzRSBv670TNc2tneeI6c47X9qm3hP/zRhVmX+Na6rJC0OLhoaxSFAu6zJCm0oBANXOCCyPdX6m45oYLdEn7LoTw6crPxUU/CFkQfvvcHRy1cayTHbJL9klIDsmAnJAzMiSC/CALckvuvJ/ejffb+/PQuuK1M9vkUXl/7wGykaZ0</latexit>

Table for state s2 partial match We want to compare them.

Table for state s2 partial match

Table for length 3 partial match

S T R I N GConstruct foreach state(target)s0

low /x := 0high, x < 1
lows1(s0 , s0 2 )low(s1 , s0 1 )high, x < 1/x0 := 0(s2 , s00 )low , x < 1, x0 < 1 low ,0 x < 1,x <1s2(s2 , s02 )low , x < 1(s1 , s01 )high, x < 1, x0 < 1State s2 partial matchin timed pattern matching
high, x < 1starts0

Infinitely many timestamps

lows1

We can use a theory of timed automata!!

s2
low , x < 1

Evaluation

6

Implementation
̶ MONAA ̶• We implemented our algorithm as a tool “MONAA”.
• https://github.com/MasWag/monaa• Input format: Timed Automata (TA) and Timed Regular
Expressions (TRE)• We also provide C++ API “libmonaa”

Table 3. Execution time (sec.)
Length of MONAA MONAA
timed word (TRE) (TA)
708
218,247436,611655,237
870,967
1,087,411
1,304,404
1,527,632
1,739,525

7.03
7.55
8.05
8.54
9.16
9.53
10.05
10.53
11.05

libmonaa
Montre Montre(TA is(online) (o✏ine)
hard coded)

0.80
1.27
1.73
2.21
2.69
3.14
3.60
4.06
4.56

Efficient12
and online

10

Table 4. Memory usage (kbytes)

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

Blow up!!

0.03
1.56
3.13
4.69
6.21
7.75
9.33
10.88
12.39

Length of MONAA MONAA
timed word (TRE) (TA)
708
218,247436,611655,237
870,967
1,087,411
1,304,404
1,527,632
1,739,525

libmonaa
Montre(TA is(o✏ine)
hard coded)

16,468 10,808
16,312 10,808
16,312 10,752
16,344 10,692
16,468 10,840
16,280 10,900
16,340 10,768
16,468 10,696
16,312 10,808

Efficient but
constant!!
offlineonly (TRE)
MONAA

7,308
7,464
7,308
7,308
7,288
7,452
7,292
7,440
7,288

27,45645,70065,76487,92899,540109,076
147,048153,992
166,660

Blow up!!

MONAA (TA)libmonaa hard-coded autom.

ime [sec.]:@A@A
連絡先: 和賀 正樹 国立情報学研究所
アーキテクチャ科学研究系
803-6273-4886. - mwaga@nii.ac.jp
03-6273-4886

0