Algebraic Methodology and Software Technology

Lecture Notes in Computer Science 6486

Commenced Publication in 1973

Founding and Former Series Editors:

Gerhard Goos, Juris Hartmanis, and Jan van Leeuwen

Editorial Board

David Hutchison

Lancaster University, UK

Takeo Kanade

Carnegie Mellon University, Pittsburgh, PA, USA

Josef Kittler

University of Surrey, Guildford, UK

Jon M. Kleinberg

Cornell University, Ithaca, NY, USA

Alfred Kobsa

University of California, Irvine, CA, USA

Friedemann Mattern

ETH Zurich, Switzerland

John C. Mitchell

Stanford University, CA, USA

Moni Naor

Weizmann Institute of Science, Rehovot, Israel

Oscar Nierstrasz

University of Bern, Switzerland

C. Pandu Rangan

Indian Institute of Technology, Madras, India

Bernhard Steffen

TU Dortmund University, Germany

Madhu Sudan

Microsoft Research, Cambridge, MA, USA

Demetri Terzopoulos

University of California, Los Angeles, CA, USA

Doug Tygar

University of California, Berkeley, CA, USA

Gerhard Weikum

Max Planck Institute for Informatics, Saarbruecken, Germany

Michael Johnson

Dusko Pavlovic (Eds.)

Algebraic Methodology

and Software Technology

13th International Conference, AMAST 2010

Lac-Beauport, QC, Canada, June 23-25, 2010

Revised Selected Papers

13

Volume Editors

Michael Johnson

Macquarie University

Sydney, Australia

E-mail: [email protected]

Dusko Pavlovic

University of Oxford

Oxford, UK

E-mail: [email protected]

Library of Congress Control Number: 2010941005

CR Subject Classification (1998): D.2, F.3, D.3, F.4.1, D.2.4, D.1

LNCS Sublibrary: SL 2 – Programming and Software Engineering

ISSN 0302-9743

ISBN-10 3-642-17795-6 Springer Berlin Heidelberg New York

ISBN-13 978-3-642-17795-8 Springer Berlin Heidelberg New York

This work is subject to copyright. All rights are reserved, whether the whole or part of the material is

concerned, specifically the rights of translation, reprinting, re-use of illustrations, recitation, broadcasting,

reproduction on microfilms or in any other way, and storage in data banks. Duplication of this publication

or parts thereof is permitted only under the provisions of the German Copyright Law of September 9, 1965,

in its current version, and permission for use must always be obtained from Springer. Violations are liable

to prosecution under the German Copyright Law.

springer.com

© Springer-Verlag Berlin Heidelberg 2011

Printed in Germany

Typesetting: Camera-ready by author, data conversion by Scientific Publishing Services, Chennai, India

Printed on acid-free paper 06/3180

Preface

This volume contains the papers presented at AMAST 2010: the 13th Inter￾national conference on Algebraic Methodology and Software Technology. The

major goal of the AMAST conferences is to promote research that may lead to

the setting of software technology on a firm, mathematical basis. Toward this

goal, the conference supports a broad cooperation between academia and in￾dustry. The virtues of a software technology developed on a mathematical basis

include the provision of software that is:

1. Correct, and the correctness can be proved mathematically

2. Safe, so that it can be used in the implementation of critical systems

3. Portable, i.e., independent of computing platforms and language generations

4. Evolutionary, i.e., it can be self-adaptable and evolves with the problem

domain

5. Secure, so that its network and user interactions can be predicted and

controlled

The previous editions of the AMAST Conference were held at Iowa City (1989,

1991), Twente (1993), Montreal (1995), Munich (1996), Sydney (1997), Man￾aus (1999), Iowa City (2000), Reunion Island (2002), Stirling (2004), Saaremaa

(2006) and Urbana-Champaign (2008). Each conference over the last fifteen years

was accompanied by a proceedings volume, published in the Springer Lecture

Notes in Computer Science series.

This 13th edition of AMAST took place during June 23–26, 2010 in Lac￾Beauport, in Qu´ebec, Canada. It was was colocated with MPC 2010: the 10th

International Conference on Mathematics of Program Construction, held during

June 21–23, 2010. There were 33 submissions. Each submission was reviewed

by at least three, and on the average 3.9, Program Committee members. The

committee decided to accept ten full-length research presentations and four sys￾tem demonstrations. The program also included two invited talks, given by Jane

Hillston (Edinburgh University), and Catuscia Palamidesi (INRIA). Jane Hill￾ston also provided a paper for Part 1 of this volume. The contributed research

papers are in Part 2 and Part 3 contains the system demonstrations.

We are grateful to the members of the Program Committee and the external

referees for their care and diligence in reviewing the submitted papers, and to the

staff of Springer-Verlag. The review process and compilation of the proceedings

were greatly helped by Andrei Voronkov’s EasyChair system.

August 2010 Michael Johnson

Dusko Pavlovic

Conference Organization

Program Chairs

Michael Johnson Macquarie University, Australia

Dusko Pavlovic Kestrel Institute, USA and University of Oxford, UK

Program Committee

Paolo Baldan Dipartimento di Matematica Pura e Applicata,

Universit´a di Padova, Italy

Gilles Barthe IMDEA Software, Spain

Michel Bidoit INRIA Saclay, France

Manfred Broy TUM, Germany

Roberto Bruni University of Pisa, Italy

Iliano Cervesato Carnegie Mellon University - Qatar Campus,

Qatar

Adriana Compagnoni Stevens Institute of Technology, USA

Jos´e Luiz Fiadeiro University of Leicester, UK

Kokichi FUTATSUGI JAIST, Japan

Rob Goldblatt Victoria University of Wellington, New Zealand

Ichiro Hasuo RIMS, Kyoto University, Japan

Rolf Hennicker Ludwig-Maximilians-Universit¨at M¨unchen,

Germany

H´el`ene Kirchner INRIA, France

Barbara K¨onig Universit¨at Duisburg-Essen, Germany

Narciso Marti Oliet Universidad Complutense de Madrid, Spain

Michael Mislove Tulane University, USA

Larry Moss Department of Mathematics, Indiana

University, Bloomington, USA

Till Mossakowski DFKI Lab Bremen, Germany

Peter D. Mosses Swansea University, UK

Andrzej Murawski University of Oxford, UK

Uwe Nestmann Technische Universit¨at Berlin, Germany

Fernando Orejas UPC, Spain

Leila Ribeiro Universidade Federal do Rio Grande do Sul,

Brazil

Grigore Rosu University of Illinois at Urbana-Champaign,

USA

Jan Rutten CWI, The Netherlands

VIII Conference Organization

Lutz Schr¨oder DFKI Bremen and Universit¨at Bremen,

Germany

Wolfram Schulte Microsoft Research, USA

Douglas Smith Kestrel Institute, USA

Carolyn Talcott SRI International, USA

Andrzej Tarlecki Institute of Informatics, Faculty of

Mathematics, Informatics and Mechanics,

Warsaw University, Poland

Varmo Vene University of Tartu, Estonia

E.P. de Vink Technische Universiteit Eindhoven,

The Netherlands

James Worrell University of Oxford, UK

External Reviewers

Ludwig Adam

Sebastian Bauer

Laura Bocchi

Jewgenij Botaschanjan

Marzia Buscemi

Yuki Chiba

Mihai Codescu

Andrea Corradini

Silvia Crafa

Vijay D’silva

Tobias Eibach

Cristian Ene

Jean-Christophe Filliˆatre

Reiner H¨ahnle

Daniel Hedin

Torsten Hildebrandt

Cl´ement Hurlin

Dieter Hutter

Stefan Kiefer

Ekaterina Komendantskaya

Dexter Kozen

C´esar Kunz

Alberto Lluch Lafuente

Masaki Nakamura

Kazuhiro Ogata

Catuscia Palamidessi

Kirstin Peters

Ricardo Pe˜na

Erik Poll

Bernhard Reus

Mehrnoosh Sadrzadeh

Francesco Tapparo

David Trachtenherz

Virginie Wiels

Local Organizers

Claude Bolduc, Jules Desharnais, and B´echir Ktari (Universit´e Laval, Canada)

Sponsoring Institutions

– Universit´e Laval, Qu´ebec, Canada, http://www.ulaval.ca

– Centre de recherches math´ematiques, Universit´e de Montr´eal, Montr´eal,

Canada, http://www.crm.umontreal.ca

Table of Contents

Part 1. Invited Paper

Structural Analysis for Stochastic Process Algebra

Models (Invited Talk) ............................................ 1

Jie Ding and Jane Hillston

Part 2. Contributed Research Papers

Verification of Common Interprocedural Compiler Optimizations Using

Visibly Pushdown Kleene Algebra .................................. 28

Claude Bolduc and B´echir Ktari

On the Expressiveness of the π-Calculus and the Mobile Ambients ..... 44

Linda Brodo

Integrating Maude into Hets....................................... 60

Mihai Codescu, Till Mossakowski, Adri´an Riesco, and

Christian Maeder

Model Refinement Using Bisimulation Quotients ..................... 76

Roland Gl¨uck, Bernhard M¨oller, and Michel Sintzoff

Type Fusion ..................................................... 92

Ralf Hinze

Coalgebraic Semantics for Parallel Derivation Strategies in Logic

Programming .................................................... 111

Ekaterina Komendantskaya, Guy McCusker, and John Power

Learning in a Changing World, an Algebraic Modal Logical

Approach ....................................................... 128

Prakash Panangaden and Mehrnoosh Sadrzadeh

Matching Logic: An Alternative to Hoare/Floyd Logic ................ 142

Grigore Ro¸su, Chucky Ellison, and Wolfram Schulte

Program Calculation in Coq ....................................... 163

Julien Tesson, Hideki Hashimoto, Zhenjiang Hu,

Fr´ed´eric Loulergue, and Masato Takeichi

Cooperation of Algebraic Constraint Domains in Higher-Order

Functional and Logic Programming ................................ 180

Rafael del Vado V´ırseda

X Table of Contents

Part 3. System Demonstrations

Proving Termination Properties with mu-term ...................... 201

Beatriz Alarc´on, Ra´ul Guti´errez, Salvador Lucas, and

Rafael Navarro-Marset

BAL Tool in Flexible Manufacturing Systems........................ 209

Diego P´erez Le´andrez, M. Carmen Ruiz, J. Jose Pardo, and

Diego Cazorla

A Complete Declarative Debugger for Maude ........................ 216

Adri´an Riesco, Alberto Verdejo, and Narciso Mart´ı-Oliet

An Assume Guarantee Approach for Checking Quantified Array

Assertions....................................................... 226

Mohamed Nassim Seghir

Author Index .................................................. 237

Structural Analysis for Stochastic Process

Algebra Models

Jie Ding1 and Jane Hillston2

1 School of Information Engineering, Yangzhou University, Yangzhou, 225009, China

[email protected] 2 LFCS, School of Informatics, Edinburgh University, UK

[email protected]

Abstract. Stochastic process algebra models have been successfully

used in the area of performance modelling for the last twenty years, and

more recently have been adopted for modelling biochemical processes

in systems biology. Most research on these modelling formalisms has

been on quantitative analysis, particularly the derivation of quantified

dynamic information about the system modelled in the face of the state

space explosion problem. In this paper we instead consider qualitative

analysis, looking at how recent developments to tackle state space explo￾sion in quantified analysis can be also harnessed to establish properties

such as freedom from deadlock in an efficient manner.

1 Introduction

Stochastic process algebras were introduced in the early 1990s as a formal

modelling formalism for performance modelling which allowed continuous time

Markov chains (CTMCs) to be specified in a rigorous, compositional manner (see

for example [1, 10, 12]). Like all discrete state modelling formalisms the process

algebra models suffered from problems of state space explosion when represent￾ing large or complex systems, and subsequent work focussed on exploiting the

compositionality of the process algebra to decompose or simplify the underlying

CTMC e.g. [2, 5, 11, 15, 19, 22].

More recently stochastic process algebras such as the stochastic π-calculus

[16, 20] and PEPA [3, 4] have been used for modelling biochemical mechanisms

within cells. In these cases the state space explosion problem becomes almost in￾surmountable. Consequently in many cases models are analysed by discrete event

simulation rather than being able to abstractly consider all possible behaviours.

However an alternative approach has emerged which is suitable for models

which are comprised of large numbers of repeated components, fluid approxi￾mation [13]. In this approach an alternative state representation is chosen, and

system dynamics are approximated by a continuous updating of state rather

than the usual discrete steps which are represented in process algebra seman￾tics. Whereas process algebra semantics usually capture the structure of the

system in terms of interacting components and each of their local states, in this

M. Johnson and D. Pavlovic (Eds.): AMAST 2010, LNCS 6486, pp. 1–27, 2011.

c Springer-Verlag Berlin Heidelberg 2011

2 J. Ding and J. Hillston

approach only a aggregation is captured which counts the number of components

which currently exhibit a particular behaviour [25].

Whilst the focus of stochastic process algebras has understandably been pri￾marily quantitative analysis, qualitative analysis can also provide valuable in￾sight into the behaviour of a system. In contrast, in Petri net modelling there

are well-established techniques of structural analysis [6, 9, 17, 23, 24]. In this

paper we show how the new state representation schema for the stochastic pro￾cess algebra PEPA, developed to support fluid approximation, makes it possible

to readily adapt structural analysis techniques for Petri nets to PEPA. More￾over, the compact representation form means that qualitative analysis can now

be applied to systems of a size and complexity which could not previously be

considered.

The remainder of this paper is organised as follows. Section 2 introduces

PEPA and the numerical representation schema used throughout this paper. In

Section 3 we explain how this representation makes apparent the P/T structure

underlying every PEPA model and in Section 4 we show how this structure can

be used to uncover invariants of a model. In Section 5 and 6 we discussed lin￾earised state space and a new deadlock checking algorithm respectively. Section 7

presents some related work and we conclude in Section 8.

2 The PEPA Modelling Formalism

This section will briefly introduce the PEPA language and its numerical repre￾sentation scheme. The numerical representation scheme for PEPA was developed

by Ding in his thesis [7], and represents a model numerically rather than syn￾tactically supporting the use of mathematical tools and methods to analyse the

model.

2.1 Introduction to PEPA

PEPA (Performance Evaluation Process Algebra) [12], developed by Hillston in

the 1990s, is a high-level model specification language for low-level stochastic

models, and describes a system as an interaction of the components which en￾gage in activities. In contrast to classical process algebras, activities are assumed

to have a duration which is a random variable governed by an exponential distri￾bution. Thus each activity in PEPA is a pair (α, r) where α is the action type and

r is the activity rate. The language has a small number of combinators, for which

we provide a brief introduction below; the structured operational semantics can

be found in [12]. The grammar is as follows:

S ::= (α, r).S | S + S | CS

P ::= P

L P | P/L | C

where S denotes a sequential component and P denotes a model component which

executes in parallel. C stands for a constant which denotes either a sequential

component or a model component as introduced by a definition. CS stands for

Structural Analysis for Stochastic Process Algebra Models 3

constants which denote sequential components. The effect of this syntactic sep￾aration between these types of constants is to constrain legal PEPA components

to be cooperations of sequential processes.

Prefix: The prefix component (α, r).S has a designated first activity (α, r),

which has action type α and a duration which satisfies exponential distribution

with parameter r, and subsequently behaves as S.

Choice: The component S + T represents a system which may behave either

as S or as T . The activities of both S and T are enabled. Since each has an

associated rate there is a race condition between them and the first to complete

is selected. This gives rise to an implicit probabilistic choice between actions

dependent of the relative values of their rates.

Hiding: Hiding provides type abstraction, but note that the duration of the

activity is unaffected. In P/L all activities whose action types are in L appear

as the “private” type τ.

Cooperation:P

L Q denotes cooperation between P and Q over action types

in the cooperation set L. The cooperands are forced to synchronise on action

types in L while they can proceed independently and concurrently with other

enabled activities (individual activities). The rate of the synchronised or shared

activity is determined by the slower cooperation (see [12] for details). We write

P Q as an abbreviation for P

L Q when L = ∅ and P[N] is used to represent

N copies of P in a parallel, i.e. P[3] = P P P.

Constant: The meaning of a constant is given by a defining equation such as

A def

= P. This allows infinite behaviour over finite states to be defined via mutually

recursive definitions.

On the basis of the operational semantic rules (please refer to [12] for details),

a PEPA model may be regarded as a labelled multi-transition system

C, Act,

(α,r) −→ |(α, r) ∈ Act

where C is the set of components, Act is the set of activities and the multi￾relation (α,r) −→ is given by the rules. If a component P behaves as Q after it

completes activity (α, r), then denote the transition as P (α,r) −→ Q.

The memoryless property of the exponential distribution, which is satisfied

by the durations of all activities, means that the stochastic process underlying

the labelled transition system has the Markov property. Hence the underlying

stochastic process is a CTMC. Note that in this representation the states of

the system are the syntactic terms derived by the operational semantics. Once

constructed the CTMC can be used to find steady state or transient probability

distributions from which quantitative performance can be derived.

2.2 Numerical Representation of PEPA Models

As explained above there have been two key steps in the use of fluid approxima￾tion for PEPA models: firstly, the shift to a numerical vector representation of

4 J. Ding and J. Hillston

the model, and secondly, the use of ordinary differential equations to approxi￾mate the dynamic behaviour of the underlying CTMC. In this paper we are only

concerned with the former modification.

This section presents the numerical representation of PEPA models developed

in [7]. For convenience, we may represent a transition P (α,r) −→ Q as P (α,rP→Q

α ) −→

Q, or often simply as P α

−→ Q since the rate is not pertinent to structural

analysis, where P and Q are two local derivatives. Following [13], hereafter the

term local derivative refers to the local state of a single sequential component.

In the standard structured operational semantics of PEPA used to derive the

underlying CTMC, the state representation is syntactic, keeping track of the

local derivative of each component in the model. In the alternative numerical

vector representation some information is lost as states only record the number

of instances of each local derivative:

Definition 1 (Numerical Vector Form[13]). For an arbitrary PEPA model

M with n component types Ci, i = 1, 2, ··· , n, each with di distinct local deriva￾tives, the numerical vector form of M, m(M), is a vector with d = n

i=1 di

entries. The entry m[Cij ] records how many instances of the jth local derivative

of component type Ci are exhibited in the current state.

In the following we will find it useful to distinguish derivatives according to

whether they enable an activity, or are the result of that activity:

Definition 2 (Pre and post local derivative)

1. If a local derivative P can enable an activity α, that is P α

−→ ·, then P is

called a pre local derivative of α. The set of all pre local derivatives of α is

denoted by pre(α), called the pre set of α.

2. If Q is a local derivative obtained by firing an activity α, i.e. · α

−→ Q, then

Q is called a post local derivative of α. The set of all post local derivatives

is denoted by post(α), called the post set of α.

3. The set of all the local derivatives derived from P by firing α, i.e.

post(P, α) = {Q | P α

−→ Q},

is called the post set of α from P.

Within a PEPA model there may be many instances of the same activity type but

we will wish to identify those that have exactly the same effect within the model.

In order to do this we additionally label activities according to the derivatives

to which they relate, giving rise to labelled activities:

Definition 3 (Labelled Activity)

1. For any individual activity α, for each P ∈ pre(α), Q ∈ post(P, α), label α

as αP→Q.