符号模型检验线性参数化系统的配置集计算

"这篇论文探讨了线性参数化系统安全性的符号模型检验配置集计算技术，特别是使用扩展技术的常规模型检测。作者Tayssir Touili在巴黎第七大学的LIAFA工作，该研究发表在电子笔记的第50期，可在VEPAS2001的网址上查看，共15页。文章关注如何用正则语言表示线性参数化系统的可达集，并提出了一种称为定期扩大的技术，用于计算正则关系和正则语言的可达集。该方法可以应用于各种参数化系统，并且可以模拟现有的一些计算方法。线性参数化系统由一组不可区分的进程组成，安全性检查涉及计算所有可达配置并排除有害状态。正则语言被用来符号化表示系统状态，每个动作对应于词上的正则关系。" 在本文中，作者Tayssir Touili着重讨论了线性参数化系统，这是分布式系统的一种常见表示，其中多个进程的行为是相互独立且不可区分的。这类系统在安全性验证方面具有挑战性，因为它们的规模通常与系统中的进程数量成比例。已知完全验证线性参数化系统是不可判定的，所以研究聚焦于寻找可判定子类或开发半决策过程。 作者提出了一种名为定期扩大的技术，该技术针对的是由正则语言表示的配置集，可以计算正则关系的可达集。这有助于在不知道系统具体规模的情况下进行符号模型检验。正则语言在这里起着关键作用，因为它能有效地表示系统可能的全局状态组合，每个进程的局部状态通过词的形式连接起来。 定期扩大技术的目的是计算正则关系R的系统可达性集或传递闭包R()。这个技术对于处理线性参数化系统特别有用，因为它允许在不具体枚举所有配置的情况下，处理安全性和可达性问题。作者进一步证明，这种方法在特定的正则关系和正则语言子类中是足够强大的，能够模拟现有的计算方法。 文章还指出，尽管线性参数化系统的模型检查问题在一般情况下是不可判定的，但通过限制到特定的子类或采用半决策过程，可以解决一些安全性问题。这种限制通常涉及识别那些其安全性可以决定的系统特性，或者开发出即使不能保证终止也能提供部分答案的算法。 在总结中，Tayssir Touili的工作提供了线性参数化系统安全性验证的新视角，通过正则语言和定期扩大技术，为模型检验配置集的计算开辟了新的可能性。这项研究对于理解分布式系统的安全性问题以及设计更有效的验证策略具有重要意义。