The Second Order Traffic Fine: Temporal Reasoning in European Transport Regulations

Authors Ana de Almeida Borges , Juan José Conejero Rodríguez , David Fernández-Duque , Mireia González Bedmar , Joost J. Joosten

Thumbnail PDF


  • Filesize: 0.54 MB
  • 16 pages

Document Identifiers

Author Details

Ana de Almeida Borges
  • University of Barcelona, Spain
Juan José Conejero Rodríguez
  • University of Barcelona, Spain
David Fernández-Duque
  • Ghent University, Belgium
Mireia González Bedmar
  • University of Barcelona, Spain
Joost J. Joosten
  • University of Barcelona, Spain


We are grateful to Albert Atserias and Martín Diéguez for insightful discussions involving Kamp’s theorem and its variants.

Cite AsGet BibTex

Ana de Almeida Borges, Juan José Conejero Rodríguez, David Fernández-Duque, Mireia González Bedmar, and Joost J. Joosten. The Second Order Traffic Fine: Temporal Reasoning in European Transport Regulations. In 26th International Symposium on Temporal Representation and Reasoning (TIME 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 147, pp. 6:1-6:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


We argue that European transport regulations can be formalized within the Sigma^1_1 fragment of monadic second order logic, and possibly weaker fragments including linear temporal logic. We consider several articles in the regulation to verify these claims.

Subject Classification

ACM Subject Classification
  • Theory of computation → Modal and temporal logics
  • Theory of computation → Higher order logic
  • Applied computing → Law
  • linear temporal logic
  • monadic second order logic
  • formalized law
  • transport regulations


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. J. Boudou, M. Diéguez, and D. Fernández-Duque. A Decidable Intuitionistic Temporal Logic. In 26th EACSL Annual Conference on Computer Science Logic (CSL), pages 14:1-14:17, 2017. Google Scholar
  2. J. del Castillo Tierz. When the laws of logic meet the logic of laws. Master’s thesis, University of Barcelona, Barcelona, 2018. URL:
  3. European Parliament and Council of the European Union. Regulation (EC) No 561/2006 of the European Parliament and of the Council of 15 March 2006 on the harmonisation of certain social legislation relating to road transport and amending council regulations (EEC) No 3821/85 and (EC) No 2135/98 and repealing council regulation (EEC) No 3820/85 (text with EEA relevance) - declaration. Official Journal of the European Union, 2006. URL:
  4. D. Fernández-Duque, M. González Bedmar, D. Sousa, J.J. Joosten, and G. Errezil Alberdi. To Drive or Not to Drive: A Formal Analysis of Requirements (51) and (52) from Regulation (EU) 2016/799. Submitted, 2019. Google Scholar
  5. D. Harel, J. Tiuryn, and D. Kozen. Dynamic Logic. MIT Press, Cambridge, MA, USA, 2000. Google Scholar
  6. J.G. Henriksen and P.S. Thiagarajan. Dynamic Linear Time Temporal Logic. Annals of Pure and Applied Logic, 96(1-3):187-207, 1999. URL:
  7. N. Kamide and H. Wansing. A Paraconsistent Linear-time Temporal Logic. Fundamenta Informaticae, 106(1):1-23, 2011. URL:
  8. H. Kamp. Tense Logic and the Theory of Linear Order. PhD thesis, UCLA, 1968. Google Scholar
  9. N. Kurtonina and M. de Rijke. Bisimulations for Temporal Logic. Journal of Logic, Language and Information, 6(4):403-425, 1997. Google Scholar
  10. O. Lichtenstein and A. Pnueli. Propositional Temporal Logics: Decidability and Completeness. Logic Jounal of the IGPL, 8(1):55-85, 2000. Google Scholar
  11. H. Weyl. The Continuum: A Critical Examination of the Foundation of Analysis. Mineola: Dover, 1994. Google Scholar