An analytical method for assessing stage-specific drug activity in Plasmodium vivax malaria : implications for ex vivo drug susceptibility testing

The emergence of highly chloroquine (CQ) resistant P. vivax in Southeast Asia has created an urgent need for an improved understanding of the mechanisms of drug resistance in these parasites, the development of robust tools for defining the spread of resistance, and the discovery of new antimalarial agents. The ex vivo Schizont Maturation Test (SMT), originally developed for the study of P. falciparum, has been modified for P. vivax. We retrospectively analysed the results from 760 parasite isolates assessed by the modified SMT to investigate the relationship between parasite growth dynamics and parasite susceptibility to antimalarial drugs. Previous observations of the stage-specific activity of CQ against P. vivax were confirmed, and shown to have profound consequences for interpretation of the assay. Using a nonlinear model we show increased duration of the assay and a higher proportion of ring stages in the initial blood sample were associated with decreased effective concentration (EC50) values of CQ, and identify a threshold where these associations no longer hold. Thus, starting composition of parasites in the SMT and duration of the assay can have a profound effect on the calculated EC50 for CQ. Our findings indicate that EC50 values from assays with a duration less than 34 hours do not truly reflect the sensitivity of the parasite to CQ, nor an assay where the proportion of ring stage parasites at the start of the assay does not exceed 66%. Application of this threshold modelling approach suggests that similar issues may occur for susceptibility testing of amodiaquine and mefloquine. The statistical methodology which has been developed also provides a novel means of detecting stage-specific drug activity for new antimalarials.

Improving the efficiency of high power piezoelectric transducers for industrial applications

Most high-power ultrasound applications are driven by two-level inverters. However, the broad spectral content of the two-level pulse results in undesired harmonics that can decrease the performance of the system significantly. On the other hand, it is crucial to excite the piezoelectric devices at their main resonant frequency in order to have maximum energy conversion. Therefore a high-quality, low-distorted power signal is needed to excite the high-power piezoelectric transducer at its resonant frequency. This study proposes an efficient approach to develop the performance of high-power ultrasonic applications using multilevel inverters along with a frequency estimation algorithm. In this method, the resonant frequencies are estimated based on relative minimums of the piezoelectric impedance frequency response. The algorithm follows the resonant frequency variation and adapts the multilevel inverter reference frequency to drive an ultrasound transducer at high power. Extensive simulation and experimental results indicate the effectiveness of the proposed approach.

Investigations of dielectric monitoring on an energised transformer oil–paper insulation system

Frequency domain spectroscopy (FDS) is being used to assess the insulation condition of oil–paper power transformers. However, it has to date only been implemented on de-energised transformers, which requires the transformers to be shut down for an extended period and may cause significant costs. To solve this issue, a newly improved monitoring method based on the FDS principle is proposed to implement the dielectric measurement on energised transformers. Moreover, a chirp waveform excitation and its novel processing method are introduced. Compared with the conventional FDS results, dielectric results from the energised insulation system have higher tanδ values because of the increased losses. To further understand the insulation ageing process, the effects of the geometric capacitance are removed from the measured imaginary admittance of the insulation system to enhance the ageing signature. The resulting imaginary admittance is then shown to correlate well with the central time constant in return voltage measurements results. The proposed methods address the issues on techniques used on energised transformers and provide a clue for on-line FDS diagnostic application.

Template-based circuit understanding

When verifying or reverse-engineering digital circuits, one often wants to identify and understand small components in a larger system. A possible approach is to show that the sub-circuit under investigation is functionally equivalent to a reference implementation. In many cases, this task is difficult as one may not have full information about the mapping between input and output of the two circuits, or because the equivalence depends on settings of control inputs. We propose a template-based approach that automates this process. It extracts a functional description for a low-level combinational circuit by showing it to be equivalent to a reference implementation, while synthesizing an appropriate mapping of input and output signals and setting of control signals. The method relies on solving an exists/forall problem using an SMT solver, and on a pruning technique based on signature computation.

Effect of morphology on electrical treeing in low density polyethylene nanocomposites

