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.     

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.     

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.     

A hierarchy of deterministic context-free ω-languages

Twenty years ago, Klaus. W. Wagner came up with a hierarchy of ω-regular sets that actually bears his name. It turned out to be exactly the Wadge hierarchy of the sets of ω-words recognized by deterministic finite automata. We describe the Wadge hierarchy of context-free ω-languages, which stands as an extension of Wagner's work from automata to pushdown automata.     

μ-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.     

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.     

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.     

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.     

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.     

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.     

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.     

On the Use of Automata-based Techniques in Symbolic Model Checking: Invited Address

Checking infinite-state systems is frequently done by encoding infinite sets of states as regular languages. Computing such a regular representation of, say, the reachable set of states of a system requires acceleration techniques that can finitely compute the effect of an unbounded number of transitions. Among the acceleration techniques that have been proposed, one finds both specific and generic techniques. Specific techniques exploit the particular type of system being analyzed, e.g. a system manipulating queues or integers, whereas generic techniques only assume that the transition relation is represented by a finite-state transducer, which has to be iterated. In this paper, we survey two generic techniques that have been presented in [B. Boigelot and A. Legay and P. Wolper, Iterating Transducers in the Large, Proc. 15th Int. Conf. on Computer Aided Verification, Boulder, USA, Lecture Notes in Computer Science, volume 2725, year 2003, pages 223–235] and [B. Boigelot and A. Legay and P. Wolper, Omega-Regular Model Checking, Proc. 10th Int. Conf. on Tools and and Algorithms for the Construction and Analysis of Systems, Barcelona, Spain, Lecture Notes in Computer Science, volume 2988, year 2004, pages 561–575]. Those techniques build on earlier work, but exploits a number of new conceptual and algorithmic ideas, often induced with the help of experiments, that give it a broad scope, as well as good performance.     

Interaction Nets vs. the ρ-calculus: Introducing Bigraphical Nets

The ρ-calculus generalises both term rewriting and the λ-calculus in a uniform framework. Interaction nets are a form of graph rewriting which proved most successful in understanding the dynamics of the λ-calculus, the prime example being the implementation of optimal β-reduction. It is thus natural to study interaction net encodings of the ρ-calculus as a first step towards the definition of efficient reduction strategies. We give two interaction net encodings which bring a new understanding to the operational semantics of the ρ-calculus; however, these encodings have some drawbacks and to overcome them we introduce bigraphical nets—a new paradigm of computation inspired by Lafont's interactions nets and Milner's bigraphs.     

一种紧同步随机Petri网模型的性能分析方法

紧同步随机Petri网模型常用于对多个子系统构成的实际系统进行建模.由于状态空间爆炸问题,这种模型的性能分析目前还没有得到很好的解决.首先给出了随机Petri网中顺序、并行、循环、选择这4种基本结构的性能近似等价公式,然后提出了一种同步变迁等价分解(synchronous transition equivalent decomposition,简称STED)法对紧同步随机Petri网进行分解求解,有效地缓解了具有一个或多个同步变迁情况下的空间爆炸问题,该方法对于子模型同构的情况处理简便且十分有效.     

An Overview of Cαml

Cαml is a tool that turns a so-called “binding specification” into an Objective Caml compilation unit. A binding specification resembles an algebraic data type declaration, but also includes information about names and binding. Cαml is meant to help writers of interpreters, compilers, or other programs-that-manipulate-programs deal with α-conversion in a safe and concise style. This paper presents an overview of Cαml's binding specification language and of the code that Cαml produces.     

Modeling,Reachability and Controllability of Bounded Petri Nets Based on Semi‐Tensor Product of Matrices

In this paper, we present a comprehensive modeling technique for bounded Petri net systems (BPNSs) in the framework of the semi‐tensor product (STP) of matrices. The two dynamic properties of BPNSs, namely, reachability and controllability, are investigated systematacially. First, the dynamics of a bounded Petri net system (BPNS), by resorting to the STP of matrices, are expressed in the form of a discrete‐time bilinear equation, which is called the marking evolution equation (MEE) of BPNSs. Second, controllability and transition‐marking adjacency matrix (TMAM) of BPNSs are defined, respectively. Further, several necessary and sufficient conditions for reachability and controllability of BPNSs are given in terms of the MEE and TMAM. Third, an efficient algorithm to verify reachability property of BPNSs, in this paper, is provided, as well as its computational complexity. Finally, an example is presented to illustrate the theoretical results in this paper. The main contribution of this paper is the presentation of a precise mathematical model for BPNSs. The main advantage of the proposed approach is that not only it can be applied to verify whether or not any given marking is reachable from the other in state space, but also it is very convenient to find all firing sequences between any two reachable markings.     

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.