I would like to understand this with an example. Also, are there other kinds of invariants related to these?
Thanks!
$\begingroup$
$\endgroup$
4
-
4$\begingroup$ Seems like homework to me. Could you explain how you came by this problem? You may want to read en.wikipedia.org/wiki/Invariant_(computer_science) and en.wikipedia.org/wiki/Loop_invariant $\endgroup$– Marcus RittNov 25, 2010 at 12:39
-
$\begingroup$ No, this isn't a homework question. I vaguely remember reading that an inductive invariant/assertion is stronger (if a predicate holds in the initial state of the system, it holds in all the reachable states) than just an invariant. But I'm not able to find any definitions in the papers. Hence the question. Any help would be appreciated. $\endgroup$– Chan LiNov 25, 2010 at 14:06
-
$\begingroup$ I think you got the right definition. For an example have look at portal.acm.org/citation.cfm?id=646485.694471 $\endgroup$– Marcus RittNov 25, 2010 at 14:56
-
1$\begingroup$ I have seen the reference you mention. The problem is this: If Inv is an invariant for a program Prog then Inv holds in all reachable states of Prog. If IInv is an inductive invariant for Prog, it holds in every initial state of Prog AND it is preserved under all the transitions, therefore it holds in all reachable states of Prog. Now, it is often mentioned that IInv -> Inv holds. But what I don't get is that why doesn't Inv -> IInv hold? Since, Inv holds in 'all' reachable states of Prog, which includes initial states, the latter should hold as well. What am I missing? $\endgroup$– Chan LiNov 25, 2010 at 15:25
Add a comment
|
2 Answers
$\begingroup$
$\endgroup$
1
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.
Program:
- Initialise: $x \gets 2$.
- Iterate: $x \gets 2x - 1$.
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.
answered Nov 25, 2010 at 17:18
-
$\begingroup$ Thanks for the example. I understand the difference now. $\endgroup$– Chan LiNov 26, 2010 at 9:41
$\begingroup$
$\endgroup$
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:
- $Init \Rightarrow I$ (I holds initially)
- $I \wedge Step \Rightarrow I'$ (if $I$ holds before a step, then it holds after the step)
- $I \Rightarrow S$ ($I$ is strong enough to establish the required property)
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$.