Influence of polymer morphology on the inception and the growth of electrical trees in unfilled low density polyethylene (LDPE) as well as LDPE filled with 1, 3 and 5% by weight nanoalumina samples stressed with 50 Hz ac voltage has been studied. It is seen that there is a significant improvement in tree inception voltage with filler loading in LDPE filled with nanoparticles. Tree inception voltage increased with the filler loading up to 3% by weight nanoalumina loading and showed a reduction at 5% by weight loading. Change in tree growth patterns from branch to bush as well as a slower tree growth with increase in filler loading in LDPE alumina nanocomposites were observed. The degree of crystallinity and change in crystalline morphology induced by the presence of alumina nanoparticles in LDPE was studied using differential scanning calorimetry (DSC) and scanning electron microscopy (SEM). DSC results show a similar melting behaviour for both unfilled LDPE and LDPE nanocomposites. However, there is a reduction in the degree of crystallinity for LDPE filled with 5% by weight nanoalumina. An increase in lamellae packing with increase in filler loadings and a highly disordered spherulitic structure for LDPE filled with 5% by weight nanoalumina was observed from the SEM images. The slow propagation of tree growth as well as reduction in tree inception voltage with increase in filler loadings were attributed to the morphological changes observed in the LDPE nanocomposites.

Analogous Synaptic Plasticity Profiles Emerge from Disparate Channel Combinations

An open question within the Bienenstock-Cooper-Munro theory for synaptic modification concerns the specific mechanism that is responsible for regulating the sliding modification threshold (SMT). In this conductance-based modeling study on hippocampal pyramidal neurons, we quantitatively assessed the impact of seven ion channels (R- and T-type calcium, fast sodium, delayed rectifier, A-type, and small-conductance calcium-activated (SK) potassium and HCN) and two receptors (AMPAR and NMDAR) on a calcium-dependent Bienenstock-Cooper-Munro-like plasticity rule. Our analysis with R- and T-type calcium channels revealed that differences in their activation-inactivation profiles resulted in differential impacts on how they altered the SMT. Further, we found that the impact of SK channels on the SMT critically depended on the voltage dependence and kinetics of the calcium sources with which they interacted. Next, we considered interactions among all the seven channels and the two receptors through global sensitivity analysis on 11 model parameters. We constructed 20,000 models through uniform randomization of these parameters and found 360 valid models based on experimental constraints on their plasticity profiles. Analyzing these 360 models, we found that similar plasticity profiles could emerge with several nonunique parametric combinations and that parameters exhibited weak pairwise correlations. Finally, we used seven sets of virtual knock-outs on these 360 models and found that the impact of different channels on the SMT was variable and differential. These results suggest that there are several nonunique routes to regulate the SMT, and call for a systematic analysis of the variability and state dependence of the mechanisms underlying metaplasticity during behavior and pathology.

Experimental characterisation and performance evaluation of a coaxial current transformer for measurement of insulated gate bipolar transistor switching current

Measurement of device current during switching characterisation of an insulated gate bipolar transistor (IGBT) requires a current sensor with low insertion impedance and high bandwidth. This study presents an experimental procedure for evaluating the performance of a coaxial current transformer (CCT), designed for the above purpose. A prototype CCT, which can be mounted directly on a power terminal of a 1200 V/50 A half-bridge IGBT module, is characterised experimentally. The measured characteristics include insertion impedance, gain and phase of the CCT at different frequencies. The bounds of linearity within which the CCT can operate without saturation are determined theoretically, and are also verified experimentally. The experimental study on linearity of the CCT requires a high-amplitude current source. A proportional-resonant (PR) controller-based current-controlled half-bridge inverter is developed for this purpose. A systematic procedure for selection of PR controller parameters is also reported in this study. This set-up is helpful to determine the limit of linearity and also to measure the frequency response of the CCT at realistic amplitudes of current in the low-frequency range.

Improving speech transcription for Mandarin-english translation

This paper describes the development of the CU-HTK Mandarin Speech-To-Text (STT) system and assesses its performance as part of a transcription-translation pipeline which converts broadcast Mandarin audio into English text. Recent improvements to the STT system are described and these give Character Error Rate (CER) gains of 14.3% absolute for a Broadcast Conversation (BC) task and 5.1% absolute for a Broadcast News (BN) task. The output of these STT systems is then post-processed, so that it consists of sentence-like segments, and translated into English text using a Statistical Machine Translation (SMT) system. The performance of the transcription-translation pipeline is evaluated using the Translation Edit Rate (TER) and BLEU metrics. It is shown that improving both the STT system and the post-STT segmentations can lower the TER scores by up to 5.3% absolute and increase the BLEU scores by up to 2.7% absolute. © 2007 IEEE.

Morphological decomposition in Arabic ASR systems

In recent years, the use of morphological decomposition strategies for Arabic Automatic Speech Recognition (ASR) has become increasingly popular. Systems trained on morphologically decomposed data are often used in combination with standard word-based approaches, and they have been found to yield consistent performance improvements. The present article contributes to this ongoing research endeavour by exploring the use of the 'Morphological Analysis and Disambiguation for Arabic' (MADA) tools for this purpose. System integration issues concerning language modelling and dictionary construction, as well as the estimation of pronunciation probabilities, are discussed. In particular, a novel solution for morpheme-to-word conversion is presented which makes use of an N-gram Statistical Machine Translation (SMT) approach. System performance is investigated within a multi-pass adaptation/combination framework. All the systems described in this paper are evaluated on an Arabic large vocabulary speech recognition task which includes both Broadcast News and Broadcast Conversation test data. It is shown that the use of MADA-based systems, in combination with word-based systems, can reduce the Word Error Rates by up to 8.1 relative. © 2012 Elsevier Ltd. All rights reserved.

Phrase linguistic classification and generalization for improving statistical machine translation

In this paper a method to incorporate linguistic information regarding single-word and compound verbs is proposed, as a first step towards an SMT model based on linguistically-classified phrases. By substituting these verb structures by the base form of the head verb, we achieve a better statistical word alignment performance, and are able to better estimate the translation model and generalize to unseen verb forms during translation. Preliminary experiments for the English - Spanish language pair are performed, and future research lines are detailed. © 2005 Association for Computational Linguistics.

N-gram posterior probability confidence measures for statistical machine translation: An empirical study

We report an empirical study of n-gram posterior probability confidence measures for statistical machine translation (SMT). We first describe an efficient and practical algorithm for rapidly computing n-gram posterior probabilities from large translation word lattices. These probabilities are shown to be a good predictor of whether or not the n-gram is found in human reference translations, motivating their use as a confidence measure for SMT. Comprehensive n-gram precision and word coverage measurements are presented for a variety of different language pairs, domains and conditions. We analyze the effect on reference precision of using single or multiple references, and compare the precision of posteriors computed from k-best lists to those computed over the full evidence space of the lattice. We also demonstrate improved confidence by combining multiple lattices in a multi-source translation framework. © 2012 The Author(s).

限界模型检测方法及其应用

形式化验证主要是通过精确的分析来证明或证伪硬件或软件系统中一些明确的声明或者性质。形式化验证方法在广义上可以分成两大类：模型检测和定理证明。模型检测由对模型的所有状态和迁移做详尽访问的自动检测机制组成。这种机制是通过对适当的抽象模型进行直接或间接的状态枚举技术来实现的，从而证明模型中存在或者不存在所谓的“瑕疵”状态。定理证明则是运用数学推理和逻辑推论来证明系统的正确性。本文所讨论的就是模型检测方法中的限界模型检测方法及其相关的改进和应用。近些年来，基于可满足性求解（SAT）的限界模型检测方法作为基于BDD的模型检测方法的一种有效的补充，已经有了一定的发展。A. Biere等人最先提出了对于线性时序逻辑公式（LTL）的限界模型检测方法，进而，W.Penczek又提出了对于全局计算树逻辑（ACTL）的限界模型检测方法。由于模型检测方法具有很高的复杂性，因此，其效率问题始终倍受关注。论文第一个方面的重要贡献就体现在提高限界模型检测效率方面的相关研究上。我们对Penczek提出的限界模型检测方法进行了两方面的改进，以提高其求解效率。第一方面的改进是通过改进所需路径条数计算函数，将时序操作符EX和其它时序操作符区分开来，以减少编码时所需的迁移关系和变量数目；第二方面的改进则是采用统一路径编码的方式来简化公式的编码。通过这两方面的改进，公式在最坏情况下的编码复杂度得到了有效的降低。同时，我们还在工具BMV中实现了改进后的方法。随着实时系统的应用日益广泛，在对全局计算树逻辑的限界模型检测方法做了改进，提高了其求解效率以后，我们又将目光转移到了对实时系统的限界模型检测上。如何将限界模型检测方法高效的运用到对实时系统的检测当中成为了本文第二个方面的重要贡献。基于SAT的限界模型检测方法在对实时系统的模型和描述性质的公式进行编码时，需要对时间变量和时钟约束进行布尔编码，由于时间的连续性和不确定性，使得在对它进行布尔编码时，往往会相当的复杂，不仅耗费大量的时间，而且还不利于SAT的求解，即使是使用改进后的限界模型检测方法，整个验证过程的效率还是很低。所以，在对实时系统进行限界模型检测方面，我们转而考虑采用基于可满足性模块理论（SMT）的方法来对实时系统的模型和描述性质的公式进行编码。由于SMT可以直接处理基于整数或者实数的线性算术表达式，因此，我们可以直接用整型或者实型变量来表示时间变量，用线性算术表达式来表示时钟约束。与基于SAT的限界模型检测方法相比，基于SMT的限界模型检测方法在处理实时系统方面，不仅简化了编码过程，而且大大提高了求解效率。在此基础上，我们运用基于SAT的对全局计算树逻辑的限界模型检测方法中的改进思想，对基于SMT的实时系统的限界模型检测方法也做了相应的改进，使其求解效率较之改进前有了较大的提升。最后，我们就基于SAT的限界模型检测方法和基于SMT的限界模型检测方法以及它们的改进方法进行了一系列的实验对比。从实验结果可以看出，改进后的方法比改进前的方法在时间效率和空间效率上都有明显的提升，同时就实时系统来说，采用了SMT和限界模型检测相结合的方法以后，效率也比没有采用这两者的方法要高很多。

基于Yices对时间自动机的有界模型检测

随着工业化程度的提高，对模型的检测方法受到越来越大的重视。通常的检测方法有推理验证和模型检测。而相对于推理验证，模型检测由于其高度自动化的检测过程，在工业界有着更广泛的应用。 模型检测自从概念雏形开始之时，就受到状态爆炸问题的困扰。为了解决这个问题，不同的技术被提了出来。McMillan提出利用OBDD的符号模型检测方法在一定程度上解决了这个问题。另外，本文所主要讲述的有界模型检测，经大量的实践证明，对符号模型检测也是一个很好的补充。 由于问题的特殊性，科学家提出来不同的模型来描述不同情况的系统。由于时间自动机能够很好地描述异步系统，而且这种系统广泛地存在于现实生活中，对时间自动机这种特殊模型的验证方法的研究变得很有必要。另外，由于时间自动机带有实数域的时钟变量，这导致了时间自动机有一个无限域的状态迁移图。为了利用模型检测的方法对其进行验证，需要对时间变量进行预处理。一般的方法是把时钟所对应的时钟区或时钟域根据等价性，化为有限的域，相应地，把时间自动机转化为有限的状态迁移图。 为了避免在对时间自动机有界模型检测过程中对变量进行布尔编码以及对时间自动机模型中的时钟进行预处理，本文给出一个利用SMT工具进行的对时间自动机进行有界模型检测的方法。该方法的主要优点是无需将时间自动机中的时钟进行预处理，也不需要将模型中的变量进行布尔编码，只需将时间自动机转变为SMT工具可解的逻辑公式，利用SMT的高效求解来进行模型检测。实验结果表明，对于某些可达性性质的验证，这种方法的效率有一定的优势。

组合对象的搜索算法研究

