Process Algebra: Open Problems and Future Directions July 21-25, 2003 University of Bologna Residential Center Bertinoro (Forlì), Italy

Titles, Abstracts and Slides of Talks

Roberto Amadio, Laboratoire d'Informatique Fondamentale de Marseille, Université de Provence. "Max-plus Quasi-interpretations".

Abstract: Quasi-interpretations are a tool to bound the size of the values computed by a first-order functional program (or a term rewriting system) and thus a mean to extract bounds on its computational complexity. We present some basic results on the synthesis of quasi-interpretations selected in the space of polynomials over the max-plus algebra of non-negative rationals. Then we discuss some preliminary ideas on how to adapt these results to Kahn networks.

Slides for the talk (PDF).

Jos Baeten, Eindhoven University of Technology. "Over Thirty Years of Process Algebra: Some History and Some Future Directions.".

Abstract: We discuss what I mean by a process algebra and look at some history. We mention the work of Bekic, Milner, Hoare, Bergstra & Klop and others. We briefly discuss the trends in the past decades, and mention some possible future directions.

Slides for the talk (Powerpoint).

Jan Bergstra, University of Amsterdam. "Polarized Process Algebra".

Abstract: Polarized process algebra is a very simplified process algebra claimed to be of use for defining the semantics of sequential program notations by means of so-called projection semantics. The connection between program notations and polarized processes is determined via a program algebra. Program equivalence is described in terms of polarized processes. Further the halting problem is analysed as an issue regarding behaviors of programs. So-called client server composition is defined on polarized processes, leading to a definition of emulation between programs.

Regarding applications an attempt is made to identify a program algebra especially suited for giving a semantics to CIL (the intermediate language of the .NET world) and the feasibility of projection semantics in the .NET setting is discussed.

Marco Bernardo, Università di Urbino. "On the Usability of Process Algebra: An Architectural View".

Abstract: Despite of their compositional nature, unfortunately process algebra (PA) is difficult to use in practice. In order to alleviate this problem, we propose to enrich PA in a way that makes it suitable to work with at the software architecture level of design. On the modeling side, our proposal consists of adding on top of PA some linguistic constructs that support a component oriented way of describing families of systems sharing some constraints both on their component internal behavior and on their topology. On the analysis side, our proposal is based on detecting mismatches that may arise when assembling many components together, and on providing diagnostic information that should serve as a useful feedback to pinpoint the components responsible for the mismatches. In the functional verification case, we show a sufficient condition for a component oriented proof of deadlock freedom, which is based on weak bisimulation and provides some diagnostic information in case of failure. In the performance evaluation case, we show that a combined use of stochastic PA and queueing networks allows us to compute some frequently occurring performance indices both at the component level and at the system level. This can be exploited to implement a methodology to quickly compare alternative designs of the same system or to rapidly improve some frequently occurring performance indices for a specific design.

Slides for the talk (gzipped, postscript file).

Mario Bravetti,Università di Bologna. "Axiomatizing Process Algebra with Time: Real-time and Stochastic-time".

Abstract: First, we show how to completely axiomatize weak bisimulation equivalence in the presence of a basic notion of priority, which is needed to express time in process algebra, over sequential recursive systems. Then we show that the peculiar kind of priority (which is neither actually global nor local to processes) used in the Hennessy-Regan discrete real-time process algebra allows for the axiomatization of such an algebra by exploiting the initial axiomatization. A modification of the Hennessy-Regan algebra and the adoption of exponentially distributed delays instead of simple ticks (discrete delays) allows for the axiomatization of a (continuous) Markovian stochastic process algebra which is a variant of the calculus of Interactive Markov Chains. Finally, we show that by adopting delays with an actual duration (represented in the semantics by clock start and clock termination events) it is possible to exploit the approach above to axiomatize both a continuous real-time process algebra and, with a little extension, a (continuous) stochastic process algebra with general distributions: a variant of the calculus of Interactive Generalized Semi-Markov Processes. The axiomatizations in the last step are based on new techniques that we introduce for the complete axiomatization of ST semantics (used for delay prefixes in the algebra above) in the presence of recursion. In particular we show three techniques to express ST semantics: the static name, the dynamic name and the stack technique.

Slides for the talk (PDF).

Ilaria Castellani, INRIA Sophia-Antipolis. "Axiomatizing Weak Equivalences for Asynchronous Calculi ".

