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

TL;DR

This paper explores the application of model-checking techniques to formalize and analyze European transport Regulation 561, focusing on the capabilities and limitations of discrete time stopwatch automata in this context.

Contribution

It introduces a formal model for algorithmic law using model-checking and evaluates its applicability to Regulation 561 with discrete time stopwatch automata.

Findings

Model-checking can formalize aspects of algorithmic law.

Discrete time stopwatch automata have limitations in modeling Regulation 561.

The approach highlights the reach and limits of formal verification in legal regulation analysis.

Abstract

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.