0
$\begingroup$

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

$\endgroup$
  • 4
    $\begingroup$ What is a "temporal" event? A timeout? $\endgroup$ – Raphael Feb 15 '11 at 9:33
  • 3
    $\begingroup$ 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 $\endgroup$ – DaniCL Feb 15 '11 at 10:20
  • $\begingroup$ @DaniCL, Thank you. cs.aau.dk/~srba/courses/MCS-07/TA.pdf $\endgroup$ – CMR Feb 15 '11 at 14:11
  • $\begingroup$ @DaniCL: make this an answer ? $\endgroup$ – Suresh Venkat Feb 15 '11 at 22:30
3
$\begingroup$

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

(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.)

$\endgroup$
2
$\begingroup$

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
 ...
$\endgroup$
0
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.