---
res:
bibo_abstract:
- "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:\n1 \tClass 1 consists
of infinite-state structures for which all safety and reachability games can be
solved.\n2 \tClass 2 consists of infinite-state structures for which all ω-regular
games can be solved.\n3 \tClass 3 consists of infinite-state structures for which
all nested positive boolean combinations of ω-regular games can be solved.\n4
\ \tClass 4 consists of infinite-state structures for which all nested boolean
combinations of ω-regular games can be solved.\nWe 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 infinitestate
games with arbitrary ω-regular objectives, and prove termination over all class-2
structures. This settles, in particular, the symbolic controller synthesis problem
for rectangular hybrid systems.@eng"
bibo_authorlist:
- foaf_Person:
foaf_givenName: Luca
foaf_name: de Alfaro, Luca
foaf_surname: De Alfaro
- foaf_Person:
foaf_givenName: Thomas A
foaf_name: Thomas Henzinger
foaf_surname: Henzinger
foaf_workInfoHomepage: http://www.librecat.org/personId=40876CD8-F248-11E8-B48F-1D18A9856A87
orcid: 0000−0002−2985−7724
- foaf_Person:
foaf_givenName: Ritankar
foaf_name: Majumdar, Ritankar S
foaf_surname: Majumdar
bibo_doi: 10.1007/3-540-44685-0_36
bibo_volume: 2154
dct_date: 2001^xs_gYear
dct_publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik@
dct_title: Symbolic algorithms for infinite-state games@
...