Abstract: When defining behavioural equivalences for asynchronous process calculi such as the asynchronous pi-calculus, where message emission is non blocking, it is appropriate to assume that the notion of observation is itself asynchronous. This is in keeping with the view, underlying most semantic theories for process calculi, that the observer is a particular kind of "witness" process.
Clearly, an observer whose outputs are asynchronous loses some control over the inputs of observed processes. This is the idea that led to the definition of asynchronous bisimulation and asynchronous testing equivalence for asynchronous calculi.
For asynchronous CCS and the asynchronous pi-calculus, alternative behavioural characterisations of the various equivalences have been given along classical lines. On the other hand, complete axiomatisations have only been worked out for strong asynchronous bisimulation and asynchronous may testing. For weak asynchronous bisimulation and for asynchronous must testing, only a set of sound laws is known so far.
In the talk I will review the existing work and elaborate on the kind of problems one has to face when trying to derive complete axiomatisations for the latter equivalences. Hopefully, I'll be able to indicate some news tracks of investigation.

Slides for the talk (PDF).

Flavio Corradini, Università degli Studi di L'Aquila. "On Equational Axiomatizations of Milner Bisimulation in Kleene Stars".

Abstract: The talk is concerned with (non deterministic) regular expressions and Milner bisimulation. We present a finite complete equational axiomatization for bisimulation equivalence over a significant subset of regular expressions; those that satisfy the so-called hereditary non-empty word property in star-contexts. This condition, however, does not lead to equational axiomatization for the classical (deterministic) interpretation. We conjecture that the set of regular expressions with the hereditary non-empty word property is the largest language for which bisimulation admits a finite equational axiomatization. The zero object deserves a special care.

Rocco De Nicola, Università di Firenze. "Open Nets, Contexts and Their Properties".

Abstract: Klaim (A Kernel Language for Agents Interaction an Mobility) is a simple formalism that can be used to model and program mobile systems; it allows programmers to concentrate on the distributed structure of programs while ignoring their precise physical allocations. Primitives are designed to provide the programmer with the distributed infrastructure for handling all issues related to physical distribution, scoping and mobility of processes. Klaim is based on process algebras but makes use of Linda-like asynchronous communication and models distribution via multiple shared tuple spaces. Tuple spaces and processes are distributed over different localities and the classical Linda operations are indexed with the location of the tuple space they operate on. For establishing properties of Klaim Nets, we have designed a logic that is based on HML but has richer action predicates that permit reasoning on the information transmitted over the net and has state formulae for testing the presence of specific tuples at given localities.
A weakness of our approach is that, in order to use Klaim and its associated logic to establish nets properties one needs to have a full implementation of the system under consideration. Obviously, this is a very strong assumption when dealing with wide area networks, because very often, only a component of the system is known; one has only a limited knowledge of the overall context in which the component is operating. In the talk, after introducing Klaim and its logic, we shall present a framework for specifying contexts for Klaim nets. By relying on a notion of agreement, defined in term of behavioural equivalence, of a net N with respect to a context specification C[..], we shall guarantee that if a context specification is partially instantiated (implemented) as a concrete net while guaranteeing agreement between specification and implementation all formulae satisfied by the more abstract description are satisfied also by the refined one. More specifically we shall prove that if C[N] satisfies a formula f and C'[N'||N] is a refinement of C[N] then also C'[N'||N] satisfies f.
This is joint work with Michele Loreti.

Slides for the talk (PDF).

Rob van Glabbeek. "Liveness respecting semantics".

Abstract: In this talk I investigate, in a setting without real-time or probabilities, which semantical equivalences respect liveness properties. Many semantics proposed in the literature do not, which makes them less suitable for verification purposes. In fact, I argue that in interleaving semantics liveness properties are preserved only in the presence of global fairness assumptions. I'll give an overview of the interleaving semantics that respect liveness, and discuss their complexity and equational axiomatizations. When global fairness assumptions are not warranted, non-interleaving semantics are needed to preserve liveness properties in the presence of a parallel composition. I speculate about the possibilities in this regard.

Slides for the talk (PDF).

Jan Friso Groote, Eindhoven University of Technology. "The Need for Proof Methodologies".

Abstract: If one tries to prove the correctness of protocols specified using a process algebraic formalism then this turns out to be unexpectedly hard. After more than a decade of experience it is more obvious than ever that the mathematics of process algebraic verification still has to be developed. Existing methodologies are Invariants, Cones and Foci, Confluence, N-process theorem and Coordinate Transformations, all necessary elements for the vocabulary of a process algebraist. As most people may not know these, I will explain them. But this may still not be enough. Development by transformation, deriviation from modal formulas, or what have you, might be needed in the future. It is unclear to me how I must currently proceed to have these techniques being detected and developed.

Slides for the talk (Powerpoint).

Holger Hermanns, University of Twente. "Axiomatising Divergence".

Abstract: We develop sound and complete axiomatisations for the divergence sensitive spectrum of weak bisimulation equivalence. The axiomatisations can be extended to a considerable fragment of the linear time -- branching time spectrum with silent moves, solving some of the open problems posed in the seminal paper by Rob van Glabbeek on this spectrum.

