Nicolas Markey

Abstract

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 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 model-checking of the temporal logic ATL*.

@inproceedings{atva2014-MV,
  author =              {Markey, Nicolas and Vester, Steen},
  title =               {Symmetry Reduction in Infinite Games with Finite
                         Branching},
  editor =              {Cassez, Franck and Raskin, Jean-Fran{\c c}ois},
  booktitle =           {{P}roceedings of the 12th {I}nternational
                         {S}ymposium on {A}utomated {T}echnology for
                         {V}erification and {A}nalysis ({ATVA}'14)},
  acronym =             {{ATVA}'14},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {8837},
  pages =               {281-296},
  year =                {2014},
  month =               nov,
  doi =                 {10.1007/978-3-319-11936-6_21},
  abstract =            {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
                         CTL\textsuperscript{*}, 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 ATL\textsuperscript{*}.},
}