使用S-DPN模型验证交换随机系统性能

"一类新的Petri网用于交换随机系统的建模和性能验证" 本文是一篇研究论文，发表在2015年7月的《IEEE Transactions on Systems, Man, and Cybernetics: Systems》第45卷第7期，由Zuohua Ding, Yuan Zhou, Mingyue Jiang和Meng Chu Zhou等人撰写。文章提出了一种名为“随机微分Petri网”（Stochastic-Differential Petri Net，简称S-DPN）的新模型，专门用于交换随机系统（Switched Stochastic Systems, SSS）的建模和性能验证。 交换随机系统是一种混合系统，它结合了离散的切换逻辑和随机动态过程。传统的建模方法由于语言的不同，无法同时有效描述这两种特性，导致设计和分析的困难。S-DPN模型通过将离散切换逻辑用马尔科夫链表示，而将随机动态过程用一组随机微分方程来表达，从而克服了这一问题。 在S-DPN模型中，离散的切换逻辑被一个马尔科夫链捕获，这允许系统在不同状态间按照概率进行无记忆的转换。另一方面，随机微分方程则描述了系统的连续时间动态行为，其中包含随机因素。通过这种方式，S-DPN模型能够综合考虑系统的离散事件和连续动态，为交换随机系统的建模提供了一个统一的框架。 论文进一步介绍了如何使用模型检查技术应用于S-DPN，以验证SSS的正确性，确保系统的行为满足预定义的需求。作者们通过一个温度控制系统实例展示了该方法的有效性，证明了S-DPN模型在交换随机系统分析中的实用价值。 关键词包括：马尔科夫跳跃、模型验证、随机微分Petri网（S-DPN）、交换随机系统（SSS）。该研究对理解和分析具有随机性和离散切换特性的复杂系统提供了新的工具和方法，对于系统工程、控制理论和计算机科学等领域有重要的理论和应用价值。