Algebraic processing technique for extracting frequency-dependent shear-wave splitting parameters in an anisotropic medium

Based on the dual source cumulative rotation technique in the time-domain proposed by Zeng and MacBeth（1993）,a new algebraic processing technique for extracting shear-wave splitting parameters from multi-component VSP data in frequency-dependent medium has been developed.By using this dual source cumulative rotation technique in the frequency-domain（DCTF）,anisotropic parameters,including polarization direction of the shear-waves and timedelay between the fast and slow shear-waves,can be estimated for each frequency component in the frequency domain.It avoids the possible error which comes from using a narrow-band filter in the current commonly used method.By using synthetic seismograms,the feasibility and validity of the technique was tested and a comparison with the currently used method was also given.The results demonstrate that the shear-wave splitting parameters frequency dependence can be extracted directly from four-component seismic data using the DCTF.In the presence of larger scale fractures,substantial frequency dependence would be found in the seismic frequency range,which implies that dispersion would occur at seismic frequencies.Our study shows that shear-wave anisotropy decreases as frequency increases.

Research Progress of the Algebraic and Geometric Signal Processing

The investigation of novel signal processing tools is one of the hottest research topics in modern signal processing community. Among them, the algebraic and geometric signal processing methods are the most powerful tools for the representation of the classical signal processing method. In this paper, we provide an overview of recent contributions to the algebraic and geometric signal processing. Specifically, the paper focuses on the mathematical structures behind the signal processing by emphasizing the algebraic and geometric structure of signal processing. The two major topics are discussed. First, the classical signal processing concepts are related to the algebraic structures, and the recent results associated with the algebraic signal processing theory are introduced. Second, the recent progress of the geometric signal and information processing representations associated with the geometric structure are discussed. From these discussions, it is concluded that the research on the algebraic and geometric structure of signal processing can help the researchers to understand the signal processing tools deeply, and also help us to find novel signal processing methods in signal processing community. Its practical applications are expected to grow significantly in years to come, given that the algebraic and geometric structure of signal processing offer many advantages over the traditional signal processing.

Model for Software Behaviour Detection Based on Process Algebra and System Call

Behaviour detection models based on automata have been studied widely. By add- ing edge ε, the local automata are combined into global automata to describe and detect soft- ware behaviour. However, these methods in- troduce nondeterminacy, leading to models that are imprecise or inefficient. We present a model of software Behaviour Detection based on Process Algebra and system call （BDPA）. In this model, a system call is mapped into an action, and a function is mapped into a process We construct a process expression for each function to describe its behaviour. Without con- strutting automata or introducing nondeter- minacy, we use algebraic properties and algo- rithms to obtain a global process expression by combining the process expressions derived from each function. Behaviour detection rules and methods based on BDPA are determined by equivalence theory. Experiments demon- strate that the BDPA model has better preci- sion and efficiency than traditional methods.

Modeling and Analysis for Supply Chain Using Stochastic Process Algebra

In order to improve the influence of the uncertain and dynamic of node enterprise behavior on the performance of supply chain,the method based on stochastic process algebra for description,analysis,validation and evaluation of supply chain business process model is proposed.Firstly,the description of the uncertainty of node enterprise behavior is given using the extended Unified Modeling Language sequence diagram,and mapping rule is defined from the extended Unified Modeling Language sequence diagram to stochastic process algebra.Secondly,on the basis of the acquired stochastic process algebra model,the supply chain business process model is verified with Mobility Workbench.Finally,according to the operational semantics of stochastic process algebra,the continuous-time Markov chain,isomorphic with stochastic process algebra model,is built; and the system performance evaluation of transient status and stable status is respectively conducted in accordance with Markov transfer relations and the current state of system,obtaining the predicted performance value and average performance index value for a specific period of time.The simulation experiments show that the proposed method can accurately describe the stochastic behaviors of supply chain system and interactions among nodes,effectively verify the validity of the model,and objectively and exactly evaluate design of the supply chain.

Modeling and analysis of cloud computing system survivability based on Bio-PEPA

For the cloud computing system,combined wth the memory function and incomplete matching of the biological immune system,a formal modeling and analysis method of the cloud computing system survivability is proposed by analyzing the survival situation of critical cloud services.First,on the basis of the SAIR(susceptible,active,infected,recovered)model,the SEIRS(susceptible,exposed,infected,recovered,susceptible)model and the vulnerability diffusion model of the distributed virtual system,the evolution state of the virus is divided into six types,and then the diffusion rules of the virus in the service domain of the cloud computing system and the propagation rules between service domains are analyzee.Finally,on the basis of Bio-PEPA(biological-performance evaluation process algebra),the formalized modeling of the survivability evolution of critical cloud services is made,and the SLIRAS(susceptible,latent,infected,recovered,antidotal,susceptible)model is obtained.Based on the stochastic simulation and the ODEs(ordinary differential equations)simulation of the Bio-PEPA model,the sensitivity parameters of the model are analyzed from three aspects,namely,the virus propagation speed of inter-domain,recovery ability and memory ability.The results showthat the proposed model has high approximate fitting degree to the actual cloud computing system,and it can well reflect the survivable change of the system.

The specification and analysis of network embedded system

This paper proposes a formal method which is used to model and analyze network devices such as touters. It is based on an algebraic process called “ACSR-VP”, which enhances the original CCS algebraic process by incorporating the notions of time, resource requirements, dynamic prioritization, and synchronization. Therefore, although there are many formal methods to analyze the timed concurrency system, ACSR-VP, due to its prominent features, is best fit for analysis of a resource bounded real-time system. This paper extends ACSR-VP to EACSR-VP, which is more adaptive to the features of network devices and specializes in analyzing this kind of embedded system. EACSR-VP adds the notion of n-way communication which allows more than two processes to participate in synchronization. It also enhances value-passing capabilities which make for more flexible specifications. Finally, specifications, verification and analysis methods with EACSR-VP are introduced by a case study of router with multiple input queues.

Bisimulation Lattice of Asymmetric Chi Calculus with Mismatch

This paper carries out a systematic investigation into the bisimulation lattice of asymmetric chi calculus with a mismatch combinator. It is shown that all the sixty three L bisimilarities collapse to twelve distinct relations and they form a bisimulation lattice with respect to set inclusion. The top of the lattice coincides with the barbed bisimilarity.

A Novel Formal Analysis Method of Network Survivability Based on Stochastic Process Algebra

Stochastic process algebras have been proposed as compositional specification formalisms for performance models. A formal analysis method of survivable network was proposed based on stochastic process algebra, which incorporates formal modeling into performance analysis perfectly, and then various performance parameters of survivable network can be simultaneously obtained after formal modeling. The formal description with process expression to the survivable network system was carried out based on the simply introduced syntax and operational semantics of stochastic process algebra. Then PEPA workbench tool was used to obtain the probability of system’s steady state availability and transient state availability. Simulation experiments show the effectiveness and feasibility of the developed method.

Event-Based Operational Semantics and a Consistency Result for Real-Time Concurrent Processes with Action Refinement

In this paper an event-based operational interleaving semantics is proposed for real-time processes, for which action refinement and a denotational true concurrency semantics are developed and defined in terms of timed event structures. The authors characterize the timed event traces that are generated by the operational semantics in a denotational way, and show that this operational semantics is consistent with the denotational semantics in the sense that they generate the same set of timed event traces, thereby eliminating the gap between the true concurrency and interleaving semantics. Keywords action refinement - real-time process algebra - semantics - timed event structure - formal method This work was supported by the National Natural Science Foundation of China (Grant No. 60373113) and the “Hundred-Talent Program” of Chinese Academy of Sciences.Xiu-Li Sun was born in 1975. She received her B.S. degree in 1998 and M.S. degree in 2002 from Taiyuan University of Technology, Shanxi. She is studying in the Institute of Computer Application, Chengdu for her doctorate.Wen-Ying Zhang was born in 1972. Now he is a Ph.D. candidate of Computer Application, the Chinese Academy of Sciences. His current research interests include formal verification, digital watermarking and pattern recognition.Jin-Zhao Wu was born in 1965. He obtained his Ph.D. degree in 1994 from the Institute of System Science, CAS. From 1994 to 1999 he was a postdoctoral researcher. His research interests include formal specification and verification, automatic reasoning, logic programming.

A Polynomial Time Algorithm for Checking Regularity of Totally Normed Process Algebra

A polynomial algorithm for the regularity problem of weak and branching bisimilarity on totally normed process algebra(PA) processes is given. Its time complexity is O(n3+ mn), where n is the number of transition rules and m is the maximal length of the rules. The algorithm works for totally normed basic process algebra(BPA) as well as basic parallel process(BPP).

Formal modeling and quantitative evaluation for information system survivability based on PEPA