现实世界中的大量问题涉及如何安排有限个离散的基本对象，使之满足特定约束，这类问题可通称为组合问题。本论文主要研究复杂的组合对象的存在性问题。我们特别关注较难求解的组合问题，从算法复杂度上来说，至少是NP难的。由于这些组合对象相应的约束一般都不太容易满足，因此局部搜索等非完备算法方法常常失效。我们致力于研究高效的完备搜索算法，能够在庞大的搜索空间中精准地找到解，当解不存在时，也能够给出确定性的回答。 作者在博士期间的工作可分为两部分：组合数学问题的自动求解和线性约束上的可满足性模理论的体积求解。 我们系统化地研究了组合数学问题的计算机求解，这部分研究包括三大类问题：幂等拟群的大集问题、正交拉丁方和正交数组。这些问题的共同特点是，要寻找的不是一个复杂的组合对象，而是一系列复杂的组合对象，这些对象相互之间还要满足一定的约束。这样一来，搜索空间比寻找单独的一个组合对象要庞大很多倍，问题的难度也大大增加了。对于每一类问题，我们都通过深入研究其结构特征，提出了有效的问题表示方法和搜索方法，发展了一系列新颖的消除同构技术来降低搜索空间，在搜索中我们应用了自动推理最新的技术和工具，如高效的一阶逻辑模型产生器和命题逻辑求解器等，取得了较好的效果。具体来说，我们的工作包括以下三点： (1) n阶幂等拟群的大集问题需要寻找n-2个不相交的幂等拟群，这比寻找单个的满足特定性质的拟群要困难的多。我们设计了约束分割的策略，解决了幂等拟群大集上的一系列开放性问题，特别是得出了LSPQ(11)不存在的结论。我们的方法不但可以回答特定的大集是否存在，还能够确定相互不相交的拟群的最大个数。这些数学结果对朱烈教授等数学家很有意义，并被收入``HandBook of Satisfiability"一书中。 (2) 正交拉丁方的存在性是组合数学中著名的问题。我们利用一阶逻辑有限模型产生器对该问题进行了尝试，提出了一种新的建模方法，称为横截建模，其效果比直接建模方法提高了若干个数量级。同时，我们也提出了一种新的打破对称策略。 (3) 正交数组是一种重要的组合数学结构，可用于软件组件的集成测试。我们设计了一个搜索正交数组的完备性算法，并提出了一些新颖的打破对称技术。与当前的其它工作不同，我们的算法是普适性的，对输入OA参数无任何限制，并且当搜索完成后总能得到确定性的答案。实验表明，我们的工具BOAS在搜索强度为3及其以上的正交数组时非常高效，而用传统的数学方法构造这些数组则很困难，局部搜索算法也对这些数组常常失效。而且，BOAS能够轻易地解决一批对于其它完备算法来说非常难的实例。 我们研究的第二个方面是线性理论上的SMT实例的体积计算问题。关于各类逻辑和约束语言的可满足性问题有大量的研究工作，比如SAT和可满足性模理论（SMT），另一方面，判定问题的计数版本在自动推理中也非常重要。我们研究了SMT的计数版本，即对给定的SMT实例（更精确地说，线性算术约束的布尔组合）如何计算解的个数，或者是说如何计算解空间的体积。这一问题同时扩展了命题逻辑的模型计数问题和凸多面体的体积计算问题。SMT实例的体积计算在许多领域都有潜在的应用价值，比如程序分析与验证和近似推理，但目前还没有相关的研究工作。我们首次研究了这一问题，提出了一个高效的体积计算方法——逐簇法，我们的算法集成了SMT求解中的最新技术。我们的原型工具在随机实例上产生了较好的效果，并可应用在实际的程序实例中，以寻找热门路径。

A Structured Prediction Approach for Statistical Machine Translation

We propose a new formally syntax-based method for statistical machine translation. Transductions between parsing trees are transformed into a problem of sequence tagging, which is then tackled by a search- based structured prediction method. This allows us to automatically acquire transla- tion knowledge from a parallel corpus without the need of complex linguistic parsing. This method can achieve compa- rable results with phrase-based method (like Pharaoh), however, only about ten percent number of translation table is used. Experiments show that the structured pre- diction approach for SMT is promising for its strong ability at combining words.