To drive or not to drive: A logical and computational analysis of European transport regulations

Abstract

This paper analyses a selection of articles from European transport regulations that contain algorithmic information, but may be problematic to implement. We focus on issues regarding the interpretation of tachograph data and requirements on weekly rest periods. We first show that the interpretation of data prescribed by these regulations is highly sensitive to minor variations in input, such that near-identical driving patterns may be regarded both as lawful and as unlawful. We then show that the content of the regulation may be represented in monadic second order logic, but argue that a more computationally tame fragment would be preferable for applications. As a case study we consider its representation in linear temporal logic, but show that a representation of the legislation requires formulas of unfeasible complexity, if at all possible.

Keywords

Linear temporal logic, monadic second order logic, formalized law, transport regulations, automated law enforcement, tachograph

Citation

de Almeida Borges, A., Conejero Rodríguez, J., Fernández-Duque, D., González Bedmar, M., & Joosten, J. J. (2021). To drive or not to drive: a logical and computational analysis of European transport regulations. Information and Computation, 280, 104636. doi:10.1016/j.ic.2020.104636

@Article{AlmeidaBorges2021_Drive,
  author = "{de Almeida Borges}, Ana and {Conejero Rodríguez}, Juan and Fernández-Duque, David and {González Bedmar}, Mireia and Joosten, Joost J.",
  title = "To drive or not to drive: A logical and computational analysis of {E}uropean transport regulations",
  journal = "Information and Computation",
  year = "2021",
  volume = "280",
  pages = "104636",
  issn = "0890-5401",
  doi = "10.1016/j.ic.2020.104636",
  keywords = "Linear temporal logic, monadic second order logic, formalized law, transport regulations, automated law enforcement, tachograph",
  abstract = "This paper analyses a selection of articles from European transport regulations that contain algorithmic information, but may be problematic to implement. We focus on issues regarding the interpretation of tachograph data and requirements on weekly rest periods. We first show that the interpretation of data prescribed by these regulations is highly sensitive to minor variations in input, such that near-identical driving patterns may be regarded both as lawful and as unlawful. We then show that the content of the regulation may be represented in monadic second order logic, but argue that a more computationally tame fragment would be preferable for applications. As a case study we consider its representation in linear temporal logic, but show that a representation of the legislation requires formulas of unfeasible complexity, if at all possible."
}