Model-checking in the Foundations of Algorithmic Law and the Case of Regulation 561

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.