I would like to understand this with an example. Also, are there other kinds of invariants related to these?
Theoretical Computer Science Stack Exchange is a question and answer site for theoretical computer scientists and researchers in related fields. It only takes a minute to sign up.Sign up to join this community
I don't know anything about the topic, so let me try to give a very simple example and let's see what others say.
Now "$x > 0$" is an invariant. It certainly holds initially and after each iteration.
However, it is not an inductive invariant: merely knowing that $x > 0$ before an iteration is not sufficient to guarantee that $x > 0$ after the iteration. After all, if $x > 0$ is all that we know, then we might have $x = 0.1$ before an iteration and thus $x < 0$ after the iteration.
On the other hand, something like "$x > 1$" is an invariant and also an inductive invariant. It is easy to check that if $x > 1$ before an iteration, then also $x > 1$ after the iteration.
Just to expand on Jukka's excellent answer, the question of finding invariants usually arises when trying to establish safety properties. A safety property $S$ is a property that we wish for the system or program to never violate. A safety property that holds at all reachable states is (an) invariant. A way to show that $S$ is indeed invariant is to find an inductive invariant (i.i.) $I$ that satisfies three conditions:
If $S$ is already an i.i. then we are done. Typically however it isn't. Thats where the fun begins. In the example given above, we may want to ensure that $x$ is always positive, and make $x>0$ a safety property. This safety property is also invariant. It is however not an i.i. An i.i. for this problem is $x>1$.
The strongest inductive invariant corresponds to (characterizes) exactly the reachable set. (The reason False which is the strongest possible property can't be an i.i. is due to the first condition above). For the example above, the property $J(x) \equiv \exists i \geq 0 \cdot x = 1 + r^i$ characterizes all the reachable states and its easy to verify that it is also an i.i. for the safety property $x>0$. It is therefore the strongest i.i. But finding the strongest i.i. in general is not easy. Hence we settle for a larger set (weaker property, also called an over-approximation) that still holds in all the reachable states but may include additional states that we don't care about. However all its states including unreachable ones are still contained in the safety property. If $II1$ is a stronger i.i. than $II2$ and $R$ is the reachable set then the following relationship always holds: $R \subseteq II1 \subseteq II2 \subseteq S$.