We present a major new version of Scenic, a probabilistic programming language for writing formal models of the environments of cyber-physical systems. Scenic has been successfully used for the design and analysis of CPS in a variety of domains, but earlier versions are limited to environments which are essentially two-dimensional. In this paper, we extend Scenic with native support for 3D geometry, introducing new syntax which provides expressive ways to describe 3D configurations while preserving the simplicity and readability of the language. We replace Scenic's simplistic representation of objects as boxes with precise modeling of complex shapes, including a ray tracing-based visibility system that accounts for object occlusion. We also extend the language to support arbitrary temporal requirements expressed in LTL, and build an extensible Scenic parser generated from a formal grammar of the language. Finally, we illustrate the new application domains these features enable with case studies that would have been impossible to accurately model in Scenic 2.

翻译：本文介绍了Scenic的重大新版本——一种用于形式化建模信息物理系统环境的概率编程语言。Scenic已成功应用于多个领域的信息物理系统设计与分析，但早期版本仅支持本质上为二维的环境。本文在Scenic中扩展了原生三维几何支持，引入新语法以提供描述三维配置的表现力，同时保持语言的简洁性与可读性。我们摒弃了Scenic将物体简化为方块的表示方式，转而采用复杂形状的精确建模，包括基于光线追踪的可见性系统（可处理物体遮挡）。此外，语言扩展支持以LTL表达的任意时序需求，并基于形式语法构建了可扩展的Scenic解析器。最后，通过案例研究展示了这些新特性所支持的应用领域——这些案例在Scenic 2中无法精确建模。