How faithfully can π be interpreted in SA?

The π calculus and the safe ambient calculus are two of the widely studied variants of process calculi in the field of concurrency theory.The former is the most classic model for mobile processes and the latter is well known for its nested structure.However,the relationship between these two models deserves further investigation.In this paper,we reinvestigate this problem thoroughly.We first give the strengthened encoding criteria.Then we propose the encoding of the synchronous π-calculus into the safe ambients calculus.The encoding scheme is a generalization and improvement of Levi and Sangiorgi’s work when moving from the asynchronous π-calculus to the synchronous π-calculus.We show the merits of the encoding by checking the mentioned criteria.     

A Formal Semantics for DAI Language NUML

Traditional AI systems are brittle in the sense that they fail miserably when presented with problems even sliphtly outside of their limited range of expertise.A powerful,extensible strategy of Distributed Artificial Intelligence (DAI) for overcoming such bounds is to put the system in a society of systems.So the ability to coordinate group activities of individuals and to communicate between each other is necessary for a language describing DAI systems.Agent-oriented language NUML is such a language.It is a specific kind of object-oriented language.To give formal semantics to NUML,there is the problem to formalise object-oriented programming paradigm which is still open.The theory of higher-order π-calculus is a concurrent computation model with sufficient capability,which provides us a mathematical tool to do the formalization.This paper tries to use higher-order π-calculus to formalise NUML.     

The faster higher-order cellular automaton for hyper-parallel undistorted data compression

This paper defines second-order and third-order permutation global functions and presents the corresponding higher-order cellular automaton approach to the hyper-parallel undistorted data compression.The genetic algorithm is successfully devoted to finding out all the correct local compression rules for the higher-order cellualr automaton.The correctness of the higher-order compression rules,the time complexity,and the systolic hardware implementation issue are discussed.In comparison with the first-order automation method reported,the proposed higher-order approach has much faster compression speed with almost the same degree of cellular structure complexity for hardware implementation.     

Towards a theory of bisimulation for the higher-order process calculi

In this paper, a labelled transition semantics for higher-order process calculi is studied. The labelled transition semantics is relatively clean and simple, and corresponding bisimulation equivalence can be easily formulated based on it. And the congruence properties of the bisimulation equivalence can be proved easily. To show the correspondence between the proposed semantics and the well-established ones, the bisimulation is characterized as a version of barbed equivalence and a version of context bisimulation.     

Behavioural equivalences of a probabilistic pi-calculus

Although different kinds of probabilistic π-calculus have been introduced and found their place in quantitative verification and evaluation,their behavioural equivalences still lack a deep investigation.We propose a simple probabilistic extension of the π-calculus,π p,which is inspired by Herescu and Palamidessi’s probabilistic asynchronous π-calculus.An early semantics of our π p is presented.We generalise several classic behavioural equivalences to probabilistic versions,obtaining the probabilistic(strong) barbed equivalence and probabilistic bisimulation for π p.Then we prove that the coincidence between the barbed equivalence and bisimilarity in the π-calculus is preserved in the probabilistic setting.     

<Emphasis Type="Italic">LFTOP</Emphasis>: An <Emphasis Type="Italic">LF</Emphasis>-Based Approach to Domain-Specific Reasoning

A new approach to domain-specific reasoning is presented that is based on a type-theoretic logical framework(LF) but does not require the user to be an expert in type theory. The concepts of the domain and its related reasoning systems are formalized in LF, but the user works with the system through a syntax and interface appropriate to his/her work. A middle layer provides translation between the user syntax and LF, and allows additional support for reasoning(e.g., model checking). Thus, the complexity of the logical framework is hidden but the benefits of using type theory and its related tools are retained, such as precision and machine-checkable proofs. This approach is investigated through a number of case studies: here, the authors consider the verification of properties of concurrency. The authors have formalized a specification language (CCS) and logic (μ-calculus) in LF, together with useful lemmas, and a user-oriented syntax has been designed. The authors demonstrate the approach with simple examples. However, applying lemmas to objects introduced by the user may result in framework-level objects which cannot be translated back to the user level. The authors discuss this problem, define a notion of adequacy, and prove that in this case study, translation can always be reversed.     

Encoding of primary structures of biological macromolecules within a data mining perspective

An encoding method has a direct effect on the quality and the representation of the discovered knowledge in data mining systems. Biological macromolecules are encoded by strings of characters, called primary structures. Knowing that data mining systems usually use relational tables to encode data, we have then to reencode these strings and transform them into relational tables. In this paper, we do a comparative study of the existing static encoding methods, that are based on the Biologist know-how, and our new dynamic encoding one, that is based on the construction of Discriminant and Minimal Substrings (DMS). Different classification methods are used to do this study. The experimental results show that our dynamic encoding method is more efficient than the static ones, to encode biological macromolecules within a data mining perspective.     

