Equivalence and Refinement (3/5)

This part provides the basis for probing whether two models can replace each other - for instance if a specification (an abstraction) is in fact properly implemented by another model (a refinement). There are a number of new concepts you should understand, but it is not necessary to dive into simulation and bi-simulation (unless you want to learn more).

The material is based on parts of chapter 14 of the textbook. 

These are the important terms you should take out from this chapter:

• models as specifications (14.1): when specifications are given as very simple (but essential) models capturing only the behavior you need
• type refinement and equivalence (14.2): describing when a model B can replace a model A; there are some constraints imposed on the inputs and outputs of A and B in order to take away one of them from its environment and put the other in its place. Two important terms related to this are abstraction and refinement, illustrated in Fig. 14.1
• stronger than the above, where one only looked at the connections to the environment for A and B are language equivalence and containment (14.3, up to page 383), where one also compares the behavior of A and B.
• the language of a state machine is the set of all behaviors (all input/output sequences it can accept/generate). A great example is in Fig. 14.2. This allows us to compare machines by looking at their language (refinement, containment).
• another interesting inset is on page 384: this makes the connection between FSMs and regular languages and regular expressions, of which you may have already heard; these are extensively used in computing.

The matters of simulation and bi-simulation go even further into talking about the case of non-deterministic FSMs, which have more special behaviors. (you are not required to read this part)