The μ-calculus as an assertion-language for fairness arguments

Various principles of proof have been proposed to reason about fairness. This paper addresses—for the first time—the question in what formalism such fairness arguments can be couched. To wit: we prove that Park's monotone first-order μ-calculus, augmented with constants for all recursive ordinals can serve as an assertion-language for proving fair termination of do-loops. In particular, the weakest precondition for fair termination of a loop w.r.t. some postcondition is definable in it. The relevance of this result to proving eventualities in the temporal logic formalism of Manna and Pnuelis (in “Foundations of Computer Science IV, Part 2,” Math. Centre Tracts, Vol. 159, Math. Centrum, Amsterdam, 1983) is discussed.     

Lifting Infinite Normal Form Definitions From Term Rewriting to Term Graph Rewriting

nfinite normal forms are a way of giving semantics to non-terminating rewrite systems. The notion is a generalization of the Böhm tree in the lambda calculus. It was first introduced in [Ariola, Z. M. and S. Blom, Cyclic lambda calculi, in: Abadi and Ito [Abadi, M. and T. Ito, editors, “Theoretical Aspects of Computer Software,” Lecture Notes in Computer Science 1281, Springer Verlag, 1997], pp. 77–106] to provide semantics for a lambda calculus on terms with letrec. In that paper infinite normal forms were defined directly on the graph rewrite system. In [Blom, S., “Term Graph Rewriting - syntax and semantics,” Ph.D. thesis, Vrije Universiteit Amsterdam (2001)] the framework was improved by defining the infinite normal form of a term graph using the infinite normal form on terms. This approach of lifting the definition makes the non-confluence problems introduced into term graph rewriting by substitution rules much easier to deal with. In this paper, we give a simplified presentation of the latter approach.     

Completeness of Continuation Models for λμ-Calculus

We show that a certain simple call-by-name continuation semantics of Parigot's λ_μ-calculus is complete. More precisely, for every λ_μ-theory we construct a cartesian closed category such that the ensuing continuation-style interpretation of λ_μ, which maps terms to functions sending abstract continuations to responses, is full and faithful. Thus, any λ_μ-category in the sense of L. Ong (1996, in “Proceedings of LICS '96,” IEEE Press, New York) is isomorphic to a continuation model (Y. Lafont, B. Reus, and T. Streicher, “Continuous Semantics or Expressing Implication by Negation,” Technical Report 93-21, University of Munich) derived from a cartesian-closed category of continuations. We also extend this result to a later call-by-value version of λ_μ developed by C.-H. L. Ong and C. A. Stewart (1997, in “Proceedings of ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Paris, January 1997,” Assoc. Comput. Mach. Press, New York).     

Focus points and convergent process operators: a proof strategy for protocol verification

We present a method for efficiently providing algebraic correctness proofs for communication systems. It is described in the setting of μCRL [J.F. Groote, A. Ponse, The syntax and semantics of μCRL, in: A. Ponse, C. Verhoef, S.F.M. van Vlijmen (Eds.), Algebra of Communicating Processes, Workshops in Computing, Springer, Berlin, 1994, pp. 26–62] which is, roughly, ACP [J.C.M. Baeten, W.P. Weijland, Process Algebra, Cambridge Tracts in Theoretical Computer Science, vol. 18, Cambridge University Press, Cambridge 1990, J.A. Bergstra, J.W. Klop, The algebra of recursively defined processes and the algebra of regular processes, in: Proceedings of the 11th ICALP, Antwerp, Lecture Notes in Computer Science, vol. 172, Springer, Berlin, 1984, pp. 82–95] extended with a formal treatment of the interaction between data and processes. The method incorporates assertional methods, such as invariants and simulations, in an algebraic framework, and centers around the idea that the state spaces of distributed systems are structured as a number of cones with focus points. As a result, it reduces a large part of algebraic protocol verification to the checking of a number of elementary facts concerning data parameters occurring in implementation and specification. The resulting method has been applied to various non-trivial case studies of which a number have been verified mechanically with the theorem checker PVS. In this paper the strategy is illustrated by several small examples and one larger example, the Concurrent Alternating Bit Protocol (CABP).     

