Realizability models and implicit complexity

New, simple, proofs of soundness (every representable function lies in a given complexity class) for Elementary Affine Logic, LFPL and Soft Affine Logic are presented. The proofs are obtained by instantiating a semantic framework previously introduced by the authors and based on an innovative modification of realizability. The proof is a notable simplification on the original already semantic proof of soundness for the above mentioned logical systems and programming languages. A new result made possible by the semantic framework is the addition of polymorphism and a modality to LFPL, thus allowing for an internal definition of inductive datatypes. The methodology presented proceeds by assigning both abstract resource bounds in the form of elements from a resource monoid and resource-bounded computations to proofs (respectively, programs).     

Realization and synthesis of reversible functions

Reversible circuits play an important role in quantum computing. This paper studies the realization problem of reversible circuits. For any n-bit reversible function, we present a constructive synthesis algorithm. Given any n-bit reversible function, there are N distinct input patterns different from their corresponding outputs, where N≤2ⁿ, and the other (2ⁿ−N) input patterns will be the same as their outputs. We show that this circuit can be synthesized by at most 2n⋅N ‘(n−1)’-CNOT gates and 4n²⋅N NOT gates. The time and space complexities of the algorithm are Ω(n⋅4ⁿ) and Ω(n⋅2ⁿ), respectively. The computational complexity of our synthesis algorithm is exponentially lower than that of breadth-first search based synthesis algorithms.     

On the axiomatizability of priority II

This paper contributes to the study of the equational theory of the priority operator of Baeten, Bergstra and Klop in the setting of the process algebra BCCSP. It is shown that, in the presence of at least two actions, the collection of process equations over BCCSP with the priority operator that are valid modulo bisimilarity, irrespective of the chosen priority order over actions, is not finitely based. This holds true even if one restricts oneself to the collection of valid process equations that do not contain occurrences of process variables.     

A linear translation from CTL* to the first-order modal μ -calculus

The modal μ-calculus is a very expressive temporal logic. In particular, logics such as LTL, CTL and CTL* can be translated into the modal μ-calculus, although existing translations of LTL and CTL* are at least exponential in size. We show that an existing simple first-order extension of the modal μ-calculus allows for a linear translation from LTL. Furthermore, we show that solving the translated formulae is as efficient as the best known methods to solve LTL formulae directly.     

A calculus for four-valued sequential logic

We present a complete axiomatisation for four-valued sequential logic. It consists of nine axioms, from which all valid laws can be derived by equational reasoning. These nine axioms are independent of each other.     

求解VLSI 电路划分问题的混合粒子群优化算法

电路划分是VLSI物理设计过程中的一个关键阶段.该问题本质上是一个NP困难的组合优化问题.针对该问题,提出了一种带FM策略的混合粒子群优化算法.引入遗传算法的两点交叉算子和随机两点交换变异算子,保证了粒子在位置更新后依然可行;为了提高算法的局部搜索能力,将具有较强局部搜索能力的FM策略融入算法的位置更新;设计了种群多样性变异策略,提高了种群多样性,避免了易陷入局部最优的缺陷.对ISCAS89标准测试电路的仿真实验结果表明,所构造的算法是有效的.     

基于软计算思想解决含干扰输入多值异或问题的研究

介绍一种解决含干扰输入多值异或问题的方法。该方法利用遗传算法寻找神经网络结构,使用模糊逻辑控制神经网络的学习率和冲量,并用传播算法训练得到神经网络。结果显示,这种方法能针对问题得到泛化性能、时间复杂度上表现都较为优秀的网络。     

光电探测器前置放大电路研究

在弱光检测中,光经过光电探测器转换为电信号,此信号极其微弱。要实现光电转换,并有效地利用这种信号,必须对光电器件采取适当偏置,然后再将已转换的电信号进行放大处理。对光电导器件、光伏型探测器、光电流型探测器的前置电路进行研究与设计。根据不同种类的探测器及探测光信号的频率特性选取不同的偏置与放大电路,使前置电路的性能达到最优。     

基于混合逻辑动态的列车运行调度模型

通过对列车运行调度问题的分析,指出列车运行过程中存在正常事件、客观事件和主观事件三种类型事件,调度的本质是主观事件通过改变列车的运行速度来克服客观事件对列车造成的影响,是典型的混杂系统.在考虑车站股道约束和区间容量两个约束条件的基础上,采用混合逻辑动态理论建立了列车运行调度模型,仿真结果表明了模型的有效性.     

一种13bit 40MS/s采样保持电路设计

设计了一个用于13bit40MS/s流水线ADC中的采样保持电路。该电路采用电容翻转结构,主运算放大器采用增益提高型折叠式共源共栅结构,以满足高速和高精度的要求。为减小与输入信号相关的非线性失真以获得良好的线性度,采用栅压自举开关。采用电源电压为3.3V的TSMC0.18μm工艺对电路进行设计和仿真,仿真结果表明,在40MHz的采样频率下,采用保持电路的SNDR达到84.8dB,SFDR达到92dB。