The paper presents a sound and (relatively) complete deductive proof system for the verification of CTL* properties over possibly infinite-state reactive systems. The proof system is based on a set of proof rules for the verification of basic CTL* formulas, namely CTL* formulas with no embedded path quantifiers. We first present proof rules for some of the most useful basic CTL* formulas, then present a methodology for transforming an arbitrary basic formula into one of these special cases. Finally, we present a rule for decomposing the proof of a general (non-basic) CTL* formula into proofs of basic CTL* formulas.

Enriched categories have been applied in the past to both event-oriented true concurrency models and state-oriented information systems, with no evident relationship between the two. Ordinary Chu spaces expose a natural duality between partially ordered temporal spaces (pomsets, event structures), and partially ordered information systems. Barr and Chu's original definition of Chu spaces however was for the general V-enriched case, with ordinary Chu spaces arising for V = Set (equivalently V = Poset at least for biextensional Chu spaces). We extend time-information duality to the general enriched case, and apply it to put on a common footing event structures, higher-dimensional automata (HDAs), a cancellation-based approach to branching time, and other models treatable by enriching either event (temporal) space or state (information) space.

In order to optimise maintenance and increase security, The Royal Netherlands Navy initiated the development of a multi-channel on-board data-acquisition system for its Lynx helicopters. This AIDA (Automatic In-flight Data Acquisition) system records usage and loads data on main rotor, engines and airframe. We used refinement in combination with model checking to arrive at a formally verified implementation of the AIDA system, starting from the functional requirements.

The objectives of this paper is to survey classical and recent expressive completeness results and to provide some external yardsticks by which the expressive power of temporal logics can be measured.

The pi-calculus is the paradigmatic calculus of mobile processes. With respect to previous formalisms for concurrency, most notably CCS, the most novel aspect of pi-calculus is probably its rich theory of types. We explain the importance of types in the pi-calculus on a concrete example: the termination property.

A process M terminates if it cannot produce an infinite sequence of reductions M -> M₁ -> M₂ ... Termination is a useful property in concurrency. For instance, a terminating applet, when loaded on a machine, will not run for ever, possibly absorbing all computing resources (a `denial of service' attack). Similarly, termination guarantees that queries to a given service originate only finite computations.

We consider the problem of proving termination of non-trivial subsets of CCS and pi-calculus. In CCS the proof is purely combinatorial, and is very simple. In the pi-calculus, by contrast, combinatorial proofs appear to be very hard. We show how to solve the problem by taking into account type information.