<p>This was a comment first, but Suresh asked me to turn it into an answer:</p>

<p>Maybe you want to take a look at <em>timed automata</em>. These are finite automata equipped with clocks; time can pass, clocks can be reset, transitions can be restricted to occur within a given time by clock guards etc. Here are some nice introductory slides: <a href="http://www.lsv.ens-cachan.fr/~bouyer/files/bouyer_chennai.pdf" rel="nofollow">lsv.ens-cachan.fr/~bouyer/files/bouyer_chennai.pdf</a></p>

<p>(This is actually the framework that Vor is using in his answer. His solution makes use of a clock that is reset and a guard for the epsilon transition.)</p>

CC BY-SA 2.5
2011-02-16T08:57:05.110Z
2011-02-16T08:57:05.110Z
DaniCL
<p>Perhaps you must add a clock to the table:</p>

<pre><code> q      x              q
-------------------------
 R      r              I
 I      o              W
 W      i  clock=0     C
 C      e              S
 S      ∈  (clock&gt;T)?  R
</code></pre>

<p>The S->R (reset) transition can occur only after T "ticks" has elapsed after the receive of [i]nput.</p>

<p>If you want the timeout to start after the [e]nd then you must reset the clock on:</p>

<pre><code> ...
 C      e  clock=0     S
 ...
</code></pre>

CC BY-SA 2.5
2011-02-15T20:29:08.677Z
2011-02-15T20:34:14.163Z
2011-02-15T20:34:14.163Z
Marzio De Biasi
<p>On a more abstract level, encode events as symbols in your trace, e.g. <code>[T]imeout</code>. As far as I know, this is standard technique when modeling (possibly labeled) transition systems.</p>

<p>This enables you to easily reason about properties your system might have, for instance statements (in temporal logic) like "After any timeout, my machine is in state <code>S</code>".</p>

<p>It does not yield a good model for implementations, though.</p>

CC BY-SA 2.5
2011-02-16T15:58:52.393Z
2011-02-16T15:58:52.393Z
Raphael
<p>I have defined a finite state machine </p>

<pre>
    Q = {Σ, S, s0, δ, F}

    where 

    Σ = {'[r]equest', '[o]ut', '[i]n', '[e]nd'}

    S = {'[R]eady', '[I]nitiating', '[W]aiting', 'Re[C]eived', 'Re[S]etting'}

    s0 = R,

    F = {R}

    δ =  (q ∈ S and x ∈ Σ)

     q      x      q
    -------------------
     R      r      I
     I      o      W
     W      i      C
     C      e      S
     S      ∈      R
</pre>

<p>However, I have a transition from  W to S via a temporal event†. How should I represent it?
If I add an epsilon-move<pre>
     W    ∈      S</pre>
it is not intuitive that it is a temporal event. </p>

<p>†possibly a timeout</p>

CC BY-SA 2.5
2011-02-15T09:33:39.057Z
What is a "temporal" event? A timeout?
Raphael
CC BY-SA 2.5
2011-02-15T10:20:17.017Z
Maybe you want to take a look at _timed automata_. These are finite automata equipped with clocks; time can pass, clocks can be reset, transitions can be restricted to occur within a given time by clock guards etc.
Here are some nice introductory slides: http://www.lsv.ens-cachan.fr/~bouyer/files/bouyer_chennai.pdf
DaniCL
CC BY-SA 2.5
2011-02-15T14:11:15.693Z
@DaniCL, Thank you. http://www.cs.aau.dk/~srba/courses/MCS-07/TA.pdf
CMR
CC BY-SA 2.5
2011-02-15T22:30:50.270Z
@DaniCL: make this an answer ?
Suresh Venkat
<fl.formal-languages><automata-theory>
A fsm with temporal events
CMR
# A fsm with temporal events

(Asked by: username_0 on 2011-02-15)

I have defined a finite state machine 

    Q = {Σ, S, s0, δ, F}

    where 

    Σ = {'[r]equest', '[o]ut', '[i]n', '[e]nd'}

    S = {'[R]eady', '[I]nitiating', '[W]aiting', 'Re[C]eived', 'Re[S]etting'}

    s0 = R,

    F = {R}

    δ =  (q ∈ S and x ∈ Σ)

     q      x      q
    -------------------
     R      r      I
     I      o      W
     W      i      C
     C      e      S
     S      ∈      R

However, I have a transition from  W to S via a temporal event†. How should I represent it?
If I add an epsilon-move
     W    ∈      S
it is not intuitive that it is a temporal event. 
†possibly a timeout

**Tags:** fl.formal-languages, automata-theory
> **Comments:**
> **username_1**: What is a "temporal" event? A timeout?  
> **username_2**: Maybe you want to take a look at _timed automata_. These are finite automata equipped with clocks; time can pass, clocks can be reset, transitions can be restricted to occur within a given time by clock guards etc. Here are some nice introductory slides: http://www.lsv.ens-cachan.fr/~bouyer/files/bouyer_chennai.pdf  
> **username_0**: @DaniCL, Thank you. http://www.cs.aau.dk/~srba/courses/MCS-07/TA.pdf  
> **username_3**: @DaniCL: make this an answer ?  

---

## 3 answers

### Answer by username_2 on 2011-02-16. Score: 3 | Accepted answer

This was a comment first, but Suresh asked me to turn it into an answer:

Maybe you want to take a look at *timed automata*. These are finite automata equipped with clocks; time can pass, clocks can be reset, transitions can be restricted to occur within a given time by clock guards etc. Here are some nice introductory slides: [lsv.ens-cachan.fr/~bouyer/files/bouyer\_chennai.pdf](http://www.lsv.ens-cachan.fr/~bouyer/files/bouyer_chennai.pdf)

(This is actually the framework that Vor is using in his answer. His solution makes use of a clock that is reset and a guard for the epsilon transition.)


---

### Answer by username_4 on 2011-02-15. Score: 2

Perhaps you must add a clock to the table:
 q      x              q
-------------------------
 R      r              I
 I      o              W
 W      i  clock=0     C
 C      e              S
 S      ∈  (clock>T)?  R

The S->R (reset) transition can occur only after T "ticks" has elapsed after the receive of [i]nput.
If you want the timeout to start after the [e]nd then you must reset the clock on:
 ...
 C      e  clock=0     S
 ...


---

### Answer by username_1 on 2011-02-16. Score: 0

On a more abstract level, encode events as symbols in your trace, e.g. `[T]imeout`. As far as I know, this is standard technique when modeling (possibly labeled) transition systems.

This enables you to easily reason about properties your system might have, for instance statements (in temporal logic) like "After any timeout, my machine is in state `S`".

It does not yield a good model for implementations, though.


---

