Symbolic Representation Based Partial Order Methods

基于符号表示的偏序法。Purushothaman Iyer符号表示用于有限和无限状态并发系统的分析。然而，在并行系统的有限状态设计分析中，它们可能会受到类似于状态爆炸的约束爆炸。这两个爆炸的原因是在它们的分析过程中考虑了所有交织，即并发系统。部分顺序技术依赖于动作之间的独立性的概念，以避免考虑所有可能的交织。这项拟议的研究将调查展开的概念，它既有助于发现独立的动作，也有助于简洁地表示系统的状态空间。特别是，拟议的研究将解决以下主题：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.