Formal representations of traffic scenarios can be used to generate test cases for the safety verification of autonomous driving. However, most existing methods are limited in highway or highly simplified intersection scenarios due to the intricacy and diversity of traffic scenarios. In response, we propose Traffic Scenario Logic (TSL), which is a spatial-temporal logic designed for modeling and reasoning of urban pedestrian-free traffic scenarios. TSL provides a formal representation of the urban road network that can be derived from OpenDRIVE, i.e., the de facto industry standard of high-definition maps for autonomous driving, enabling the representation of a broad range of traffic scenarios. We implemented the reasoning of TSL using Telingo, i.e., a solver for temporal programs based on the Answer Set Programming, and tested it on different urban road layouts. Demonstrations show the effectiveness of TSL in test scenario generation and its potential value in areas like decision-making and control verification of autonomous driving.

翻译：交通场景的形式化表示可用于生成自动驾驶安全验证的测试用例。然而，由于交通场景的复杂性和多样性，现有方法大多局限于高速公路或高度简化的交叉口场景。为此，我们提出了交通场景逻辑（TSL），这是一种专为无行人的城市交通场景建模与推理而设计的时空逻辑。TSL提供了一种可从OpenDRIVE（即自动驾驶高精地图的事实工业标准）导出的城市路网形式化表示，从而能够表征广泛的交通场景。我们使用Telingo（一种基于答案集编程的时序程序求解器）实现了TSL的推理，并在不同的城市道路布局上进行了测试。实验结果表明，TSL在测试场景生成方面具有有效性，并在自动驾驶决策与控制验证等领域展现出潜在应用价值。