This category is for discussing information flow properties based on totally ordered sequences of messages (refining the partial order of messages in a message sequence chart). The relation to information flow control is as follows.[1]
– An information flow property is a hyperproperty of the system.
– An information flow control mechanism is an enforcement mechanism that ensures the behavior of a system satisfies an information flow property.
Often, we may want to consider models that are more structured than just sequences of actions.