Slides for the talk (gzipped PDF).

Joost-Pieter Katoen, University of Twente. "On the Design of the Stochastic Process Algebra MoDeST"

Abstract: The philosophy behind the modeling language MoDeST is to have a single specification that addresses various aspects of the system under consideration. It is a single-formalism, multi-solution approach. Analysis takes place by extracting simpler models from MoDeST specifications, tailored to the proper- ties of interest. For instance, for checking reachability properties, one may ``distill'' an automaton and feed it into an existing model checker. For analysis of QoS aspects, stochastic models are extracted and analyzed by numerical engines or discrete event simulators.
MoDeST has a stochastic process algebra ``core'' and contains features such as simple data types, structuring mechanisms like composition and abstraction, atomic statements to control the granularity of transitions, non-deterministic and probabilistic branching and timing. MoDeST may thus be viewed as an overarching notation for a wide spectrum of models, ranging from finite-state automata, to (probabilistic) timed automata, and models like stochastic automata (or GSMPs) and Markov decision processes.
The prototype tool-suite MOTOR (MoDeST Tool enviRonment) supports the modeling and analysis of MoDeST models. It contains an interactive simulator and a state-space generator. The simulator allows to traverse the (infinite) tree of possible behaviors of the MoDeST specification under study and supports real-time, discrete probabilistic branching, and probabilistic timing.
This talk reports on the semantics of MoDeST, its current tool support and its future perspectives.

Slides for the talk (gzipped, postscript file).

Anna Labella, Università di Roma "La Sapienza". "Process Algebras and Arithmetics".

Abstract: The category Tree, that we have studied as a model of behaviours of non-deterministic parallel agents, is equipped with two kinds of Natural Numbers Object The first one is the usual symmetric universal object, the other one is definable analogously after replacing categorical product by concatenation. For this reason, the second it is only a left natural numbers object. Nonetheless one can, accordingly, develop two kinds of recursion, one for the first one, one for the second. More interesting is the fact that both objects can be expressed through regular expressions, as solutions of right linear hierarchical systems. Thus, we have that they belong to the smaller category of non-deterministic regular normal forms Tree* . Since Tree* is a pretopos, we can still develop there two kinds of arithmetics and recursion. Interestingly enough, these constructions trivially collapse when considering the classical interpretation of regular expressions as regular languages, essentially because of the equivalence of terms like 1 and 1*.
This is joint work with Rocco De Nicola.

Slides for the talk (PDF).

Kim G. Larsen, BRICS and Aalborg University. "Optimal Scheduling and Priced Timed Automata".

Abstract: Recently timed automata technology has been successfully applied to the modelling and solution of several real time scheduling problem. Compared with traditional approaches -- such as LP and MILP -- the use of an automata based approach makes it much simpler to model complex logical constraints. Also the solution method -- based on reachability analysis and model checking -- seem very different (and efficiency-wise incomparable) to traditional approaches.

In order to address optimal scheduling problems the basic timed automata model has been extended with one additional continuous variable -- cost -- which may grow with different rates in different locations.

In the talk we shall introduce investigate the resulting model Priced Timed Automata. We shall review the first positive results for this model, namely computability of optimal reachability as well as datastructures allowing for efficient computability. Also, we present ongoing work on optimal infinite schedules as well as optimal dynamic scheduling using Priced Timed Automata with controllable as well as uncontrollable transitions. To address the ever-present problem of state-explosion a notion of refinement between Priced Timed Automata is introduced allowing (optimal) scheduling problems too complicated for analysis to be replaced with simpler and more abstract ones.

Bas Luttik, Vrije Universiteit, Amsterdam. "Unique Parallel Decomposition".

Abstract: In the realm of process theory, unique decomposability with respect to parallel composition is crucial in the proofs that bisimulation is decidable for normed BPP and for normed PA. It also plays an important role in the analysis of axiom systems involving an operation for parallel composition (e.g., in the proof that PA is finitely based).
We discuss a general unique decomposition theorem for a class of ordered commutative monoids and indicate how it can be used to establish the unique decomposition property with respect to parallel composition in a variety of process theories. We shall also discuss how we intend to employ the unique decomposition property as a tool in the analysis of several ACP-related axiom systems.

Slides for the talk (PDF).

Dale Miller, INRIA/Futurs/Saclay and LIX, Ecole Polytechnique. "Encryption as an Abstract Datatype".

