System properties
System properties are properties which are described in the system model's entities. For a blackbox system one can claim a system property, though only for a whitebox system which is
described by a model we can express a system propery explicitly in its model's entities.
Below we define several system properties which are taken from [AW10], [Tre08] and [AH01] and when needed generalized.
For labelled transition systems, which only have observable and internal actions, we have the properties:
- Action enabled
- The system always allows any observable action a.
Formal: for each state q ∈ Q and for each action a ∈ L there is at least one outgoing transition of q with observable action a.
- Action deterministic
- For each state there is at most one outgoing transition for a specific observable action.
Formal: for each state q ∈ Q and for each observable action a ∈ L there is at most one outgoing transition of q with observable action a.
- Deterministic
- For every possible trace of observable actions, the state of the system after the trace is the same for every run of the trace. Deterministic is short for state deterministic.
An action deterministic system doesn't has to be deterministic because an internal transition can bring the system to a different state.
For systems with inputs, outputs and possibly internal actions we have the properties:
- Active
- The system has always the possibility to do an output.
An interface automaton is active when each state has at least one outgoing output transition.
Formal: for each state q ∈ Q there is at least one outgoing transition of q with an output action o ∈ O.
DFA,NFA,Moore and Mealy machines are by definition not active, but they are reactive.
- Reactive
- The system has only the possibility to do an output after an input from the environment.
DFA,NFA,Moore and Mealy machines are by definition reactive, because they need an input to trigger a transition to another state which only then causes an output to happen.
- Input enabled
- The system always allows any input i from the environment.
Formal: for each state q ∈ Q and for each action i ∈ I there is at least one outgoing transition of q with input action i.
- Output determined
- The system does not have a choice in the output it can do.
An interface automaton is output determined when each state has at most one outgoing output transition.
Formal: for each state q ∈ Q there is at most one outgoing transition of q with an output action o ∈ O.
DFA,NFA,Moore and Mealy machines are by definition output determined.
- Input deterministic
- The system behaves deterministic for an input.
Each state has at most one outgoing input transition for input action i.
Formal: for each state q ∈ Q and for each action i ∈ I there is at most one outgoing transition of q with input action i.
- Output deterministic
- The system behaves deterministic for an output.
Each state has at most one outgoing output transition for output action o.
Formal: for each state q ∈ Q and for each action o ∈ O there is at most one outgoing transition of q with output action o.
- Deterministic
- For every possible trace of inputs and outputs, the state of the system after the trace is the same for every run of the same trace. Deterministic is short for state deterministic.
This means that a system which is input and output deterministic and does not have internal transitions is deterministic.
However a deterministic system doesn't has to be behavior deterministic.
NFA,Moore and Mealy machines are reactive systems meaning that an output only occurs after an input. Therefore an input deterministic NFA/Moore/Mealy machine is also deterministic in output. Hence an input deterministic NFA/Moore/Mealy machine is a deterministic NFA/Moore/Mealy machine. Remember that Moore and Mealy machines have by definition no internal transitions.
- Behavior deterministic
- The observed behavior by the system for a stream of input values that is provided by the environment is the same for every run.
That is for every stream of input values that is provided by the environment, the stream of output values that is computed by the system is unique. [AH01]
This means that, if for a given a set of inputs you can predict the outputs of the system by a single path through the model, then the system is behavior deterministic.
Behavior deterministic is what people in general think you mean when you say something is deterministic.
A DFA, a deterministic Mealy and a deterministic Moore machine are all behavior deterministic.
An Interface Automata in general is not behavior deterministic, but an output determined deterministic Interface Automata without internal actions is behavior deterministic under a stronger notion of observation where we make quiescence observable. That is we allow the observer either directly send a new input or to just wait some time to see what the system does. We assume that if the system does not produce an output within some fixed time then it will never produce an output. So we extend the input alphabet with a fresh delay action to give the system the opportunity to either perform its next output or when it cannot do an output to be explicitly quiescent. Thus an output is only observable when doing a fresh delay input, and therefore making the output behaviour predictable for an output determined deterministic interface automaton. [AW10]
Note that an Interface Automata must also be output determined next to output deterministic, because only output deterministic still allows the system to output several different outputs in a single state so that a different run can give a different output.
Above definitions can also be applied for extended statemachines when actions also have data parameters. Sentences like "at most one input" should then be read as "at most one input for which the guard is enabled".
