Symmetry Reduction in Infinite Games with Finite Branching

Nicolas Markey, Steen Vester

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

Abstract

Symmetry reduction has been applied extensively for verification of finite state concurrent systems and hardware designs using model-checking of the temporal logics LTL, CTL and CTL, as well as real-time and probabilistic system model-checking. In this paper we extend the technique to handle infinite-state games on graphs with finite branching where the objectives of the players can be very general. As particular applications, it is shown that the technique can be applied to reduce the state space in parity games as well as when doing modelchecking of the Alternating-time temporal logic ATL.
Original languageEnglish
Title of host publicationProceedings of the 12th International Symposium on Automated Technology for Verification and Analysis (ATVA 2014)
EditorsFranck Cassez, Jean-François Raskin
Number of pages15
PublisherSpringer
Publication date2014
Pages281-296
ISBN (Print)978-3-319-11935-9
Publication statusPublished - 2014
Event12th International Symposium on Automated Technology for Verification and Analysis (ATVA 2014) - Sydney, Australia
Duration: 3 Nov 20147 Nov 2014
Conference number: 12

Conference

Conference12th International Symposium on Automated Technology for Verification and Analysis (ATVA 2014)
Number12
CountryAustralia
CitySydney
Period03/11/201407/11/2014
SeriesLecture Notes in Computer Science
Number8837
ISSN0302-9743

Cite this

Markey, N., & Vester, S. (2014). Symmetry Reduction in Infinite Games with Finite Branching. In F. Cassez, & J-F. Raskin (Eds.), Proceedings of the 12th International Symposium on Automated Technology for Verification and Analysis (ATVA 2014) (pp. 281-296). Springer. Lecture Notes in Computer Science, No. 8837