首页 | 本学科首页   官方微博 | 高级检索  
文章检索
  按 检索   检索词:      
出版年份:   被引次数:   他引次数: 提示:输入*表示无穷大
  收费全文   27篇
  完全免费   5篇
  自动化技术   32篇
  2016年   1篇
  2014年   1篇
  2011年   2篇
  2010年   3篇
  2009年   3篇
  2008年   1篇
  2007年   4篇
  2006年   1篇
  2004年   1篇
  2003年   4篇
  2002年   2篇
  2000年   3篇
  1999年   2篇
  1998年   1篇
  1996年   1篇
  1993年   1篇
  1991年   1篇
排序方式: 共有32条查询结果,搜索用时 187 毫秒
1.
一种Agent数据库系统框架及其规则并行算法   总被引:11,自引:0,他引:11       下载免费PDF全文
张茂元  卢正鼎 《软件学报》2004,15(8):1157-1164
面向对象方法描述的对象是被动的,与主动机制存在矛盾,不能很好地定义分布式主动数据库中对象的功能和特性.分布式主动数据库中的主动规则还带来了终止性、合流性的问题.首先分析面向对象方法的局限性,将Agent技术、分布式数据库、主动数据库相结合,给出一种面向Agent的分布式主动数据库系统框架.然后在这个框架基础上,提出扩展事件规则图方法和改进的Coffman-Graham规则并行算法,并分析它们的性能.分析结果表明,前者在一定程度上解决了数据库系统的终止性问题,后者在保持合流性的基础上提高了规则并行处理效率.这个框架对研究Agent技术在分布式主动数据库中的应用有一定的启示.  相似文献
2.
Nonterminating Rewritings with Head Boundedness   总被引:1,自引:1,他引:0       下载免费PDF全文
We define here the concept of head boundedness,head normal form and head confluence of term rewriting systems that allow infinite derivation.Head confluence iw weaker than confluence,but sufficient to guarantee the correctness of lazy implementations of equational logic programming languages.Then we prove several results.First,if a left-linear system is locally confluent and head-bounded.then it is head-confluent.Second,head-confluent and head-bounded systems have the heau Church-Rosser property.Last,if an orthogonal system is head-terminating,then it is head-bounded.These results can be applied to generalize equational logic programming languages.  相似文献
3.
几种满足汇合性质的Petri网子类   总被引:1,自引:1,他引:0       下载免费PDF全文
证明活的标识S-图、活的标识T-图、有界的冲突无关的Petri网、有界的标识T.图具有汇合性质,讨论共享合成与同步合成操作对Petri网汇合性质的保持性,得出由上述简单的Petri网子类通过共享合成及同步合成得到的复杂的网系统也具有汇合性质。通过一个具有汇合性质的复杂网系统实例验证该结论。  相似文献
4.
The use of rules in a distributed environment creates new challenges for the development of active rule execution models. In particular, since a single event can trigger multiple rules that execute over distributed sources of data, it is important to make use of concurrent rule execution whenever possible. This paper presents the details of the integration rule scheduling (IRS) algorithm. Integration rules are active database rules that are used for component integration in a distributed environment. The IRS algorithm identifies rule conflicts for multiple rules triggered by the same event through static, compile-time analysis of the read and write sets of each rule. A unique aspect of the algorithm is that the conflict analysis includes the effects of nested rule execution that occurs as a result of using an execution model with an immediate coupling mode. The algorithm therefore identifies conflicts that may occur as a result of the concurrent execution of different rule triggering sequences. The rules are then formed into a priority graph before execution, defining the order in which rules triggered by the same event should be processed. Rules with the same priority can be executed concurrently. The IRS algorithm guarantees confluence in the final state of the rule execution. The IRS algorithm is applicable for rule scheduling in both distributed and centralized rule execution environments.  相似文献
5.
The notion of confluence is studied on the context of bigraphs. Confluence will be important in modelling real-world systems, both natural (as in biology) and artificial (as in pervasive computing). The paper uses bigraphs in which names have multiple locality; this enables a formulation of the lambda calculus with explicit substitutions. The paper reports work in progress, seeking conditions on a bigraphical reactive system that are sufficient to ensure confluence; the conditions must deal with the way that bigraphical redexes can be intricately intertwined. The conditions should also be satisfied by the lambda calculus. After discussion of these issues, two conjectures are put forward.  相似文献
6.
We present a method for pipeline verification using SMT solvers. It is based on a non-deterministic “mother pipeline” machine (MOP) that abstracts the instruction set architecture (ISA). The MOP vs. ISA correctness theorem splits naturally into a large number of simple subgoals. This theorem reduces proving the correctness of a given pipelined implementation of the ISA to verifying that each of its transitions can be modeled as a sequence of MOP state transitions.  相似文献
7.
We propose a compositional technique for efficient verification of networks of parallel processes. It is based on an automatic analysis of LTSs of individual processes (using a failure-based equivalence which preserves divergences) that determines their sets of “conflict-free” actions, called untangled actions. Untangled actions are compositional, i.e. synchronisation on untangled actions will not destroy their “conflict-freedom”. For networks of processes, using global untangled actions derived from local ones, efficient reduction algorithms have been devised for systems with a large number of small processes running in parallel.  相似文献
8.
In this paper the context-splittable normal form for rewriting systems defining Church–Rosser languages is introduced. Context-splittable rewriting rules look like rules of context-sensitive grammars with swapped sides. To be more precise, they have the form uvwuxw with u,v,w being words, v being nonempty and x being a single letter or the empty word. It is proved that this normal form can be achieved for each Church–Rosser language and that the construction is effective. Some interesting consequences of this characterization are given, too.  相似文献
9.
The unification problem for term rewriting systems (TRSs) is the problem of deciding, for a given TRS R and two terms M and N, whether there exists a substitution θ such that Mθ and Nθ are congruent modulo R (i.e., Mθ↔R*Nθ). In this paper, the unification problem for confluent right-ground TRSs is shown to be decidable. To show this, the notion of minimal terms is introduced and a new unification algorithm for obtaining a substitution whose range consists of minimal terms is proposed. Our result extends the decidability of unification for canonical (i.e., terminating and confluent) right-ground TRSs given by Hullot [Proceedings of the 5th Conference on Automated Deduction, LNCS, vol. 87, 1980, p. 318] in the sense that the termination condition can be omitted.  相似文献
10.
We present the titular proof development that has been verified in Isabelle/HOL. As a first, the proof is conducted exclusively by the primitive proof principles of the standard syntax and of the considered reduction relations: the naive way, so to speak. Curiously, the Barendregt Variable Convention takes on a central technical role in the proof. We also show: (i) that our presentation of the λ-calculus coincides with Curry’s and Hindley’s when terms are considered equal up to α-equivalence and (ii) that the confluence properties of all considered systems are equivalent.  相似文献
设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号