On the Jacopini Technique

The general concern of the Jacopini technique is the question: “Is it consistent to extend a given lambda calculus with certain equations?” The technique was introduced by Jacopini in 1975 in his proof that in the untyped lambda calculusΩis easy, i.e.,Ωcan be assumed equal to any other (closed) term without violating the consistency of the lambda calculus. The presentations of the Jacopini technique that are known from the literature are difficult to understand and hard to generalise. In this paper we generalise the Jacopini technique for arbitrary lambda calculi. We introduce the concept ofproof-replaceabilityby which the structure of the technique is simplified considerably. We illustrate the simplicity and generality of our formulation of the technique with some examples. We apply the Jacopini technique to theλμ-calculus, and we prove a general theorem concerning the consistency of extensions of theλμ-calculus of a certain form. Many well known examples (e.g., the easiness ofΩ) are immediate consequences of this general theorem.     

A Model in κ for DNA Addition

DNA computing is a hot research topic in recent years. Formalization and verification using theories(π-calculus, bioambients, κ-calculus and etc.) in Computer Science attract attention because it can help prove and predict to a certian degree various kinds of biological processes. Combining these two aspects, formal methods can be used to verify algorithms in DNA computing, including basic arithmetic operations if they are to be included in a DNA chip. In this paper, we first introduce a newly-designed algorithm for solving binary addition with DNA, which contributes to a unit in DNA computer processor, and then formalize the algorithm in κ-calculus(a formal method well suited for describing protein interactions) to show the correctness of it in a sense, and a sensible example is provided. Finally, some discussion on the described model is made, in addition to a few possible future improvement directions.     

Term Collections in λ and ρ-calculi

The ρ-calculus generalises term rewriting and the λ-calculus by defining abstractions on arbitrary patterns and by using a pattern-matching algorithm which is a parameter of the calculus. In particular, equational theories that do not have unique principal solutions may be used. In the latter case, all the principal solutions of a matching problem are stored in a “structure” that can also be seen as a collection of terms.Motivated by the fact that there are various approaches to the definition of structures in the ρ-calculus, we study in this paper a version of the λ-calculus with term collections.The contributions of this work include a new syntax and operational semantics for a λ-calculus with term collections, which is related to the λ-calculi with strict parallel functions studied by Boudol and Dezani et al. and a proof of the confluence of the β-reduction relation defined for the calculus (which is a suitable extension of the standard rule of β-reduction in the λ-calculus).     

Discounting Infinite Games But How and Why?

