Re: RTS graph and "temporal formulas"

[optikos@verizon.net]

On Wednesday, August 21, 2013 3:04:00 PM UTC-5, Emanuel Berg wrote:
> I have an exam the 30th on RTS and there is one problem I cannot
> solve, because there is nothing on this in the material, and the
> teacher doesn't answer mails with questions.
>
> I turn to you

  You turn to the Ada-language Usenet group for a question about 1950s mathematics-nomenclature?  Oh well.  Instead of "get off my lawn", I will point you in the right direction, which generally leads away from here. :-)

>, not to solve the problem, but to explain what it
> means - once there, I hope to solve it myself.
> 
> The problem involves a graph.

Apparently, your instructor is assuming that you already know Mealy finite-state machines and their canonical notation (as opposed to Moore finite-state machines).  Most of your question is answered by http://en.wikipedia.org/wiki/Mealy_machine (as opposed to http://en.wikipedia.org/wiki/Moore_machine, which utilizes the same stimulus/response notation but on the states=vertexes instead of on the transitions=edges).  I will utilize the initialism FSA (for finite-state automaton) below.

> - there are states: circles with names (e.g., "B") and conditions
>   (x <= 10) (sometimes, the states do not have conditions)


> - one state has a double circle: is this the initial state?

 yes.  If there were a terminal state, it would be solid black, instead of white with a black perimeter.

> - there are edges

  Here you are utilizing graph-theoretic terminology.  Edges are known as transitions in Mealy & Moore FSAs (and depending on context, either transitions or arcs in Petri networks).

> between the states

  Here you revert to Mealy & Moore FSA terminology.  States are known as vertexes or vertices in graph-theoretic terminology.

> , that are directed

  All transitions in Mealy & Moore FSAs are directed.  There is only traversal as "go to" running forward in time, not untraversal as "come from" running backward in time.

> : those
>   edges are tagged: sometimes with conditions (x < 5)

  In Mealy's FSA notation, each edge may be labeled by a stimulus/response. [Note the slash; it is part of the notation.]  The Mealy FSA stays in its current state v until one of the transitions egressing v has a stimulus-constraint that matches an actual stimulus in the FSA's environmental context.  Hence, your "condition" is a stimulus.

> , sometimes
> 
>   with assignments (x := 0)

  And your "assignment" is a response actualized by traversing that transition e, proceeding to the state into e ingresses.

> , and sometimes with both (y < 0 and y
> 
>   := 0)

  Your professor should have his hand smacked for abuse of notation firmly established in the 1950s and still widely utilized in electrical engineering (and deriving from Petri nets in chemical-manufacturing plants in the 1930s).  Your professor's logical comparisons are Mealy's "leftward of the slash" for stimulus.  Your professor's ":=" is Mealy's "rightward of the slash" for response.  Apparently your professor's exposure to FSAs is 2nd hand from C-language source-code in imperative-instruction sequential software, not from seminal references in the 1950s (or the 1930s).

> - the variables (x and y are "clocks")

  Progress of monotonically-increasing measured realtime is merely yet another "sensor" from which the Mealy FSA is hooked up to the contextual environment to receive stimuli (much as your brain acquires stimuli from its five senses as sensors).  [In electrical engineering, often the sensors are merely digital-logic lines.]  Out of the potentially vast avalanche of incoming stimuli from the sensors, only the stimulus-constraints that are actionable (to progress to a different state and/or to evoke a response) at each particular transition egressing from each state (when it is the current state) are overtly stated.  When the multitude of stimulus-constraints are not actionable, that multitude is unmentioned at that transition.  Likewise, out of the multitude of responses not effected by a transition, that multitude is unmentioned at that transition.

> What does it all mean?

  It means either that you are missing a prerequisite for this class or (if this is the course of first exposure to FSAs and their brethren) that your professor has failed to introduce you to Mealy FSAs, Moore FSAs, Petri nets, Viterbi dynamic-programming algorithm, and Markov chains.  (Only the first of these 5 related concepts is utilized in Problem 7, but you should, at your leisure, study the other 4 sometime too.)

> Check out the graph here:
> http://user.it.uu.se/~embe8573/2011.pdf
> (Problem 7, the last one.)

> They also mention "temporal formulas" to describe properties of
> the system, that the graph is a model of. Do you know of a
> resource, that describes the syntax and semantics of such
> formulas?

  Formulae from temporal logic: https://en.wikipedia.org/wiki/Temporal_logic

  a branch of symbolic logic:  https://en.wikipedia.org/wiki/Symbolic_logic

> Thanks :)
> 
> 
> 
> -- 
> 
> Emanuel Berg - programmer (hire me! CV below)
> computer projects: http://user.it.uu.se/~embe8573
> internet activity: http://home.student.uu.se/embe8573