Selected Papers of the Conference ''Foundations of Software Science and Computation Structures 2007"


Editor: Helmut Seidl

This special issue contains extended versions of papers presented at FoSSaCS 2007, the international conference Foundations of Software Science and Computations Structures (FOSSACS) 2007, held in Braga, Portugal, March 26-28, 2007, as part of the Joint European Conferences on Theory and Practice of Software (ETAPS) 2007.

The 11 papers collected in this special issue have been invited by the guest editor. The selection was made on the basis of the ranking of the papers by the Program Committee and the opinion of the expert reviewers who assisted the Program Committee. The papers reect the high level of the conference and represent a wide range of topics including separation logic, process calculi, probabilistic systems, higher-order pushdowns, verification of functional programs with state and model-checking. We are grateful to the authors for their excellent submissions.

All papers were refereed in accordance with the usual high standards of LMCS. We also thank the members of the Program Committee of FoSSaCS 2007 and their subreferees as well as to all those who have served as reviewers of the papers submitted to this special issue. We would also like to thank Jiri Adámek, Executive Editor of LMCS for his assistance and guidance.

Helmut Seidl Université Paris-Diderot (Paris 7)
Guest Editor and FoSSaCS 2007 Program Chair

1. Approximating a Behavioural Pseudometric without Discount for<br> Probabilistic Systems

van Breugel, Franck ; Sharma, Babita ; Worrell, James.
Desharnais, Gupta, Jagadeesan and Panangaden introduced a family of behavioural pseudometrics for probabilistic transition systems. These pseudometrics are a quantitative analogue of probabilistic bisimilarity. Distance zero captures probabilistic bisimilarity. Each pseudometric has a discount […]

2. A Distribution Law for CCS and a New Congruence Result for the pi-calculus

Hirschkoff, Daniel ; Pous, Damien.
We give an axiomatisation of strong bisimilarity on a small fragment of CCS that does not feature the sum operator. This axiomatisation is then used to derive congruence of strong bisimilarity in the finite pi-calculus in absence of sum. To our knowledge, this is the only nontrivial subcalculus of […]

3. A lower bound on web services composition

Muscholl, Anca ; Walukiewicz, Igor.
A web service is modeled here as a finite state machine. A composition problem for web services is to decide if a given web service can be constructed from a given set of web services; where the construction is understood as a simulation of the specification by a fully asynchronous product of the […]

4. Relational Parametricity and Separation Logic

Birkedal, Lars ; Yang, Hongseok.
Separation logic is a recent extension of Hoare logic for reasoning about programs with references to shared mutable data structures. In this paper, we provide a new interpretation of the logic for a programming language with higher types. Our interpretation is based on Reynolds's […]

5. On the Expressiveness and Complexity of ATL

Laroussinie, Francois ; Markey, Nicolas ; Oreiby, Ghassan.
ATL is a temporal logic geared towards the specification and verification of properties in multi-agents systems. It allows to reason on the existence of strategies for coalitions of agents in order to enforce a given property. In this paper, we first precisely characterize the complexity of […]

6. Visibly Tree Automata with Memory and Constraints

Comon-Lundh, Hubert ; Jacquemard, Florent ; Perrin, Nicolas.
Tree automata with one memory have been introduced in 2001. They generalize both pushdown (word) automata and the tree automata with constraints of equality between brothers of Bogaert and Tison. Though it has a decidable emptiness problem, the main weakness of this model is its lack of good […]

7. Model Checking One-clock Priced Timed Automata

Bouyer, Patricia ; Larsen, Kim G. ; Markey, Nicolas.
We consider the model of priced (a.k.a. weighted) timed automata, an extension of timed automata with cost information on both locations and transitions, and we study various model-checking problems for that model based on extensions of classical temporal logics with cost constraints on […]

8. Enriched MU-Calculi Module Checking

Ferrante, Alessandro ; Murano, Aniello ; Parente, Mimmo.
The model checking problem for open systems has been intensively studied in the literature, for both finite-state (module checking) and infinite-state (pushdown module checking) systems, with respect to Ctl and Ctl*. In this paper, we further investigate this problem with respect to the […]

9. Logical Reasoning for Higher-Order Functions with Local State

Yoshida, Nobuko ; Honda, Kohei ; Berger, Martin.
We introduce an extension of Hoare logic for call-by-value higher-order functions with ML-like local reference generation. Local references may be generated dynamically and exported outside their scope, may store higher-order functions and may be used to construct complex mutable data structures. […]

10. Symbolic Backwards-Reachability Analysis for Higher-Order Pushdown Systems

Hague, Matthew ; Ong, C. -H. Luke.
Higher-order pushdown systems (PDSs) generalise pushdown systems through the use of higher-order stacks, that is, a nested "stack of stacks" structure. These systems may be used to model higher-order programs and are closely related to the Caucal hierarchy of infinite graphs and safe […]

11. Formalising the pi-calculus using nominal logic

Bengtson, Jesper ; Parrow, Joachim.
We formalise the pi-calculus using the nominal datatype package, based on ideas from the nominal logic by Pitts et al., and demonstrate an implementation in Isabelle/HOL. The purpose is to derive powerful induction rules for the semantics in order to conduct machine checkable proofs, closely […]