A Proof Search Specification of the π-Calculus

We present a meta-logic that contains a new quantifier (for encoding “generic judgments”) and inference rules for reasoning within fixed points of a given specification. We then specify the operational semantics and bisimulation relations for the finite π-calculus within this meta-logic. Since we restrict to the finite case, the ability of the meta-logic to reason within fixed points becomes a powerful and complete tool since simple proof search can compute this one fixed point. The quantifier helps with the delicate issues surrounding the scope of variables within π-calculus expressions and their executions (proofs). We shall illustrate several merits of the logical specifications we write: they are natural and declarative; they contain no side conditions concerning names of variables while maintaining a completely formal treatment of such variables; differences between late and open bisimulation relations are easy to see declaratively; and proof search involving the application of inference rules, unification, and backtracking can provide complete proof systems for both one-step transitions and for bisimulation.     

UppDMC: A Distributed Model Checker for Fragments of the μ-Calculus

We present UppDMC, a distributed model-checking tool. It is tailored for checking finite-state systems and μ-calculus specifications with at most one alternation of minimal and maximal fixed-point operators. This fragment is also known as . Recently, efficient game-based algorithms for this logic have been outlined.We describe the implementation of these algorithms within UppDMC and study their performance on practical examples. Running UppDMC on a simple workstation cluster, we were able to check liveness properties of the largest examples given in the VLTS Benchmark Suite, for which no answers were previously known.     

Handling Liveness Properties in (ω-)Regular Model Checking

Since the topic emerged several years ago, work on regular model checking has mostly been devoted to the verification of state reachability and safety properties. Though it was known that liveness properties could also be checked within this framework, little has been done about working out the corresponding details, and experimentally evaluating the approach. This paper addresses these issues in the context of regular model checking based on the encoding of states by finite or infinite words. It works out the exact constructions to be used in both cases, and solves the problem resulting from the fact that infinite computations of unbounded configurations might never contain the same configuration twice, thus making cycle detection problematic. Several experiments showing the applicability of the approach were successfully conducted.     

On the ω-language Expressive Power of Extended Petri Nets

In this paper, we study the expressive power of several monotonic extensions of Petri nets. We compare the expressive power of Petri nets, Petri nets extended with non-blocking arcs and Petri nets extended with transfer arcs, in terms of ω-languages. We show that the hierarchy of expressive powers of those models is strict. To prove these results, we propose original techniques that rely on well-quasi orderings and monotonicity properties.     

Strong normalisation in the π-calculus

We introduce a typed π-calculus where strong normalisation is ensured by typability. Strong normalisation is a useful property in many computational contexts, including distributed systems. In spite of its simplicity, our type discipline captures a wide class of converging name-passing interactive behaviour. The proof of strong normalisability combines methods from typed λ-calculi and linear logic with process-theoretic reasoning. It is adaptable to systems involving state, non-determinism, polymorphism, control and other extensions. Strong normalisation is shown to have significant consequences, including finite axiomatisation of weak bisimilarity, a fully abstract embedding of the simply typed λ-calculus with products and sums and basic liveness in interaction. Strong normalisability has been extensively studied as a fundamental property in functional calculi, term rewriting and logical systems. This work is one of the first steps to extend theories and proof methods for strong normalisability to the context of name-passing processes.     

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.     

μ-Bases and singularities of rational planar curves

We provide a technique to detect the singularities of rational planar curves and to compute the correct order of each singularity including the infinitely near singularities without resorting to blow ups. Our approach employs the given parametrization of the curve and uses a μ-basis for the parametrization to construct two planar algebraic curves whose intersection points correspond to the parameters of the singularities including infinitely near singularities with proper multiplicity. This approach extends Abhyankar's method of t-resultants from planar polynomial curves to rational planar curves. We also derive the classical result that for a rational planar curve of degree n the sum of all the singularities with proper multiplicity is (n−1)(n−2)/2. Examples are provided to flesh out our results.     

Expressiveness of Probabilistic π-calculus

