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 language | English |
---|---|
Title of host publication | Proceedings of the 12th International Symposium on Automated Technology for Verification and Analysis (ATVA 2014) |
Editors | Franck Cassez, Jean-François Raskin |
Number of pages | 15 |
Publisher | Springer |
Publication date | 2014 |
Pages | 281-296 |
ISBN (Print) | 978-3-319-11935-9 |
Publication status | Published - 2014 |
Event | 12th International Symposium on Automated Technology for Verification and Analysis - Sydney, Australia Duration: 3 Nov 2014 → 7 Nov 2014 Conference number: 12 |
Conference
Conference | 12th International Symposium on Automated Technology for Verification and Analysis |
---|---|
Number | 12 |
Country/Territory | Australia |
City | Sydney |
Period | 03/11/2014 → 07/11/2014 |
Series | Lecture Notes in Computer Science |
---|---|
Number | 8837 |
ISSN | 0302-9743 |