print · source · login   

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 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 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
For every stream of input values that is provided by the environment, the stream of output values that is computed by the system is the same for every run. [AH01]
This means that a system which is deterministic and output determined is behavior deterministic.
An Interface Automata in general is not behavior deterministic, but an output determined deterministic Interface Automata without internal actions is behavior deterministic. [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.
A NFA/Moore/Mealy machine is output determined and therefore a deterministic NFA/Moore/Mealy machine is also behavior deterministic.
Thus a DFA is always behavior deterministic.

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".