面向 falsification 及更广应用的 3D 环境建模：Scenic 3.0
编程语言
2023-07-10 v1
摘要
我们呈现 Scenic 的一个重要新版本，Scenic 是一种用于编写信息物理系统环境形式化模型的概率编程语言。Scenic 已成功用于多种领域 CPS 的设计与分析，但早期版本仅限于本质上是二维的环境。在本文中，我们扩展 Scenic 以原生支持 3D 几何，引入新的语法，以富有表现力的方式描述 3D 构型，同时保持语言的简洁与可读性。我们将 Scenic 把物体简单表示为盒体的方式替换为复杂形状的精确建模，包括一个基于光线追踪的、考虑物体遮挡的可见性系统。我们还扩展该语言以支持用 LTL 表达的任意时序需求，并构建了一个由语言形式文法生成的、可扩展的 Scenic 解析器。最后，我们通过案例研究展示了这些新特性所赋能的新应用领域，这些案例在 Scenic 2 中是不可能精确建模的。
引用
@article{arxiv.2307.03325,
title = {3D Environment Modeling for Falsification and Beyond with Scenic 3.0},
author = {Eric Vin and Shun Kashiwa and Matthew Rhea and Daniel J. Fremont and Edward Kim and Tommaso Dreossi and Shromona Ghosh and Xiangyu Yue and Alberto L. Sangiovanni-Vincentelli and Sanjit A. Seshia},
journal= {arXiv preprint arXiv:2307.03325},
year = {2023}
}
备注
13 pages, 6 figures. Full version of a CAV 2023 tool paper, to appear in the Springer Lecture Notes in Computer Science series