Predicting Winning Regions in Parity Games via Graph Neural Networks

2025-05-02 0 0 633.68KB 4 页 10玖币

侵权投诉

Predicting Winning Regions in Parity Games via

Graph Neural Networks

Tobias Hecking∗

German Aerospace Center (DLR)

Institute for Software Technology

Cologne, Germany

tobias.hecking@dlr.de

Swathy Muthukrishnan∗

University of Stuttgart

Stuttgart, Germany

swathy.muthukrishnan.24@gmail.com

Alexander Weinert∗

German Aerospace Center (DLR)

Institute for Software Technology

Cologne, Germany

alexander.weinert@dlr.de

Abstract

Solving parity games is a major building block for numerous

applications in reactive program verication and synthesis.

While they can be solved eciently in practice, no known

approach has a polynomial worst-case runtime complexity.

We present a incomplete polynomial-time approach to de-

termining the winning regions of parity games via graph

neural networks.

Our evaluation on 900 randomly generated parity games

shows that this approach is eective and ecient in prac-

tice. It correctly determines the winning regions of

∼

60% of

the games in our data set and only incurs minor errors in

the remaining ones. We believe that this approach can be

extended to eciently solve parity games as well.

ACM Reference Format:

Tobias Hecking, Swathy Muthukrishnan, and Alexander Weinert.

2023. Predicting Winning Regions in Parity Games via Graph Neural

Networks. In Proceedings of First International Workshop on Deep

Learning-aided Verication (DAV ’23). ACM, New York, NY, USA,

4pages. hps://doi.org/XXXXXXX.XXXXXXX

1 Introduction

Parity games are innite arena-based games between Player 0

and Player 1that capture all

𝜔

-regular languages. They are

the canonical model for specications of reactive systems,

where Player 0and Player 1represent the system and its

environment, respectively. Solving them is a major building

block for reactive program verication and synthesis. [

]

Solving comprises determining the winning regions of both

players as well as a winning strategy for both players.

∗

Authors are listed in alphabetical order and have contributed equally to

this work

Permission to make digital or hard copies of all or part of this work for

personal or classroom use is granted without fee provided that copies are not

made or distributed for prot or commercial advantage and that copies bear

this notice and the full citation on the rst page. Copyrights for components

of this work owned by others than ACM must be honored. Abstracting with

credit is permitted. To copy otherwise, or republish, to post on servers or to

redistribute to lists, requires prior specic permission and/or a fee. Request

permissions from permissions@acm.org.

DAV ’23, July 18, 2023, Paris, France

ACM ISBN 978-1-4503-XXXX-X/18/06. . . $15.00

hps://doi.org/XXXXXXX.XXXXXXX

The problem of solving parity games is known to be in

UP∩coUP

[

] and to be solvable in quasi-polynomial time [

There exist parity game solvers that are ecient in prac-

tice [

], all of which suer from a non-polynomial

worst-case runtime complexity.

Here, we trade completeness for eciency in determining

the winning regions. Classically, parity games are solved by

building a correct-by-construction strategy, which yields the

winning regions as a by-product. We instead train graph neu-

ral networks (GNNs) [

] to determine the winning regions.

Applying the trained GNN to a parity game

then yields a

prediction of the winning region of G.

In a preliminary evaluation we constructed two GNNs and

trained these on 2 100 randomly generated parity games. We

then predicted the winning region of another 900 randomly

generated parity games using these GNNs. This approach

yields correct winning regions in 537 (433) cases, as well as

regions that dier by one vertices from the correct result in

245 (279) cases.

2 Preliminaries

We write

and

R𝑘,𝑙

to denote the real numbers and the set

𝑘×𝑙

-matrices over the reals, respectively. Moreover, given

a set

𝑆

, we write

𝑆𝑛

to denote the

𝑛

-ary cartesian power of

𝑆

Parity Games. An arena

A=(𝑉 ,𝑉0,𝑉1, 𝐸)

comprises

a nite set of vertices

𝑉

, a partition

(𝑉0, 𝑉1)

𝑉

, as well

as a set of edges

𝐸⊆𝑉×𝑉

with

∀𝑣∈𝑉 . ({𝑣}×𝑉) ∩

𝐸≠∅

. We call

𝑉𝑖

the vertices of Player

𝑖

. A play

𝜌=

𝑣0𝑣1𝑣2···

is an innite path through

(𝑉 , 𝐸)

. A par-

ity game

(A,Parity(Ω))

comprises an arena

with vertex

set

𝑉

and a coloring

Ω:𝑉→N

. The play

𝜌

is winning for

Player 𝑖if (max {Ω(𝑣𝑖) | 𝑖∈N})mod 2 =𝑖.

A strategy

𝜎:𝑉𝑖→𝑉

for Player

𝑖

is a mapping with

∀𝑣∈𝑉𝑖.(𝑣, 𝜎 (𝑣)) ∈ 𝐸

. A play

𝜌=𝑣0𝑣1𝑣2···

is consistent

with

𝜎

∀𝑗∈N. 𝑣𝑗∈𝑉𝑖⇒𝑣𝑗+1=𝜎(𝑣𝑗)

. We say that

Player

𝑖

wins

from vertex

𝑣∈𝑉

if she has a strategy

𝜎

such that all plays starting in

𝑣

and consistent with

𝜎

are

winning for her. The winning region

𝑊𝑖(G)

of Player

𝑖

is the set of all vertices from which Player 𝑖wins G.

Neural Network Layers. A

𝑘, 𝑙

-neural network layer is a

function

ℎ:R𝑘→R𝑙

. In this work we use the linear layer

ℎ𝐴,𝑏 (𝑥)=𝑥𝐴𝑇+𝑏

, where

𝐴∈R𝑙×𝑘

and

𝑏∈R1×𝑙

, the rectied

arXiv:2210.09924v2 [cs.GT] 27 Jul 2023

文档加载中……请稍候！
如果长时间未打开，您也可以点击刷新试试。

下载文档到电脑，查找使用更方便

10 玖币 0人已下载

立即下载

摘要：

PredictingWinningRegionsinParityGamesviaGraphNeuralNetworksTobiasHecking∗GermanAerospaceCenter(DLR)InstituteforSoftwareTechnologyCologne,Germanytobias.hecking@dlr.deSwathyMuthukrishnan∗UniversityofStuttgartStuttgart,Germanyswathy.muthukrishnan.24@gmail.comAlexanderWeinert∗GermanAerospaceCenter(DLR)I...

展开>> 收起<<

Predicting Winning Regions in Parity Games via Graph Neural Networks.pdf

共4页,预览1页

还剩页未读，继续阅读

声明：本站为文档C2C交易模式，即用户上传的文档直接被用户下载，本站只是中间服务平台，本站所有文档下载所得的收益归上传人(含作者)所有。玖贝云文库仅提供信息存储空间，仅对用户上传内容的表现方式做保护处理，对上载内容本身不做任何修改或编辑。若文档所含内容侵犯了您的版权或隐私，请立即通知玖贝云文库，我们立即给予删除！

Predicting Winning Regions in Parity Games via Graph Neural Networks

相关推荐

开通VIP享超值会员特权

作者详情

相关内容

热门标签

举报选择: