## Symbolic Algorithms for Infinite-state Games

*Luca de Alfaro,
Thomas A. Henzinger,
and Rupak Majumdar*

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, 2001, pp. 536-550.

Download inofficial, sometimes updated
PostScript /
PDF document.
© 2001 Springer.