<?xml version="1.0" encoding="UTF-8"?>
<rdf:RDF xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"
         xmlns:dc="http://purl.org/dc/terms/"
         xmlns:foaf="http://xmlns.com/foaf/0.1/"
         xmlns:bibo="http://purl.org/ontology/bibo/"
         xmlns:fabio="http://purl.org/spar/fabio/"
         xmlns:owl="http://www.w3.org/2002/07/owl#"
         xmlns:event="http://purl.org/NET/c4dm/event.owl#"
         xmlns:ore="http://www.openarchives.org/ore/terms/">

    <rdf:Description rdf:about="https://research-explorer.ista.ac.at/record/3354">
        <ore:isDescribedBy rdf:resource="https://research-explorer.ista.ac.at/record/3354"/>
        <dc:title>Qualitative concurrent parity games</dc:title>
        <bibo:authorList rdf:parseType="Collection">
            <foaf:Person>
                <foaf:name></foaf:name>
                <foaf:surname></foaf:surname>
                <foaf:givenname></foaf:givenname>
            </foaf:Person>
            <foaf:Person>
                <foaf:name></foaf:name>
                <foaf:surname></foaf:surname>
                <foaf:givenname></foaf:givenname>
            </foaf:Person>
            <foaf:Person>
                <foaf:name></foaf:name>
                <foaf:surname></foaf:surname>
                <foaf:givenname></foaf:givenname>
            </foaf:Person>
        </bibo:authorList>
        <bibo:abstract>We consider two-player games played on a finite state space for an infinite number of rounds. The games are concurrent: in each round, the two players (player 1 and player 2) choose their moves independently and simultaneously; the current state and the two moves determine the successor state. We consider ω-regular winning conditions specified as parity objectives. Both players are allowed to use randomization when choosing their moves. We study the computation of the limit-winning set of states, consisting of the states where the sup-inf value of the game for player 1 is 1: in other words, a state is limit-winning if player 1 can ensure a probability of winning arbitrarily close to 1. We show that the limit-winning set can be computed in O(n2d+2) time, where n is the size of the game structure and 2d is the number of priorities (or colors). The membership problem of whether a state belongs to the limit-winning set can be decided in NP ∩ coNP. While this complexity is the same as for the simpler class of turn-based parity games, where in each state only one of the two players has a choice of moves, our algorithms are considerably more involved than those for turn-based games. This is because concurrent games do not satisfy two of the most fundamental properties of turn-based parity games. First, in concurrent games limit-winning strategies require randomization; and second, they require infinite memory.</bibo:abstract>
        <bibo:volume>12</bibo:volume>
        <bibo:issue>4</bibo:issue>
        <dc:publisher>ACM</dc:publisher>
        <bibo:doi rdf:resource="10.1145/1970398.1970404" />
        <ore:similarTo rdf:resource="info:doi/10.1145/1970398.1970404"/>
    </rdf:Description>
</rdf:RDF>
