LTL-Constrained Steady-State Policy Synthesis

D 2021

LTL-Constrained Steady-State Policy Synthesis

KŘETÍNSKÝ, Jan

Základní údaje

Originální název

LTL-Constrained Steady-State Policy Synthesis

Autoři

KŘETÍNSKÝ, Jan

Vydání

Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence, IJCAI 2021, Virtual Event / Montreal, Canada, 19-27 August 2021. od s. 4104-4111, 8 s. 2021

Další údaje

Typ výsledku

Stať ve sborníku

Označené pro přenos do RIV

Organizační jednotka

Fakulta informatiky

ISBN

9780999241196

ISSN

DOI

https://doi.org/10.24963/IJCAI.2021/565

Změněno: 17. 3. 2025 14:43, RNDr. Pavel Šmerk, Ph.D.

Anotace

V originále

Decision-making policies for agents are often synthesized with the constraint that a formal specification of behaviour is satisfied. Here we focus on infinite-horizon properties. On the one hand, Linear Temporal Logic (LTL) is a popular example of a formalism for qualitative specifications. On the other hand, Steady-State Policy Synthesis (SSPS) has recently received considerable attention as it provides a more quantitative and more behavioural perspective on specifications, in terms of the frequency with which states are visited. Finally, rewards provide a classic framework for quantitative properties. In this paper, we study Markov decision processes (MDP) with the specification combining all these three types. The derived policy maximizes the reward among all policies ensuring the LTL specification with the given probability and adhering to the steady-state constraints. To this end, we provide a unified solution reducing the multi-type specification to a multi-dimensional long-run average reward. This is enabled by Limit-Deterministic Büchi Automata (LDBA), recently studied in the context of LTL model checking on MDP, and allows for an elegant solution through a simple linear programme. The algorithm also extends to the general ?-regular properties and runs in time polynomial in the sizes of the MDP as well as the LDBA.

Citovat

KŘETÍNSKÝ, Jan. LTL-Constrained Steady-State Policy Synthesis. In Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence, IJCAI 2021, Virtual Event / Montreal, Canada, 19-27 August 2021. 2021, s. 4104-4111. ISBN 9780999241196. Dostupné z: https://doi.org/10.24963/IJCAI.2021/565.

@inproceedings{2484783,
   author = {Křetínský, Jan},
   booktitle = {Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence, IJCAI 2021, Virtual Event / Montreal, Canada, 19-27 August 2021.},
   doi = {https://doi.org/10.24963/IJCAI.2021/565},
   isbn = {9780999241196},
   pages = {4104-4111},
   title = {LTL-Constrained Steady-State Policy Synthesis},
   year = {2021}
}

TY  - CONF
ID  - 2484783
AU  - Křetínský, Jan
PY  - 2021
TI  - LTL-Constrained Steady-State Policy Synthesis
SN  - 9780999241196
N2  - Decision-making policies for agents are often synthesized with the constraint that a formal specification of behaviour is satisfied. Here we focus on infinite-horizon properties. On the one hand, Linear Temporal Logic (LTL) is a popular example of a formalism for qualitative specifications. On the other hand, Steady-State Policy Synthesis (SSPS) has recently received considerable attention as it provides a more quantitative and more behavioural perspective on specifications, in terms of the frequency with which states are visited. Finally, rewards provide a classic framework for quantitative properties. In this paper, we study Markov decision processes (MDP) with the specification combining all these three types. The derived policy maximizes the reward among all policies ensuring the LTL specification with the given probability and adhering to the steady-state constraints. To this end, we provide a unified solution reducing the multi-type specification to a multi-dimensional long-run average reward. This is enabled by Limit-Deterministic Büchi Automata (LDBA), recently studied in the context of LTL model checking on MDP, and allows for an elegant solution through a simple linear programme. The algorithm also extends to the general ?-regular properties and runs in time polynomial in the sizes of the MDP as well as the LDBA.
ER  -

KŘETÍNSKÝ, Jan. LTL-Constrained Steady-State Policy Synthesis. In \textit{Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence, IJCAI 2021, Virtual Event / Montreal, Canada, 19-27 August 2021.}. 2021, s.~4104-4111. ISBN~9780999241196. Dostupné z: https://doi.org/10.24963/IJCAI.2021/565.

Přehled o publikaci