IFIP Working Group 2.2 Meeting
25 - 29 September 2000, Oldenburg, Germany.

Abstracts of the talks

Wojciech Penczek
Reducing Model Checking from Multi-Valued CTL* to CTL*

A multi-valued version of CTLS* (mv-CTLS), where both the propositions and the accessibility relation are multi-valued taking values in a finite quasi-boolean algebra, is considered. A general translation from mv-CTL* to CTL* model checking is defined. An application of the translation is shown for the most commonly used quasi-boolean algebras.

Jan Rutten
A Coinductive Calculus of Component Connectors

Reo is channel-based coordination model, recently introduced by Farhad Arbab (CWI, Amsterdam), wherein complex coordinators, called connectors, are compositionally built out of simpler ones. Reo is intended as a ``glue language'' for construction of connectors that orchestrate component instances in a component-based system. The emphasis in Reo is on connectors and their composition only, not on the components that are being connected.

Here we shall present a relational model for (a fragment of) Reo, constructed in terms of streams, that is, infinite sequences. The set of all streams is a final coalgebra and therewith comes equipped with coinduction definition and proof principles. One of the crucial features of Reo is the fact that through subtle timing, various coordination patters can be established. This will be captured in our model by considering not only data streams but also so-called time streams. Thus we shall have a double benefit of our coinductive machinery: it applies both to data streams and to time streams.

Shmuel Katz
Validating Model Translations


Erik Poll
Specification of Transacted Memory in Smart Cards Using Java and JML

This talk is about a case study using the Java Modeling Language (JML) to specify a component of a smart card operating system, a so-called transacted memory.

Programs running on a smart card can be interrupted at any moment by a sudden loss of power, namely when someone removes the smart card from the card reader. Therefore the miniature operating system on the smart card has to provide support for "transactions", updates of the persistent memory of the smart card that are atomic, in the sense that any partial updates that are interrupted by a loss of power will be undone when the card start up again.

The central issue in the specification of the transacted memory is how to model the interruption of a program by a loss of power. This also affects the Hoare logic to be used to reason about programs running on the smart card.

Masami Hagiya
Abstract A+ Algorithm and Applications (Recent Work on Timed Systems)


Markus Mueller-Olm
Exact Dependence Analysis in Parallel Programs


Jos Baeten
Another Look at tau and Time: Verification on Timed Algebra


Roberto Segala
Probabilistic Automata and Compositionality

We view Probabilistic Automata as a conservative extension of Labeled Transition Systems and we show how simulation based and trace based semantics can be extended to the probabilistic framework. Although the natural extension of simulation relations is compositional, the natural extension of trace inclusion is not compositional. In this talk we show the reasons for the failure of compositionality and we describe alternative characterizations of the coarsest compositional relation that is included in trace inclusion. We identify a simple context that is sufficiently expressive to characterize the compositional relation and we provide a testing scenario that characterizes the compositional relation. Finally, we show that the compositional relation coincides with probabilistic forward simulations.

This shows that the natural extension of trace inclusion leads to a branching relation rather than to a linear relation. Although alternative linear relations that extend trace inclusion do exist, the real problem is to find meaningful linear relations, which is currently still open.

The contents of this talk include results that are joint work with Nancy Lynch and Frits Vaandrager.

Stephan Merz
Toward a Mobile TLA


Frank de Boer
A Sound and Complete Hoare logic for a Sequential Subset of Java


Mariangiola Dezani-Ciancaglini (joint work with M. Coppo, E. Giovannetti, I. Salvo)
M3: Mobility Types for Mobile Processes in Mobile Ambients

We present an ambient calculus in which some of the most known calculi of concurrency and mobility can be encoded in a natural way. The calculus comes equipped with an incremental type system which allows typing components in possibly incomplete environments. Types are intended as a way of controlling both the kind of values exchanged in communications and the access and mobility properties of processes. A type inference procedure determines the "minimal" requirements to accept a system or a component as well typed. This gives a kind of principal type.

Anders Ravn
Components


Catuscia Palamidessi
On the Expressive Power of Temporal Constraint Programming Language


Bernhard Steffen
Regular Extrapolation


Furio Honsell
Reflection on Modelling Names and Binders (Induction, Recursion and Bialgebras on Terms up to alpha-equivalence)

We model fresh names in the pi-calculus using abstractions w.r.t. a new binding operator theta. Both the theory and the metatheory of the pi-calculus benefit from this simple extension. The operational semantics of this new calculus is finitely branching. Bisimulation can be given without mentioning any constraint on names, thus allowing for a straightforward definition of a coalgebraic semantics. This is cast within a category of coalgebras over algebras with infinitely many unary operators, in order to capitalize on theta. Following previous work by Montanari and Pistore, we present also a finite representation for finitary processes and a finite state verification procedure for bisimilarity, based on the new notion of theta-automaton. Finally, we improve previous encodings of the pi-calculus in the Calculus of Inductive Constructions.
WG 2.2 (darondeau@irisa.fr)