Control of Non-Deterministic Systems With μ-Calculus Specifications Using Quotienting

The supervisory control problem for discrete event system(DES) under control involves identifying the supervisor, if one exists, which, when synchronously composed with the DES,results in a system that conforms to the control specification. In this context, we consider a non-deterministic DES under complete observation and control specification expressed in action-based propositional μ-calculus. The key to our solution is the process of quotienting the control specification against the plan resulting in a new μ-calculus formula such that a model for the formula is the supervisor. Thus the task of control synthesis is reduced a problem of μ-calculus satisfiability. In contrast to the existing μ-calculus quotienting-based techniques that are developed in deterministic setting, our quotienting rules can handle nondeterminism in the plant models. Another distinguishing feature of our technique is that while existing techniques use a separate μ-calculus formula to describe the controllability constraint(that uncontrollable events of plants are never disabled by a supervisor), we absorb this constraint as part of quotienting which allows us to directly capture more general state-dependent controllability constraints. Finally, we develop a tableau-based technique for verifying satisfiability of quotiented formula and model generation. The runtime for the technique is exponential in terms of the size of the plan and the control specification. A better complexity result that is polynomial to plant size and exponential to specification size is obtained when the controllability property is state-independent. A prototype implementation in a tabled logic programming language as well as some experimental results are presented.     

Bus-Switch Encoding for Power Optimization of Address Bus

This paper presents a novel encoding technique to minimize the switch activities on the highly capacitive memory address bus so as to reduce power dissipation of bus. This technique is based on the temporal locality and spatial locality of instruction address. The experimental results based on an instruction set simulator and SPEC2000 benchmarks show that the presented encoding technique can reduce signal transitions on the address bus by 83.8%, and the actual overhead of the encoder circuit is estimated after encoder has been designed and synthesized with 0.18-μm CMOS technology. The results show that our technique well outperforms specialized low-power encoding schemes presented in the past.     

An Abstract Reachability Approach by Combining HOL Induction and Multiway Decision Graphs

In this paper, we provide a necessary infrastructure to define an abstract state exploration in the HOL theorem prover. Our infrastructure is based on a deep embedding of the Multiway Decision Graphs (MDGs) theory in HOL. MDGs generalize Reduced Ordered Binary Decision Diagrams (ROBDDs) to represent and manipulate a subset of first-order logic formulae. The MDGs embedding is based on the logical formulation of an MDG as Directed Formulae (DF). Then, the MDGs operations are defined and the correctness pro...     

A CPS Encoding of Name-Passing in Higher-Order Mobile Embedded Resources

We present an encoding of the synchronous π-calculus in the calculus of Higher-Order Mobile Embedded Resources (Homer), a pure higher-order calculus with mobile processes in nested locations, defined as a simple, conservative extension of the core process-passing subset of Thomsen's Plain CHOCS. We prove that our encoding is fully abstract with respect to barbed bisimulation and sound with respect to barbed congruence. Our encoding demonstrates that higher-order process-passing together with mobile resources in (local) named locations are sufficient to express π-calculus name-passing. The encoding uses a novel continuation passing style to facilitate the encoding of synchronous communication.     

A theory of bisimulation for the π-calculus

 We study a new formulation of bisimulation for the π-calculus [MPW92], which we have called open bisimulation (∼). In contrast with the previously known bisimilarity equivalences, ∼ is preserved by allπ-calculus operators, including input prefix. The differences among all these equivalences already appear in the sublanguage without name restrictions: Here the definition of ∼ can be factorised into a “standard” part which, modulo the different syntax of actions, is the CCS bisimulation, and a part specific to the π-calculus, which requires name instantiation. Attractive features of ∼ are: A simple axiomatisation (of the finite terms), with a completeness proof which leads to the construction of minimal canonical representatives for the equivalence classes of ∼; an “efficient” characterisation, based on a modified transition system. This characterisation seems promising for the development of automated-verification tools and also shows the call-by-need flavour of ∼. Although in the paper we stick to the π-calculus, the issues developed may be relevant to value-passing calculi in general. Received: June 11, 1993/November 28, 1994     

A CPS encoding of name-passing in Higher-order mobile embedded resources

We present an encoding of the synchronous π$\pi$-calculus in the calculus of Higher-order mobile embedded resources (Homer), a pure higher-order calculus with mobile processes in nested locations, defined as a simple, conservative extension of the core process-passing subset of Thomsen's Plain CHOCS. We prove that our encoding is fully abstract with respect to barbed bisimulation and sound with respect to barbed congruence. Our encoding demonstrates that higher-order process-passing together with mobile resources in, possibly local, named locations are sufficient to express π$\pi$-calculus name-passing. The encoding uses a novel continuation passing style to facilitate the encoding of synchronous communication.     

