We discuss model-checking problems as formal models of algorithmic law. Specifically, we ask for an algorithmically tractable general purpose model-checking problem that naturally models the European transport Regulation 561, and discuss the reaches and limits of a version of discrete time stopwatch automata.

翻译：我们探讨了模型检测问题作为算法法律的形式化模型。具体而言，我们寻求一种算法可处理的通用模型检测问题，使其能够自然地建模欧洲运输第561号法规，并讨论了离散时间秒表自动机的一种变体的适用范围与局限性。