基于BDD的增量启发式方法及其应用

增量启发式搜索是一种利用先前的搜索信息和启发信息提高本次搜索效率的方法，通常可用来解决动态环境下的重规划问题。在人工智能领域，一些实时系统常常需要根据外界环境的变化不断修正自身，这样就会产生一系列变化较小的相似问题，此时应用增量启发式搜索将会非常有效。 另一方面，基于BDD的强大的搜索技术利用BDD有效操作性以及化简后唯一性的优点，在一定程度上缓解了模型检测的状态爆炸问题，使得被检测状态的个数大大增加。 1、本文结合基于BDD的启发式搜索和基于BDD的增量搜索这两种方法给出了基于BDD的增量启发式搜索方法，基于BDD的增量启发式搜索综合了基于BDD的搜索、增量搜索以及启发式搜索这三种方法的优点。它既用BDD作为数据结构以提高搜索的空间效率，又结合了增量搜索的思想来提高重搜索的效率，同时，又引入了启发函数来进一步压缩搜索空间。 2、本文介绍了基于BDD的增量启发式搜索算法BDDRPA*并用大量的实验结果证明BDDRPA*的高效性。给定一个搜索问题，BDDRPA*算法先用基于BDD的启发式搜索方法搜出一条从初始节点到目标节点的最短路径；接着，问题的状态格局发生改变，BDDRPA*再用基于BDD的增量搜索方法根据旧格局的迁移关系BDD_T构造出新格局的迁移关系BDD_{T'}，然后再用启发式方法搜索路径，如此反复下去。 3、本文介绍了基于BDD的动态增量启发式搜索算法BDDD*并用大量的实验结果证明BDDD*的高效性。BDDD*算法在机器人边走边扫描的过程中，不断根据机器人新获得的信息更新已知地图并重新规划路线。每次规划时，BDDD*都假设未知的领域没有任何障碍物，也就是每个位置都是可通的，它按照这个假设去计算从当前位置到目标位置的最短路径。如果在行走的过程中扫描到了障碍物，它就把这条信息添加到它的地图中，然后重复上面的过程，直到到达目标位置或者发现每条路径都被堵死为止。 BDDRPA*算法和BDDD*算法可以应用到机器人线路规划、智能交通及计算机网络的线路规划问题中。另外，在机器学习和控制领域，也可以考虑使用BDDRPA*算法和BDDD*算法。

基于BDD的增量启发式搜索

增量搜索是一种利用先前的搜索信息提高本次搜索效率的方法,通常可以用来解决动态环境下的重规划问题.在人工智能领域,一些实时系统常常需要根据外界环境的变化不断修正自身,这样就会产生一系列变化较小的相似问题,此时应用增量搜索将会非常有效.另外,基于BDD(binary decision diagram)的启发式搜索,结合了基于BDD的搜索和启发式搜索这两种方法的优点.它既用BDD这一紧凑的数据结构来表示系统的状态空间,又通过使用启发信息来进一步压缩搜索树的大小.在介绍基于BDD的启发式搜索和增量搜索之后,结合这两种方法给出了基于BDD的增量启发式搜索算法——BDDRPA*.大量的实验结果表明,BDDRPA*算法是非常有效的,它可以被广泛地应用到智能规划、移动机器人问题等领域中.

基于BDD的增量启发式搜索方法及其应用

增量启发式搜索是一种利用先前的搜索信息和启发信息提高本次搜索效率的方法，通常可用来解决动态环境下的重规划问题。在人工智能领域，一些实时系统常常需要根据外界环境的变化不断修正自身，这样就会产生一系列变化较小的相似问题，此时应用增量启发式搜索将会非常有效。另一方面，基于BDD的强大的搜索技术利用BDD有效操作性以及化简后唯一性的优点， 在一定程度上缓解了模型检测的状态爆炸问题，使得被检测状态的个数大大增加。 1、本文结合基于BDD的启发式搜索和基于BDD的增量搜索这两种方法给出了基于BDD的增量启发式搜索方法， 基于BDD的增量启发式搜索综合了基于BDD的搜索、增量搜索以及启发式搜索这三种方法的优点。它既用BDD作为数据结构以提高搜索的空间效率， 又结合了增量搜索的思想来提高重搜索的效率，同时，又引入了启发函数来进一步压缩搜索空间。 2、本文介绍了基于BDD的增量启发式搜索算法BDDRPA*并用大量的实验结果证明BDDRPA*的高效性。给定一个搜索问题， BDDRPA*算法先用基于BDD的启发式搜索方法搜出一条从初始节点到目标节点的最短路径；接着， 问题的状态格局发生改变，BDDRPA*再用基于BDD的增量搜索方法根据旧格局的迁移关系BDD_T构造出新格局的迁移关系BDD_{T'}， 然后再用启发式方法搜索路径，如此反复下去。 3、本文介绍了基于BDD的动态增量启发式搜索算法BDDD*并用大量的实验结果证明BDDD*的高效性。 BDDD*算法在机器人边走边扫描的过程中，不断根据机器人新获得的信息更新已知地图并重新规划路线。每次规划时，BDDD*都假设未知的领域没有任何障碍物， 也就是每个位置都是可通的，它按照这个假设去计算从当前位置到目标位置的最短路径。如果在行走的过程中扫描到了障碍物，它就把这条信息添加到它的地图中，然后重复 上面的过程，直到到达目标位置或者发现每条路径都被堵死为止。 BDDRPA*算法和BDDD*算法可以应用到机器人线路规划、智能交通及计算机网络的线路规划问题中。 另外，在机器学习和控制领域，也可以考虑使用BDDRPA*算法和BDDD*算法。

Fabrication and characterization of active and sequential circuits utilizing Schottky-wrap-gate-controlled GaAs hexagonal nanowire network structures

For realization of hexagonal BDD-based digital systems, active and sequential circuits including inverters, flip flops and ring oscillators are designed and fabricated on GaAs-based hexagonal nanowire networks controlled by Schottky wrap gates (WPGs), and their operations are characterized. Fabricated inverters show comparatively high transfer gain of more than 10. Clear and correct operation of hexagonal set-reset flip flops (SR-FFs) is obtained at room temperature. Fabricated hexagonal D-type flip flop (D-FF) circuits integrating twelve WPG field effect transistors (FETs) show capturing input signal by triggering although the output swing is small. Oscillatory output is successfully obtained in a fabricated 7-stage hexagonal ring oscillator. Obtained results confirm that a good possibility to realize practical digital systems can be implemented by the present circuit approach.

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

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

一种新型二元判定图器件和电路

提出了一种基于二元判定图(BDD)原理的新型逻辑器件和电路.BDD器件以电流模式的开关电流存储器为基本单元,具有符合二元判定图的两向通路的特点.用这种器件按照BDD树形图可以构成任意形式的组合逻辑电路.给出了或门、异或门及四位加法器电路的例子,并使用HSPICE仿真器进行了仿真,验证了这种器件及其电路的正确性.

Concentrations and distribution of organochlorine pesticides in shellfish from Changjiang estuary

To analyze and evaluate the status of organochlorine pollutants in the Changjiang (Yangtze River) estuary and adjacent waters, the concentrations of hexachlorocyclohexane (HCHs) and dichlorodiphenyltrichloroethane (DDTs) in shellfish collected in study area from 2006 to 2007 were determined with gas chromatography (GC). The concentration range of HCHs was (ND-12.13)x10(-3) mg/kg wet weight and averaged at 0.54x10(-3) mg/kg while the concentration of DDTs was in the range of (4.06-281.73) x10(-3) mg/kg with a mean of 57.52x10(-3) mg/kg in the survey areas. The concentrations of DDTs in the shellfish were higher than HCHs', so that DDTs could be considered as typical organochlorine pollutants in the areas. The concentrations of DDTs in the shellfish were higher than HCHs', so that DDTs could be considered as typical organochlorines pollutants. The HCHs in all the shellfish conformed to the first level of criterion (0.02 mg/kg) of the Marion Biology Quality (GB 18421-2001), and that of DDTs in most samples were beyond the first level (0.01 mg/kg) but conformed to the second level (0.10 mg/kg). On average, alpha-HCH and delta-HCH occupied the most part of HCHs, while O,P'-DDT and P,P'-DDT occupied the most part of DDTs. The concentrations of organocholorine pesticides in shellfish samples varied in site and in species. The highest level occurred at the Shengsi (SS), followed by Yangkougang (YKG), Lvsi (LS), Dongyuan (DY) and Beibayao (BBY), low concentrations were observed at Changsha (CS), Beidaodi (BDD), and Gouqi (GQ). The concentration of HCHs and DDTs in most sites decreased clearly from 2006 to 2007 except for YKG, DY, BDD, LYS, and SS. All of above results suggested that the study area was slightly affected by organochlorine pesticide, special by DDTs.