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

arXiv: https://arxiv.org/abs/2307.05658 · HTML: https://mlsanity.com/paper/2307.05658/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 11 Jul 2023.

## Built on by (most cited first, 3 of 3)

- [Le Nozze di Giustizia. Interactions between Artificial Intelligence, Law, Logic, Language and Computation with some case studies in Traffic Regulations and Health Care](https://mlsanity.com/paper/2402.06487/) (2024)
- [Specification languages for computational laws versus basic legal principles](https://mlsanity.com/paper/2503.09129/) (2025)
- [Coherency through formalisations of Structured Natural Language, A case study on FRETish](https://mlsanity.com/paper/2605.10462/) (2026)

## Abstract (arXiv)

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.