Survivability should be considered beyond security for information system. To assess system survivability accurately, for improvement, a formal modeling and analysis method based on stochastic process algebra is proposed in this article. By abstracting the interactive behaviors between intruders and information system, a transferring graph of system state oriented survivability is constructed. On that basis, parameters are defined and system behaviors are characterized precisely with performance evaluation process algebra （PEPA）, simultaneously considering the influence of different attack modes. Ultimately the formal model for survivability is established and quantitative analysis results are obtained by PEPA Workbench tool. Simulation experiments show the effectiveness and feasibility of the developed method, and it can help to direct the designation of survivable system.

Reaction Graph

The paper proposes reaction graphs as graphical representations of computational objects.A reaction graph is a directed graph with all its arrows and some of its nodes labeled. Compu-tations are modeled by graph rewriting of a simple nature. The basic rewriting rules embodythe essence of both the communications among processes and cut-eliminations in proofs. Cal-culi of graphs are identified to give a formal and algebraic account of reaction graphs in thespirit of process algebra. With the help of the calculi, it is demonstrated that reaction graphscapture many interesting aspects of computations.

The Infinite Evolution Mechanism of ∈-Bisimilarity

In this paper, we focus on the convergence mechanism of ε-bisimulation under probabilistic processes to discuss the dynamic correctness of the software. Firstly, ε-limit bisimulation is defined for reflecting the dynamic relation between software specification and implementation. Some special ε-limit bisimulations are showed. Secondly, ε-bisimulation limit is proposed, which states the specification is the limit of implementation under ε-bisimulation. The uniqueness of ε-bisimulation limit and consistence with ε-bisimulation are presented. Finally, the substitutivity laws of ε-bisimulation limit with various combinators are proved.

Modeling and Verifying Concurrent Programs with Finite Chu Spaces

Finite Chu spaces are proposed for the modeling and verification of concurrent programs.In order to model not only typical concurrent behaviors but also modern exception handling and synchronization mechanisms,we design an enriched process algebra of Chu spaces from a practical point of view.To illustrate the power of finite Chu spaces and the process algebra while abstracting away from language-specific details,an imaginary concurrent programming language（ICL） is designed.A denotational semantics of ICL is presented using finite Chu spaces and the enriched process algebra.The valuation functions are fairly straightforward since the carefully designed operators have done much of the job.The enriched process algebra is also used as the specification language for Chu spaces,with which process-algebraic properties can be specified.Verification algorithms are presented with their time complexities discussed.

An Invitation to Friendly Testing

We present a new testing semantics, called friendly testing, whose main property is thatthe induced preorder between processes fr is consistent with the conformance relation, andso we have, for instance, a b fr a fr a + b. The new theory is strongly based on De Nicola& Hennessy's work on testing. Friendly tests are defined exactly as in their work, except thatinternal actions are not allowed. However, in order to obtain the desired notion of friendlytesting this restriction is not enough and we also have to relax the conditions to pass a test.Thus we obtain a new testing semantics and a new preorder between processes which is strictlyweaker than the relation must. Moreover, we present an alternative characterization of ournew testing semantics by defining a modification of acceptance sets.

Performance Modelling of Patient Flow Scheduling Through a Formal Method

Smart environment is being used in many areas to deliver more services to individuals in a physical space, such as a hospital. In the UK, the National Health Service(NHS) provides free and high quality healthcare service for all residents. Smart hospital environment is able to support NHS and provide more convenience. Patient flow scheduling is a crucial section in a smart hospital environment. Smart hospital environment aims to provide a smart environment in the hospital to facilitate individual experience and improve the quality of healthcare service.First of all, this paper investigates a real world patient flow scenario of a hospital in the UK and models a general scheduling scheme based on the scenario using a compositional formal approach, i.e. performance evaluation process algebra(PEPA). This scheduling scheme uses an easy-implemented solution(the grouping scheme) to reduce the waiting queue in the hospital. Secondly, fluid flow analysis is used for the performance analysis by generating a set of ordinary differential equations(ODEs) in terms of the PEPA model.

A functional presentation of Pi calculus

From the very beginning process algebra introduced the dichotomy between channels and processes. This dichotomy prevails in all present process calculi. The situation is in contrast to that withlambda calculus which has only one class of entities-the lambda terms. We introduce in this papera process calculus called Lamp in which channels are process names. The language is more uniform than existing process calculi in two aspects: First it has a unified treatment of channels and processes.There is only one class of syntactical entities-processes. Second it has a unified presentation ofboth first order and higher order process calculi. The language is functional in the sense that lambda calculus is functional. Two bisimulation equivalences, barbed and closed bisimilarities, are proved to coincide.A natural translation from Pi calculus to Lamp is shown to preserve both operational and algebraic semantics. The relationship between lazy lambda calculus and Lamp is discussed.