EXPRESS 97: Abstracts of Accepted Papers
-------------------------------------------------------------------------------
Absolute versus Relative Time in Process Algebras
by Flavio Corradini
Abstract:
Timed process algebras are useful tools for the specification and
verification of real time systems. We study the relationships between
two of these algebras, cIpa (`Closed Interval Process Algebra')
and TCCS (`Temporal CCS'), which deal with
temporal aspects of concurrent systems by following very different
interpretations: durational actions versus durationless actions,
absolute time versus relative time,
timed functional behavior versus time and functional behavior,
local clocks versus global clocks. We show that these different choices are
not irreconcilable by presenting a simple mapping from cIpa
to TCCS which preserves the behavioral equivalences over the two
timed calculi.
-------------------------------------------------------------------------------
On Expressive Completeness of Duration and Mean Value Calculi
by Alexander Rabinovich
Abstract:
The Duration Calculus is a logic for the specification of real time
systems. DC is based on interval logic and uses real numbers
to model time.
DC was successfully applied in case studies of
software embedded systems
and was used to define the real time semantics of other
languages.
DC was extended to Mean Value Calculus in order to handle
instantaneous events.
In this paper we compare the expressive power of the propositional versions
of DC and MVC with the expressive power of monadic first order logic of order
over the reals. Our results show that PMVC is expressively
complete for
monadic first order logic of order.
We provide a characterization of
the expressive power of the propositional duration calculus.
Finally, we show that there exists at least an exponential gap between
the succinctness of PMVC (PDC) and the monadic logic.
~
-------------------------------------------------------------------------------
What is a `Good' Encoding of Guarded Choice?
by Uwe Nestmann
Abstract:
The with synchronous output and mixed-guarded choices is strictly more
expressive than the pi-calculus with asynchronous output and no choice.
More precisely, Palamidessi recently proved that there is no fully
compositional encoding from the former into the latter that preserves
divergence-freedom and symmetries.
In this paper, we present a series of deadlock-free encodings for languages
with (1) input-guarded choice, (2) both input- and output-guarded choice,
and (3) mixed-guarded choice, and investigate them with respect to
compositionality and divergence-freedom. The first and second encoding
satisfy all criteria, but various `good' candidates for the third
encoding---inspired by existing distributed implementations---invalidate
one or the other. While essentially confirming Palamidessi's result, our
study suggests that the combination of strong compositionality and
divergence-freedom is too strong for rather practical purposes.
-------------------------------------------------------------------------------
Eager, Busy-Waiting and Lazy Actions in Timed Computation
by Flavio Corradini,GianLuigi Ferrari,Marco Pistore
Abstract:
This paper develops a formal framework to describe and reason about
semantic theories which provide measures of the
efficiency in time of process behaviours. The framework relies on the
notions of reduction and observability and permits to naturally
explain the possible choices to incorporate timing information
in terms of process interaction mechanisms. The framework provides a parameteri
zed context where
well-known and new theories can be formally compared and classified by
a suitable instantiation of the parameters. Alternative SOS-based
characterizations are also provided.
-------------------------------------------------------------------------------
Process Rewrite Systems
by Richard Mayr
Abstract:
Many common formalisms for the description of infinite
state concurrent systems can be expressed by special
classes of rewrite systems.
We present a syntactic classification of these systems,
define a hierarchy of rewrite systems w.r.t.
their expressiveness and show
how common models fit into this hierarchy.
The most general and most expressive class of systems
in this hierarchy is described by a so-far unused, yet very
natural rewriting formalism. We will call these systems
process rewrite systems (PRS).
They subsume Petri nets, PA-Processes and pushdown processes and
are strictly more expressive than any of these formalisms.
We show that in spite of being very expressive, PRS are
still not Turing-powerful, because the reachability problem
is still decidable.
-------------------------------------------------------------------------------
Domain Equations for Probabilistic Processes
by Christel Baier, Marta Kwiatkowska
Abstract:
In this paper we consider Milner's calculus CCS enriched by
a probabilistic choice operator. The calculus is given operational
semantics based on probabilistic transition systems. We define
operational notions of preorder and equivalence as probabilistic
extensions of the simulation preorder and the bisimulation equivalence
respectively. We extend existing category-theoretic techniques for
solving domain equations to the probabilistic case and give two
denotational semantics for the calculus. The first, ``smooth'',
semantic model arises as a solution of a domain equation involving the
probabilistic powerdomain and solved in the category CONT of
continuous domains. The second model also involves appropriately
restricted probabilistic powerdomain, but is constructed in the
category CUM of complete ultra-metric spaces, and hence is necessarily
``discrete''. We show that the domain-theoretic semantics is fully
abstract with respect to the simulation preorder, and that the metric
semantics is fully abstract with respect to bisimulation.
-------------------------------------------------------------------------------
Process Creation and Full Sequential Composition in a Name-Passing Calculus
by Thomas Gehrke,Arend Rensink
Abstract:
This paper presents the underlying theory for a process calculus
featuring process creation and sequential composition,
instead of the more usual parallel composition and
action prefixing, in a setting where mobility is achieved by
communicating channel names. We discuss the questions of scope and
name binding, raised by the interaction of mobility and sequential
composition. Substitution of names is integrated as a syntactic
operator in the calculus. We present an axiomatic theory for the
calculus and show its soundness and completeness w.r.t. bisimulation
equivalence.
-------------------------------------------------------------------------------
Relating Semantic Models for the Object Calculus: Preliminary report
by Luca Aceto, Hans Huttel, Anna Ingolfsdottir, Josva Kleist
Abstract:
Abadi and Cardelli have investigated several versions of the object calculus, a
calculus for describing central features of object-oriented programs,
with particular emphasis on various type systems. In this paper we
study the properties of a denotational semantics due to Abadi and
Cardelli vis-a-vis the notion of observational congruence for the
first order object calculus with subtyping. In particular, we prove that the denotational
semantics based on partial equivalence relations is correct with
respect to observational congruence. By means of a counter-example, we
argue that the denotational model is not fully abstract with
respect to observational congruence. In fact, the model is able to
distinguish objects that have the same behaviour in every context.
-------------------------------------------------------------------------------
Specification in CTL+Past, Verification in CTL
by F. Laroussinie, Ph. Schnoebelen
Abstract:
We describe PCTL, a temporal logic extending CTL with connectives allowing
to refer to the past of a current state. This incorporates the new N,
``From Now On'', combinator we recently introduced [LS95].
PCTL has branching future but determined, finite and cumulative past. We
argue this is the right choice and we show, through an extensive example,
that PCTL is a more convenient specification language than CTL.
Finally, we demonstrate how a translation-based approach allows
model-checking specification written in NCTL, a fragment of PCTL.
-------------------------------------------------------------------------------
On the Turing--Equivalence of Linda Coordination Primitives
by Nadia Busi, Roberto Gorrieri, Gianluigi Zavattaro
Abstract:
We introduce a process algebra L comprising the coordination
primitives of Linda (asynchronous communication via a shared data
space, read operation, non-blocking test operators on the shared space).
We compare two possible semantics for the output operation, following
two different intuitions expressed in Linda reference
manual [SCA95]. The former,
we call ordered, defines the output as an operation that returns
when the message has reached the shared data space; the latter, we call
unordered, returns just after sending the message to the tuple space.
The process algebra under the ordered semantics is Turing powerful, as
we are able to program a Random Access Machine.
The main result of the paper is that the process algebra under the
unordered semantics is not Turing powerful. This result is achieved
by resorting to a net semantics in terms of
contextual nets (P/T nets with inhibitor and read arcs), and
showing that there exists a deadlock-preserving simulation
of such nets by finite P/T nets (a formalism where termination is
decidable).
-------------------------------------------------------------------------------
Bisimilarity of Open Terms
by Arend Rensink
Abstract:
Traditionally, in process calculi, relations over open terms, i.e., terms
with free process variables, have been defined as extensions of closed-term
relations: two open terms are related if and only if all their closed
instantiations are related. Working in the context of bisimulation, in this
paper we study a different approach: we define semantic models for open
terms, so-called conditional transition systems, and define
bisimulation directly on those models. It turns out that this can be done in
two different ways, giving rise formal hypothesis and {\em
hypothesis-preserving} bisimilarity (denoted \fhbis and \hpbis,
respectively). As far as we have seen, only the former has been studied
before in the literature. For open terms, we have (strict) inclusions
\fhbiso \subset \hpbiso \subset \cibiso (the latter denoting the standard
extension of bisimilarity to open terms); for closed terms, the three
coincide. Each of these relations is congruent in the usual sense. We also
give an alternative characterisation of \hpbis in terms of non-conditional
transitions. Finally, we study the issue of recursive congruence: we
give general theorems for the congruence of each of the above variants with
respect to the recursion combinator, where, however, the results we achieve
for \fhbis and \hpbis hold in a more general setting than the one for
\cibis.
-------------------------------------------------------------------------------
Confluent Rewriting of Bisimilar Term Graphs
by Zena M. Ariola, Jan Willem Klop, Detlef Plump
Abstract:
We present a survey of confluence properties of (acyclic) term graph
rewriting. Results and counterexamples are given for four different
kinds of term graph rewriting: besides plain applications of rewrite
rules, extensions with the operations of collapsing and copying, and
with both operations together are considered. Collapsing and copying
together constitute bisimilarity of term graphs. We establish sufficient
conditions for, and counterexamples to, confluence modulo bisimilarity
over various classes of rewrite rules.
-------------------------------------------------------------------------------
Zero-Safe Nets, or Transition Synchronization Made Simple
by Roberto Bruni, Ugo Montanari
Abstract:
In addition to ordinary places, called stable, zero-safe nets
are equipped with zero places, which in a stable marking cannot
contain any token. An evolution between two stable markings, instead,
can be a complex computation called stable transaction, which
may use zero places, but which is atomic when seen from stable places: no
stable token generated in a transaction can be reused in the same
transaction. Every zero-safe net has an ordinary Place-Transition net as
its abstract counterpart, where only stable places are mantained, and
where every transaction becomes a transition. The two nets allow us to
look at the same system from both an abstract and a refined viewpoint.
To achieve this result no new interaction mechanism is used, besides
the ordinary token-pushing rules of nets. The refined zero-safe nets
can be much smaller than their corresponding abstract P/T nets, since
they take advantage of a transition synchronization mechanism. For
instance, when transactions of unlimited length are possible in a zero
safe net, the abstract net becomes infinite, even if the refined net
is finite. In the second part of the paper two universal constructions
- both following the Petri nets are monoids approach and the
collective token philosophy - are used to give evidence of the
naturality of our definitions. More precisely, the operational
semantics of zero-safe nets is characterized as an adjunction, and the
derivation of abstract P/T nets as a coreflection.
-------------------------------------------------------------------------------