Timed Automata

In this document, we show how to use MONAA to monitor a timed automata specification. We assume that you know the basics of timed automata (e.g., [AD94]) and what MONAA does. If you have never used MONAA, we recommend to read Getting Started.

We use the following timed word as the input. It is also in example/getting_started/timed_word.txt.

A 0.5
B 0.8
C 1.5
A 2.0
B 3.2
A 3.5
C 4.6

DOT language

In MONAA, timed automata are represented by DOT language for Graphviz. Because we use various custom attributes to represent timed automata in DOT, it is not suitable to be visualized by Graphviz. Please consider using visualize-monaa-dot to translate to a DOT suitable for visualization.

The list of our custom attributes are as follows.

	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

Untimed example

The following is a timed automaton equivalent to the TRE (A(B|C))+$.

digraph G {
        1 [init=1,match=0];
        2 [init=0,match=0];
        3 [init=0,match=1];
        1->2 [label=A];
        2->1 [label=B];
        2->1 [label=C];
        2->3 [label="$"];
}

The result of the timed pattern matching is as follows.

../build/monaa -f ../examples/TA/untimed.dot < ../examples/getting_started/timed_word.txt

 -0.000000       <= t <   0.500000
  0.500000        < t' <=   0.800000
 -0.000000        < t' - t <=   0.800000
=============================
  1.500000       <= t <   2.000000
  2.000000        < t' <=   3.200000
 -0.000000        < t' - t <=   1.700000
=============================
  1.500000       <= t <   2.000000
  3.500000        < t' <=   4.600000
  1.500000        < t' - t <=   3.100000
=============================
  3.200000       <= t <   3.500000
  3.500000        < t' <=   4.600000
 -0.000000        < t' - t <=   1.400000
=============================

Timed example

We can add timing constraints to the above timed automaton. In the following example the added timing constraint is as follows.

• The initial A must occur within 1 time unit after the trimming
• Any B or C must occur within 1 time unit after the previous A
• Any non-initial A must occur within 1 time unit after the previous B or C
• The blank interval after the last B or C must be less than 1 time unit

digraph G {
        1 [init=1,match=0];
        2 [init=0,match=0];
        3 [init=0,match=1];
        1->2 [label=A,reset="{0}",guard="{x0 < 1}"];
        2->1 [label=B,reset="{0}",guard="{x0 < 1}"];
        2->1 [label=C,reset="{0}",guard="{x0 < 1}"];
        2->3 [label="$",guard="{x0 > 1}"];
}

The result of the timed pattern matching is as follows.

../build/monaa -f ../examples/TA/timed.dot < ../examples/getting_started/timed_word.txt

  1.500000       <= t <   2.000000
  3.000000        < t' <=   3.200000
  1.000000        < t' - t <=   1.700000
=============================
  3.200000       <= t <   3.500000
  4.500000        < t' <=   4.600000
  1.000000        < t' - t <=   1.400000
=============================

References

• [AD94] A theory of timed automata. Rajeev Alur and David L. Dill, Theoretical Computer Science, Volume 126, Issue 2, 1994, Pages 183-235