2
$\begingroup$

I'm looking for formal statements and proofs that I can make when using SCXML statecharts. As such, I'm trying to categorize it properly.

SCXML supports hierarchical states. I believe that any hierarchical state machine can be converted into an equivalent non-hierarchical state machine. And I believe that a "simple" non-hierarchical state machine can be considered a DFA (deterministic finite automata).

SCXML is not a "simple" state machine, however:

  • Transitions between states may be guarded by arbitrary code conditions. Only one transition from an active state will be taken as a result of a single event, but which transition is taken may vary. Given this, I believe that SCXML should be considered (for certain configurations) an NFA (non-deterministic finite automata).

  • Certain transitions may be taken not in response to an event, but as soon as a condition is valid. Given this, I believe that SCXML may at times be considered an NFA with ε-moves.

  • SCXML supports not just hierarchical states, but also "parallel" (orthogonal) states. These allow the runtime to be in more than one atomic ("leaf") state simultaneously.

This last detail gives me pause, as I have not found any formal statements classifying parallel state machines. Does the introduction of concurrent parallel states break any NFA definition?

I think that it doesn't. I think that you can convert any parallel state machine into an equivalent non-parallel machine via combinatorial explosion. But I'd like to know it for sure.

$\endgroup$
  • 1
    $\begingroup$ Are you familiar with Petri nets? $\endgroup$ – Raphael Mar 6 '14 at 18:49
  • $\begingroup$ @Raphael No, I am not. $\endgroup$ – Phrogz Mar 6 '14 at 20:01
  • $\begingroup$ They are often used for modelling parallelism, so you might want to check them out. $\endgroup$ – Raphael Mar 7 '14 at 7:15
1
$\begingroup$

The paper Parallel Finite Automata for Modeling Concurrent Software Systems contains a proof and examples showing that a (non-hierarchical) parallel state machine can be converted into a non-parallel version. The technique is somewhat obvious: simply create the cartesian product of all concurrent sections and you have a DFA.

Combine with a proof that any hierarchical section of a state machine can be flattened into an equivalent non-hierarchal version, and there exists an obvious—but hard for me to formally notate—conversion process that involves flattening hierarchies and expanding parallel sections from the leaves on upwards.

The result is that any SCXML state machine can be converted into an equivalent version that contains neither hierarchy nor parallel states. At this point the state machine may be DFA, NFA, or NFA with ε-moves (depending on the transitions used), but all of these are similarly equivalent.

In summary, I believe that any SCXML state machine can be converted into an equivalent DFA, and as such the formalisms of DFA apply.

$\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.