A taxonomy of process calculi for distribution and mobility

In this paper, we comparatively analyze some mainstream calculi for mobility and distribution, together with some of their variants: asynchronous π-calculus, distributed π-calculus, and some dialects of Mobile/Boxed/Safe ambients. In particular, we focus on their relative expressive power, i.e. we try to encode every language in the other while respecting some reasonable properties. According to the possibility or the impossibility for such results, we set up a taxonomy of these languages. Our study enables understanding, for every pair of calculi, which features of one can be rendered in the other and how this is possible, or which features cannot be rendered and why this is impossible.     

On the representation of McCarthy's in the -calculus

We study the encoding of , the call-by-name λ-calculus enriched with McCarthy's amb operator, into the π-calculus. Semantically, amb is a challenging operator, for the fairness constraints that it expresses. We prove that, under a certain interpretation of divergence in the λ-calculus (weak divergence), a faithful encoding is impossible. However, with a different interpretation of divergence (strong divergence), the encoding is possible, and for this case we derive results and coinductive proof methods to reason about that are similar to those for the encoding of pure λ-calculi. We then use these methods to derive the most important laws concerning amb. We take bisimilarity as behavioural equivalence on the π-calculus, which sheds some light on the relationship between fairness and bisimilarity.     

Symmetric π-Calculus

An alternative presentation of the π－calculus is given.This version of the π-calculus is symmetric in the sense that communications are symmetric and there is no difference between input and output prefixes.The point of the symmetric π-calculus is that it has no abstract names.The set of closed names is therefore homogeneous.The π－calculus can be fully embedded into the symmetric π-calculus.The symmetry changes the emphasis of the communication mechanism of the π-calculus and opens up possibility for further variations.     

Parametric synchronizations in mobile nominal calculi

We present and compare P-PRISMA and F-PRISMA, two parametric calculi that can be instantiated with different interaction policies, defined as synchronization algebras with mobility of names (SAMs). In particular, P-PRISMA is based on name transmission (P-SAM), like π-calculus, and thus exploits directional (input–output) communication only, while F-PRISMA is based on name fusion (F-SAM), like Fusion calculus, and thus exploits a more symmetric form of communication. However, P-PRISMA and F-PRISMA can easily accommodate many other high-level synchronization mechanisms than the basic ones available in π-calculus and Fusion, hence allowing for the development of a general meta-theory of mobile calculi. We define for both the labeled operational semantics and a form of strong bisimilarity, showing that the latter is compositional for any SAM. We also discuss reduction semantics and weak bisimilarity. We give several examples based on heterogeneous SAMs, we investigate the case studies of π-calculus and Fusion calculus giving correspondence theorems, and we show how P-PRISMA can be encoded in F-PRISMA. Finally, we show that basic categorical tools can help to relate and to compose SAMs and PRISMA processes in an elegant way.     

Expressing combinatory reduction systems derivations in the rewriting calculus

The last few years have seen the development of the rewriting calculus (also called rho-calculus or ρ-calculus) that uniformly integrates first-order term rewriting and the λ-calculus. The combination of these two latter formalisms has been already handled either by enriching first-order rewriting with higher-order capabilities, like in the Combinatory Reduction Systems (CRS), or by adding to the λ-calculus algebraic features. The various higher-order rewriting systems and the rewriting calculus share similar concepts and have similar applications, and thus, it is important to compare these formalisms to better understand their respective strengths and differences. We show in this paper that we can express Combinatory Reduction Systems derivations in terms of rewriting calculus derivations. The approach we present is based on a translation of each possible CRS-reduction into a corresponding ρ-reduction. Since for this purpose we need to make precise the matching used when evaluating CRS, the second contribution of the paper is to present an original matching algorithm for CRS terms that uses a simple term translation and the classical matching of lambda terms.     

A Partition Refinement Algorithm for the π-Calculus

The partition refinement algorithm is the basis for most of the tools for checking bisimulation equivalences and for computing minimal realisations of CCS-like finite state processes. In this paper, we present a partition refinement algorithm for the π-calculus, a development of CCS where channel names can be communicated. It can be used to check bisimilarity and to compute minimal realisations of finite control processes—the π-calculus counterpart of CCS finite state processes. The algorithm is developed for strong open bisimulation and can be adapted to late and early bisimulations, as well as to weak bisimulations. To arrive at the algorithm, a few laws, proof techniques, and four characterizations of open bisimulation are proved.