Temporal logic control of general Markov decision processes by approximate policy refinement

Sofie Haesaert, Sadegh Soudjani, Alessandro Abate

Onderzoeksoutput: Bijdrage aan tijdschriftTijdschriftartikelAcademicpeer review

Uittreksel

The formal verification and controller synthesis for Markov decision processes that evolve over uncountable state spaces are computationally hard and thus generally rely on the use of approximations. In this work, we consider the correct-by-design control of general Markov decision processes (gMDPs) with respect to temporal logic properties by leveraging approximate probabilistic relations between the original model and its abstraction. We newly work with a robust satisfaction for the construction and verification of control strategies, which allows for both deviations in the outputs of the gMDPs and in the probabilistic transitions. The computation is done over the reduced or abstracted models, such that when a property is robustly satisfied on the abstract model, it is also satisfied on the original model with respect to a refined control strategy.
TaalEngels
Artikelnummer1712.07622v1
Aantal pagina's23
TijdschriftarXiv.org, e-Print Archive, Physics
Volume2017
StatusGepubliceerd - 20 dec 2017

Vingerafdruk

Temporal logic
Controllers

Bibliografische nota

22 pages, 3 figures, submitted to the 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2018

Trefwoorden

    Citeer dit

    @article{ed2776b9b3d246098d91c5a4e5fd0619,
    title = "Temporal logic control of general Markov decision processes by approximate policy refinement",
    abstract = "The formal verification and controller synthesis for Markov decision processes that evolve over uncountable state spaces are computationally hard and thus generally rely on the use of approximations. In this work, we consider the correct-by-design control of general Markov decision processes (gMDPs) with respect to temporal logic properties by leveraging approximate probabilistic relations between the original model and its abstraction. We newly work with a robust satisfaction for the construction and verification of control strategies, which allows for both deviations in the outputs of the gMDPs and in the probabilistic transitions. The computation is done over the reduced or abstracted models, such that when a property is robustly satisfied on the abstract model, it is also satisfied on the original model with respect to a refined control strategy.",
    keywords = "cs.SY, cs.LO, math.OC, 93E03, 93E20, 68W25",
    author = "Sofie Haesaert and Sadegh Soudjani and Alessandro Abate",
    note = "22 pages, 3 figures, submitted to the 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2018",
    year = "2017",
    month = "12",
    day = "20",
    language = "English",
    volume = "2017",
    journal = "arXiv.org, e-Print Archive, Physics",

    }

    Temporal logic control of general Markov decision processes by approximate policy refinement. / Haesaert, Sofie; Soudjani, Sadegh; Abate, Alessandro.

    In: arXiv.org, e-Print Archive, Physics, Vol. 2017, 1712.07622v1, 20.12.2017.

    Onderzoeksoutput: Bijdrage aan tijdschriftTijdschriftartikelAcademicpeer review

    TY - JOUR

    T1 - Temporal logic control of general Markov decision processes by approximate policy refinement

    AU - Haesaert,Sofie

    AU - Soudjani,Sadegh

    AU - Abate,Alessandro

    N1 - 22 pages, 3 figures, submitted to the 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2018

    PY - 2017/12/20

    Y1 - 2017/12/20

    N2 - The formal verification and controller synthesis for Markov decision processes that evolve over uncountable state spaces are computationally hard and thus generally rely on the use of approximations. In this work, we consider the correct-by-design control of general Markov decision processes (gMDPs) with respect to temporal logic properties by leveraging approximate probabilistic relations between the original model and its abstraction. We newly work with a robust satisfaction for the construction and verification of control strategies, which allows for both deviations in the outputs of the gMDPs and in the probabilistic transitions. The computation is done over the reduced or abstracted models, such that when a property is robustly satisfied on the abstract model, it is also satisfied on the original model with respect to a refined control strategy.

    AB - The formal verification and controller synthesis for Markov decision processes that evolve over uncountable state spaces are computationally hard and thus generally rely on the use of approximations. In this work, we consider the correct-by-design control of general Markov decision processes (gMDPs) with respect to temporal logic properties by leveraging approximate probabilistic relations between the original model and its abstraction. We newly work with a robust satisfaction for the construction and verification of control strategies, which allows for both deviations in the outputs of the gMDPs and in the probabilistic transitions. The computation is done over the reduced or abstracted models, such that when a property is robustly satisfied on the abstract model, it is also satisfied on the original model with respect to a refined control strategy.

    KW - cs.SY

    KW - cs.LO

    KW - math.OC

    KW - 93E03, 93E20, 68W25

    M3 - Article

    VL - 2017

    JO - arXiv.org, e-Print Archive, Physics

    T2 - arXiv.org, e-Print Archive, Physics

    JF - arXiv.org, e-Print Archive, Physics

    M1 - 1712.07622v1

    ER -