共查询到19条相似文献,搜索用时 218 毫秒
1.
朱惠彪 《计算机工程与科学》1993,15(4):9-18
本文主要讨论了确定性进程单向模拟,与R.Milner的双向模拟相比,本文定义的模拟是单方向的。我们给出了确定性进程的转换规则,并证明了确定性进程单向模拟的正确性与完备性。同时也讨论了单向模拟的转换规律,并把单向模拟看作是一个特定函数的不动点。最后我们讨论了单向模拟的分层性,并且对单向模拟与双向模拟作了比较,证明了双向模拟可以由两个单向模拟组成。 相似文献
2.
3.
本文提出数据传送进程的符号迁移语义,引入符号互模拟的概念,证明了两个进程在传统意义下互模拟当且仅当它们符号互模拟.由于无穷域上的数据传送进程的传统迁移图是无穷的,而其中相当一部分的符号迁移图是有穷的,文章的结果为在有穷时间和空间内判定这类进程的互模拟关系开辟了可能性. 相似文献
4.
传统离散事件动态系统中的离散事件状态的转换具有不确定性,其不确定性主要来自状态转向发生时刻的不确定性,而所转向的状态一般具有确定性。本文对具有状态转向时刻和转向状态的二重不确定性的离散事件动态系统进行了讨论,用模糊专家系统来对未来状态和状态迁移时刻二重不确定性的离散事件动态系统进行评价,并以智能交通系统中车辆诱导技术为例,说明了此类模糊专家规则的应用价值。本文提出了一种模拟淬火算法,通过模拟物质加温后急剧冷却的过程来求得目标函数的局部极值,以模拟淬火算法的转向概率作为模糊专家系统中的规则选择概率。该方法有效地保证了事件转换的实时性,提高了交通疏导的效率。 相似文献
5.
一个移动进程演算的互模拟同余定义框架 总被引:1,自引:0,他引:1
并发计算模型是理论计算机科学研究的重要领域之一。以π演算为代表的移动进程演算是目前并发理论的研究热点。互模拟等价定义是移动进程演算研究中的核心概念和问题,而传名机制使得移动进程演算中的互模拟同余关系更加复杂和有趣。本文在分析了常见的互模拟同余定义的基础上,通过抽取定义的核心要素,提出了一个三维的互模拟同余定义模型,从而将一般文献中常见的互模拟定义纳入到一个统一的框架中来,加深了我们对移动进程演算中互模拟概念的理解;同时本文利用这个模型,系统分析了各种互模拟之阿的关系。模型的优点在于它的普适性和开放性。 相似文献
6.
7.
过程模拟技术及其支持环境PMMSE 总被引:3,自引:0,他引:3
过程模拟是对过程模型进行分析,验证,改进和优化的实用方法,它在过程工程中起着非常重要的作用,本文首先定义了过程工程中与过程模拟有关的概念,之后过程模拟的基本原理进行了讨论提出了解决问题的方法。 相似文献
8.
一类排队系统模型的计算机模拟 总被引:8,自引:0,他引:8
吴庆标 《计算机应用与软件》1993,10(6):35-38
排队系统是离散事件系统最典型的问题之一,本文讨论了服务时间与队长有关的排队系统模拟,在单服务台及串联,并联多服务台情形下,建立了六个模拟模型,并给出模拟模型的计算实例。 相似文献
9.
织物模拟中的自适应网格剖分研究 总被引:1,自引:0,他引:1
本文提出一种在织物模拟中的动态网格剖分方法,针对传统模拟算法中因网格剖分固定和曲面整体网格均匀剖分造成模拟误差与计算耗费,分别从织物物理和几何角度出发,提出在动态模拟过程中的自适应的网格剖分方法。利用模拟过程中曲面片局部形变信息,对网格进行动态剖分与合并,有效提高了模拟效率。经实际应用表明:该算法具有模拟效率高、易于计算机实现等优点,特别在对非均匀形变物体模拟中,该算法从模拟效率和精度均得到满意结果。 相似文献
10.
11.
He Jifeng 《Formal Aspects of Computing》1989,1(1):229-241
In this paper we deal with the problem of (nondeterministic and parallel) process refinement. The basic notion of refinement is defined via the improved failure semantics of CSP [BHR84, BrR85, Hoa85, Ros88]. The concept of simulation of Communicating Systems introduced in [Mil80, Par81] is generalised and proved to be sound for the correctness of refinement. A Galois connection is presented to show that up-simulation and down-simulation together provide a complete proof method. The paper also suggests that simulation can be employed to derive an implementation from a specification. 相似文献
12.
Hing Leung 《Acta Informatica》1998,35(7):595-624
We develop a new algorithm for determining if a given nondeterministic finite automaton is limited in nondeterminism. From
this, we show that the number of nondeterministic moves of a finite automaton, if limited, is bounded by where is the number of states. If the finite automaton is over a one-letter alphabet, using Gohon's result the number of nondeterministic
moves, if limited, is less than . In both cases, we present families of finite automata demonstrating that the upper bounds obtained are almost tight. We
also show that the limitedness problem of the number of nondeterministic moves of finite automata is PSPACE-hard. Since the
problem is already known to be in PSPACE, it is therefore PSPACE-complete.
Received: 14 June 1994 / 3 December 1997 相似文献
13.
In this paper we consider two-way counter machines, i.e., two-way finite automata with counters whose contents have no effect on transitions except that an attempt to decrement an empty counter will abort the computation. We show that the deterministic machines have an unsolvable emptiness problem, but that their universe problem is solvable because they accept languages whose complements are context free. In the nondeterministic case, we show that these machines are equivalent to two-way nondeterministic logspace Turing machines, and establish an infinite hierarchy based on the number of weak counters. Finally, we disprove two conjectures concerning the nondeterministic machines. 相似文献
14.
本文提出了一种基于有限关联团块观点的成员系统模型,主要针对不确定性情况给出了其归约操作的形式化描述,讨论了它与产生式系统的关系,并根据该模型及其归约过程,成功地设计实现了一种并发成员系统程序计算语言,对研究支持多种AI问题求解的模型及其语言做了有益的尝试。 相似文献
15.
Yih-Kuen Tsay Bagrodia R.L. 《Parallel and Distributed Systems, IEEE Transactions on》1994,5(7):737-748
The implementation of nondeterministic pairwise synchronous communication among a set of asynchronous processes is modeled as the binary interaction problem. The paper describes an algorithm for this problem that satisfies a strong fairness property that guarantees freedom from process starvation. This is the first algorithm for binary interactions with strong fairness whose message cost and response time are independent of the total number of processes in the system. The paper also describes how the fair algorithm may be extended to tolerate detectable fail-stop failures. Finally, we show how any solution to the dining philosophers problem can be embedded to design a fair algorithm for binary interactions. In particular, this embedding is used to derive a fair algorithm that can cope with undetectable fail-stop failures 相似文献
16.
Existence and Verification for Decentralized Nondeterministic Discrete‐Event Systems Under Bisimulation Equivalence 下载免费PDF全文
In this paper, we study the decentralized control problem for nondeterministic discrete‐event systems (DESs) under bisimulation equivalence. In order to exactly achieve the desired specification in the sense of bisimulation equivalence, we present a synchronous composition for the supervised system based on the simulation relation between the specification and the plant. After introducing the notions of simulation‐based controllability and simulation‐based coobservability, we present the necessary and sufficient condition for the existence of a decentralized supervisor such that the controlled system is bisimilar to the specification, and an algorithm for verifying the simulation‐based coobservability is proposed by constructing a computational tree. 相似文献
17.
Polynomial synthesis of supervisor for partially observed discrete-event systems by allowing nondeterminism in control 总被引:1,自引:0,他引:1
Kumar R. Shengbing Jiang Changyan Zhou Wenbin Qiu 《Automatic Control, IEEE Transactions on》2005,50(4):463-475
We study the supervisory control of discrete-event systems (DESs) under partial observation using nondeterministic supervisors. We formally define a nondeterministic control policy and also a control & observation compatible nondeterministic state machine and prove their equivalence. The control action of a nondeterministic supervisor is chosen online, nondeterministically from among a set of choices determined offline. Also, the control action can be changed online nondeterministically (prior to any new observation) in accordance with choices determined offline. The online choices, once made, can be used to affect the set of control action choices in future. We show that when control is exercised using a nondeterministic supervisor, the specification language is required to satisfy a weaker notion of observability, which we define in terms of recognizability and achievability. Achievability serves as necessary and sufficient condition for the existence of a nondeterministic supervisor, and it is weaker than controllability and observability combined. When all events are controllable, achievability reduces to recognizability. We show that both existence, and synthesis of nondeterministic supervisors can be determined polynomially. (For deterministic supervisors, only existence can be determined polynomially.) Both achievability and recognizability are preserved under union, and also under intersection (when restricted over prefix-closed languages). Using the intersection closure property we derive a necessary and sufficient condition for the range control problem for the prefix-closed case. Unlike the deterministic supervisory setting where the complexity of existence is exponential, our existence condition is polynomially verifiable, and also a supervisor can be polynomially synthesized. 相似文献
18.
Previous investigations have suggested the use of multiple communicating processors for executing logic programs. However, this strategy lacks efficiency due to competition for memory and communication bandwidth, and this is a problem that has been largely neglected. In this paper we propose a realistic model for executing logic programs with low overhead on multiple processors. Our proposal does not involve shared memory or copying computation state between processors. The model organises computations over the nondeterministic proof tree so that different processors explore unique deterministic computation paths independently, in order to exploit the “OR-parallelism” present in a program. We discuss the advantages of this approach over previous ones, and suggest control strategies for making it effective in practice. 相似文献
19.
Richard Salter 《Computer Languages, Systems and Structures》1983,8(2):61-68
In this paper we introduce a methodology for utilizing concurrency in place of backtracking in the implementation of nondeterministic algorithms. This is achieved in an applicative setting through the use of the Friedman-Wise multiprogramming primitive frons, and a paradigm which views the action of nondeterministic algorithms as one of data structure construction. The element by element nondeterminism arising from a linearized search is replaced by a control structure which is oriented towards constructing sets of partial computations. This point of view is facilitated by the use of suspensions, which allow control disciplines to be embodied in the form of conceptual data structures that in reality manifest themselves only for purposes of control.We apply this methodology to the class of problems usually solved through the use of simple backtracking (e.g. “eight queens”), and to a problem presented by Lindstrom to illustrate the use of coroutine controlled backtracking, to produce backtrack-free solutions. Our solution to the latter illustrates the coroutine capability of suspended structures, but also demonstrates a need for further investigations into resolving problems of process communication in applicative languages. 相似文献