Abstract: Specifying and analyzing security protocols is notoriously difficult on many levels. One approach to dividing up the work of such analysis uses what is commonly called the Dolev-Yao model of security execution and attack. It has been observed by various people recently, that this abstraction can be captured in large part by multiset rewriting augmented with a mechanism for generating new symbols to be used for nonces and session and encryption keys. Proof search (logic programming) in linear logic can capture both multiset rewriting and the generation of new symbols via the proof theoretical device of eigenvariables. We examine an encoding of security protocols into higher-order linear logic. In particular, we shall find that multiset rewriting and a simple asynchronous processes calculus can be seen as logically equivalent, that encryption can be understood as an abstract data type, and that an interpolation theorem can help in characterizing communications between principals and intruders. Given that linear logic and proof search can capture the operational semantics of protocols in a high-level fashion, we propose using this level of abstraction as a setting to explore common security properties.

Slides for the talk (PDF).

Ugo Montanari, Università di Pisa. "Tile Systems for Process Algebras".

Abstract: Tiles [5] are logical sequents¹ which represent transition steps of system components. They are equipped with horizontal and vertical composition operations which represent composition in space and in time respectively. Ordinary SOS specifications, context systems [6] by Larsen and Xinxin and rewriting theories by Meseguer (in the nonconditional case) can be seen as special cases of tile systems.
The additional expressiveness of tiles is given by the possibility of choosing as system components and as transition labels data structures more general than ordinary term contexts and (sequences of) actions. Typically they are certain classes of graphs [2], like term graphs or partial orders, equipped with operations of parallel and sequential composition. Tile systems consist of activity tiles, analogous to SOS rules, and of auxiliary tiles, which express the way in which connections between graphs and transition labels can be modified in time and space: For instance two free variables can be permuted, provided the exchange is observed. Certain well know process algebras where causality [3] or locality [4] links are needed, or names can be generated and passed [4], can be represented in a natural way. Bisimilarity can be easily defined on tiles, and expressive tile formats can be specified [5,1], which guarantee that bisimilarity is a congruence.

1. Tiles can be seen as cells of a double category. However here we will stick to the logical view of tiles.

Bibliography

Slides for the talk (PDF).

Uwe Nestmann, EPFL. "Modeling Consensus in a Process Calculus".

Abstract: We give a process calculus model that formalizes a well-known algorithm (introduced by Chandra and Toueg) solving Consensus in the presence of a particular class of failure detectors (Diamond-S); we use our model to formally prove that the algorithm satisfies its specification.

Slides for the talk (gzipped, postscript file).

Catuscia Palamidessi, INRIA/Futurs/Saclay.

Slides for the talk (Powerpoint).

Alban Ponse, University of Amsterdam. "Orthogonality and Logic, of course in Process Algebra".

Abstract: Orthogonal bisimulation is a refinement of branching bisimulation. Typically, this equivalence models compression (reduction to a single tau) instead of abstraction, and is a congruence for priority operators. An open question is to characterize this equivalence via van Glabbeek's observational content of traces (1994). (Work with Bergstra and van der Zwaag, to appear in TCS.) If time and interest permit, I'll shortly discuss The Logic of ACP (with van der Zwaag, his PhD Thesis). Some (difficult) ingredients of ACP are choice and deadlock/inaction. Both can be seen as a conditional composition (if-then-else) in which the condition has a non-classical truth value. This led us to a characterization via the corresponding four-valued logic (with conditional composition as its only connective) and supports/explains the axiom

Slides for the talk (PDF).

Irek Ulidowski, University of Leicester. "Actions in Formats of SOS Rules".

Abstract: The majority of research on formats of SOS rules is carried out under an assumption that actions used in the rules have a uniform meaning. This is perfectly appropriate when addressing some of the original challenges in this area: given a process language defined by SOS rules of certain form, "how does one associate a transition relation with the process language?", and "is a certain strong equivalence a congruence for the process language?". The outcome of this research, manifested in several well-behaved formats of SOS rules, is a thorough understanding of the structure of process terms that can appear safely in rules, with actions playing no role. However, when modelling realistic systems it is often necessary to differentiate the meaning of actions: we regularly distinguish between visible and silent actions. Other examples include timed and untimed actions, actions that denote termination, high level and low level actions when modelling security, and others. I will investigate how sets of actions with non-uniform meaning affect the definitions of formats of rules that use such actions in the setting of weak equivalence semantics.

Slides for the talk (gzipped, postscript file).

Walter Vogler Universität Augsburg. "Measuring the Performance of Asynchronous Systems with PAFAS".

Abstract: Based on PAFAS (Process Algebra for Faster Asynchronous Systems), a testing-based faster-than relation has previously been developed that compares the worst-case efficiency of asynchronous systems. While the testing definition is qualitative, we point out that it can also be seen as considering quantitative performance measures. Then we adapt the PAFAS-approach to a setting where user behaviour is known to belong to a very specific, but often occurring class of request-response behaviours, and show how to determine an asymptotic performance measure for finite-state processes. We discuss a number of examples showing the usefulness of this setting, in particular for explaining in what sense pipelining improves the efficiency.

Slides for the talk (PDF).