一个基于图像的不透明度概念的通用建模与验证框架
A General Language-Based Framework for Specifying and Verifying Notions of Opacity
摘要：
不透明性是一种信息流属性，它描述了动态系统中的合理可否认性，即入侵者是否可以推断出发生了“秘密”行为。在本文中，我们提供了一个一般的框架，不透明度统一的离散事件系统中存在的不透明度的许多现有的概念。我们使用这个框架来讨论基于语言和基于状态的概念不透明的自动机。我们提出了几种基于语言的不透明性验证的方法，和一个通用的方法来转换基于状态的概念到基于语言的。我们证明了这种方法的当前状态和初始状态的不透明度，统一现有的结果。然后，我们调查的K步不透明度的概念。我们提供了一个基于语言的K步不透明度，包括两个现有的概念和两个新的。然后，我们分析了相应的基于语言的验证方法，正式和数值例子。在每种情况下，所提出的方法提供显着减少运行时间和空间复杂度。
英文摘要：
Opacity is an information flow property that captures the notion of plausible deniability in dynamic systems, that is whether an intruder can deduce that "secret" behavior has occurred. In this paper we provide a general framework of opacity to unify the many existing notions of opacity that exist for discrete event systems. We use this framework to discuss language-based and state-based notions of opacity over automata. We present several methods for language-based opacity verification, and a general approach to transform state-based notions into language-based ones. We demonstrate this approach for current-state and initial-state opacity, unifying existing results. We then investigate the notions of K-step opacity. We provide a language-based view of K-step opacity encompassing two existing notions and two new ones. We then analyze the corresponding language-based verification methods both formally and with numerical examples. In each case, the proposed methods offer significant reductions in runtime and space complexity.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