In this work we propose a probabilistic extension of the π-calculus. The main novelty is a probabilistic mixed choice operator, that is, a choice construct with a probability distribution on the branches, and where input and output actions can both occur as guards. We develop the operational semantics of this calculus, and then we investigate its expressiveness. In particular, we compare it with the sublanguage with the two separate choices, where input and output guards are not allowed together in the same choice construct. Our main result is that the separate choices can encode the mixed one. Further, we show that input-guarded choice can encode output-guarded choice and viceversa. In contrast, we conjecture that neither of them can encode the pair of the two separate choices.     

A Behavioural Pseudometric based on λ–Bisimilarity

In order to describe approximate equivalence among processes, the notions of λ–bisimilarity and behavioural pseudometric have been introduced by Ying and van Breugel respectively. Van Breugel provides a distance function induced by λ–bisimilarity, and conjectures that his behavioural pseudometric coincides with this function. This paper is inspired by this conjecture. We give a negative answer for van Breugel's conjecture first. Moreover, we show that the distance function induced by λ–bisimilarity is a pseudometric on states, and provide a fixed point characterization of this pseudometric.     

Divide and Congruence Applied to η-Bisimulation

We present congruence formats for η- and rooted η-bisimulation equivalence. These formats are derived using a method for decomposing modal formulas in process algebra. To decide whether a process algebra term satisfies a modal formula, one can check whether its subterms satisfy formulas that are obtained by decomposing the original formula. The decomposition uses the structural operational semantics that underlies the process algebra.     

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.     

Preparation and characterization of nanocrystalline α-Fe2O3 by a sol-gel process

α-Fe₂O₃ ultra-fine powder with an average particle size of 6–26nm has been prepared by a sol-gel process. Thermal analysis, X-ray diffraction and transmission electron microscope were used to study its formation process and micro-structure. The temperature dependence of the electric conductance of the elements made of nanocrystalline α-Fe₂O₃ shows that the gas-sensing properties are strongly related to its surface. The elements exhibited good sensitivity and selectivity to ethyl alcohol, indicating it is a promising alcohol-sensing material.     

On discrete lower π-strategies

Two-person zero-sum differential games of survival are investigated. It is assumed that player I, as well as player II, can employ during the course of the game any lower π-strategy [2], π(t_i) being a finite partition of [t₀, ∞). The concept of a discrete lower π-strategy is introduced and it is shown that if player I (II) confines himself to the space of discrete lower π-strategies, being a subset of the space of lower π-strategies, then he will be able to force the same lower (upper) value as if he could employ any lower π-strategy. Since we do not use any deep facts about differential games, the results contained here might be extended to continuous games.     

Open Bisimulation, Revisited

In the context of the π-calculus, open bisimulation is prominent and popular due to its congruence properties and its easy implementability. Motivated by the attempt to generalise it to the spi-calculus, we offer a new, more refined definition and show in how far it coincides with the original one.     

Gas sensitivity of Zn doped α-Fe2O3(SO4, Sn, Zn) to carbon monoxide

It is shown that the doping of Zn and Sn can improve the gas sensitivity of α-Fe₂O₃-based sensing material to CO. X-ray photo-electron spectroscopy analysis suggests that this is mainly due to the fact that the simultaneous doping of Zn and Sn can increase the S and hence SO₄²⁻ contents in the α-Fe₂O₃(SO₄²⁻, Sn, Zn) sensing material. The results also suggest that under a given condition, the gas sensitivity of α-Fe₂O₃(SO₄²⁻, Sn, Zn) to CO can be optimised by properly adjusting the doped Zn content.     

Interaction in Time and Space

Distributed π-calculus and ambient calculus are extended with timers which may trigger timeout recovery processes. Timers provide a useful notion of relative time with respect to the interaction in a distributed system. The rather flat notion of space in timed distributed π-calculus is improved by considering a hierarchical representation of space in timed mobile ambients. Some basic results are proven, making sound both formal approaches. An easily understood example is used for both extensions, showing how it is possible to describe a non-monotonic behaviour and use a decentralized control to coordinate the interacting components in time and space.