Reasoning about Reactive Systems

The main concern of this thesis is the formal reasoning about reactive systems.

We first consider the automated verification of safety properties of finite systems. We propose a practical framework for integrating the behavioural reasoning about distributed reactive systems with model-checking methods. We devise a small self-contained theory of distributed reactive systems including standard concepts like implementation, abstraction, and proof methods for compositional reasoning. The proof methods are based on trace abstractions that relate the behaviours of the program with the specification. We show that trace abstractions and the proof methods can be expressed in a decidable Monadic Second-Order Logic (M2L) on words. To demonstrate the practical pertinence of the approach, we give a self-contained, introductory account of the method applied to an RPC-memory specification problem proposed by Broy and Lamport. The purely behavioural descriptions which we formulate from the informal specifications are written in the high-level symbolic language FIDO, a syntactic extension of M2L. Our solution involves FIDO-formulas more than 10 pages long. They are translated into M2L-formulas of length more than 100 pages which are decided automatically within minutes. Hence, our work shows that complex behaviours of reactive systems can be formulated and reasoned about without explicit state-based programming, and moreover that temporal properties can be stated succinctly while enjoying automated analysis and verification.

Next, we consider the theoretical borderline of decidability of behavioural equivalences for infinite-state systems. We provide a systematic study of the decidability of non-interleaving linear-time behavioural equivalences for infinite-state systems defined by CCS and TCSP style process description languages. We compare standard language equivalence with two generalisations based on the predominant approaches for capturing non-interleaving behaviour: pomsets representing global causal dependency, and locality representing spatial distribution of events. Beginning with the process calculus of Basic Parallel Processes (BPP) obtained as a minimal concurrent extension of finite processes, we systematically investigate extensions towards full CCS and TCSP. Our results show that whether a non-interleaving equivalence is based on global causal dependency between events or whether it is based on spatial distribution of events can have an impact on decidability. Furthermore, we investigate tau-forgetting versions of the two non-interleaving equivalences, and show that for BPP they are decidable.

Finally, we address the issue of synthesising distributed systems - modelled as elementary net systems - from purely sequential behaviours represented by synchronisation trees. Based on the notion of regions, Ehrenfeucht and Rozenberg have characterised the transition systems that correspond to the behaviour of elementary net systems. Building upon their results, we characterise the synchronisation trees that correspond to the behaviour of active elementary net systems, that is, those in which each condition can always cease to hold. The identified class of synchronisation trees is definable in a monadic second order logic over infinite trees. Hence, our work provides a theoretical foundation for smoothly combining techniques for the synthesis of nets from transition systems with the synthesis of synchronisation trees from logical specifications

Reasoning about Reactive Systems

Abstract: