Repository logo

Infoscience

  • English
  • French
Log In
Logo EPFL, École polytechnique fédérale de Lausanne

Infoscience

  • English
  • French
Log In
  1. Home
  2. Academic and Research Output
  3. Reports, Documentation, and Standards
  4. Jurdzinski-ing Rabin and Streett
 
report

Jurdzinski-ing Rabin and Streett

Piterman, Nir
•
Pnueli, Amir
2005

In this paper we give a recursive fixpoint characterization of the winning regions in Rabin and Streett games. We use this characterization in two ways. First, we introduce direct Rabin and Streett ranking that are a sound and complete way to characterize the winning sets in the respective games. By computing directly and explicitly the ranking we can solve such games in time $O(mn^{k+1}kk!)$ and space $O(nk)$ for Rabin and $O(nkk!)$ for Streett where $n$ is the number of states, $m$ the number of transitions, and $k$ the number of pairs in the winning condition. Second, by keeping intermediate values during the fixpoint evaluation, we can solve such games symbolically in time $O(n^{k+1}k!)$ and space $O(n^{k+1}k!)$. These results improve on the current bounds of O(mn^{2k}k!)$ time in the case of direct (symbolic) solution or $O(m(nk^2k!)^k)$ in the case of reduction to parity games.

  • Files
  • Details
  • Metrics
Type
report
Author(s)
Piterman, Nir
•
Pnueli, Amir
Date Issued

2005

Subjects

Verification

•

Games

•

Rabin Games

•

Streett Games

Written at

EPFL

EPFL units
MTC  
Available on Infoscience
September 22, 2005
Use this identifier to reference this record
https://infoscience.epfl.ch/handle/20.500.14299/217079
Logo EPFL, École polytechnique fédérale de Lausanne
  • Contact
  • infoscience@epfl.ch

  • Follow us on Facebook
  • Follow us on Instagram
  • Follow us on LinkedIn
  • Follow us on X
  • Follow us on Youtube
AccessibilityLegal noticePrivacy policyCookie settingsEnd User AgreementGet helpFeedback

Infoscience is a service managed and provided by the Library and IT Services of EPFL. © EPFL, tous droits réservés