Working Group 2.2
25 - 29 September 2000, Oldenburg, Germany.
Abstracts of the talks
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,
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.
Reducing Model Checking from Multi-Valued CTL* to CTL*
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.
A Coinductive Calculus of Component Connectors
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.
Validating Model Translations
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
Specification of Transacted Memory in Smart Cards Using Java and JML
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.
Abstract A+ Algorithm and Applications (Recent Work on Timed Systems)
Exact Dependence Analysis in Parallel Programs
Another Look at tau and Time: Verification on Timed Algebra
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
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
Probabilistic Automata and Compositionality
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.
Toward a Mobile TLA
Frank de Boer
A Sound and Complete Hoare logic for a Sequential Subset of Java
(joint work with M. Coppo, E. Giovannetti, I. Salvo)
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
This gives a kind of principal type.
M3: Mobility Types for Mobile Processes in Mobile Ambients
On the Expressive Power of Temporal Constraint Programming Language
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
Reflection on Modelling Names and Binders (Induction, Recursion and
Bialgebras on Terms up to alpha-equivalence)