pessimistic predicate/transform model for long running business processes

Many business processes in enterprise applications are both long running and transactional in nature. However, no current transaction model can provide full transaction support for such long running business processes. This paper proposes a new transaction model, the pessimistic predicate/transform (PP/T) model, which can provide full transaction support for long running business processes. A framework was proposed on the enterprise JavaBeans platform to implement the PP/T model. The framework enables application developers to focus on the business logic, with the underlying platform providing the required transactional semantics. The development and maintenance effort are therefore greatly reduced. Simulations show that the model has a sound concurrency management ability for long running business processes.

Progress of Si-based nanocrystalline luminescent materials

Si-based nanomaterials are some new photoeletronic and informational materials developed rapidly in recent years, and they have potential applications in the light emitting devices, e. g. Si light emitting diode, Si laser and integrated Si-based photoelectronics. Among them are nano-scale porous silicon (ps), Si nanocrystalline embedded SiO2 (SiOx, x < 2.0) matrices, Si nanoquantum dot and Si/SiO2 superlattice, etc. At present, there are various indications that if these materials can achieve efficient and stable luminescence, which are photoluminescence (PL) and electroluminescence (EL), it is possible for them to lead to a new informational revolution in the early days of the 21st century. In this article, we will mainly review the progress of study on Si-based nanomaterials in the past ten years. The involved contents are the fabricated methods, structural characterizations and light emitting properties. Finally, we predicate the developed tendency of this field in the following ten years.

reducing symmetries to generate easier sat instances

Finding countermodels is an effective way of disproving false conjectures. In first-order predicate logic, model finding is an undecidable problem. But if a finite model exists, it can be found by exhaustive search. The finite model generation problem in the first-order logic can also be translated to the satisfiability problem in the propositional logic. But a direct translation may not be very efficient. This paper discusses how to take the symmetries into account so as to make the resulting problem easier. A static method for adding constraints is presented, which can be thought of as an approximation of the least number heuristic (LNH). Also described is a dynamic method, which asks a model searcher like SEM to generate a set of partial models, and then gives each partial model to a propositional prover. The two methods are analyzed, and compared with each other.

传值系统的互模拟与谓词等式系

National Natural Science Foundation of China; Public Administration and Civil Service Bureau of Macau SAR; Companhia de Telecomunicacoes de Macau S.A.R.L.; Macau SAR Government Tourist Office

带复杂数据结构的模型检测工具

模型检测是近二十几年来最成功的自动验证技术之一,而模型检测工具的开发是将模型检测和实际相结合的关键.为了有效地对涉及到复杂数据类型的并发传值系统进行模型检测,总结了以扩展的带赋值符号迁移图和模态图分别作为并发系统和逻辑公式的语义模型来实现模型检测工具的工作,特别是将复杂数据结构引入传值进程定义语言和带赋值符号迁移图.同时结合实际例子说明模型检测工具的有效性.

谓词μ演算和模态图的语义一致性

模态图是谓词μ演算的一种有效的图形表示形式。证明了谓词μ演算和模态图的语义一致性，详细讨论了谓词μ演算公式、嵌套谓词等式系和模态图之间的关系，并给出了一种优化的从线性公式到嵌套谓词等式系的转换算法。

面向传值进程的谓词μ-演算与FO(HML)的完备推演系统

National Natural Science Foundation of China; Public Administration and Civil Service Bureau of Macau SAR; Companhia de Telecomunicacoes de Macau S.A.R.L.; Macau SAR Government Tourist Office

嵌套谓词等式系与弱互模拟

National Natural Science Foundation of China; Public Administration and Civil Service Bureau of Macau SAR; Companhia de Telecomunicacoes de Macau S.A.R.L.; Macau SAR Government Tourist Office

Alkali metal ions transfer across a water/1,2-dichloroethane interface facilitated by a novel monoaza-B15C5 derivative

In this paper, a novel monoaza-B15C5 derivative, N-(2-tosylamino)-isopentyl-monoaza-15-crown-5 (L), is used as an ionophore to facilitate alkali metal cations transfer across a water/1,2-dichloroethane (W/DCE) interface. Well-defined voltammetric behaviors are observed at the polarized W/DCE interfaces supported at micro- and nano-pipets except Cs+. The diffusion coefficient of this ionophore in the DCE phase is calculated to be equal to (3.3+/-0.2) x 10(-6) cm(2) s(-1). The experimental results indicate that a 1:1 (metal: ionophore) complex is formed at the interface with a TIC/TID mechanism. The selectivity of this ionophore towards alkali ions follows the sequence Na+ > Li+ > K+ > Rb+ > Cs+. The logarithm of the association constants (log beta(1)(0)) of the LiL+, NaL+, KL+ and RbL+ complexes in the DCE phase are calculated to be 10.6, 11.6, 9.0 and 7.1, respectively. The kinetic parameters are determined by steady-state voltammograms using nanopipets. The standard rate constants (k(0)) for Li+, Na+, K+ and Rb+ transfers facilitated by L are 0.54+/-0.05, 0.63+/-0.09, 0.51+/-0.04 and 0.46+/-0.06 cm s(-1), respectively. The pH values of aqueous solution have little effect on the electrochemical behaviors of these facilitated processes. The results predicate that this new type of ionophore might be useful to fabricate electrochemical sensor of sodium ion.

基于谓词不变性的状态反馈控制在机器人遥操作中的应用

传统的基于事件遥操作系统虽然巧妙地避开了变化时延问题[8] ,但是它具有“走走停停”的特点 ,即机器人将当前状态发送出去之后直到操作者的下一个指令到来之前机器人必须保证状态没有变化。对此本文首次提出了利用基于谓词不变性的状态反馈控制来对原有的方法进行改进 ,使机器人能够对动态环境具有适应性