---
_id: '3846'
abstract:
- lang: eng
text: We summarize classical and recent results about two-player games played on
graphs with ω-regular objectives. These games have applications in the verification
and synthesis of reactive systems. Important distinctions are whether a graph
game is turn-based or concurrent; deterministic or stochastic; zero-sum or not.
We cluster known results and open problems according to these classifications.
acknowledgement: This research was supported in part by the ONR grant N00014-02-1-0671,
by the AFOSR MURI grant F49620-00-1-0327, and by the NSF grants CCR-9988172, CCR-0085949,
and CCR-0225610.
article_processing_charge: No
article_type: original
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
citation:
ama: Chatterjee K, Henzinger TA. A survey of stochastic ω regular games. Journal
of Computer and System Sciences. 2012;78(2):394-413. doi:10.1016/j.jcss.2011.05.002
apa: Chatterjee, K., & Henzinger, T. A. (2012). A survey of stochastic ω regular
games. Journal of Computer and System Sciences. Elsevier. https://doi.org/10.1016/j.jcss.2011.05.002
chicago: Chatterjee, Krishnendu, and Thomas A Henzinger. “A Survey of Stochastic
ω Regular Games.” Journal of Computer and System Sciences. Elsevier, 2012.
https://doi.org/10.1016/j.jcss.2011.05.002.
ieee: K. Chatterjee and T. A. Henzinger, “A survey of stochastic ω regular games,”
Journal of Computer and System Sciences, vol. 78, no. 2. Elsevier, pp.
394–413, 2012.
ista: Chatterjee K, Henzinger TA. 2012. A survey of stochastic ω regular games.
Journal of Computer and System Sciences. 78(2), 394–413.
mla: Chatterjee, Krishnendu, and Thomas A. Henzinger. “A Survey of Stochastic ω
Regular Games.” Journal of Computer and System Sciences, vol. 78, no. 2,
Elsevier, 2012, pp. 394–413, doi:10.1016/j.jcss.2011.05.002.
short: K. Chatterjee, T.A. Henzinger, Journal of Computer and System Sciences 78
(2012) 394–413.
date_created: 2018-12-11T12:05:29Z
date_published: 2012-03-02T00:00:00Z
date_updated: 2022-05-24T08:00:54Z
day: '02'
ddc:
- '000'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1016/j.jcss.2011.05.002
file:
- access_level: open_access
checksum: 241b939deb4517cdd4426d49c67e3fa2
content_type: application/pdf
creator: kschuh
date_created: 2019-01-29T10:54:28Z
date_updated: 2020-07-14T12:46:17Z
file_id: '5897'
file_name: a_survey_of_stochastic_omega-regular_games.pdf
file_size: 336450
relation: main_file
file_date_updated: 2020-07-14T12:46:17Z
has_accepted_license: '1'
intvolume: ' 78'
issue: '2'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.1016/j.jcss.2011.05.002
month: '03'
oa: 1
oa_version: Submitted Version
page: 394 - 413
publication: Journal of Computer and System Sciences
publication_status: published
publisher: Elsevier
publist_id: '2341'
quality_controlled: '1'
scopus_import: '1'
status: public
title: A survey of stochastic ω regular games
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 78
year: '2012'
...
---
_id: '3128'
abstract:
- lang: eng
text: 'We consider two-player zero-sum stochastic games on graphs with ω-regular
winning conditions specified as parity objectives. These games have applications
in the design and control of reactive systems. We survey the complexity results
for the problem of deciding the winner in such games, and in classes of interest
obtained as special cases, based on the information and the power of randomization
available to the players, on the class of objectives and on the winning mode.
On the basis of information, these games can be classified as follows: (a) partial-observation
(both players have partial view of the game); (b) one-sided partial-observation
(one player has partial-observation and the other player has complete-observation);
and (c) complete-observation (both players have complete view of the game). The
one-sided partial-observation games have two important subclasses: the one-player
games, known as partial-observation Markov decision processes (POMDPs), and the
blind one-player games, known as probabilistic automata. On the basis of randomization,
(a) the players may not be allowed to use randomization (pure strategies), or
(b) they may choose a probability distribution over actions but the actual random
choice is external and not visible to the player (actions invisible), or (c) they
may use full randomization. Finally, various classes of games are obtained by
restricting the parity objective to a reachability, safety, Büchi, or coBüchi
condition. We also consider several winning modes, such as sure-winning (i.e.,
all outcomes of a strategy have to satisfy the winning condition), almost-sure
winning (i.e., winning with probability 1), limit-sure winning (i.e., winning
with probability arbitrarily close to 1), and value-threshold winning (i.e., winning
with probability at least ν, where ν is a given rational). '
acknowledgement: 'The research was supported by Austrian Science Fund (FWF) Grant
No. P 23499-N23 on Modern Graph Algorithmic Techniques in Formal Verification, FWF
NFN Grant No. S11407-N23(RiSE), ERC Start grant (279307: Graph Games), Microsoft
faculty fellows award, ERC Advanced grant QUAREM, and FWF Grant No. S11403-N23 (RiSE).'
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Laurent
full_name: Doyen, Laurent
last_name: Doyen
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
citation:
ama: Chatterjee K, Doyen L, Henzinger TA. A survey of partial-observation stochastic
parity games. Formal Methods in System Design. 2012;43(2):268-284. doi:10.1007/s10703-012-0164-2
apa: Chatterjee, K., Doyen, L., & Henzinger, T. A. (2012). A survey of partial-observation
stochastic parity games. Formal Methods in System Design. Springer. https://doi.org/10.1007/s10703-012-0164-2
chicago: Chatterjee, Krishnendu, Laurent Doyen, and Thomas A Henzinger. “A Survey
of Partial-Observation Stochastic Parity Games.” Formal Methods in System Design.
Springer, 2012. https://doi.org/10.1007/s10703-012-0164-2.
ieee: K. Chatterjee, L. Doyen, and T. A. Henzinger, “A survey of partial-observation
stochastic parity games,” Formal Methods in System Design, vol. 43, no.
2. Springer, pp. 268–284, 2012.
ista: Chatterjee K, Doyen L, Henzinger TA. 2012. A survey of partial-observation
stochastic parity games. Formal Methods in System Design. 43(2), 268–284.
mla: Chatterjee, Krishnendu, et al. “A Survey of Partial-Observation Stochastic
Parity Games.” Formal Methods in System Design, vol. 43, no. 2, Springer,
2012, pp. 268–84, doi:10.1007/s10703-012-0164-2.
short: K. Chatterjee, L. Doyen, T.A. Henzinger, Formal Methods in System Design
43 (2012) 268–284.
date_created: 2018-12-11T12:01:33Z
date_published: 2012-10-01T00:00:00Z
date_updated: 2021-01-12T07:41:15Z
day: '01'
ddc:
- '005'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1007/s10703-012-0164-2
ec_funded: 1
file:
- access_level: open_access
checksum: dd3d590f383bb2ac6cfda1489ac1c42a
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:11:27Z
date_updated: 2020-07-14T12:46:00Z
file_id: '4882'
file_name: IST-2014-303-v1+1_Survey_Partial-Observation_Stochastic_Parity_Games.pdf
file_size: 163983
relation: main_file
file_date_updated: 2020-07-14T12:46:00Z
has_accepted_license: '1'
intvolume: ' 43'
issue: '2'
language:
- iso: eng
month: '10'
oa: 1
oa_version: Submitted Version
page: 268 - 284
project:
- _id: 2584A770-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: P 23499-N23
name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _id: 2587B514-B435-11E9-9278-68D0E5697425
name: Microsoft Research Faculty Fellowship
publication: Formal Methods in System Design
publication_status: published
publisher: Springer
publist_id: '3570'
pubrep_id: '303'
quality_controlled: '1'
scopus_import: 1
status: public
title: A survey of partial-observation stochastic parity games
type: journal_article
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 43
year: '2012'
...
---
_id: '3155'
abstract:
- lang: eng
text: 'We propose synchronous interfaces, a new interface theory for discrete-time
systems. We use an application to time-triggered scheduling to drive the design
choices for our formalism; in particular, additionally to deriving useful mathematical
properties, we focus on providing a syntax which is adapted to natural high-level
system modeling. As a result, we develop an interface model that relies on a guarded-command
based language and is equipped with shared variables and explicit discrete-time
clocks. We define all standard interface operations: compatibility checking, composition,
refinement, and shared refinement. Apart from the synchronous interface model,
the contribution of this paper is the establishment of a formal relation between
interface theories and real-time scheduling, where we demonstrate a fully automatic
framework for the incremental computation of time-triggered schedules.'
acknowledgement: Research partially supported by the Danish-Chinese Center for Cyber
Physical Systems (Grant No.61061130541) and VKR Center of Excellence MT-LAB.
alternative_title:
- LNCS
author:
- first_name: Benoît
full_name: Delahaye, Benoît
last_name: Delahaye
- first_name: Uli
full_name: Fahrenberg, Uli
last_name: Fahrenberg
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Axel
full_name: Legay, Axel
last_name: Legay
- first_name: Dejan
full_name: Nickovic, Dejan
id: 41BCEE5C-F248-11E8-B48F-1D18A9856A87
last_name: Nickovic
citation:
ama: 'Delahaye B, Fahrenberg U, Henzinger TA, Legay A, Nickovic D. Synchronous interface
theories and time triggered scheduling. In: Vol 7273. Springer; 2012:203-218.
doi:10.1007/978-3-642-30793-5_13'
apa: 'Delahaye, B., Fahrenberg, U., Henzinger, T. A., Legay, A., & Nickovic,
D. (2012). Synchronous interface theories and time triggered scheduling (Vol.
7273, pp. 203–218). Presented at the FORTE: Formal Techniques for Networked and
Distributed Systems & FMOODS: Formal Methods for Open Object-Based Distributed
Systems , Stockholm, Sweden: Springer. https://doi.org/10.1007/978-3-642-30793-5_13'
chicago: Delahaye, Benoît, Uli Fahrenberg, Thomas A Henzinger, Axel Legay, and Dejan
Nickovic. “Synchronous Interface Theories and Time Triggered Scheduling,” 7273:203–18.
Springer, 2012. https://doi.org/10.1007/978-3-642-30793-5_13.
ieee: 'B. Delahaye, U. Fahrenberg, T. A. Henzinger, A. Legay, and D. Nickovic, “Synchronous
interface theories and time triggered scheduling,” presented at the FORTE: Formal
Techniques for Networked and Distributed Systems & FMOODS: Formal Methods
for Open Object-Based Distributed Systems , Stockholm, Sweden, 2012, vol. 7273,
pp. 203–218.'
ista: 'Delahaye B, Fahrenberg U, Henzinger TA, Legay A, Nickovic D. 2012. Synchronous
interface theories and time triggered scheduling. FORTE: Formal Techniques for
Networked and Distributed Systems & FMOODS: Formal Methods for Open Object-Based
Distributed Systems , LNCS, vol. 7273, 203–218.'
mla: Delahaye, Benoît, et al. Synchronous Interface Theories and Time Triggered
Scheduling. Vol. 7273, Springer, 2012, pp. 203–18, doi:10.1007/978-3-642-30793-5_13.
short: B. Delahaye, U. Fahrenberg, T.A. Henzinger, A. Legay, D. Nickovic, in:, Springer,
2012, pp. 203–218.
conference:
end_date: 2012-06-16
location: Stockholm, Sweden
name: 'FORTE: Formal Techniques for Networked and Distributed Systems & FMOODS:
Formal Methods for Open Object-Based Distributed Systems '
start_date: 2012-06-13
date_created: 2018-12-11T12:01:43Z
date_published: 2012-06-01T00:00:00Z
date_updated: 2021-01-12T07:41:26Z
day: '01'
ddc:
- '004'
department:
- _id: ToHe
doi: 10.1007/978-3-642-30793-5_13
file:
- access_level: open_access
checksum: feae2e07f2d9a59843f8ddabf25d179f
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:11:25Z
date_updated: 2020-07-14T12:46:01Z
file_id: '4879'
file_name: IST-2012-88-v1+1_Synchronous_interface_theories_and_time_triggered_scheduling.pdf
file_size: 493198
relation: main_file
file_date_updated: 2020-07-14T12:46:01Z
has_accepted_license: '1'
intvolume: ' 7273'
language:
- iso: eng
month: '06'
oa: 1
oa_version: Submitted Version
page: 203 - 218
publication_status: published
publisher: Springer
publist_id: '3539'
pubrep_id: '88'
quality_controlled: '1'
scopus_import: 1
status: public
title: Synchronous interface theories and time triggered scheduling
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 7273
year: '2012'
...
---
_id: '3836'
abstract:
- lang: eng
text: Hierarchical Timing Language (HTL) is a coordination language for distributed,
hard real-time applications. HTL is a hierarchical extension of Giotto and, like
its predecessor, based on the logical execution time (LET) paradigm of real-time
programming. Giotto is compiled into code for a virtual machine, called the EmbeddedMachine
(or E machine). If HTL is targeted to the E machine, then the hierarchicalprogram
structure needs to be flattened; the flattening makes separatecompilation difficult,
and may result in E machinecode of exponential size. In this paper, we propose
a generalization of the E machine, which supports a hierarchicalprogram structure
at runtime through real-time trigger mechanisms that are arranged in a tree. We
present the generalized E machine, and a modular compiler for HTL that generates
code of linear size. The compiler may generate code for any part of a given HTL
program separately in any order.
author:
- first_name: Arkadeb
full_name: Ghosal, Arkadeb
last_name: Ghosal
- first_name: Daniel
full_name: Iercan, Daniel
last_name: Iercan
- first_name: Christoph
full_name: Kirsch, Christoph
last_name: Kirsch
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Alberto
full_name: Sangiovanni Vincentelli, Alberto
last_name: Sangiovanni Vincentelli
citation:
ama: Ghosal A, Iercan D, Kirsch C, Henzinger TA, Sangiovanni Vincentelli A. Separate
compilation of hierarchical real-time programs into linear-bounded embedded machine
code. Science of Computer Programming. 2012;77(2):96-112. doi:10.1016/j.scico.2010.06.004
apa: Ghosal, A., Iercan, D., Kirsch, C., Henzinger, T. A., & Sangiovanni Vincentelli,
A. (2012). Separate compilation of hierarchical real-time programs into linear-bounded
embedded machine code. Science of Computer Programming. Elsevier. https://doi.org/10.1016/j.scico.2010.06.004
chicago: Ghosal, Arkadeb, Daniel Iercan, Christoph Kirsch, Thomas A Henzinger, and
Alberto Sangiovanni Vincentelli. “Separate Compilation of Hierarchical Real-Time
Programs into Linear-Bounded Embedded Machine Code.” Science of Computer Programming.
Elsevier, 2012. https://doi.org/10.1016/j.scico.2010.06.004.
ieee: A. Ghosal, D. Iercan, C. Kirsch, T. A. Henzinger, and A. Sangiovanni Vincentelli,
“Separate compilation of hierarchical real-time programs into linear-bounded embedded
machine code,” Science of Computer Programming, vol. 77, no. 2. Elsevier,
pp. 96–112, 2012.
ista: Ghosal A, Iercan D, Kirsch C, Henzinger TA, Sangiovanni Vincentelli A. 2012.
Separate compilation of hierarchical real-time programs into linear-bounded embedded
machine code. Science of Computer Programming. 77(2), 96–112.
mla: Ghosal, Arkadeb, et al. “Separate Compilation of Hierarchical Real-Time Programs
into Linear-Bounded Embedded Machine Code.” Science of Computer Programming,
vol. 77, no. 2, Elsevier, 2012, pp. 96–112, doi:10.1016/j.scico.2010.06.004.
short: A. Ghosal, D. Iercan, C. Kirsch, T.A. Henzinger, A. Sangiovanni Vincentelli,
Science of Computer Programming 77 (2012) 96–112.
date_created: 2018-12-11T12:05:26Z
date_published: 2012-02-01T00:00:00Z
date_updated: 2021-01-12T07:52:32Z
day: '01'
department:
- _id: ToHe
doi: 10.1016/j.scico.2010.06.004
intvolume: ' 77'
issue: '2'
language:
- iso: eng
month: '02'
oa_version: None
page: 96 - 112
publication: Science of Computer Programming
publication_status: published
publisher: Elsevier
publist_id: '2370'
quality_controlled: '1'
scopus_import: 1
status: public
title: Separate compilation of hierarchical real-time programs into linear-bounded
embedded machine code
type: journal_article
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 77
year: '2012'
...
---
_id: '2967'
abstract:
- lang: eng
text: For programs whose data variables range over Boolean or finite domains, program
verification is decidable, and this forms the basis of recent tools for software
model checking. In this article, we consider algorithmic verification of programs
that use Boolean variables, and in addition, access a single read-only array whose
length is potentially unbounded, and whose elements range over an unbounded data
domain. We show that the reachability problem, while undecidable in general, is
(1) PSPACE-complete for programs in which the array-accessing for-loops are not
nested, (2) decidable for a restricted class of programs with doubly nested loops.
The second result establishes connections to automata and logics defining languages
over data words.
acknowledgement: This research was supported in part by the NSF Cybertrust award CNS
0524059, by the European Research Council (ERC) Advanced Investigator Grant QUAREM,
and by the Austrian Science Fund (FWF) project S11402-N23.
article_number: '27'
author:
- first_name: Rajeev
full_name: Alur, Rajeev
last_name: Alur
- first_name: Pavol
full_name: Cerny, Pavol
id: 4DCBEFFE-F248-11E8-B48F-1D18A9856A87
last_name: Cerny
- first_name: Scott
full_name: Weinstein, Scott
last_name: Weinstein
citation:
ama: Alur R, Cerny P, Weinstein S. Algorithmic analysis of array-accessing programs.
ACM Transactions on Computational Logic (TOCL). 2012;13(3). doi:10.1145/2287718.2287727
apa: Alur, R., Cerny, P., & Weinstein, S. (2012). Algorithmic analysis of array-accessing
programs. ACM Transactions on Computational Logic (TOCL). ACM. https://doi.org/10.1145/2287718.2287727
chicago: Alur, Rajeev, Pavol Cerny, and Scott Weinstein. “Algorithmic Analysis of
Array-Accessing Programs.” ACM Transactions on Computational Logic (TOCL).
ACM, 2012. https://doi.org/10.1145/2287718.2287727.
ieee: R. Alur, P. Cerny, and S. Weinstein, “Algorithmic analysis of array-accessing
programs,” ACM Transactions on Computational Logic (TOCL), vol. 13, no.
3. ACM, 2012.
ista: Alur R, Cerny P, Weinstein S. 2012. Algorithmic analysis of array-accessing
programs. ACM Transactions on Computational Logic (TOCL). 13(3), 27.
mla: Alur, Rajeev, et al. “Algorithmic Analysis of Array-Accessing Programs.” ACM
Transactions on Computational Logic (TOCL), vol. 13, no. 3, 27, ACM, 2012,
doi:10.1145/2287718.2287727.
short: R. Alur, P. Cerny, S. Weinstein, ACM Transactions on Computational Logic
(TOCL) 13 (2012).
date_created: 2018-12-11T12:00:36Z
date_published: 2012-08-01T00:00:00Z
date_updated: 2023-02-23T12:09:43Z
day: '01'
department:
- _id: ToHe
doi: 10.1145/2287718.2287727
ec_funded: 1
intvolume: ' 13'
issue: '3'
language:
- iso: eng
month: '08'
oa_version: None
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
publication: ACM Transactions on Computational Logic (TOCL)
publication_status: published
publisher: ACM
publist_id: '3748'
quality_controlled: '1'
related_material:
record:
- id: '4403'
relation: earlier_version
status: public
scopus_import: 1
status: public
title: Algorithmic analysis of array-accessing programs
type: journal_article
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 13
year: '2012'
...