5
$\begingroup$

I need some help with basic definitions and intuition to understand why and how it's possible to verify systems with infinitely many states.

For example, if I consider an x86 computer, and assuming the CPU architecture is a large and finite state machine, it will have infinitely ($\aleph_0$) many possible states (sequences) it can run, so how can systems with infinitely many states be theoretically verified at all?

$\endgroup$
  • 1
    $\begingroup$ 1. I don't understand. You say "assuming the system is a finite state machine it will have infinite states". If it's a finite state machine it has finitely many states, not infinitely many... 2. What research have you done? If you just do a Google search, or search in Google Scholar, for 'infinite state verification', you will find lots of material on the subject. $\endgroup$ – D.W. Feb 14 '18 at 0:33
  • $\begingroup$ @D.W., of course I did google search before, but I didn't find any widely cited resource yet, I guess because it's new, so I need some direction on basic concept in order to be able to search and find the right things.. Regards x86 CPU I am not sure if it's infinite state machine or not. $\endgroup$ – 0x90 Feb 14 '18 at 0:42
  • $\begingroup$ I suggesting doing another search. I typed it into Google just now and found a whole bunch of papers on the topic. I don't know why you're limiting yourself to a widely cited resource; just grab some papers and start reading their introduction & related work sections. $\endgroup$ – D.W. Feb 14 '18 at 0:46
  • 1
    $\begingroup$ This is a rather broad topic... $\endgroup$ – Yuval Filmus Feb 14 '18 at 6:32
9
$\begingroup$

Infinite-state system verification is indeed a rather broad topic. First of all, all computers used nowadays can only have a finite number of states, as the amount of RAM is fixed. But that's is mainly a matter of terminology -- any verification technique that needs to iterate over all possible states is doomed from the beginning due to computation time.

Also note that you used "verification" in your title, and "to validate" in your question. These are different concepts that should not be confused. I will assume that you meant "verification".

To solve a verification problem with a large number of states, one typically constructs a proof of correctness of some sort. Such proofs do not need to refer to all possible states, rather they group sets of states by constraints that they satisfy. The description of the constraints can indeed by small, so that in the end we get a small proof.

For example consider the following function:

int comp(int parameter) {
    int p=parameter;
    if (p<0) {
        return p*p;
    } else {
        return p;
    }
}

We want to verify that the function comp never returns a negative number. If "int" is an arbitrary-length integer datatype, this program can already have an infinite number of states. To verify this program, we can perform a case split on whether "parameter" is negative or not, and then apply basic mathematical rules that we assume the integer data type to follow. What we get is a small correctness proof for an infinite-state system.

When researchers say that they work on infinite-state verification, they typically mean that they work of verifying systems in some type of modelling framework that allows to express systems with an infinite number of states - this does not mean that they can verify arbitrary such systems and their techniques are typically sound, but not complete.

$\endgroup$
  • $\begingroup$ What's the difference between verification and validation? I know the difference in the context of HW development, but not in this context. $\endgroup$ – 0x90 Feb 14 '18 at 13:30
  • $\begingroup$ In your last paragraph, assume the researchers want to verify a switch ... case(int) and for any arbitrary-length integer (namely infinite cases) what would or code they do? $\endgroup$ – 0x90 Feb 14 '18 at 13:36
4
$\begingroup$

While DCTLib's answer provides some insight in the general ideas, I think it is useful to give a more concrete example that has some use in practice.

One kind of 'infinite state system' is a labelled transition system $L$, where we describe a finite number of groups of states and transitions, but give each state a 'free' parameter from some domain, typically the natural numbers $\mathbb{N}$, and define transitions based on that parameter. We can ask whether certain proposition $P$ in the modal $\mu$-calculus hold (these include, but are not limited to CTL* and thus can encode many questions about the process the state machine represents, such as whether the process will always halt).

If we restrict these transitions such that they are 'linear process equations', we can (relatively efficiently) transform the pair $(L,P)$ into a Parameterised Boolean Equation System (PBES) $E$, such that some state $s$ is true in the solution for this system if and only if the proposition $P$ on $L$ holds on $s$.

Although we cannot always solve this system $E$, there are approaches that work reasonably well and tools that implement them. One such tool is mCRL2. This tool uses various techniques to try to solve PBES's, but most generally boil down to attempt to construct an equivalent Boolean Equation System (BES), which is the 'finite version' of the PBES and can therefore be solved using Gaussian elimination.


The method of proof graphs might also be instructive:

The idea is to pick only a finite number of states as vertices in a graph, with an explicit parameter, e.g. $X(1)$, $Y(7)$, $X(3)$. Then, we take a labelling on the vertices and a (directed) edge relation on them that models the 'dependency' between these states. If a certain property over all finite prefixes of all infinite paths on this graph holds, we call this graph a proof graph (the general structure without this property is called a dependency graph).

The nice part is that we have that a certain variable ($\approx$state) $s$ is true in the PBES if and only if there exists a proof graph containing that state!

So, we have transformed a question of potentially infinite paths (CTL^*) over an infinite system to a question of potentially infinite paths over a finite system. As all infinite paths on a finite system must eventually cycle, we can actually show that a graph is a proof graph automatically (Determining whether the proof graph exist may not be so easy, however. There is no panacea here!)

$\endgroup$

Your Answer

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

Not the answer you're looking for? Browse other questions tagged or ask your own question.