Concurrent Stochastic Lossy Channel Games

Daniel Stan, Muhammad Najib, Anthony Widjaja Lin, Parosh Aziz Abdulla

Research output: Chapter in Book/Report/Conference proceedingConference contribution

36 Downloads (Pure)

Abstract

Concurrent stochastic games are an important formalism for the rational verification of probabilistic multi-agent systems, which involves verifying whether a temporal logic property is satisfied in some or all game-theoretic equilibria of such systems. In this work, we study the rational verification of probabilistic multi-agent systems where agents can cooperate by communicating over unbounded lossy channels. To model such systems, we present concurrent stochastic lossy channel games (CSLCG) and employ an equilibrium concept from cooperative game theory known as the core, which is the most fundamental and widely studied cooperative equilibrium concept. Our main contribution is twofold. First, we show that the rational verification problem is undecidable for systems whose agents have almost-sure LTL objectives. Second, we provide a decidable fragment of such a class of objectives that subsumes almost-sure reachability and safety. Our techniques involve reductions to solving infinite-state zero-sum games with conjunctions of qualitative objectives. To the best of our knowledge, our result represents the first decidability result on the rational verification of stochastic multi-agent systems on infinite arenas.
Original languageEnglish
Title of host publication32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)
EditorsAniello Murano, Alexandra Silva
PublisherSchloss Dagstuhl - Leibniz-Zentrum für Informatik
Pages46:1-46:19
Number of pages19
ISBN (Print)9783959773102
DOIs
Publication statusPublished - 7 Feb 2024

Publication series

NameLeibniz International Proceedings in Informatics (LIPIcs)
Volume288
ISSN (Print)1868-8969

Keywords

  • Nash equilibrium
  • concurrent
  • cooperative
  • core
  • finite attractor property
  • games
  • lossy channels
  • stochastic
  • wqo

ASJC Scopus subject areas

  • Software

Fingerprint

Dive into the research topics of 'Concurrent Stochastic Lossy Channel Games'. Together they form a unique fingerprint.

Cite this