Symmetry Reduction in Infinite Games with Finite Branching

Autor:	Steen Vester, Nicolas Markey
Rok vydání:	2014
Předmět:	Discrete mathematics TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Computer Science::Logic in Computer Science Temporal logic Symmetry reduction Symmetry group Mathematics
Zdroj:	Automated Technology for Verification and Analysis ISBN: 9783319119359 ATVA Lecture Notes in Computer Science
DOI:	10.1007/978-3-319-11936-6_21
Popis:	Symmetry reductions have been applied extensively for the verification of finite-state concurrent systems and hardware designs using model-checking of temporal logics such as LTL, CTL and CTLs, 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 model-checking of the temporal logic ATLs.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_dedup___::b1bca832d919e13cf4f788f33fe2425d https://doi.org/10.1007/978-3-319-11936-6_21 Zobrazit plný text záznamu