Enforcing Timing Properties in Motorway Traffic

Christopher Bischopink
(University Oldenburg)

In previous work, we proposed a Runtime Enforcement Approach to deal with timing properties in motorway traffic, which are present in form of Timed Multi-Lane Spatial Logic (TMLSL) formulae, a logic tailored to express both spatial and timing properties. Employing communication between the cars, we utilised a nondeterministic controller guessing which actions to execute next for each car, before asking the local monitors of the cars for permission to execute the announced actions. In this contribution, we consider a more reasonable controller that only considers sequences that satisfy its own properties. This is done utilising region automata that one can generate from the cars' specifications. In the approach, we also came along a minor decidability result for TMLSL.

In Marie Farrell, Matt Luckcuck, Mario Gleirscher and Maike Schwammberger: Proceedings Fifth International Workshop on Formal Methods for Autonomous Systems (FMAS 2023), Leiden, The Netherlands, 15th and 16th of November 2023, Electronic Proceedings in Theoretical Computer Science 395, pp. 130–143.
Published: 15th November 2023.

ArXived at: https://dx.doi.org/10.4204/EPTCS.395.9 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org