Symbolic Representation Based Partial Order Methods

基于偏序方法的符号表示。用符号表示法分析了有限和无限大并发系统。然而，在并行系统的有限空间设计分析中，它们可能会受到约束爆炸的影响，就像状态爆炸一样。这两个爆炸的原因是在分析它们时考虑了并发系统的所有交错。偏序技术依赖于动作之间的独立概念，以避免考虑所有可能的交织。提出的研究将调查展开的概念，这有助于发现独立的行动和简洁地表示系统的状态空间。具体而言，拟议的研究将涉及以下主题：o如何为可用的实时自动机构建展开，例如，在工具集UPPAAL中。o基于展开的UPPAAL偏序方法的实现。o展开和当前偏序方法的比较（理论）研究，目的是将展开推广到其他无限状态系统。o根据现行做法对拟议的实施进行实证评估。所提出的研究将有助于比目前可能的更快、更完整地分析有限状态并发系统。

Symbolic Representation Based Partial Order MethodsS. Purushothaman Iyer Symbolic representations are used in analysis of finite and infinitestate concurrent system. However, they could be subjected toconstraint explosion much like state explosion in analysis of finitestate designs of concurrent systems. The reason for both of these explosionsis the consideration of all interleavings, of a concurrent system, during theiranalysis.Partial-order techniques depend upon the notion of independence amongactions to avoid considering all possible interleavings. The proposedresearch will investigate the notion of unfolding, which aids both indiscovery of independent actions and in succinctly representing the statespace of systems. In particular, the proposed research will address the following topics: o How to build unfoldings for real-time automata as available, for instance, in the tool-set UPPAAL. o Implementation of an unfolding-based partial order method for UPPAAL. o A comparative (theoretical) investigation of unfoldings and current partial order methods, with a view to generalizing unfoldings to other infinite state systems. o Empirical evaluation of the proposed implementation against current practices.The proposed research will aid in faster, and more complete, analysis ofinfinite state concurrent systems than is currently possible.