A procedure for the analysis of state spaces is called symbolic if it manipulates not individual states, but sets of states that are represented by constraints. Such a procedure can be used for the analysis of infinite state spaces, provided termination is guaranteed. We present symbolic procedures, and corresponding termination criteria, for the solution of infinite-state games, which occur in the control and modular verification of infinite-state systems. To characterize the termination of symbolic procedures for solving infinite-state games, we classify these game structures into four increasingly restrictive categories:
Class 1 consists of infinite-state structures for which all safety and reachability games can be solved.
Class 2 consists of infinite-state structures for which all omega-regular games can be solved.
Class 3 consists of infinite-state structures for which all nested positive boolean combinations of omega-regular games can be solved.
Class 4 consists of infinite-state structures for which all nested boolean combinations of omega-regular games can be solved.
We give a structural characterization for each class, using equivalence relations on the state spaces of games which range from game versions of trace equivalence to a game version of bisimilarity. We provide infinite-state examples for all four classes of games from control problems for hybrid systems. We conclude by presenting symbolic algorithms for the synthesis of winning strategies ("controller synthesis") for infinite-state games with arbitrary omega-regular objectives, and prove termination over all class-2 structures. This settles, in particular, the symbolic controller synthesis problem for rectangular hybrid systems.
Proceedings of the 12th International Conference on Concurrency Theory (CONCUR), Lecture Notes in Computer Science 2154, Springer-Verlag, 2001, pp. 536-550.