Mastering the Visualization of Larger State Spaces with Projection Diagrams
Mastering the Visualization of Larger State Spaces with Projection Diagrams
复制标题
使用投影图掌握更大状态空间的可视化
DOI：
10.1007/978-3-319-25423-4_10
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
M. Leuschel
中科院分区：
文献类型：
--
作者：
L. Ladenberger;M. Leuschel
状态空间可视化是一种支持形式化模型分析的流行技术。它通常允许用户获得系统的全局视图，并识别结构相似性，对称性和意外属性。然而，状态空间通常变得非常大，因此可视化的人工检查变得困难。为了克服这一挑战，我们提出了一种方法，它可以大大减少状态空间的大小通过创建投影图。此外，我们提出了一种方法来连接投影图与特定领域的可视化。投影图构造可以直接从用户选择的图形元素开始，而无需用户编写公式或必须知道模型的变量或内部结构。这使得投影图的检查和构造对非形式化方法专家来说是容易的。这些技术已经在theProBtoolset中实现，我们在几个例子中展示了它们的好处和实用性。
State space visualization is a popular technique for supporting the analysis of formal models. It often allows users to get a global view of the system and to identify structural similarities, symmetries, and unanticipated properties. However, state spaces typically become very large, so human inspection of the visualization becomes difficult. To overcome this challenge, we present an approach which can considerably reduce the size of the state space by creatingprojection diagrams. Moreover, we present an approach to link a projection diagram with a domain specific visualization. The projection diagram construction can be initiated directly from user-selected graphical elements without the user having to write formulas or having to know the variables or internal structure of the model. This makes the projection diagram inspection and construction accessible to non-formal method experts. These techniques have been implemented within theProBtoolset, and we demonstrate their benefits and usefulness on several examples.