In a recent paper de Alfaro, Henzinger and Majumdar [Luca de Alfaro, Thomas A. Henzinger, and Rupak Majumdar. Discounting the future in systems theory. In ICALP 2003, volume 2719 of LNCS, pages 1022–1037. Springer, 2003] observed that discounting successive payments, the procedure that is employed in the classical stochastic game theory since the seminal paper of Shapley [L.S. Shapley. Stochastic games. Proceedings Nat. Acad. of Science USA, 39:1095–1100, 1953], is also pertinent in the context of much more recent theory of stochastic parity games [L. de Alfaro and R. Majumdar. Quantitative solution to omega-regular games. In STOC'01, pages 675–683. ACM Press, 2001. final version to appear in Journal of Computer and System Sciences, L. de Alfaro, T.A. Henzinger, and O. Kupferman. Concurrent reachability games. In FOCS'98, pages 564–575. IEEE Computer Society Press, 1998, L. de Alfaro and T.A. Henzinger. Concurrent ω-regular games. In LICS'00, pages 142–154. IEEE Computer Society Press, 2000] which were proposed as a tool for verification of probabilistic systems. We show that, surprisingly perhaps, the particular discounting used in [Luca de Alfaro, Thomas A. Henzinger, and Rupak Majumdar. Discounting the future in systems theory. In ICALP 2003, volume 2719 of LNCS, pages 1022–1037. Springer, 2003] is in fact very close to the original ideas of Shapley. This observation allows to realize that the specific discounting of [Luca de Alfaro, Thomas A. Henzinger, and Rupak Majumdar. Discounting the future in systems theory. In ICALP 2003, volume 2719 of LNCS, pages 1022–1037. Springer, 2003] suffers in fact from some needless restrictions. We advocate that dropping the constraints imposed in [Luca de Alfaro, Thomas A. Henzinger, and Rupak Majumdar. Discounting the future in systems theory. In ICALP 2003, volume 2719 of LNCS, pages 1022–1037. Springer, 2003] leads to a more general and elegant theory that includes parity and mean payoff games as particular limit cases.     

What is a “Good” Encoding of Guarded Choice?

The π-calculus with synchronous output and mixed-guarded choices is strictly more expressive than the π-calculus with asynchronous output and no choice. This result was recently proved by C. Palamidessi and, as a corollary, she showed that there is no fully compositional encoding from the former into the latter that preserves divergence-freedom and symmetries. This paper argues that there are nevertheless “good” encodings between these calculi. In detail, we present a series of 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 of the above criteria, but various “good” candidates for the third encoding—inspired by an existing distributed implementation—invalidate one or the other criterion. While essentially confirming Palamidessi's result, our study suggests that the combination of strong compositionality and divergence-freedom is too strong for more practical purposes.     

A Logical Process Calculus

This paper presents the Logical Process Calculus (LPC), a formalism that supports heterogeneous system specifications containing both operational and declarative subspecifications. Syntactically, LPC extends Milner's Calculus of Communicating Systems with operators from the alternation-free linear-time μ-calculus (LTμ). Semantically, LPC is equipped with a behavioral preorder that generalizes Hennessy's and De Nicola's must-testing preorder as well as LTμ's satisfaction relation, while being compositional for all LPC operators. From a technical point of view, the new calculus is distinguished by the inclusion of (i) both minimal and maximal fixed-point operators and (ii) an unimplementability predicate on process terms which tags inconsistent specifications. The utility of LPC is demonstrated by means of an example highlighting the benefits of heterogeneous system specification.     

Probabilistic π-Calculus and Event Structures

This paper proposes two semantics of a probabilistic variant of the π-calculus: an interleaving semantics in terms of Segala automata and a true concurrent semantics, in terms of probabilistic event structures. The key technical point is a use of types to identify a good class of non-deterministic probabilistic behaviours which can preserve a compositionality of the parallel operator in the event structures and the calculus. We show an operational correspondence between the two semantics. This allows us to prove a “probabilistic confluence” result, which generalises the confluence of the linearly typed π-calculus.     

On Term Graphs as an Adhesive Category

The recent interest in bisimulation congruences for reduction systems, stimulated by the research on general (often graphical) frameworks for nominal calculi, has brought forward many proposals for categorical formalisms where relevant properties of observational equivalences could be auto- matically verified.Interestingly, some of these formalisms also identified suitable categories where the standard tools and techniques developed for the double-pushout approach to graph transformation [A. Corradini, U. Montanari, F. Rossi, H. Ehrig, R. Heckel and M. Löwe, Algebraic approaches to graph transformation I: Basic concepts and double pushout approach, in: G. Rozenberg, editor, Handbook of Graph Grammars and Computing by Graph Transformation, I: Foundations, World Scientific, 1997, pp. 163–246] could be recast, thus providing a valid alternative to the High-Level Replacement Systems paradigm [H. Ehrig, A. Habel, H.-J. Kreowski and F. Parisi-Presicce, Parallelism and concurrency in highlevel replacement systems, Mathematical Structures in Computer Science 1 (1991) 361–404].In this paper we consider the category of term graphs, and we prove that it (partly) fits in the general framework for adhesive categories, developed in [S. Lack, and P. Sobociński, Adhesive categories, in: I. Walukiewicz, editor, Foundations of Software Science and Computation Structures, Lect. Notes in Comp. Sci. 2987 (2004), pp. 273–288, P. Sobociński, “Deriving bisimulation congruences from reduction systems”, Ph.D. thesis, BRICS, Department of Computer Science, University of Aaurhus (2004)], extended in [H. Ehrig, A. Habel, J. Padberg and U. Prange, Adhesive high-level replacement categories and systems, in: G. Engels and F. Parisi-Presicce, editors, Graph Transformation, Lect. Notes in Comp. Sci. (2004)] and applied to reduction systems in [V. Sassone, and P. Sobociński, Congruences for contextual graph-rewriting, Technical Report RS-04-11, BRICS, Department of Computer Science, University of Aarhus (2004)]. The main technical achievement concerns the proof that the category of term graphs is actually quasi-adhesive, obtained by proving the existence of suitable Van Kampen squares.     

Explicit Substitutions à la de Bruijn: the local and global way

Kamareddine and Nederpelt[9], resp. Kamareddine and Ríos [11] gave two calculi of explicit of substitutions highly influenced by de Bruijn's notation of the λ-calculus. These calculi added to the explosive pool of work on explicit substitution in the past 15 years. As far as we know, calculi of explicit substitutions: a) are unable to handle local substitutions, and b) have answered (positively or negatively) the question of the termination of the underlying calculus of substitutions. The exception to a) is the calculus of [9] where substitution is handled both locally and globally. However, the calculus of [9] does not satisfy properties like confluence and termination. The exception to b) is the λs_e-calculus of [11] for which termination of the s_e-calculus, the underlying calculus of substitutions, remains unsolved. This paper has two aims:

(i) To provide a calculus à la de Bruijn which deals with local substitution and whose underlying calculus of substitutions is terminating and confluent.

(ii) To pose the problem of the termination of the substitution calculus of [11] in the hope that it can generate interest as a termination problem which at least for curiosity, needs to be settled. The answer here can go either way. On the one hand, although the λσ-calculus [1] does not preserve termination, the σ-calculus itself terminates. On the other hand, could the non-preservation of termination in the λs_e-calculus imply the non-termination of the s_e-calculus?

Closure properties of uniform convergence of empirical means and PAC learnability under a family of probability measures

Open Problem No. 12.2 of (Vidyasagar, A Theory of Learning and Generalization: with Application to Neural Networks and Control Systems, Springer, London, 1997) asks: “Are the properties of uniform convergence of empirical means, and learnability preserved when the family of probability measures is replaced by its closure?” In this note, the question is answered in the affirmative. Further, it is shown that these properties are not preserved in general if the family of probability measures is replaced by its convex closure. An open question is posed as to whether it is possible to replace the family of probability measures by its convex closure in case the family is compact.     

Fair Π

In this paper, we define fair computations in the π-calculus [Milner, R., Parrow, J. & Walker, D., A Calculus of Mobile Processes, Part I and II, Information and Computation 100 (1992) 1–78]. We follow Costa and Stirling's approach for CCS-like languages [Costa, G. & Stirling, C., A Fair Calculus of Communicating Systems, Acta Informatica 21 (1984) 417–441, Costa, G. & Stirling, C., Weak and Strong Fairness in CCS, Information and Computation 73 (1987) 207–244] but exploit a more natural labeling method of process actions to filter out unfair process executions. The new labeling allows us to prove all the significant properties of the original one, such as unicity, persistence and disappearance of labels. It also turns out that the labeled π-calculus is a conservative extension of the standard one. We contrast the existing fair testing [Brinksma, E., Rensink, A. & Vogler, W., Fair Testing, Proc. of CONCUR'95, LNCS, 962 (1995) 313–327, Natarajan, V. & Cleaveland, R., Divergence and Fair Testing, Proc. of ICALP '95, LNCS, 944 (1995) 648–659] with those that naturally arise by imposing weak and strong fairness as defined by Costa and Stirling. This comparison provides the expressiveness of the various fair testing-based semantics and emphasizes the discriminating power of the one already proposed in the literature.     

A Simple Calculus for Proteins and Cells

The use of process calculi to represent biological systems has led to the design of different calculi such as brane calculi [Luca Cardelli. Brane calculi. In CMSB, pages 257–278, 2004] and κ-calculus [Vincent Danos and Cosimo Laneve. Formal molecular biology. Theoritical Computer Science, 325(1):69–110, 2004]. Both have proved to be useful to model different types of biological systems.As an attempt to unify the two directions, we introduce the bioκ-calculus, a simple calculus for describing proteins and cells, in which bonds are represented by means of shared names and interactions are modelled at the domain level. Protein-protein interactions have to be at most binary and cell interactions have to fit with sort constraints.We define the semantics of bioκ-calculus, analyse its properties, and discuss its expressiveness by modelling two significant examples: a signalling pathway and a virus infection.     

Verification of multiprocess probabilistic protocols

In this paper we demonstrate the utility of temporal logic to the formal verification of probabilistic distributed programs. The approach taken is to represent the quantitative notion of probabilistic computations by the qualitative abstraction ofextreme fairness. The method is illustrated first on the dining philosophers problem [3] and then on a new probabilistic symmetric solution to then-processes mutual exclusion problem. Two related solutions are presented corresponding to different assumptions about the granularity of a compound test.Amir Pnueli, graduated at the Technion, Haifa, Israel 1962. Received a Ph.D. degree in Applied Mathematics at the Weizmann Institute, Rehovot, Israel, 1967.He is currently a Professor of Computer Science at the Weizmann Institute. His research interests include the Semantics, Verification, Specification and Development of Concurrent and Distributed Systems using Temporal Logic and other Formalisms.Lenore Zuck was born in Tel Aviv, Israel, on September 26, 1958. She received her B.Sc. degree in Computer Science from the Technion, Haifa, Israel in 1979, and the M.Sc. degree in Computer Science at the Weizmann Institute of Science, Rehovot, Israel, in 1983, where she is currently completing her Ph.D. studies. Her areas of interest include the Analysis and Verification of Distributed and Probabilistic Systems and Pre-Classic Music.The work of this author was supported by the Eshkol Fund     

Bisimulation for Higher-Order Process Calculi

Ahigher-order process calculusis a calculus for communicating systems which contains higher-order constructs like communication of terms. We analyse the notion ofbisimulationin these calculi. We argue that both the standard definition of bisimulation (i.e., the one for CCS and related calculi), as well ashigher-order bisimulation[E. Astesiano, A. Giovini, and G. Reggio,in“STACS '88,” Lecture Notes in Computer Science, Vol. 294, pp. 207–226, Springer-Verlag, Berlin/New York, 1988; G. Boudol,in“TAPSOFT '89,” Lecture Notes in Computer Science, Vol. 351, pp. 149–161, Springer-Verlag, Berlin/New York, 1989; B. Thomsen, Ph.D. thesis, Dept. of Computing, Imperial College, 1990] are in general unsatisfactory, because of their over-discrimination. We propose and study a new form of bisimulation for such calculi, calledcontext bisimulation, which yields a more satisfactory discriminanting power. A drawback of context bisimulation is the heavy use of universal quantification in its definition, which is hard to handle in practice. To resolve this difficulty we introducetriggered bisimulationandnormal bisimulation, and we prove that they both coincide with context bisimulation. In the proof, we exploit thefactorisation theorem: When comparing the behaviour of two processes, it allows us to “isolate” subcomponents which might give differences, so that the analysis can be concentrated on them