Formal System: Transition System Encoding(s)

[ShinyKate]

While the formal system should offer great freedom in modeling formal systems and specifying properties, most automated methods we will implement will require a specific form. To ensure that different methods can be combined and are able to exchange facts, we need to document a common way to encode transition systems using our formal system.

Not all methods might work best with the same encoding, in particular it could be useful to have both

1. an encoding based on infinite streams that uses stream-delay operators to represent registers, and
2. an encoding based on a state transition function.

Methods are also free to use other encodings internally, but we want a documented standard encoding for these two variants and make sure that we can exchange derived facts across these encodings.