A synthesis method for zero-sum mean-payoff asynchronous probabilistic games
Abstract The traditional synthesis problem aims to automatically construct a reactive system (if it exists) satisfying a given Linear Temporal Logic (LTL) specifications, and is often referred to as a qualitative problem. There is also a class of synthesis problems aiming at quantitative properties,...
Saved in:
| Main Authors: | , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Nature Portfolio
2025-01-01
|
| Series: | Scientific Reports |
| Online Access: | https://doi.org/10.1038/s41598-025-85589-9 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1832594687455657984 |
|---|---|
| author | Wei Zhao Wanwei Liu Zhiming Liu Tiexin Wang |
| author_facet | Wei Zhao Wanwei Liu Zhiming Liu Tiexin Wang |
| author_sort | Wei Zhao |
| collection | DOAJ |
| description | Abstract The traditional synthesis problem aims to automatically construct a reactive system (if it exists) satisfying a given Linear Temporal Logic (LTL) specifications, and is often referred to as a qualitative problem. There is also a class of synthesis problems aiming at quantitative properties, such as mean-payoff values, and this type of problem is called a quantitative problem. For the two types of synthesis problems, the research on the former has been relatively mature, and the latter also has received huge amounts of attention. System designers prefer to synthesize systems that satisfy resource constraints. To this end, this paper focuses on the reactive synthesis problem of combining quantitative and qualitative objectives. First, zero-sum mean-payoff asynchronous probabilistic games are proposed, where the system aims at the expected mean payoff in a probabilistic environment while satisfying an LTL winning condition against an adversarial environment. Then, the case of taking the wider class of Generalized Reactivity(1) (GR(1)) formula as an LTL winning condition is studied, that is, the synthesis problem of the expected mean payoffs is studied for the system with the probability of winning. Next, two symbolic algorithms running in polynomial time are proposed to calculate the expected mean payoffs, and both algorithms adopt uniform random strategies. Combining the probability of system winning, the expected mean payoffs of the system when it has the probability of winning is calculated. Finally, our two algorithms are implemented, and their convergence and volatility are demonstrated through experiments. |
| format | Article |
| id | doaj-art-49c784847d014f1f9440d400ecff750d |
| institution | Kabale University |
| issn | 2045-2322 |
| language | English |
| publishDate | 2025-01-01 |
| publisher | Nature Portfolio |
| record_format | Article |
| series | Scientific Reports |
| spelling | doaj-art-49c784847d014f1f9440d400ecff750d2025-01-19T12:24:16ZengNature PortfolioScientific Reports2045-23222025-01-0115111310.1038/s41598-025-85589-9A synthesis method for zero-sum mean-payoff asynchronous probabilistic gamesWei Zhao0Wanwei Liu1Zhiming Liu2Tiexin Wang3The Department of Computer Engineering, Jiangsu University of TechnologyThe National University of Defense TechnologySouthwest UniversityThe College of Computer Science and Technology, Nanjing University of Aeronautics and AstronauticsAbstract The traditional synthesis problem aims to automatically construct a reactive system (if it exists) satisfying a given Linear Temporal Logic (LTL) specifications, and is often referred to as a qualitative problem. There is also a class of synthesis problems aiming at quantitative properties, such as mean-payoff values, and this type of problem is called a quantitative problem. For the two types of synthesis problems, the research on the former has been relatively mature, and the latter also has received huge amounts of attention. System designers prefer to synthesize systems that satisfy resource constraints. To this end, this paper focuses on the reactive synthesis problem of combining quantitative and qualitative objectives. First, zero-sum mean-payoff asynchronous probabilistic games are proposed, where the system aims at the expected mean payoff in a probabilistic environment while satisfying an LTL winning condition against an adversarial environment. Then, the case of taking the wider class of Generalized Reactivity(1) (GR(1)) formula as an LTL winning condition is studied, that is, the synthesis problem of the expected mean payoffs is studied for the system with the probability of winning. Next, two symbolic algorithms running in polynomial time are proposed to calculate the expected mean payoffs, and both algorithms adopt uniform random strategies. Combining the probability of system winning, the expected mean payoffs of the system when it has the probability of winning is calculated. Finally, our two algorithms are implemented, and their convergence and volatility are demonstrated through experiments.https://doi.org/10.1038/s41598-025-85589-9 |
| spellingShingle | Wei Zhao Wanwei Liu Zhiming Liu Tiexin Wang A synthesis method for zero-sum mean-payoff asynchronous probabilistic games Scientific Reports |
| title | A synthesis method for zero-sum mean-payoff asynchronous probabilistic games |
| title_full | A synthesis method for zero-sum mean-payoff asynchronous probabilistic games |
| title_fullStr | A synthesis method for zero-sum mean-payoff asynchronous probabilistic games |
| title_full_unstemmed | A synthesis method for zero-sum mean-payoff asynchronous probabilistic games |
| title_short | A synthesis method for zero-sum mean-payoff asynchronous probabilistic games |
| title_sort | synthesis method for zero sum mean payoff asynchronous probabilistic games |
| url | https://doi.org/10.1038/s41598-025-85589-9 |
| work_keys_str_mv | AT weizhao asynthesismethodforzerosummeanpayoffasynchronousprobabilisticgames AT wanweiliu asynthesismethodforzerosummeanpayoffasynchronousprobabilisticgames AT zhimingliu asynthesismethodforzerosummeanpayoffasynchronousprobabilisticgames AT tiexinwang asynthesismethodforzerosummeanpayoffasynchronousprobabilisticgames AT weizhao synthesismethodforzerosummeanpayoffasynchronousprobabilisticgames AT wanweiliu synthesismethodforzerosummeanpayoffasynchronousprobabilisticgames AT zhimingliu synthesismethodforzerosummeanpayoffasynchronousprobabilisticgames AT tiexinwang synthesismethodforzerosummeanpayoffasynchronousprobabilisticgames |