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.