EXPRESS 97: Abstracts of Accepted Papers

Absolute versus Relative Time in Process Algebras
by Flavio Corradini

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

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

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

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

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

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

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

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

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

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

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

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

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.