Logics for Concurrency: Structure vs Automata

Faron Moller
Computing Science Department
Uppsala University
.

Faron Moller
Uppsala University


There has been a great deal of effort spent on developing methodologies for specifying and reasoning about the logical properties of systems, be they hardware or software. Of particular concern are issues involving the verification of safety and liveness conditions, which may be of mammoth importance to the safe functioning of a system. While there is a large body of techniques in existence for sequential program verification, current technologies and programming languages permit for ever greater degrees of concurrent computation, which make for a substantial increase in both the conceptual complexity of systems, as well as the complexity of the techniques for their analysis.

One fruitful line of research has involved the development of process logics. Although Hoare-style proof systems have been successful for reasoning about sequential systems, they have only been of minor impact when primitives for expressing concurrent computation are introduced. Of greater importance in this instance are, for example, dynamic, modal, and temporal logics. Such logics express capabilities available to a computation at various points of time during its execution. Two major varieties of such logics exist: linear-time logics express properties of complete runs, whilst branching-time logics permit a finer consideration of when choices within computation paths are made. The study of such logics is now quite broad and detailed.

There is, however, a perceived dichotomy which exists in the area of temporal logic research; a divide which appears to be defined to a large extent by geography (though, as with all things, this division is far from clear-cut). On the one hand, the North American approach has exploited automata-theoretic techniques which have been studied for decades. The benefit of this is the ability to adapt theoretical techniques from traditional automata theory. Hence, for example, to verify that a particular system satisfies a particular property, one would construct an automaton which represents in essence the cartesian product of the system in question with the negation of the property in question, and thus reduce the problem to one of checking emptiness of the language generated by an automaton. One obvious drawback to this approach is the overhead incurred in constructing such an automaton: even if the system being analysed can be represented by a finite-state automaton, this automaton will typically be of a size which is exponential in its description (due to the so-called state space explosion problem), and hence this approach to the verification problem will be (at least) exponential in the worst case. Of course this approach is inapplicable to infinite-state systems unless you first introduce symbolic techniques for encoding infinite sets of states efficiently.

On the other hand, the "Eurotheory" approach to the verification problem is based more on exploiting structural properties. The essence of this approach is to work as far as possible with the syntactic system and property descriptions rather than their semantic interpretations as automata. Typically this involves the development of tableau-based proof systems which exploit congruence and decomposition properties. This allows more of a so-called "local" model checking technique which feasibly could handle even infinite-state systems, as the overhead of constructing the relevant semantic automata is avoided.

Whichever approach is considered, there are common goals which are stressed. Firstly and of utmost importance, the methodology must be faithful to the system descriptions being modelled, as well as to the intended properties being defined. The methodology must be sound with respect to its intended purpose. Of great importance as well is the ability to automate the techniques; as economically- and safety-critical systems being developed become more and more complex, the need for automated support for their verification becomes an imperative of ever greater importance. Mechanical procedures for carrying out the verification of such properties are required due to the sheer magnitude of the systems to be verified. Beyond this, such algorithms must be tractable. There will clearly be trade-offs between the expressivity of a formalism employed to define system properties, and the complexity of the verification of these properties. The verification procedures, beyond being sound, must be effective, as well as of an acceptable level of time- and space-complexity.

We thus have the following important themes appearing in the ongoing research in concurrency theory:


Faron Moller (fm@csd.uu.se)