Symbolic Representation Based Partial Order Methods

基于符号表示的偏序方法

• 批准号: 0204159
• 负责人: S. Iyer
• 金额: $ 16万
• 依托单位: North Carolina State University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2002
• 资助国家: 美国
• 起止时间: 2002-09-01 至 2006-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0204159&HistoricalAwards=false
• 关键词: Symbolic; Representation; Based; Partial; Order

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.

基于符号表示的偏序方法。PurushothamanIyer符号表示法用于分析有限和无限状态并发系统。 然而，在并发系统的有限状态设计分析中，它们可能会像状态爆炸一样受到约束爆炸的影响。 这两个爆炸的原因是考虑所有的交织，并发系统，在他们的分析。偏序技术依赖于独立的概念，以避免考虑所有可能的交织。 拟议的研究将调查的概念展开，这有助于发现独立的行动，并在简洁地表示系统的状态空间。 特别是，拟议的研究将解决以下主题：o如何建立实时自动机的展开， 实例，在工具集UPPAAL中。o实现UPPAAL的基于展开的偏序方法。o展开和当前部分展开的比较（理论）研究 顺序方法，以期推广到其他无限展开 国家制度。 o对照当前的执行情况对拟议的执行情况进行经验评价 所提出的研究将有助于更快，更完整，offinite状态并发系统的分析比目前可能的。