---
OA_place: publisher
OA_type: hybrid
_id: '17474'
abstract:
- lang: eng
text: Entropic risk (ERisk) is an established risk measure in finance, quantifying
risk by an exponential re-weighting of rewards. We study ERisk for the first time
in the context of turn-based stochastic games with the total reward objective.
This gives rise to an objective function that demands the control of systems in
a risk-averse manner. We show that the resulting games are determined and, in
particular, admit optimal memoryless deterministic strategies. This contrasts
risk measures that previously have been considered in the special case of Markov
decision processes and that require randomization and/or memory. We provide several
results on the decidability and the computational complexity of the threshold
problem, i.e. whether the optimal value of ERisk exceeds a given threshold. Furthermore,
an approximation algorithm for the optimal value of ERisk is provided.
acknowledgement: Krishnendu Chatterjee reports financial support was provided by European
Research Council.
article_number: '105214'
article_processing_charge: Yes (in subscription journal)
article_type: original
arxiv: 1
author:
- first_name: Christel
full_name: Baier, Christel
last_name: Baier
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Tobias
full_name: Meggendorfer, Tobias
id: b21b0c15-30a2-11eb-80dc-f13ca25802e1
last_name: Meggendorfer
orcid: 0000-0002-1712-2165
- first_name: Jakob
full_name: Piribauer, Jakob
last_name: Piribauer
citation:
ama: Baier C, Chatterjee K, Meggendorfer T, Piribauer J. Entropic risk for turn-based
stochastic games. Information and Computation. 2024;301. doi:10.1016/j.ic.2024.105214
apa: Baier, C., Chatterjee, K., Meggendorfer, T., & Piribauer, J. (2024). Entropic
risk for turn-based stochastic games. Information and Computation. Elsevier.
https://doi.org/10.1016/j.ic.2024.105214
chicago: Baier, Christel, Krishnendu Chatterjee, Tobias Meggendorfer, and Jakob
Piribauer. “Entropic Risk for Turn-Based Stochastic Games.” Information and
Computation. Elsevier, 2024. https://doi.org/10.1016/j.ic.2024.105214.
ieee: C. Baier, K. Chatterjee, T. Meggendorfer, and J. Piribauer, “Entropic risk
for turn-based stochastic games,” Information and Computation, vol. 301.
Elsevier, 2024.
ista: Baier C, Chatterjee K, Meggendorfer T, Piribauer J. 2024. Entropic risk for
turn-based stochastic games. Information and Computation. 301, 105214.
mla: Baier, Christel, et al. “Entropic Risk for Turn-Based Stochastic Games.” Information
and Computation, vol. 301, 105214, Elsevier, 2024, doi:10.1016/j.ic.2024.105214.
short: C. Baier, K. Chatterjee, T. Meggendorfer, J. Piribauer, Information and Computation
301 (2024).
corr_author: '1'
date_created: 2024-09-01T22:01:07Z
date_published: 2024-12-01T00:00:00Z
date_updated: 2025-09-08T09:10:06Z
day: '01'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1016/j.ic.2024.105214
external_id:
arxiv:
- '2307.06611'
isi:
- '001301143400001'
file:
- access_level: open_access
checksum: f68e0c2f46f9b9c86815406bcf2ee2d4
content_type: application/pdf
creator: dernst
date_created: 2025-01-09T13:49:03Z
date_updated: 2025-01-09T13:49:03Z
file_id: '18817'
file_name: 2024_InformationComputation_Baier.pdf
file_size: 724703
relation: main_file
success: 1
file_date_updated: 2025-01-09T13:49:03Z
has_accepted_license: '1'
intvolume: ' 301'
isi: 1
language:
- iso: eng
month: '12'
oa: 1
oa_version: Published Version
publication: Information and Computation
publication_identifier:
eissn:
- 1090-2651
issn:
- 0890-5401
publication_status: published
publisher: Elsevier
quality_controlled: '1'
related_material:
record:
- id: '14417'
relation: earlier_version
status: public
scopus_import: '1'
status: public
title: Entropic risk for turn-based stochastic games
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 301
year: '2024'
...
---
_id: '11756'
abstract:
- lang: eng
text: We give two fully dynamic algorithms that maintain a (1 + ε)-approximation
of the weight M of a minimum spanning forest (MSF) of an n-node graph G with edges
weights in [1, W ], for any ε > 0. (1) Our deterministic algorithm takes O (W
2 log W /ε3) worst-case update time, which is O (1) if both W and ε are constants.
(2) Our randomized (Monte-Carlo style) algorithm works with high probability and
runs in worst-case O (log W /ε4) update time if W = O ((m∗)1/6/log2/3 n), where
m∗ is the minimum number of edges in the graph throughout all the updates. It
works even against an adaptive adversary. We complement our algorithmic results
with two cell-probe lower bounds for dynamically maintaining an approximation
of the weight of an MSF of a graph.
article_number: '104805'
article_processing_charge: No
article_type: original
arxiv: 1
author:
- first_name: Monika H
full_name: Henzinger, Monika H
id: 540c9bbd-f2de-11ec-812d-d04a5be85630
last_name: Henzinger
orcid: 0000-0002-5008-6530
- first_name: Pan
full_name: Peng, Pan
last_name: Peng
citation:
ama: Henzinger M, Peng P. Constant-time dynamic weight approximation for minimum
spanning forest. Information and Computation. 2021;281(12). doi:10.1016/j.ic.2021.104805
apa: Henzinger, M., & Peng, P. (2021). Constant-time dynamic weight approximation
for minimum spanning forest. Information and Computation. Elsevier. https://doi.org/10.1016/j.ic.2021.104805
chicago: Henzinger, Monika, and Pan Peng. “Constant-Time Dynamic Weight Approximation
for Minimum Spanning Forest.” Information and Computation. Elsevier, 2021.
https://doi.org/10.1016/j.ic.2021.104805.
ieee: M. Henzinger and P. Peng, “Constant-time dynamic weight approximation for
minimum spanning forest,” Information and Computation, vol. 281, no. 12.
Elsevier, 2021.
ista: Henzinger M, Peng P. 2021. Constant-time dynamic weight approximation for
minimum spanning forest. Information and Computation. 281(12), 104805.
mla: Henzinger, Monika, and Pan Peng. “Constant-Time Dynamic Weight Approximation
for Minimum Spanning Forest.” Information and Computation, vol. 281, no.
12, 104805, Elsevier, 2021, doi:10.1016/j.ic.2021.104805.
short: M. Henzinger, P. Peng, Information and Computation 281 (2021).
date_created: 2022-08-08T10:58:29Z
date_published: 2021-12-01T00:00:00Z
date_updated: 2024-11-06T12:09:22Z
day: '01'
doi: 10.1016/j.ic.2021.104805
extern: '1'
external_id:
arxiv:
- '2011.00977'
intvolume: ' 281'
issue: '12'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/2011.00977
month: '12'
oa: 1
oa_version: Preprint
publication: Information and Computation
publication_identifier:
issn:
- 0890-5401
publication_status: published
publisher: Elsevier
quality_controlled: '1'
scopus_import: '1'
status: public
title: Constant-time dynamic weight approximation for minimum spanning forest
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 281
year: '2021'
...
---
_id: '11757'
abstract:
- lang: eng
text: We develop a dynamic version of the primal-dual method for optimization problems,
and apply it to obtain the following results. (1) For the dynamic set-cover problem,
we maintain an O ( f 2)-approximately optimal solution in O ( f · log(m + n))
amortized update time, where f is the maximum “frequency” of an element, n is
the number of sets, and m is the maximum number of elements in the universe at
any point in time. (2) For the dynamic b-matching problem, we maintain an O (1)-approximately
optimal solution in O (log3 n) amortized update time, where n is the number of
nodes in the graph.
article_processing_charge: No
article_type: original
author:
- first_name: Sayan
full_name: Bhattacharya, Sayan
last_name: Bhattacharya
- first_name: Monika H
full_name: Henzinger, Monika H
id: 540c9bbd-f2de-11ec-812d-d04a5be85630
last_name: Henzinger
orcid: 0000-0002-5008-6530
- first_name: Giuseppe
full_name: Italiano, Giuseppe
last_name: Italiano
citation:
ama: Bhattacharya S, Henzinger M, Italiano G. Dynamic algorithms via the primal-dual
method. Information and Computation. 2018;261(08):219-239. doi:10.1016/j.ic.2018.02.005
apa: Bhattacharya, S., Henzinger, M., & Italiano, G. (2018). Dynamic algorithms
via the primal-dual method. Information and Computation. Elsevier. https://doi.org/10.1016/j.ic.2018.02.005
chicago: Bhattacharya, Sayan, Monika Henzinger, and Giuseppe Italiano. “Dynamic
Algorithms via the Primal-Dual Method.” Information and Computation. Elsevier,
2018. https://doi.org/10.1016/j.ic.2018.02.005.
ieee: S. Bhattacharya, M. Henzinger, and G. Italiano, “Dynamic algorithms via the
primal-dual method,” Information and Computation, vol. 261, no. 08. Elsevier,
pp. 219–239, 2018.
ista: Bhattacharya S, Henzinger M, Italiano G. 2018. Dynamic algorithms via the
primal-dual method. Information and Computation. 261(08), 219–239.
mla: Bhattacharya, Sayan, et al. “Dynamic Algorithms via the Primal-Dual Method.”
Information and Computation, vol. 261, no. 08, Elsevier, 2018, pp. 219–39,
doi:10.1016/j.ic.2018.02.005.
short: S. Bhattacharya, M. Henzinger, G. Italiano, Information and Computation 261
(2018) 219–239.
date_created: 2022-08-08T11:20:03Z
date_published: 2018-08-01T00:00:00Z
date_updated: 2024-11-06T08:13:33Z
day: '01'
doi: 10.1016/j.ic.2018.02.005
extern: '1'
intvolume: ' 261'
issue: '08'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.1016/j.ic.2018.02.005
month: '08'
oa: 1
oa_version: Published Version
page: 219-239
publication: Information and Computation
publication_identifier:
issn:
- 0890-5401
publication_status: published
publisher: Elsevier
quality_controlled: '1'
scopus_import: '1'
status: public
title: Dynamic algorithms via the primal-dual method
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 261
year: '2018'
...
---
_id: '681'
abstract:
- lang: eng
text: Two-player games on graphs provide the theoretical framework for many important
problems such as reactive synthesis. While the traditional study of two-player
zero-sum games has been extended to multi-player games with several notions of
equilibria, they are decidable only for perfect-information games, whereas several
applications require imperfect-information. In this paper we propose a new notion
of equilibria, called doomsday equilibria, which is a strategy profile where all
players satisfy their own objective, and if any coalition of players deviates
and violates even one of the players' objective, then the objective of every player
is violated. We present algorithms and complexity results for deciding the existence
of doomsday equilibria for various classes of ω-regular objectives, both for imperfect-information
games, and for perfect-information games. We provide optimal complexity bounds
for imperfect-information games, and in most cases for perfect-information games.
article_processing_charge: No
article_type: original
arxiv: 1
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: Emmanuel
full_name: Filiot, Emmanuel
last_name: Filiot
- first_name: Jean
full_name: Raskin, Jean
last_name: Raskin
citation:
ama: Chatterjee K, Doyen L, Filiot E, Raskin J. Doomsday equilibria for omega-regular
games. Information and Computation. 2017;254:296-315. doi:10.1016/j.ic.2016.10.012
apa: Chatterjee, K., Doyen, L., Filiot, E., & Raskin, J. (2017). Doomsday equilibria
for omega-regular games. Information and Computation. Elsevier. https://doi.org/10.1016/j.ic.2016.10.012
chicago: Chatterjee, Krishnendu, Laurent Doyen, Emmanuel Filiot, and Jean Raskin.
“Doomsday Equilibria for Omega-Regular Games.” Information and Computation.
Elsevier, 2017. https://doi.org/10.1016/j.ic.2016.10.012.
ieee: K. Chatterjee, L. Doyen, E. Filiot, and J. Raskin, “Doomsday equilibria for
omega-regular games,” Information and Computation, vol. 254. Elsevier,
pp. 296–315, 2017.
ista: Chatterjee K, Doyen L, Filiot E, Raskin J. 2017. Doomsday equilibria for omega-regular
games. Information and Computation. 254, 296–315.
mla: Chatterjee, Krishnendu, et al. “Doomsday Equilibria for Omega-Regular Games.”
Information and Computation, vol. 254, Elsevier, 2017, pp. 296–315, doi:10.1016/j.ic.2016.10.012.
short: K. Chatterjee, L. Doyen, E. Filiot, J. Raskin, Information and Computation
254 (2017) 296–315.
corr_author: '1'
date_created: 2018-12-11T11:47:53Z
date_published: 2017-06-01T00:00:00Z
date_updated: 2026-04-16T10:00:03Z
day: '01'
department:
- _id: KrCh
doi: 10.1016/j.ic.2016.10.012
ec_funded: 1
external_id:
arxiv:
- '1311.3238'
isi:
- '000402025600008'
intvolume: ' 254'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1311.3238
month: '06'
oa: 1
oa_version: Submitted Version
page: 296 - 315
project:
- _id: 2584A770-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: P 23499-N23
name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11407
name: Game Theory
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 25681D80-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '291734'
name: International IST Postdoc Fellowship Programme
publication: Information and Computation
publication_identifier:
issn:
- 0890-5401
publication_status: published
publisher: Elsevier
publist_id: '7036'
quality_controlled: '1'
related_material:
record:
- id: '10885'
relation: earlier_version
status: public
scopus_import: '1'
status: public
title: Doomsday equilibria for omega-regular games
type: journal_article
user_id: ba8df636-2132-11f1-aed0-ed93e2281fdd
volume: 254
year: '2017'
...
---
_id: '11758'
article_processing_charge: No
article_type: letter_note
author:
- first_name: Luca
full_name: Aceto, Luca
last_name: Aceto
- first_name: Monika H
full_name: Henzinger, Monika H
id: 540c9bbd-f2de-11ec-812d-d04a5be85630
last_name: Henzinger
orcid: 0000-0002-5008-6530
- first_name: Jiří
full_name: Sgall, Jiří
last_name: Sgall
citation:
ama: Aceto L, Henzinger M, Sgall J. 38th International Colloquium on Automata, Languages
and Programming. Information and Computation. 2013;222(1):1. doi:10.1016/j.ic.2012.11.002
apa: Aceto, L., Henzinger, M., & Sgall, J. (2013). 38th International Colloquium
on Automata, Languages and Programming. Information and Computation. Elsevier.
https://doi.org/10.1016/j.ic.2012.11.002
chicago: Aceto, Luca, Monika Henzinger, and Jiří Sgall. “38th International Colloquium
on Automata, Languages and Programming.” Information and Computation. Elsevier,
2013. https://doi.org/10.1016/j.ic.2012.11.002.
ieee: L. Aceto, M. Henzinger, and J. Sgall, “38th International Colloquium on Automata,
Languages and Programming,” Information and Computation, vol. 222, no.
1. Elsevier, p. 1, 2013.
ista: Aceto L, Henzinger M, Sgall J. 2013. 38th International Colloquium on Automata,
Languages and Programming. Information and Computation. 222(1), 1.
mla: Aceto, Luca, et al. “38th International Colloquium on Automata, Languages and
Programming.” Information and Computation, vol. 222, no. 1, Elsevier, 2013,
p. 1, doi:10.1016/j.ic.2012.11.002.
short: L. Aceto, M. Henzinger, J. Sgall, Information and Computation 222 (2013)
1.
date_created: 2022-08-08T11:25:34Z
date_published: 2013-01-01T00:00:00Z
date_updated: 2024-11-06T12:01:32Z
day: '01'
doi: 10.1016/j.ic.2012.11.002
extern: '1'
intvolume: ' 222'
issue: '1'
language:
- iso: eng
month: '01'
oa_version: None
page: '1'
publication: Information and Computation
publication_identifier:
issn:
- 0890-5401
publication_status: published
publisher: Elsevier
quality_controlled: '1'
scopus_import: '1'
status: public
title: 38th International Colloquium on Automata, Languages and Programming
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 222
year: '2013'
...
---
OA_place: publisher
OA_type: free access
_id: '4556'
abstract:
- lang: eng
text: We study the problem of determining stack boundedness and the exact maximum
stack size for three classes of interrupt-driven programs. Interrupt-driven programs
are used in many real-time applications that require responsive interrupt handling.
In order to ensure responsiveness, programmers often enable interrupt processing
in the body of lower-priority interrupt handlers. In such programs a programming
error can allow interrupt handlers to be interrupted in a cyclic fashion to lead
to an unbounded stack, causing the system to crash. For a restricted class of
interrupt-driven programs, we show that there is a polynomial-time procedure to
check stack boundedness, while determining the exact maximum stack size is PSPACE-complete.
For a larger class of programs, the two problems are both PSPACE-complete, and
for the largest class of programs we consider, the two problems are PSPACE-hard
and can be solved in exponential time. While the complexities are high, our algorithms
are exponential only in the number of handlers, and polynomial in the size of
the program.
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: Di
full_name: Ma, Di
last_name: Ma
- first_name: Ritankar
full_name: Majumdar, Ritankar
last_name: Majumdar
- first_name: Tian
full_name: Zhao, Tian
last_name: Zhao
- 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: Jens
full_name: Palsberg, Jens
last_name: Palsberg
citation:
ama: Chatterjee K, Ma D, Majumdar R, Zhao T, Henzinger TA, Palsberg J. Stack size
analysis for interrupt-driven programs. Information and Computation. 2004;194(2):144-174.
doi:10.1016/j.ic.2004.06.001
apa: Chatterjee, K., Ma, D., Majumdar, R., Zhao, T., Henzinger, T. A., & Palsberg,
J. (2004). Stack size analysis for interrupt-driven programs. Information and
Computation. Elsevier. https://doi.org/10.1016/j.ic.2004.06.001
chicago: Chatterjee, Krishnendu, Di Ma, Ritankar Majumdar, Tian Zhao, Thomas A Henzinger,
and Jens Palsberg. “Stack Size Analysis for Interrupt-Driven Programs.” Information
and Computation. Elsevier, 2004. https://doi.org/10.1016/j.ic.2004.06.001.
ieee: K. Chatterjee, D. Ma, R. Majumdar, T. Zhao, T. A. Henzinger, and J. Palsberg,
“Stack size analysis for interrupt-driven programs,” Information and Computation,
vol. 194, no. 2. Elsevier, pp. 144–174, 2004.
ista: Chatterjee K, Ma D, Majumdar R, Zhao T, Henzinger TA, Palsberg J. 2004. Stack
size analysis for interrupt-driven programs. Information and Computation. 194(2),
144–174.
mla: Chatterjee, Krishnendu, et al. “Stack Size Analysis for Interrupt-Driven Programs.”
Information and Computation, vol. 194, no. 2, Elsevier, 2004, pp. 144–74,
doi:10.1016/j.ic.2004.06.001.
short: K. Chatterjee, D. Ma, R. Majumdar, T. Zhao, T.A. Henzinger, J. Palsberg,
Information and Computation 194 (2004) 144–174.
date_created: 2018-12-11T12:09:28Z
date_published: 2004-11-01T00:00:00Z
date_updated: 2026-05-29T09:10:28Z
day: '01'
doi: 10.1016/j.ic.2004.06.001
extern: '1'
intvolume: ' 194'
issue: '2'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.1016/j.ic.2004.06.001
month: '11'
oa: 1
oa_version: Accepted Version
page: 144 - 174
publication: Information and Computation
publication_identifier:
eissn:
- 1090-2651
issn:
- 0890-5401
publication_status: published
publisher: Elsevier
publist_id: '156'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Stack size analysis for interrupt-driven programs
type: journal_article
user_id: ba8df636-2132-11f1-aed0-ed93e2281fdd
volume: 194
year: '2004'
...
---
_id: '4474'
abstract:
- lang: eng
text: 'The simulation preorder for labeled transition systems is defined locally,
and operationally, as a game that relates states with their immediate successor
states. Simulation enjoys many appealing properties. First, simulation has a denotational
characterization: system S simulates system I iff every computation tree embedded
in the unrolling of I can be embedded also in the unrolling of S. Second, simulation
has a logical characterization: S simulates I iff every universal branching-time
formula satisfied by S is satisfied also by I. It follows that simulation is a
suitable notion of implementation, and it is the coarsest abstraction of a system
that preserves universal branching-time properties. Third, based on its local
definition, simulation between finite-state systems can be checked in polynomial
time. Finally, simulation implies trace containment, which cannot be defined locally
and requires polynomial space for verification. Hence simulation is widely used
both in manual and in automatic verification. Liveness assumptions about transition
systems are typically modeled using fairness constraints. Existing notions of
simulation for fair transition systems, however, are not local, and as a result,
many appealing properties of the simulation preorder are lost. We propose a new
view of fair simulation by extending the local definition of simulation to account
for fairness: system View the MathML sourcefairly simulates system View the MathML
source iff in the simulation game, there is a strategy that matches with each
fair computation of View the MathML source a fair computation of View the MathML
source. Our definition enjoys a denotational characterization and has a logical
characterization: View the MathML source fairly simulates View the MathML source
iff every fair computation tree (whose infinite paths are fair) embedded in the
unrolling of View the MathML source can be embedded also in the unrolling of View
the MathML source or, equivalently, iff every Fair-∀AFMC formula satisfied by
View the MathML source is satisfied also by View the MathML source (∀AFMC is the
universal fragment of the alternation-free μ-calculus). The locality of the definition
leads us to a polynomial-time algorithm for checking fair simulation for finite-state
systems with weak and strong fairness constraints. Finally, fair simulation implies
fair trace containment and is therefore useful as an efficiently computable local
criterion for proving linear-time abstraction hierarchies of fair systems.'
acknowledgement: We thank Ramin Hojati, Doron Bustan, and the anonymous reviewers
for their comments on this paper.
article_processing_charge: No
article_type: original
author:
- 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: Orna
full_name: Kupferman, Orna
last_name: Kupferman
- first_name: Sriram
full_name: Rajamani, Sriram
last_name: Rajamani
citation:
ama: Henzinger TA, Kupferman O, Rajamani S. Fair simulation. Information and
Computation. 2002;173(1):64-81. doi:10.1006/inco.2001.3085
apa: Henzinger, T. A., Kupferman, O., & Rajamani, S. (2002). Fair simulation.
Information and Computation. Elsevier. https://doi.org/10.1006/inco.2001.3085
chicago: Henzinger, Thomas A, Orna Kupferman, and Sriram Rajamani. “Fair Simulation.”
Information and Computation. Elsevier, 2002. https://doi.org/10.1006/inco.2001.3085.
ieee: T. A. Henzinger, O. Kupferman, and S. Rajamani, “Fair simulation,” Information
and Computation, vol. 173, no. 1. Elsevier, pp. 64–81, 2002.
ista: Henzinger TA, Kupferman O, Rajamani S. 2002. Fair simulation. Information
and Computation. 173(1), 64–81.
mla: Henzinger, Thomas A., et al. “Fair Simulation.” Information and Computation,
vol. 173, no. 1, Elsevier, 2002, pp. 64–81, doi:10.1006/inco.2001.3085.
short: T.A. Henzinger, O. Kupferman, S. Rajamani, Information and Computation 173
(2002) 64–81.
date_created: 2018-12-11T12:09:02Z
date_published: 2002-02-25T00:00:00Z
date_updated: 2023-06-05T07:53:27Z
day: '25'
doi: 10.1006/inco.2001.3085
extern: '1'
intvolume: ' 173'
issue: '1'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://www.sciencedirect.com/science/article/pii/S0890540101930858?via%3Dihub
month: '02'
oa: 1
oa_version: Published Version
page: 64 - 81
publication: Information and Computation
publication_identifier:
issn:
- 0890-5401
publication_status: published
publisher: Elsevier
publist_id: '255'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Fair simulation
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 173
year: '2002'
...
---
_id: '4501'
abstract:
- lang: eng
text: 'We extend the specification language of temporal logic, the corresponding
verification framework, and the underlying computational model to deal with real-;time
properties of reactive systems. The abstract notion of timed transition systems
generalizes traditional transition systems conservatively: qualitative fairness
requirements are replaced (and superseded) by quantitative lower-bound and upper-bound
timing constraints on transitions. This framework can model real-time systems
that communicate either through shared variables or by message passing and real-time
issues such as timeouts, process priorities (interrupts), and process scheduling.
We exhibit two styles for the specification of real-time systems. While the first
approach uses time-bounded versions of the temporal operators, the second approach
allows explicit references to time through a special clock variable. Corresponding
to the two styles of specification, we present and compare two different proof
methodologies for the verification of timing requirements that are expressed in
these styles. For the bounded-operator style, we provide a set of proof rules
for establishing bounded-invariance and bounded-responce properties of timed transition
systems. This approach generalizes the standard temporal proof rules for verifying
invariance and response properties conservatively. For the explicit-clock style,
we exploit the observation that every time-bounded property is a safety property
and use the standard temporal proof rules for establishing safety properties.'
acknowledgement: 'This research was supported in part by an IBM graduate fellowship,
by the National Science Foundation under Grants CCR-9223226 and CCR-9200794. by
the Defense Advanced Research Projects Agency under Contract N00039-84-C-0211. by
the United States Air Force OMee of Scientific Research under Contracts F49620-93-141139
and F4962043-1-0056. and by the European Community ESPRIT Basic Research Action
Project 6021 (REACT). A preliminary version of Part 1 of this paper appeared in
the proceedings of the 1991 REX Workshop on Real Time Theory In Prate [HMP92a I
a preliminary version of Part II appeared in the proceedings of the 1991 ACM Symposium
on Principles of Programming Languages RIMP911. '
article_processing_charge: No
article_type: original
author:
- 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: Zohar
full_name: Manna, Zohar
last_name: Manna
- first_name: Amir
full_name: Pnueli, Amir
last_name: Pnueli
citation:
ama: Henzinger TA, Manna Z, Pnueli A. Temporal proof methodologies for timed transition
systems. Information and Computation. 1994;112(2):273-337. doi:10.1006/inco.1994.1060
apa: Henzinger, T. A., Manna, Z., & Pnueli, A. (1994). Temporal proof methodologies
for timed transition systems. Information and Computation. Elsevier. https://doi.org/10.1006/inco.1994.1060
chicago: Henzinger, Thomas A, Zohar Manna, and Amir Pnueli. “Temporal Proof Methodologies
for Timed Transition Systems.” Information and Computation. Elsevier, 1994.
https://doi.org/10.1006/inco.1994.1060.
ieee: T. A. Henzinger, Z. Manna, and A. Pnueli, “Temporal proof methodologies for
timed transition systems,” Information and Computation, vol. 112, no. 2.
Elsevier, pp. 273–337, 1994.
ista: Henzinger TA, Manna Z, Pnueli A. 1994. Temporal proof methodologies for timed
transition systems. Information and Computation. 112(2), 273–337.
mla: Henzinger, Thomas A., et al. “Temporal Proof Methodologies for Timed Transition
Systems.” Information and Computation, vol. 112, no. 2, Elsevier, 1994,
pp. 273–337, doi:10.1006/inco.1994.1060.
short: T.A. Henzinger, Z. Manna, A. Pnueli, Information and Computation 112 (1994)
273–337.
date_created: 2018-12-11T12:09:10Z
date_published: 1994-08-01T00:00:00Z
date_updated: 2022-06-02T09:24:58Z
day: '01'
doi: 10.1006/inco.1994.1060
extern: '1'
intvolume: ' 112'
issue: '2'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://www.sciencedirect.com/science/article/pii/S0890540184710601?via%3Dihub
month: '08'
oa: 1
oa_version: None
page: 273 - 337
publication: Information and Computation
publication_identifier:
issn:
- 0890-5401
publication_status: published
publisher: Elsevier
publist_id: '227'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Temporal proof methodologies for timed transition systems
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 112
year: '1994'
...
---
_id: '4503'
abstract:
- lang: eng
text: 'We describe finite-state programs over real-numbered time in a guarded-command
language with real-valued clocks or, equivalently, as finite automata with real-valued
clocks. Model checking answers the question which states of a real-time program
satisfy a branching-time specification (given in an extension of CTL with clock
variables). We develop an algorithm that computes this set of states symbolically
as a fixpoint of a functional on state predicates, without constructing the state
space. For this purpose, we introduce a μ-calculus on computation trees over real-numbered
time. Unfortunately, many standard program properties, such as response for all
nonzeno execution sequences (during which time diverges), cannot be characterized
by fixpoints: we show that the expressiveness of the timed μ-calculus is incomparable
to the expressiveness of timed CTL. Fortunately, this result does not impair the
symbolic verification of "implementable" real-time programs-those whose
safety constraints are machine-closed with respect to diverging time and whose
fairness constraints are restricted to finite upper bounds on clock values. All
timed CTL properties of such programs are shown to be computable as finitely approximable
fixpoints in a simple decidable theory.'
acknowledgement: We thank Peter Kopke for a careful reading.
article_processing_charge: No
article_type: original
author:
- 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: Xavier
full_name: Nicollin, Xavier
last_name: Nicollin
- first_name: Joseph
full_name: Sifakis, Joseph
last_name: Sifakis
- first_name: Sergio
full_name: Yovine, Sergio
last_name: Yovine
citation:
ama: Henzinger TA, Nicollin X, Sifakis J, Yovine S. Symbolic model checking for
real-time systems. Information and Computation. 1994;111(2):193-244. doi:10.1006/inco.1994.1045
apa: Henzinger, T. A., Nicollin, X., Sifakis, J., & Yovine, S. (1994). Symbolic
model checking for real-time systems. Information and Computation. Elsevier.
https://doi.org/10.1006/inco.1994.1045
chicago: Henzinger, Thomas A, Xavier Nicollin, Joseph Sifakis, and Sergio Yovine.
“Symbolic Model Checking for Real-Time Systems.” Information and Computation.
Elsevier, 1994. https://doi.org/10.1006/inco.1994.1045.
ieee: T. A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine, “Symbolic model checking
for real-time systems,” Information and Computation, vol. 111, no. 2. Elsevier,
pp. 193–244, 1994.
ista: Henzinger TA, Nicollin X, Sifakis J, Yovine S. 1994. Symbolic model checking
for real-time systems. Information and Computation. 111(2), 193–244.
mla: Henzinger, Thomas A., et al. “Symbolic Model Checking for Real-Time Systems.”
Information and Computation, vol. 111, no. 2, Elsevier, 1994, pp. 193–244,
doi:10.1006/inco.1994.1045.
short: T.A. Henzinger, X. Nicollin, J. Sifakis, S. Yovine, Information and Computation
111 (1994) 193–244.
date_created: 2018-12-11T12:09:11Z
date_published: 1994-06-01T00:00:00Z
date_updated: 2022-06-02T09:02:02Z
day: '01'
doi: 10.1006/inco.1994.1045
extern: '1'
intvolume: ' 111'
issue: '2'
language:
- iso: eng
main_file_link:
- url: https://www.sciencedirect.com/science/article/pii/S0890540184710455?via%3Dihub
month: '06'
oa_version: None
page: 193 - 244
publication: Information and Computation
publication_identifier:
issn:
- 0890-5401
publication_status: published
publisher: Elsevier
publist_id: '226'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Symbolic model checking for real-time systems
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 111
year: '1994'
...