为形式化方法设计轻量级绘图语言，提升模型可读性。
Grounded Language Design for Lightweight Diagramming for Formal Methods
- 基于认知科学设计一组正交的绘图原语，支持领域信息嵌入。
- 实测显示生成图有助于推理，优于传统可视化工具。
- 适合形式化建模者快速构建清晰、可靠模型图示。
模型查找（如SAT求解器）广泛应用于形式化方法中，用于增量式定义、探索、验证和诊断复杂系统规范。例如Alloy工具利用SAT求解能力，结合可视化功能帮助用户图形化分析生成的模型。然而，我们发现默认的可视化工具因缺乏领域知识而无效，甚至违背呈现与认知原则。完全定制化可视化虽效果好，但代价高且易出现静默失败等缺陷。为此，本文提出一种轻量级绘图语言，基于认知科学文献与大量自定义可视化案例，提炼出关键元素并抽象为一组正交原语。我们扩展了类似Alloy的工具以支持这些原语，并通过评估证明其生成的图表显著提升推理效率。进一步对比多种绘图语言与工具，表明该方法开辟了一个兼具轻量、高效与理论基础的新方向。
原文摘要 · Abstract (English)
Model finding, as embodied by SAT solvers and similar tools, is used widely, both in embedding settings and as a tool in its own right. For instance, tools like Alloy target SAT to enable users to incrementally define, explore, verify, and diagnose sophisticated specifications for a large number of complex systems. These tools critically include a visualizer that lets users graphically explore these generated models. As we show, however, default visualizers, which know nothing about the domain, are unhelpful and even actively violate presentational and cognitive principles. At the other extreme, full-blown visualizations require significant effort as well as knowledge a specifier might not possess; they can also exhibit bad failure modes (including silent failure). Instead, we need a language to capture essential domain information for lightweight diagramming. We ground our language design in both the cognitive science literature on diagrams and on a large number of example custom visualizations. This identifies the key elements of lightweight diagrams. We distill these into a small set of orthogonal primitives. We extend an Alloy-like tool to support these primitives. We evaluate the effectiveness of the produced diagrams, finding them good for reasoning. We then compare this against many other drawing languages and tools to show that this work defines a new niche that is lightweight, effective, and driven by sound principles.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。