正式交通场景的表示可以用于生成自动驾驶安全验证的测试用例。然而，由于交通场景的复杂性和多样性，大多数现有方法仅限于高速公路或高度简化的交叉路口场景。针对这一问题，我们提出了交通场景逻辑（TSL），这是一种用于建模和推理城市无行人交通场景的时空逻辑。TSL提供了一种可以从OpenDRIVE（即自动驾驶高清地图的事实标准）中派生的城市道路网络的形式表示，能够在不进行离散化近似的情况下表示广泛的交通场景。我们使用基于答案集编程的时序程序求解器Telingo实现了TSL的推理，并在不同的城市道路布局上进行了测试。演示表明，TSL在测试场景生成中具有有效性，并在自动驾驶的决策和控制验证等方面具有潜在价值。TSL推理的代码已公开。