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.


    Zugriff

    Download


    Exportieren, teilen und zitieren



    Titel :

    Enforcing Timing Properties in Motorway Traffic


    Beteiligte:

    Erscheinungsdatum :

    2023


    Anmerkungen:

    In Proceedings FMAS 2023, arXiv:2311.08987
    EPTCS 395, 2023, pp. 130-143



    Medientyp :

    Preprint


    Format :

    Elektronische Ressource


    Sprache :

    Englisch




    Motorway traffic patterns

    Hollis, Erica / Evans, Ruth | TIBKAT | 1976


    Motorway traffic signs

    Engineering Index Backfile | 1959


    Motorway traffic control system

    Brinkman, A. / Bloemendaal, A.L. | Tema Archiv | 1984


    Motorway traffic supervision system

    Parker, E. | Engineering Index Backfile | 1965


    Motorway Traffic Surveillance and Control

    Papamichail, I. / Papageorgiou, M. / Wang, Y. | British Library Online Contents | 2007