I'm doing the exercises from the first chapter of the book "Temporal Verification of Reactive Systems Safety" by Manna and Pnueli. However I find very difficult to solve the point c of problem 0.2.

At point a of problem 0.2 they introduce the program $ANY{-}NAT$. This program has the following propoerties:

  • All its computations terminate
  • For every $n \in \mathbb{N}$ there exist a computation that, when the program terminates, has $y = n$.

These properties are obtained by using parallel composition of processes (they ask to informally show these properties).

The point b asks to write a single process program that behaves like $ANY{-}NAT$. And I've done so, using the select operation to simulate interleaving and using compassion to exclude infinite runs from being valid computations.

In point c they ask to prove that no single-process program with only just transitions can have the semantics of $ANY{-}NAT$. The idea is that without compassion you cannot force termination and hence either the program only produce a finite number of outputs or it has a divergent computation.

But, how do I prove that? In particular, is there an elegant way to prove this?

What I was thinking was arguing that such a program must be of the form:

$$ \begin{array}{c} I_0 \\ \textbf{while}~C_1~\textbf{do}~\ldots S_{1,1}~\textbf{or}~\cdots~\textbf{or}~S_{1, n_1} \ldots \\ I_1 \\ \vdots \\ I_{k-1} \\ \textbf{while}~C_k~\textbf{do}~\ldots S_{k, 1}~\textbf{or}~\cdots~\textbf{or}~S_{k, n_k} \ldots \\ I_k \\ \end{array} $$

where all the instructions in $I_i$ must always terminate and the loops $\textbf{while}~C_i$ have a non deterministic number of iterations, i.e. their condition $C_i$ "depends" on some select instruction inside the loop body.

This is true because the program is non deterministic and must be able to produce all numbers in $\mathbb{N}$, and so it must have at least one loop. Moreover this loop must have a non deterministic number of iterations otherwise it wouldn't be able to produce all naturals.

Now I'd like to argue that, if no compassion transition is allowed, then any such program could avoid executing the correct sequences of istructions $S_{i, j}$ that make the loop terminate and thus have an infinite computation.

However the whole thing seems rather ugly. Moreover it's not strictly true that such loops are at top level, they could be contained inside other loops that always terminate in a finite number of iterations etc. etc.

In other words I have big doubts on whether this is the correct way to go.

I believe there could be a proof that doesn't require considering the program structure at all but simply consider the possible runs of such a program and, by arguments about justice/compassion, argue that any such program must have an infinite computation.

Something like: consider the tree of all runs of such a program $P$. Since it is finitely-branching and its infinite then by Konig's lemma there must be an infinite run. Now (argument) so such a run is a valid computation and hence the program can diverge and it cannot be equivalent to $ANY{-}NAT$.

How would you fill the (argument) there? One thing that bothers me is that there could be infinitely many infinite runs, which, I find, invalidate some of the reasoning I'm trying to do about having a run from which an infinite number of finite paths must generate an infinite number of values.

  • $\begingroup$ I don't understand your references to "justice" and "compassion". Are these technical terms I'm not familiar with? $\endgroup$ – David Richerby May 16 '15 at 11:13
  • 1
    $\begingroup$ @DavidRicherby Justice means weak fairness: if a transition is always enabled from a certain time onwards then, at a certain point, it must be executed (this also implies that it is executed an infinite number of times). Compassion means: if a transition is enabled an infinite number of times (but may be disabled at times) then it must be executed an infinite number of times. My question presumes you are familiar with the first part of the first chapter of that book where the fair transition systems are defined and the semantics of SPL is given. I can't copy&paste the whole chapter here... $\endgroup$ – Bakuriu May 16 '15 at 11:18
  • $\begingroup$ "I can't copy&paste the whole chapter here..." Of course. Thanks for giving the context. $\endgroup$ – David Richerby May 16 '15 at 11:59

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.