---
_id: '2238'
abstract:
- lang: eng
text: "We study the problem of achieving a given value in Markov decision processes
(MDPs) with several independent discounted reward objectives. We consider a generalised
version of discounted reward objectives, in which the amount of discounting depends
on the states visited and on the objective. This definition extends the usual
definition of discounted reward, and allows to capture the systems in which the
value of different commodities diminish at different and variable rates.\r\n\r\nWe
establish results for two prominent subclasses of the problem, namely state-discount
models where the discount factors are only dependent on the state of the MDP (and
independent of the objective), and reward-discount models where they are only
dependent on the objective (but not on the state of the MDP). For the state-discount
models we use a straightforward reduction to expected total reward and show that
the problem whether a value is achievable can be solved in polynomial time. For
the reward-discount model we show that memory and randomisation of the strategies
are required, but nevertheless that the problem is decidable and it is sufficient
to consider strategies which after a certain number of steps behave in a memoryless
way.\r\n\r\nFor the general case, we show that when restricted to graphs (i.e.
MDPs with no randomisation), pure strategies and discount factors of the form
1/n where n is an integer, the problem is in PSPACE and finite memory suffices
for achieving a given value. We also show that when the discount factors are not
of the form 1/n, the memory required by a strategy can be infinite.\r\n"
alternative_title:
- LNCS
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Vojtěch
full_name: Forejt, Vojtěch
last_name: Forejt
- first_name: Dominik
full_name: Wojtczak, Dominik
last_name: Wojtczak
citation:
ama: Chatterjee K, Forejt V, Wojtczak D. Multi-objective discounted reward verification
in graphs and MDPs. 2013;8312:228-242. doi:10.1007/978-3-642-45221-5_17
apa: 'Chatterjee, K., Forejt, V., & Wojtczak, D. (2013). Multi-objective discounted
reward verification in graphs and MDPs. Presented at the LPAR: Logic for Programming,
Artificial Intelligence, and Reasoning, Stellenbosch, South Africa: Springer.
https://doi.org/10.1007/978-3-642-45221-5_17'
chicago: Chatterjee, Krishnendu, Vojtěch Forejt, and Dominik Wojtczak. “Multi-Objective
Discounted Reward Verification in Graphs and MDPs.” Lecture Notes in Computer
Science. Springer, 2013. https://doi.org/10.1007/978-3-642-45221-5_17.
ieee: K. Chatterjee, V. Forejt, and D. Wojtczak, “Multi-objective discounted reward
verification in graphs and MDPs,” vol. 8312. Springer, pp. 228–242, 2013.
ista: Chatterjee K, Forejt V, Wojtczak D. 2013. Multi-objective discounted reward
verification in graphs and MDPs. 8312, 228–242.
mla: Chatterjee, Krishnendu, et al. Multi-Objective Discounted Reward Verification
in Graphs and MDPs. Vol. 8312, Springer, 2013, pp. 228–42, doi:10.1007/978-3-642-45221-5_17.
short: K. Chatterjee, V. Forejt, D. Wojtczak, 8312 (2013) 228–242.
conference:
end_date: 2013-12-19
location: Stellenbosch, South Africa
name: 'LPAR: Logic for Programming, Artificial Intelligence, and Reasoning'
start_date: 2013-12-14
date_created: 2018-12-11T11:56:30Z
date_published: 2013-12-01T00:00:00Z
date_updated: 2020-08-11T10:09:42Z
day: '01'
department:
- _id: KrCh
doi: 10.1007/978-3-642-45221-5_17
ec_funded: 1
intvolume: ' 8312'
language:
- iso: eng
month: '12'
oa_version: None
page: 228 - 242
project:
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
publication_status: published
publisher: Springer
publist_id: '4723'
quality_controlled: '1'
scopus_import: 1
series_title: Lecture Notes in Computer Science
status: public
title: Multi-objective discounted reward verification in graphs and MDPs
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 8312
year: '2013'
...
---
_id: '2247'
abstract:
- lang: eng
text: Cooperative behavior, where one individual incurs a cost to help another,
is a wide spread phenomenon. Here we study direct reciprocity in the context of
the alternating Prisoner's Dilemma. We consider all strategies that can be implemented
by one and two-state automata. We calculate the payoff matrix of all pairwise
encounters in the presence of noise. We explore deterministic selection dynamics
with and without mutation. Using different error rates and payoff values, we observe
convergence to a small number of distinct equilibria. Two of them are uncooperative
strict Nash equilibria representing always-defect (ALLD) and Grim. The third equilibrium
is mixed and represents a cooperative alliance of several strategies, dominated
by a strategy which we call Forgiver. Forgiver cooperates whenever the opponent
has cooperated; it defects once when the opponent has defected, but subsequently
Forgiver attempts to re-establish cooperation even if the opponent has defected
again. Forgiver is not an evolutionarily stable strategy, but the alliance, which
it rules, is asymptotically stable. For a wide range of parameter values the most
commonly observed outcome is convergence to the mixed equilibrium, dominated by
Forgiver. Our results show that although forgiving might incur a short-term loss
it can lead to a long-term gain. Forgiveness facilitates stable cooperation in
the presence of exploitation and noise.
article_number: e80814
article_processing_charge: No
author:
- first_name: Benjamin
full_name: Zagorsky, Benjamin
last_name: Zagorsky
- first_name: Johannes
full_name: Reiter, Johannes
id: 4A918E98-F248-11E8-B48F-1D18A9856A87
last_name: Reiter
orcid: 0000-0002-0170-7353
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Martin
full_name: Nowak, Martin
last_name: Nowak
citation:
ama: Zagorsky B, Reiter J, Chatterjee K, Nowak M. Forgiver triumphs in alternating
prisoner’s dilemma . PLoS One. 2013;8(12). doi:10.1371/journal.pone.0080814
apa: Zagorsky, B., Reiter, J., Chatterjee, K., & Nowak, M. (2013). Forgiver
triumphs in alternating prisoner’s dilemma . PLoS One. Public Library of
Science. https://doi.org/10.1371/journal.pone.0080814
chicago: Zagorsky, Benjamin, Johannes Reiter, Krishnendu Chatterjee, and Martin
Nowak. “Forgiver Triumphs in Alternating Prisoner’s Dilemma .” PLoS One.
Public Library of Science, 2013. https://doi.org/10.1371/journal.pone.0080814.
ieee: B. Zagorsky, J. Reiter, K. Chatterjee, and M. Nowak, “Forgiver triumphs in
alternating prisoner’s dilemma ,” PLoS One, vol. 8, no. 12. Public Library
of Science, 2013.
ista: Zagorsky B, Reiter J, Chatterjee K, Nowak M. 2013. Forgiver triumphs in alternating
prisoner’s dilemma . PLoS One. 8(12), e80814.
mla: Zagorsky, Benjamin, et al. “Forgiver Triumphs in Alternating Prisoner’s Dilemma
.” PLoS One, vol. 8, no. 12, e80814, Public Library of Science, 2013, doi:10.1371/journal.pone.0080814.
short: B. Zagorsky, J. Reiter, K. Chatterjee, M. Nowak, PLoS One 8 (2013).
date_created: 2018-12-11T11:56:33Z
date_published: 2013-12-12T00:00:00Z
date_updated: 2026-04-09T14:26:23Z
day: '12'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1371/journal.pone.0080814
ec_funded: 1
external_id:
isi:
- '000328731800009'
file:
- access_level: open_access
checksum: 808e8b9e6e89658bee4ffbbfac1bd19d
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:11:15Z
date_updated: 2020-07-14T12:45:34Z
file_id: '4868'
file_name: IST-2016-409-v1+1_journal.pone.0080814.pdf
file_size: 1050042
relation: main_file
file_date_updated: 2020-07-14T12:45:34Z
has_accepted_license: '1'
intvolume: ' 8'
isi: 1
issue: '12'
language:
- iso: eng
month: '12'
oa: 1
oa_version: Published Version
project:
- _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: 2584A770-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: P 23499-N23
name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 2587B514-B435-11E9-9278-68D0E5697425
name: Microsoft Research Faculty Fellowship
publication: PLoS One
publication_status: published
publisher: Public Library of Science
publist_id: '4702'
pubrep_id: '409'
quality_controlled: '1'
related_material:
record:
- id: '9749'
relation: research_data
status: public
- id: '1400'
relation: dissertation_contains
status: public
scopus_import: '1'
status: public
title: 'Forgiver triumphs in alternating prisoner''s dilemma '
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: 8
year: '2013'
...
---
_id: '2279'
abstract:
- lang: eng
text: We consider two-player games played on weighted directed graphs with mean-payoff
and total-payoff objectives, two classical quantitative objectives. While for
single-dimensional games the complexity and memory bounds for both objectives
coincide, we show that in contrast to multi-dimensional mean-payoff games that
are known to be coNP-complete, multi-dimensional total-payoff games are undecidable.
We introduce conservative approximations of these objectives, where the payoff
is considered over a local finite window sliding along a play, instead of the
whole play. For single dimension, we show that (i) if the window size is polynomial,
deciding the winner takes polynomial time, and (ii) the existence of a bounded
window can be decided in NP ∩ coNP, and is at least as hard as solving mean-payoff
games. For multiple dimensions, we show that (i) the problem with fixed window
size is EXPTIME-complete, and (ii) there is no primitive-recursive algorithm to
decide the existence of a bounded window.
acknowledgement: 279307; ERC; Fonds National de la Reserche Luxembourg; 279499; ERC;
Fonds National de la Reserche Luxembourg
alternative_title:
- LNCS
article_processing_charge: No
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: Mickael
full_name: Randour, Mickael
last_name: Randour
- first_name: Jean
full_name: Raskin, Jean
last_name: Raskin
citation:
ama: Chatterjee K, Doyen L, Randour M, Raskin J. Looking at mean-payoff and total-payoff
through windows. 2013;8172:118-132. doi:10.1007/978-3-319-02444-8_10
apa: 'Chatterjee, K., Doyen, L., Randour, M., & Raskin, J. (2013). Looking at
mean-payoff and total-payoff through windows. Presented at the ATVA: Automated
Technology for Verification and Analysis, Hanoi, Vietnam: Springer. https://doi.org/10.1007/978-3-319-02444-8_10'
chicago: Chatterjee, Krishnendu, Laurent Doyen, Mickael Randour, and Jean Raskin.
“Looking at Mean-Payoff and Total-Payoff through Windows.” Lecture Notes in Computer
Science. Springer, 2013. https://doi.org/10.1007/978-3-319-02444-8_10.
ieee: K. Chatterjee, L. Doyen, M. Randour, and J. Raskin, “Looking at mean-payoff
and total-payoff through windows,” vol. 8172. Springer, pp. 118–132, 2013.
ista: Chatterjee K, Doyen L, Randour M, Raskin J. 2013. Looking at mean-payoff and
total-payoff through windows. 8172, 118–132.
mla: Chatterjee, Krishnendu, et al. Looking at Mean-Payoff and Total-Payoff through
Windows. Vol. 8172, Springer, 2013, pp. 118–32, doi:10.1007/978-3-319-02444-8_10.
short: K. Chatterjee, L. Doyen, M. Randour, J. Raskin, 8172 (2013) 118–132.
conference:
end_date: 2013-10-18
location: Hanoi, Vietnam
name: 'ATVA: Automated Technology for Verification and Analysis'
start_date: 2013-10-15
date_created: 2018-12-11T11:56:44Z
date_published: 2013-01-01T00:00:00Z
date_updated: 2025-09-23T09:29:54Z
day: '01'
department:
- _id: KrCh
doi: 10.1007/978-3-319-02444-8_10
ec_funded: 1
external_id:
arxiv:
- '1302.4248'
intvolume: ' 8172'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1302.4248
month: '01'
oa: 1
oa_version: Preprint
page: 118 - 132
project:
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
publication_status: published
publisher: Springer
publist_id: '4656'
quality_controlled: '1'
related_material:
record:
- id: '523'
relation: later_version
status: public
scopus_import: '1'
series_title: Lecture Notes in Computer Science
status: public
title: Looking at mean-payoff and total-payoff through windows
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 8172
year: '2013'
...
---
_id: '2292'
abstract:
- lang: eng
text: This book constitutes the thoroughly refereed conference proceedings of the
38th International Symposium on Mathematical Foundations of Computer Science,
MFCS 2013, held in Klosterneuburg, Austria, in August 2013. The 67 revised full
papers presented together with six invited talks were carefully selected from
191 submissions. Topics covered include algorithmic game theory, algorithmic learning
theory, algorithms and data structures, automata, formal languages, bioinformatics,
complexity, computational geometry, computer-assisted reasoning, concurrency theory,
databases and knowledge-based systems, foundations of computing, logic in computer
science, models of computation, semantics and verification of programs, and theoretical
issues in artificial intelligence.
alternative_title:
- LNCS
citation:
ama: Chatterjee K, Sgall J, eds. Mathematical Foundations of Computer Science
2013. Vol 8087. Springer; 2013:VI-854. doi:10.1007/978-3-642-40313-2
apa: 'Chatterjee, K., & Sgall, J. (Eds.). (2013). Mathematical Foundations
of Computer Science 2013 (Vol. 8087, p. VI-854). Presented at the MFCS: Mathematical
Foundations of Computer Science, Klosterneuburg, Austria: Springer. https://doi.org/10.1007/978-3-642-40313-2'
chicago: Chatterjee, Krishnendu, and Jiri Sgall, eds. Mathematical Foundations
of Computer Science 2013. Vol. 8087. Lecture Notes in Computer Science. Springer,
2013. https://doi.org/10.1007/978-3-642-40313-2.
ieee: K. Chatterjee and J. Sgall, Eds., Mathematical Foundations of Computer
Science 2013, vol. 8087. Springer, 2013, p. VI-854.
ista: Chatterjee K, Sgall J eds. 2013. Mathematical Foundations of Computer Science
2013, Springer,p.
mla: Chatterjee, Krishnendu, and Jiri Sgall, editors. Mathematical Foundations
of Computer Science 2013. Vol. 8087, Springer, 2013, p. VI-854, doi:10.1007/978-3-642-40313-2.
short: K. Chatterjee, J. Sgall, eds., Mathematical Foundations of Computer Science
2013, Springer, 2013.
conference:
end_date: 2013-08-30
location: Klosterneuburg, Austria
name: 'MFCS: Mathematical Foundations of Computer Science'
start_date: 2013-08-26
date_created: 2018-12-11T11:56:48Z
date_published: 2013-08-08T00:00:00Z
date_updated: 2020-08-11T10:09:45Z
day: '08'
department:
- _id: KrCh
doi: 10.1007/978-3-642-40313-2
editor:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Jiri
full_name: Sgall, Jiri
last_name: Sgall
intvolume: ' 8087'
language:
- iso: eng
month: '08'
oa_version: None
page: VI - 854
publication_identifier:
isbn:
- 978-3-642-40312-5
publication_status: published
publisher: Springer
publist_id: '4636'
quality_controlled: '1'
scopus_import: 1
series_title: Lecture Notes in Computer Science
status: public
title: Mathematical Foundations of Computer Science 2013
type: conference_editor
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 8087
year: '2013'
...
---
_id: '2295'
abstract:
- lang: eng
text: We consider partially observable Markov decision processes (POMDPs) with ω-regular
conditions specified as parity objectives. The qualitative analysis problem given
a POMDP and a parity objective asks whether there is a strategy to ensure that
the objective is satisfied with probability 1 (resp. positive probability). While
the qualitative analysis problems are known to be undecidable even for very special
cases of parity objectives, we establish decidability (with optimal EXPTIME-complete
complexity) of the qualitative analysis problems for POMDPs with all parity objectives
under finite-memory strategies. We also establish asymptotically optimal (exponential)
memory bounds.
alternative_title:
- LIPIcs
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Martin
full_name: Chmelik, Martin
id: 3624234E-F248-11E8-B48F-1D18A9856A87
last_name: Chmelik
- first_name: Mathieu
full_name: Tracol, Mathieu
id: 3F54FA38-F248-11E8-B48F-1D18A9856A87
last_name: Tracol
citation:
ama: Chatterjee K, Chmelik M, Tracol M. What is decidable about partially observable
Markov decision processes with omega-regular objectives. 2013;23:165-180. doi:10.4230/LIPIcs.CSL.2013.165
apa: 'Chatterjee, K., Chmelik, M., & Tracol, M. (2013). What is decidable about
partially observable Markov decision processes with omega-regular objectives.
Presented at the CSL: Computer Science Logic, Torino, Italy: Schloss Dagstuhl
- Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CSL.2013.165'
chicago: Chatterjee, Krishnendu, Martin Chmelik, and Mathieu Tracol. “What Is Decidable
about Partially Observable Markov Decision Processes with Omega-Regular Objectives.”
Leibniz International Proceedings in Informatics. Schloss Dagstuhl - Leibniz-Zentrum
für Informatik, 2013. https://doi.org/10.4230/LIPIcs.CSL.2013.165.
ieee: K. Chatterjee, M. Chmelik, and M. Tracol, “What is decidable about partially
observable Markov decision processes with omega-regular objectives,” vol. 23.
Schloss Dagstuhl - Leibniz-Zentrum für Informatik, pp. 165–180, 2013.
ista: Chatterjee K, Chmelik M, Tracol M. 2013. What is decidable about partially
observable Markov decision processes with omega-regular objectives. 23, 165–180.
mla: Chatterjee, Krishnendu, et al. What Is Decidable about Partially Observable
Markov Decision Processes with Omega-Regular Objectives. Vol. 23, Schloss
Dagstuhl - Leibniz-Zentrum für Informatik, 2013, pp. 165–80, doi:10.4230/LIPIcs.CSL.2013.165.
short: K. Chatterjee, M. Chmelik, M. Tracol, 23 (2013) 165–180.
conference:
end_date: 2013-09-05
location: Torino, Italy
name: 'CSL: Computer Science Logic'
start_date: 2013-09-02
date_created: 2018-12-11T11:56:50Z
date_published: 2013-08-27T00:00:00Z
date_updated: 2025-09-18T11:38:38Z
day: '27'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.4230/LIPIcs.CSL.2013.165
ec_funded: 1
file:
- access_level: open_access
checksum: ba2828322955574d9283bea0e17a37a6
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:09:42Z
date_updated: 2020-07-14T12:45:37Z
file_id: '4766'
file_name: IST-2017-756-v1+1_2.pdf
file_size: 345171
relation: main_file
file_date_updated: 2020-07-14T12:45:37Z
has_accepted_license: '1'
intvolume: ' 23'
language:
- iso: eng
month: '08'
oa: 1
oa_version: Published Version
page: 165 - 180
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: 2587B514-B435-11E9-9278-68D0E5697425
name: Microsoft Research Faculty Fellowship
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '4633'
pubrep_id: '756'
quality_controlled: '1'
related_material:
record:
- id: '5400'
relation: earlier_version
status: public
- id: '1477'
relation: later_version
status: public
scopus_import: 1
series_title: Leibniz International Proceedings in Informatics
status: public
title: What is decidable about partially observable Markov decision processes with
omega-regular objectives
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: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 23
year: '2013'
...
---
_id: '2299'
abstract:
- lang: eng
text: 'The standard hardware design flow involves: (a) design of an integrated circuit
using a hardware description language, (b) extensive functional and formal verification,
and (c) logical synthesis. However, the above-mentioned processes consume significant
effort and time. An alternative approach is to use a formal specification language
as a high-level hardware description language and synthesize hardware from formal
specifications. Our work is a case study of the synthesis of the widely and industrially
used AMBA AHB protocol from formal specifications. Bloem et al. presented the
first formal specifications for the AMBA AHB Arbiter and synthesized the AHB Arbiter
circuit. However, in the first formal specification some important assumptions
were missing. Our contributions are as follows: (a) We present detailed formal
specifications for the AHB Arbiter incorporating the missing details, and obtain
significant improvements in the synthesis results (both with respect to the number
of gates in the synthesized circuit and with respect to the time taken to synthesize
the circuit), and (b) we present formal specifications to generate compact circuits
for the remaining two main components of AMBA AHB, namely, AHB Master and AHB
Slave. Thus with systematic description we are able to automatically and completely
synthesize an important and widely used industrial protocol.'
author:
- first_name: Yashdeep
full_name: Godhal, Yashdeep
id: 5B547124-EB61-11E9-8887-89D9C04DBDF5
last_name: Godhal
- 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: 'Godhal Y, Chatterjee K, Henzinger TA. Synthesis of AMBA AHB from formal specification:
A case study. International Journal on Software Tools for Technology Transfer.
2013;15(5-6):585-601. doi:10.1007/s10009-011-0207-9'
apa: 'Godhal, Y., Chatterjee, K., & Henzinger, T. A. (2013). Synthesis of AMBA
AHB from formal specification: A case study. International Journal on Software
Tools for Technology Transfer. Springer. https://doi.org/10.1007/s10009-011-0207-9'
chicago: 'Godhal, Yashdeep, Krishnendu Chatterjee, and Thomas A Henzinger. “Synthesis
of AMBA AHB from Formal Specification: A Case Study.” International Journal
on Software Tools for Technology Transfer. Springer, 2013. https://doi.org/10.1007/s10009-011-0207-9.'
ieee: 'Y. Godhal, K. Chatterjee, and T. A. Henzinger, “Synthesis of AMBA AHB from
formal specification: A case study,” International Journal on Software Tools
for Technology Transfer, vol. 15, no. 5–6. Springer, pp. 585–601, 2013.'
ista: 'Godhal Y, Chatterjee K, Henzinger TA. 2013. Synthesis of AMBA AHB from formal
specification: A case study. International Journal on Software Tools for Technology
Transfer. 15(5–6), 585–601.'
mla: 'Godhal, Yashdeep, et al. “Synthesis of AMBA AHB from Formal Specification:
A Case Study.” International Journal on Software Tools for Technology Transfer,
vol. 15, no. 5–6, Springer, 2013, pp. 585–601, doi:10.1007/s10009-011-0207-9.'
short: Y. Godhal, K. Chatterjee, T.A. Henzinger, International Journal on Software
Tools for Technology Transfer 15 (2013) 585–601.
corr_author: '1'
date_created: 2018-12-11T11:56:51Z
date_published: 2013-10-01T00:00:00Z
date_updated: 2024-10-09T20:55:16Z
day: '01'
ddc:
- '000'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1007/s10009-011-0207-9
file:
- access_level: open_access
checksum: 57b06a732dd8d6349190dba6b5b0d33b
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:11:53Z
date_updated: 2020-07-14T12:45:37Z
file_id: '4910'
file_name: IST-2012-87-v1+1_Synthesis_of_AMBA_AHB_from_formal_specifications-_A_case_study.pdf
file_size: 277372
relation: main_file
file_date_updated: 2020-07-14T12:45:37Z
has_accepted_license: '1'
intvolume: ' 15'
issue: 5-6
language:
- iso: eng
month: '10'
oa: 1
oa_version: Submitted Version
page: 585 - 601
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 2587B514-B435-11E9-9278-68D0E5697425
name: Microsoft Research Faculty Fellowship
publication: International Journal on Software Tools for Technology Transfer
publication_status: published
publisher: Springer
publist_id: '4629'
pubrep_id: '87'
quality_controlled: '1'
scopus_import: 1
status: public
title: 'Synthesis of AMBA AHB from formal specification: A case study'
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 15
year: '2013'
...
---
_id: '2305'
abstract:
- lang: eng
text: We study the complexity of central controller synthesis problems for finite-state
Markov decision processes, where the objective is to optimize both the expected
mean-payoff performance of the system and its stability. e argue that the basic
theoretical notion of expressing the stability in terms of the variance of the
mean-payoff (called global variance in our paper) is not always sufficient, since
it ignores possible instabilities on respective runs. For this reason we propose
alernative definitions of stability, which we call local and hybrid variance,
and which express how rewards on each run deviate from the run's own mean-payoff
and from the expected mean-payoff, respectively. We show that a strategy ensuring
both the expected mean-payoff and the variance below given bounds requires randomization
and memory, under all the above semantics of variance. We then look at the problem
of determining whether there is a such a strategy. For the global variance, we
show that the problem is in PSPACE, and that the answer can be approximated in
pseudo-polynomial time. For the hybrid variance, the analogous decision problem
is in NP, and a polynomial-time approximating algorithm also exists. For local
variance, we show that the decision problem is in NP. Since the overall performance
can be traded for stability (and vice versa), we also present algorithms for approximating
the associated Pareto curve in all the three cases. Finally, we study a special
case of the decision problems, where we require a given expected mean-payoff together
with zero variance. Here we show that the problems can be all solved in polynomial
time.
article_processing_charge: No
arxiv: 1
author:
- first_name: Tomáš
full_name: Brázdil, Tomáš
last_name: Brázdil
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Vojtěch
full_name: Forejt, Vojtěch
last_name: Forejt
- first_name: Antonín
full_name: Kučera, Antonín
last_name: Kučera
citation:
ama: 'Brázdil T, Chatterjee K, Forejt V, Kučera A. Trading performance for stability
in Markov decision processes. In: 28th Annual ACM/IEEE Symposium. IEEE;
2013:331-340. doi:10.1109/LICS.2013.39'
apa: 'Brázdil, T., Chatterjee, K., Forejt, V., & Kučera, A. (2013). Trading
performance for stability in Markov decision processes. In 28th Annual ACM/IEEE
Symposium (pp. 331–340). New Orleans, LA, United States: IEEE. https://doi.org/10.1109/LICS.2013.39'
chicago: Brázdil, Tomáš, Krishnendu Chatterjee, Vojtěch Forejt, and Antonín Kučera.
“Trading Performance for Stability in Markov Decision Processes.” In 28th Annual
ACM/IEEE Symposium, 331–40. IEEE, 2013. https://doi.org/10.1109/LICS.2013.39.
ieee: T. Brázdil, K. Chatterjee, V. Forejt, and A. Kučera, “Trading performance
for stability in Markov decision processes,” in 28th Annual ACM/IEEE Symposium,
New Orleans, LA, United States, 2013, pp. 331–340.
ista: 'Brázdil T, Chatterjee K, Forejt V, Kučera A. 2013. Trading performance for
stability in Markov decision processes. 28th Annual ACM/IEEE Symposium. LICS:
Logic in Computer Science, 331–340.'
mla: Brázdil, Tomáš, et al. “Trading Performance for Stability in Markov Decision
Processes.” 28th Annual ACM/IEEE Symposium, IEEE, 2013, pp. 331–40, doi:10.1109/LICS.2013.39.
short: T. Brázdil, K. Chatterjee, V. Forejt, A. Kučera, in:, 28th Annual ACM/IEEE
Symposium, IEEE, 2013, pp. 331–340.
conference:
end_date: 2013-06-28
location: New Orleans, LA, United States
name: 'LICS: Logic in Computer Science'
start_date: 2013-06-25
date_created: 2018-12-11T11:56:53Z
date_published: 2013-08-01T00:00:00Z
date_updated: 2025-09-29T14:16:57Z
day: '01'
department:
- _id: KrCh
doi: 10.1109/LICS.2013.39
ec_funded: 1
external_id:
arxiv:
- '1305.4103'
isi:
- '000326815000038'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1305.4103
month: '08'
oa: 1
oa_version: Preprint
page: 331 - 340
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: 2587B514-B435-11E9-9278-68D0E5697425
name: Microsoft Research Faculty Fellowship
publication: 28th Annual ACM/IEEE Symposium
publication_status: published
publisher: IEEE
publist_id: '4622'
quality_controlled: '1'
related_material:
record:
- id: '1294'
relation: later_version
status: public
scopus_import: '1'
status: public
title: Trading performance for stability in Markov decision processes
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
year: '2013'
...
---
_id: '2329'
abstract:
- lang: eng
text: 'Two-player games on graphs are central in many problems in formal verification
and program analysis such as synthesis and verification of open systems. In this
work, we consider both finite-state game graphs, and recursive game graphs (or
pushdown game graphs) that model the control flow of sequential programs with
recursion. The objectives we study are multidimensional mean-payoff objectives,
where the goal of player 1 is to ensure that the mean-payoff is non-negative in
all dimensions. In pushdown games two types of strategies are relevant: (1) global
strategies, that depend on the entire global history; and (2) modular strategies,
that have only local memory and thus do not depend on the context of invocation.
Our main contributions are as follows: (1) We show that finite-state multidimensional
mean-payoff games can be solved in polynomial time if the number of dimensions
and the maximal absolute value of the weights are fixed; whereas if the number
of dimensions is arbitrary, then the problem is known to be coNP-complete. (2)
We show that pushdown graphs with multidimensional mean-payoff objectives can
be solved in polynomial time. For both (1) and (2) our algorithms are based on
hyperplane separation technique. (3) For pushdown games under global strategies
both one and multidimensional mean-payoff objectives problems are known to be
undecidable, and we show that under modular strategies the multidimensional problem
is also undecidable; under modular strategies the one-dimensional problem is NP-complete.
We show that if the number of modules, the number of exits, and the maximal absolute
value of the weights are fixed, then pushdown games under modular strategies with
one-dimensional mean-payoff objectives can be solved in polynomial time, and if
either the number of exits or the number of modules is unbounded, then the problem
is NP-hard. (4) Finally we show that a fixed parameter tractable algorithm for
finite-state multidimensional mean-payoff games or pushdown games under modular
strategies with one-dimensional mean-payoff objectives would imply the fixed parameter
tractability of parity games.'
alternative_title:
- LNCS
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: Yaron
full_name: Velner, Yaron
last_name: Velner
citation:
ama: Chatterjee K, Velner Y. Hyperplane separation technique for multidimensional
mean-payoff games. 2013;8052:500-515. doi:10.1007/978-3-642-40184-8_35
apa: 'Chatterjee, K., & Velner, Y. (2013). Hyperplane separation technique for
multidimensional mean-payoff games. Presented at the CONCUR: Concurrency Theory,
Buenos Aires, Argentinia: Springer. https://doi.org/10.1007/978-3-642-40184-8_35'
chicago: Chatterjee, Krishnendu, and Yaron Velner. “Hyperplane Separation Technique
for Multidimensional Mean-Payoff Games.” Lecture Notes in Computer Science. Springer,
2013. https://doi.org/10.1007/978-3-642-40184-8_35.
ieee: K. Chatterjee and Y. Velner, “Hyperplane separation technique for multidimensional
mean-payoff games,” vol. 8052. Springer, pp. 500–515, 2013.
ista: Chatterjee K, Velner Y. 2013. Hyperplane separation technique for multidimensional
mean-payoff games. 8052, 500–515.
mla: Chatterjee, Krishnendu, and Yaron Velner. Hyperplane Separation Technique
for Multidimensional Mean-Payoff Games. Vol. 8052, Springer, 2013, pp. 500–15,
doi:10.1007/978-3-642-40184-8_35.
short: K. Chatterjee, Y. Velner, 8052 (2013) 500–515.
conference:
end_date: 2013-08-30
location: Buenos Aires, Argentinia
name: 'CONCUR: Concurrency Theory'
start_date: 2013-08-27
date_created: 2018-12-11T11:57:01Z
date_published: 2013-08-01T00:00:00Z
date_updated: 2025-09-10T11:00:30Z
day: '01'
department:
- _id: KrCh
doi: 10.1007/978-3-642-40184-8_35
ec_funded: 1
external_id:
arxiv:
- '1210.3141'
intvolume: ' 8052'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1210.3141
month: '08'
oa: 1
oa_version: Preprint
page: 500 - 515
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: 2587B514-B435-11E9-9278-68D0E5697425
name: Microsoft Research Faculty Fellowship
publication_status: published
publisher: Springer
publist_id: '4597'
quality_controlled: '1'
related_material:
record:
- id: '717'
relation: later_version
status: public
scopus_import: 1
series_title: Lecture Notes in Computer Science
status: public
title: Hyperplane separation technique for multidimensional mean-payoff games
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 8052
year: '2013'
...
---
_id: '2444'
abstract:
- lang: eng
text: 'We consider two core algorithmic problems for probabilistic verification:
the maximal end-component decomposition and the almost-sure reachability set computation
for Markov decision processes (MDPs). For MDPs with treewidth k, we present two
improved static algorithms for both the problems that run in time O(n·k 2.38·2k
) and O(m·logn· k), respectively, where n is the number of states and m is the
number of edges, significantly improving the previous known O(n·k·√n· k) bound
for low treewidth. We also present decremental algorithms for both problems for
MDPs with constant treewidth that run in amortized logarithmic time, which is
a huge improvement over the previously known algorithms that require amortized
linear time.'
alternative_title:
- LNCS
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: Jakub
full_name: Ła̧Cki, Jakub
last_name: Ła̧Cki
citation:
ama: Chatterjee K, Ła̧Cki J. Faster algorithms for Markov decision processes with
low treewidth. 2013;8044:543-558. doi:10.1007/978-3-642-39799-8_36
apa: 'Chatterjee, K., & Ła̧Cki, J. (2013). Faster algorithms for Markov decision
processes with low treewidth. Presented at the CAV: Computer Aided Verification,
St. Petersburg, Russia: Springer. https://doi.org/10.1007/978-3-642-39799-8_36'
chicago: Chatterjee, Krishnendu, and Jakub Ła̧Cki. “Faster Algorithms for Markov
Decision Processes with Low Treewidth.” Lecture Notes in Computer Science. Springer,
2013. https://doi.org/10.1007/978-3-642-39799-8_36.
ieee: K. Chatterjee and J. Ła̧Cki, “Faster algorithms for Markov decision processes
with low treewidth,” vol. 8044. Springer, pp. 543–558, 2013.
ista: Chatterjee K, Ła̧Cki J. 2013. Faster algorithms for Markov decision processes
with low treewidth. 8044, 543–558.
mla: Chatterjee, Krishnendu, and Jakub Ła̧Cki. Faster Algorithms for Markov Decision
Processes with Low Treewidth. Vol. 8044, Springer, 2013, pp. 543–58, doi:10.1007/978-3-642-39799-8_36.
short: K. Chatterjee, J. Ła̧Cki, 8044 (2013) 543–558.
conference:
end_date: 2013-07-19
location: St. Petersburg, Russia
name: 'CAV: Computer Aided Verification'
start_date: 2013-07-13
date_created: 2018-12-11T11:57:42Z
date_published: 2013-07-01T00:00:00Z
date_updated: 2020-08-11T10:09:47Z
day: '01'
department:
- _id: KrCh
doi: 10.1007/978-3-642-39799-8_36
ec_funded: 1
external_id:
arxiv:
- '1304.0084'
intvolume: ' 8044'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1304.0084
month: '07'
oa: 1
oa_version: Preprint
page: 543 - 558
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: 2587B514-B435-11E9-9278-68D0E5697425
name: Microsoft Research Faculty Fellowship
publication_status: published
publisher: Springer
publist_id: '4459'
quality_controlled: '1'
scopus_import: 1
series_title: Lecture Notes in Computer Science
status: public
title: Faster algorithms for Markov decision processes with low treewidth
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 8044
year: '2013'
...
---
_id: '2446'
abstract:
- lang: eng
text: The model-checking problem for probabilistic systems crucially relies on the
translation of LTL to deterministic Rabin automata (DRW). Our recent Safraless
translation [KE12, GKE12] for the LTL(F,G) fragment produces smaller automata
as compared to the traditional approach. In this work, instead of DRW we consider
deterministic automata with acceptance condition given as disjunction of generalized
Rabin pairs (DGRW). The Safraless translation of LTL(F,G) formulas to DGRW results
in smaller automata as compared to DRW. We present algorithms for probabilistic
model-checking as well as game solving for DGRW conditions. Our new algorithms
lead to improvement both in terms of theoretical bounds as well as practical evaluation.
We compare PRISM with and without our new translation, and show that the new translation
leads to significant improvements.
alternative_title:
- LNCS
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: Andreas
full_name: Gaiser, Andreas
last_name: Gaiser
- first_name: Jan
full_name: Kretinsky, Jan
id: 44CEF464-F248-11E8-B48F-1D18A9856A87
last_name: Kretinsky
orcid: 0000-0002-8122-2881
citation:
ama: Chatterjee K, Gaiser A, Kretinsky J. Automata with generalized Rabin pairs
for probabilistic model checking and LTL synthesis. 2013;8044:559-575. doi:10.1007/978-3-642-39799-8_37
apa: 'Chatterjee, K., Gaiser, A., & Kretinsky, J. (2013). Automata with generalized
Rabin pairs for probabilistic model checking and LTL synthesis. Presented at the
CAV: Computer Aided Verification, St. Petersburg, Russia: Springer. https://doi.org/10.1007/978-3-642-39799-8_37'
chicago: Chatterjee, Krishnendu, Andreas Gaiser, and Jan Kretinsky. “Automata with
Generalized Rabin Pairs for Probabilistic Model Checking and LTL Synthesis.” Lecture
Notes in Computer Science. Springer, 2013. https://doi.org/10.1007/978-3-642-39799-8_37.
ieee: K. Chatterjee, A. Gaiser, and J. Kretinsky, “Automata with generalized Rabin
pairs for probabilistic model checking and LTL synthesis,” vol. 8044. Springer,
pp. 559–575, 2013.
ista: Chatterjee K, Gaiser A, Kretinsky J. 2013. Automata with generalized Rabin
pairs for probabilistic model checking and LTL synthesis. 8044, 559–575.
mla: Chatterjee, Krishnendu, et al. Automata with Generalized Rabin Pairs for
Probabilistic Model Checking and LTL Synthesis. Vol. 8044, Springer, 2013,
pp. 559–75, doi:10.1007/978-3-642-39799-8_37.
short: K. Chatterjee, A. Gaiser, J. Kretinsky, 8044 (2013) 559–575.
conference:
end_date: 2013-07-19
location: St. Petersburg, Russia
name: 'CAV: Computer Aided Verification'
start_date: 2013-07-13
date_created: 2018-12-11T11:57:42Z
date_published: 2013-07-01T00:00:00Z
date_updated: 2020-08-11T10:09:47Z
day: '01'
department:
- _id: KrCh
doi: 10.1007/978-3-642-39799-8_37
ec_funded: 1
external_id:
arxiv:
- '1304.5281'
intvolume: ' 8044'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1304.5281
month: '07'
oa: 1
oa_version: Preprint
page: 559 - 575
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: 2587B514-B435-11E9-9278-68D0E5697425
name: Microsoft Research Faculty Fellowship
publication_status: published
publisher: Springer
publist_id: '4457'
quality_controlled: '1'
scopus_import: 1
series_title: Lecture Notes in Computer Science
status: public
title: Automata with generalized Rabin pairs for probabilistic model checking and
LTL synthesis
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 8044
year: '2013'
...
---
_id: '2814'
abstract:
- lang: eng
text: We study the problem of generating a test sequence that achieves maximal coverage
for a reactive system under test. We formulate the problem as a repeated game
between the tester and the system, where the system state space is partitioned
according to some coverage criterion and the objective of the tester is to maximize
the set of partitions (or coverage goals) visited during the game. We show the
complexity of the maximal coverage problem for non-deterministic systems is PSPACE-complete,
but is NP-complete for deterministic systems. For the special case of non-deterministic
systems with a re-initializing "reset" action, which represent running
a new test input on a re-initialized system, we show that the complexity is coNP-complete.
Our proof technique for reset games uses randomized testing strategies that circumvent
the exponentially large memory requirement of deterministic testing strategies.
We also discuss the memory requirement for deterministic strategies and extensions
of our results to other models, such as pushdown systems and timed systems.
article_processing_charge: No
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: Luca
full_name: Alfaro, Luca
last_name: Alfaro
- first_name: Ritankar
full_name: Majumdar, Ritankar
last_name: Majumdar
citation:
ama: Chatterjee K, Alfaro L, Majumdar R. The complexity of coverage. International
Journal of Foundations of Computer Science. 2013;24(2):165-185. doi:10.1142/S0129054113400066
apa: Chatterjee, K., Alfaro, L., & Majumdar, R. (2013). The complexity of coverage.
International Journal of Foundations of Computer Science. World Scientific
Publishing. https://doi.org/10.1142/S0129054113400066
chicago: Chatterjee, Krishnendu, Luca Alfaro, and Ritankar Majumdar. “The Complexity
of Coverage.” International Journal of Foundations of Computer Science.
World Scientific Publishing, 2013. https://doi.org/10.1142/S0129054113400066.
ieee: K. Chatterjee, L. Alfaro, and R. Majumdar, “The complexity of coverage,” International
Journal of Foundations of Computer Science, vol. 24, no. 2. World Scientific
Publishing, pp. 165–185, 2013.
ista: Chatterjee K, Alfaro L, Majumdar R. 2013. The complexity of coverage. International
Journal of Foundations of Computer Science. 24(2), 165–185.
mla: Chatterjee, Krishnendu, et al. “The Complexity of Coverage.” International
Journal of Foundations of Computer Science, vol. 24, no. 2, World Scientific
Publishing, 2013, pp. 165–85, doi:10.1142/S0129054113400066.
short: K. Chatterjee, L. Alfaro, R. Majumdar, International Journal of Foundations
of Computer Science 24 (2013) 165–185.
date_created: 2018-12-11T11:59:44Z
date_published: 2013-02-01T00:00:00Z
date_updated: 2025-09-29T14:02:41Z
day: '01'
department:
- _id: KrCh
doi: 10.1142/S0129054113400066
ec_funded: 1
external_id:
arxiv:
- '0804.4525'
isi:
- '000319838100002'
intvolume: ' 24'
isi: 1
issue: '2'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/0804.4525
month: '02'
oa: 1
oa_version: Preprint
page: 165 - 185
project:
- _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: 2587B514-B435-11E9-9278-68D0E5697425
name: Microsoft Research Faculty Fellowship
publication: International Journal of Foundations of Computer Science
publication_status: published
publisher: World Scientific Publishing
publist_id: '4070'
quality_controlled: '1'
scopus_import: '1'
status: public
title: The complexity of coverage
type: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 24
year: '2013'
...
---
_id: '2816'
abstract:
- lang: eng
text: In solid tumors, targeted treatments can lead to dramatic regressions, but
responses are often short-lived because resistant cancer cells arise. The major
strategy proposed for overcoming resistance is combination therapy. We present
a mathematical model describing the evolutionary dynamics of lesions in response
to treatment. We first studied 20 melanoma patients receiving vemurafenib. We
then applied our model to an independent set of pancreatic, colorectal, and melanoma
cancer patients with metastatic disease. We find that dual therapy results in
long-term disease control for most patients, if there are no single mutations
that cause cross-resistance to both drugs; in patients with large disease burden,
triple therapy is needed. We also find that simultaneous therapy with two drugs
is much more effective than sequential therapy. Our results provide realistic
expectations for the efficacy of new drug combinations and inform the design of
trials for new cancer therapeutics.
article_number: e00747
article_processing_charge: No
author:
- first_name: Ivana
full_name: Božić, Ivana
last_name: Božić
- first_name: Johannes
full_name: Reiter, Johannes
id: 4A918E98-F248-11E8-B48F-1D18A9856A87
last_name: Reiter
orcid: 0000-0002-0170-7353
- first_name: Benjamin
full_name: Allen, Benjamin
last_name: Allen
- first_name: Tibor
full_name: Antal, Tibor
last_name: Antal
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Preya
full_name: Shah, Preya
last_name: Shah
- first_name: Yo
full_name: Moon, Yo
last_name: Moon
- first_name: Amin
full_name: Yaqubie, Amin
last_name: Yaqubie
- first_name: Nicole
full_name: Kelly, Nicole
last_name: Kelly
- first_name: Dung
full_name: Le, Dung
last_name: Le
- first_name: Evan
full_name: Lipson, Evan
last_name: Lipson
- first_name: Paul
full_name: Chapman, Paul
last_name: Chapman
- first_name: Luis
full_name: Diaz, Luis
last_name: Diaz
- first_name: Bert
full_name: Vogelstein, Bert
last_name: Vogelstein
- first_name: Martin
full_name: Nowak, Martin
last_name: Nowak
citation:
ama: Božić I, Reiter J, Allen B, et al. Evolutionary dynamics of cancer in response
to targeted combination therapy. eLife. 2013;2. doi:10.7554/eLife.00747
apa: Božić, I., Reiter, J., Allen, B., Antal, T., Chatterjee, K., Shah, P., … Nowak,
M. (2013). Evolutionary dynamics of cancer in response to targeted combination
therapy. ELife. eLife Sciences Publications. https://doi.org/10.7554/eLife.00747
chicago: Božić, Ivana, Johannes Reiter, Benjamin Allen, Tibor Antal, Krishnendu
Chatterjee, Preya Shah, Yo Moon, et al. “Evolutionary Dynamics of Cancer in Response
to Targeted Combination Therapy.” ELife. eLife Sciences Publications, 2013.
https://doi.org/10.7554/eLife.00747.
ieee: I. Božić et al., “Evolutionary dynamics of cancer in response to targeted
combination therapy,” eLife, vol. 2. eLife Sciences Publications, 2013.
ista: Božić I, Reiter J, Allen B, Antal T, Chatterjee K, Shah P, Moon Y, Yaqubie
A, Kelly N, Le D, Lipson E, Chapman P, Diaz L, Vogelstein B, Nowak M. 2013. Evolutionary
dynamics of cancer in response to targeted combination therapy. eLife. 2, e00747.
mla: Božić, Ivana, et al. “Evolutionary Dynamics of Cancer in Response to Targeted
Combination Therapy.” ELife, vol. 2, e00747, eLife Sciences Publications,
2013, doi:10.7554/eLife.00747.
short: I. Božić, J. Reiter, B. Allen, T. Antal, K. Chatterjee, P. Shah, Y. Moon,
A. Yaqubie, N. Kelly, D. Le, E. Lipson, P. Chapman, L. Diaz, B. Vogelstein, M.
Nowak, ELife 2 (2013).
date_created: 2018-12-11T11:59:45Z
date_published: 2013-06-25T00:00:00Z
date_updated: 2026-04-09T14:26:23Z
day: '25'
ddc:
- '570'
- '610'
department:
- _id: KrCh
doi: 10.7554/eLife.00747
external_id:
isi:
- '000328619300005'
file:
- access_level: open_access
checksum: 2c38c47815eacd8fa66cb8b404cf7c61
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:12:48Z
date_updated: 2020-07-14T12:45:49Z
file_id: '4967'
file_name: IST-2013-134-v1+1_e00747.full.pdf
file_size: 3358321
relation: main_file
file_date_updated: 2020-07-14T12:45:49Z
has_accepted_license: '1'
intvolume: ' 2'
isi: 1
language:
- iso: eng
month: '06'
oa: 1
oa_version: Published Version
publication: eLife
publication_status: published
publisher: eLife Sciences Publications
publist_id: '3985'
pubrep_id: '134'
quality_controlled: '1'
related_material:
record:
- id: '1400'
relation: dissertation_contains
status: public
scopus_import: '1'
status: public
title: Evolutionary dynamics of cancer in response to targeted combination therapy
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: 2
year: '2013'
...
---
_id: '2817'
abstract:
- lang: eng
text: The basic idea of evolutionary game theory is that payoff determines reproductive
rate. Successful individuals have a higher payoff and produce more offspring.
But in evolutionary and ecological situations there is not only reproductive rate
but also carrying capacity. Individuals may differ in their exposure to density
limiting effects. Here we explore an alternative approach to evolutionary game
theory by assuming that the payoff from the game determines the carrying capacity
of individual phenotypes. Successful strategies are less affected by density limitation
(crowding) and reach higher equilibrium abundance. We demonstrate similarities
and differences between our framework and the standard replicator equation. Our
equation is defined on the positive orthant, instead of the simplex, but has the
same equilibrium points as the replicator equation. Linear stability analysis
produces the classical conditions for asymptotic stability of pure strategies,
but the stability properties of internal equilibria can differ in the two frameworks.
For example, in a two-strategy game with an internal equilibrium that is always
stable under the replicator equation, the corresponding equilibrium can be unstable
in the new framework resulting in a limit cycle.
article_processing_charge: No
author:
- first_name: Sebastian
full_name: Novak, Sebastian
id: 461468AE-F248-11E8-B48F-1D18A9856A87
last_name: Novak
orcid: 0000-0002-2519-824X
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Martin
full_name: Nowak, Martin
last_name: Nowak
citation:
ama: Novak S, Chatterjee K, Nowak M. Density games. Journal of Theoretical Biology.
2013;334:26-34. doi:10.1016/j.jtbi.2013.05.029
apa: Novak, S., Chatterjee, K., & Nowak, M. (2013). Density games. Journal
of Theoretical Biology. Elsevier. https://doi.org/10.1016/j.jtbi.2013.05.029
chicago: Novak, Sebastian, Krishnendu Chatterjee, and Martin Nowak. “Density Games.”
Journal of Theoretical Biology. Elsevier, 2013. https://doi.org/10.1016/j.jtbi.2013.05.029.
ieee: S. Novak, K. Chatterjee, and M. Nowak, “Density games,” Journal of Theoretical
Biology, vol. 334. Elsevier, pp. 26–34, 2013.
ista: Novak S, Chatterjee K, Nowak M. 2013. Density games. Journal of Theoretical
Biology. 334, 26–34.
mla: Novak, Sebastian, et al. “Density Games.” Journal of Theoretical Biology,
vol. 334, Elsevier, 2013, pp. 26–34, doi:10.1016/j.jtbi.2013.05.029.
short: S. Novak, K. Chatterjee, M. Nowak, Journal of Theoretical Biology 334 (2013)
26–34.
corr_author: '1'
date_created: 2018-12-11T11:59:45Z
date_published: 2013-10-07T00:00:00Z
date_updated: 2025-09-29T13:59:11Z
day: '07'
ddc:
- '000'
department:
- _id: NiBa
- _id: KrCh
doi: 10.1016/j.jtbi.2013.05.029
ec_funded: 1
external_id:
isi:
- '000323629500003'
file:
- access_level: open_access
checksum: 3c29059ab03a4b8f97a07646b817ddbb
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:14:54Z
date_updated: 2020-07-14T12:45:49Z
file_id: '5110'
file_name: IST-2016-400-v1+1_1-s2.0-S0022519313002609-main.pdf
file_size: 834604
relation: main_file
file_date_updated: 2020-07-14T12:45:49Z
has_accepted_license: '1'
intvolume: ' 334'
isi: 1
language:
- iso: eng
month: '10'
oa: 1
oa_version: Published Version
page: 26 - 34
project:
- _id: 25B07788-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '250152'
name: Limits to selection in biology and in evolutionary computation
- _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: 2587B514-B435-11E9-9278-68D0E5697425
name: Microsoft Research Faculty Fellowship
publication: Journal of Theoretical Biology
publication_status: published
publisher: Elsevier
publist_id: '3984'
pubrep_id: '400'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Density 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: 334
year: '2013'
...
---
_id: '2819'
abstract:
- lang: eng
text: 'We introduce quantatitive timed refinement metrics and quantitative timed
simulation functions, incorporating zenoness checks, for timed systems. These
functions assign positive real numbers between zero and infinity which quantify
the timing mismatches between two timed systems, amongst non-zeno runs. We quantify
timing mismatches in three ways: (1) the maximum timing mismatch that can arise,
(2) the "steady-state" maximum timing mismatches, where initial transient
timing mismatches are ignored; and (3) the (long-run) average timing mismatches
amongst two systems. These three kinds of mismatches constitute three important
types of timing differences. Our event times are the global times, measured from
the start of the system execution, not just the time durations of individual steps.
We present algorithms over timed automata for computing the three quantitative
simulation functions to within any desired degree of accuracy. In order to compute
the values of the quantitative simulation functions, we use a game theoretic formulation.
We introduce two new kinds of objectives for two player games on finite state
game graphs: (1) eventual debit-sum level objectives, and (2) average debit-sum
level objectives. We present algorithms for computing the optimal values for these
objectives for player 1, and then use these algorithms to compute the values of
the quantitative timed simulation functions. '
acknowledgement: 'This work has been financially supported in part by the European
Commission FP7-ICT Cognitive Systems, Interaction, and Robotics under the contract
# 270180 (NOP-TILUS); by Fundacao para Ciencia e Tecnologia under project PTDC/EEA-CRO/104901/2008
(Modeling and control of Networked vehicle systems in persistent autonomous operations);
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); and the Microsoft faculty fellows award'
article_processing_charge: No
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: Vinayak
full_name: Prabhu, Vinayak
last_name: Prabhu
citation:
ama: 'Chatterjee K, Prabhu V. Quantitative timed simulation functions and refinement
metrics for real-time systems. In: Proceedings of the 16th International Conference
on Hybrid Systems: Computation and Control. Vol 1. Springer; 2013:273-282.
doi:10.1145/2461328.2461370'
apa: 'Chatterjee, K., & Prabhu, V. (2013). Quantitative timed simulation functions
and refinement metrics for real-time systems. In Proceedings of the 16th International
Conference on Hybrid Systems: Computation and Control (Vol. 1, pp. 273–282).
Philadelphia, PA USA: Springer. https://doi.org/10.1145/2461328.2461370'
chicago: 'Chatterjee, Krishnendu, and Vinayak Prabhu. “Quantitative Timed Simulation
Functions and Refinement Metrics for Real-Time Systems.” In Proceedings of
the 16th International Conference on Hybrid Systems: Computation and Control,
1:273–82. Springer, 2013. https://doi.org/10.1145/2461328.2461370.'
ieee: 'K. Chatterjee and V. Prabhu, “Quantitative timed simulation functions and
refinement metrics for real-time systems,” in Proceedings of the 16th International
Conference on Hybrid Systems: Computation and Control, Philadelphia, PA USA,
2013, vol. 1, pp. 273–282.'
ista: 'Chatterjee K, Prabhu V. 2013. Quantitative timed simulation functions and
refinement metrics for real-time systems. Proceedings of the 16th International
Conference on Hybrid Systems: Computation and Control. HSCC: Hybrid Systems -
Computation and Control vol. 1, 273–282.'
mla: 'Chatterjee, Krishnendu, and Vinayak Prabhu. “Quantitative Timed Simulation
Functions and Refinement Metrics for Real-Time Systems.” Proceedings of the
16th International Conference on Hybrid Systems: Computation and Control,
vol. 1, Springer, 2013, pp. 273–82, doi:10.1145/2461328.2461370.'
short: 'K. Chatterjee, V. Prabhu, in:, Proceedings of the 16th International Conference
on Hybrid Systems: Computation and Control, Springer, 2013, pp. 273–282.'
conference:
end_date: 2013-04-11
location: Philadelphia, PA USA
name: 'HSCC: Hybrid Systems - Computation and Control'
start_date: 2013-04-08
date_created: 2018-12-11T11:59:46Z
date_published: 2013-04-01T00:00:00Z
date_updated: 2025-06-11T08:04:41Z
day: '01'
department:
- _id: KrCh
doi: 10.1145/2461328.2461370
ec_funded: 1
external_id:
arxiv:
- '1212.6556'
intvolume: ' 1'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1212.6556
month: '04'
oa: 1
oa_version: Preprint
page: 273 - 282
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: 2587B514-B435-11E9-9278-68D0E5697425
name: Microsoft Research Faculty Fellowship
publication: 'Proceedings of the 16th International Conference on Hybrid Systems:
Computation and Control'
publication_status: published
publisher: Springer
publist_id: '3982'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Quantitative timed simulation functions and refinement metrics for real-time
systems
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 1
year: '2013'
...
---
_id: '2820'
abstract:
- lang: eng
text: 'In this paper, we introduce the powerful framework of graph games for the
analysis of real-time scheduling with firm deadlines. We introduce a novel instance
of a partial-observation game that is suitable for this purpose, and prove decidability
of all the involved decision problems. We derive a graph game that allows the
automated computation of the competitive ratio (along with an optimal witness
algorithm for the competitive ratio) and establish an NP-completeness proof for
the graph game problem. For a given on-line algorithm, we present polynomial time
solution for computing (i) the worst-case utility; (ii) the worst-case utility
ratio w.r.t. a clairvoyant off-line algorithm; and (iii) the competitive ratio.
A major strength of the proposed approach lies in its flexibility w.r.t. incorporating
additional constraints on the adversary and/or the algorithm, including limited
maximum or average load, finiteness of periods of overload, etc., which are easily
added by means of additional instances of standard objective functions for graph
games. '
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Alexander
full_name: Kößler, Alexander
last_name: Kößler
- first_name: Ulrich
full_name: Schmid, Ulrich
last_name: Schmid
citation:
ama: 'Chatterjee K, Kößler A, Schmid U. Automated analysis of real-time scheduling
using graph games. In: Proceedings of the 16th International Conference on
Hybrid Systems: Computation and Control. ACM; 2013:163-172. doi:10.1145/2461328.2461356'
apa: 'Chatterjee, K., Kößler, A., & Schmid, U. (2013). Automated analysis of
real-time scheduling using graph games. In Proceedings of the 16th International
conference on Hybrid systems: Computation and control (pp. 163–172). Philadelphia,
PA, United States: ACM. https://doi.org/10.1145/2461328.2461356'
chicago: 'Chatterjee, Krishnendu, Alexander Kößler, and Ulrich Schmid. “Automated
Analysis of Real-Time Scheduling Using Graph Games.” In Proceedings of the
16th International Conference on Hybrid Systems: Computation and Control,
163–72. ACM, 2013. https://doi.org/10.1145/2461328.2461356.'
ieee: 'K. Chatterjee, A. Kößler, and U. Schmid, “Automated analysis of real-time
scheduling using graph games,” in Proceedings of the 16th International conference
on Hybrid systems: Computation and control, Philadelphia, PA, United States,
2013, pp. 163–172.'
ista: 'Chatterjee K, Kößler A, Schmid U. 2013. Automated analysis of real-time scheduling
using graph games. Proceedings of the 16th International conference on Hybrid
systems: Computation and control. HSCC: Hybrid Systems - Computation and Control,
163–172.'
mla: 'Chatterjee, Krishnendu, et al. “Automated Analysis of Real-Time Scheduling
Using Graph Games.” Proceedings of the 16th International Conference on Hybrid
Systems: Computation and Control, ACM, 2013, pp. 163–72, doi:10.1145/2461328.2461356.'
short: 'K. Chatterjee, A. Kößler, U. Schmid, in:, Proceedings of the 16th International
Conference on Hybrid Systems: Computation and Control, ACM, 2013, pp. 163–172.'
conference:
end_date: 2013-04-11
location: Philadelphia, PA, United States
name: 'HSCC: Hybrid Systems - Computation and Control'
start_date: 2013-04-08
date_created: 2018-12-11T11:59:46Z
date_published: 2013-04-01T00:00:00Z
date_updated: 2025-04-15T08:12:28Z
day: '01'
department:
- _id: KrCh
doi: 10.1145/2461328.2461356
ec_funded: 1
language:
- iso: eng
month: '04'
oa_version: None
page: 163 - 172
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11407
name: Game Theory
- _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: 2587B514-B435-11E9-9278-68D0E5697425
name: Microsoft Research Faculty Fellowship
publication: 'Proceedings of the 16th International conference on Hybrid systems:
Computation and control'
publication_identifier:
isbn:
- '978-1-4503-1567-8 '
publication_status: published
publisher: ACM
publist_id: '3981'
quality_controlled: '1'
related_material:
record:
- id: '738'
relation: later_version
status: public
scopus_import: 1
status: public
title: Automated analysis of real-time scheduling using graph games
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2013'
...
---
_id: '2824'
abstract:
- lang: eng
text: We study synthesis of controllers for real-time systems, where the objective
is to stay in a given safe set. The problem is solved by obtaining winning strategies
in the setting of concurrent two player timed automaton games with safety objectives.
To prevent a player from winning by blocking time, we restrict each player to
strategies that ensure that the player cannot be responsible for causing a Zeno
run. We construct winning strategies for the controller which require access only
to (1) the system clocks (thus, controllers which require their own internal infinitely
precise clocks are not necessary), and (2) a logarithmic (in the number of clocks)
number of memory bits (i.e. a linear number of memory states). Precisely, we show
that for safety objectives, a memory of size (3 + lg (| C | + 1)) bits suffices
for winning controller strategies, where C is the set of clocks of the timed automaton
game, significantly improving the previous known exponential memory states bound.
We also settle the open question of whether winning region-based strategies require
memory for safety objectives by showing with an example the necessity of memory
for such strategies to win for safety objectives. Finally, we show that the decision
problem of determining if there exists a receptive player-1 winning strategy for
safety objectives is EXPTIME-complete over timed automaton games.
article_processing_charge: No
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Vinayak
full_name: Prabhu, Vinayak
last_name: Prabhu
citation:
ama: Chatterjee K, Prabhu V. Synthesis of memory-efficient, clock-memory free, and
non-Zeno safety controllers for timed systems. Information and Computation.
2013;228-229:83-119. doi:10.1016/j.ic.2013.04.003
apa: Chatterjee, K., & Prabhu, V. (2013). Synthesis of memory-efficient, clock-memory
free, and non-Zeno safety controllers for timed systems. Information and Computation.
Elsevier. https://doi.org/10.1016/j.ic.2013.04.003
chicago: Chatterjee, Krishnendu, and Vinayak Prabhu. “Synthesis of Memory-Efficient,
Clock-Memory Free, and Non-Zeno Safety Controllers for Timed Systems.” Information
and Computation. Elsevier, 2013. https://doi.org/10.1016/j.ic.2013.04.003.
ieee: K. Chatterjee and V. Prabhu, “Synthesis of memory-efficient, clock-memory
free, and non-Zeno safety controllers for timed systems,” Information and Computation,
vol. 228–229. Elsevier, pp. 83–119, 2013.
ista: Chatterjee K, Prabhu V. 2013. Synthesis of memory-efficient, clock-memory
free, and non-Zeno safety controllers for timed systems. Information and Computation.
228–229, 83–119.
mla: Chatterjee, Krishnendu, and Vinayak Prabhu. “Synthesis of Memory-Efficient,
Clock-Memory Free, and Non-Zeno Safety Controllers for Timed Systems.” Information
and Computation, vol. 228–229, Elsevier, 2013, pp. 83–119, doi:10.1016/j.ic.2013.04.003.
short: K. Chatterjee, V. Prabhu, Information and Computation 228–229 (2013) 83–119.
date_created: 2018-12-11T11:59:47Z
date_published: 2013-04-24T00:00:00Z
date_updated: 2025-09-29T13:56:16Z
day: '24'
department:
- _id: KrCh
doi: 10.1016/j.ic.2013.04.003
ec_funded: 1
external_id:
isi:
- '000322295300005'
isi: 1
language:
- iso: eng
month: '04'
oa_version: None
page: 83-119
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: 2587B514-B435-11E9-9278-68D0E5697425
name: Microsoft Research Faculty Fellowship
publication: Information and Computation
publication_status: published
publisher: Elsevier
publist_id: '3977'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Synthesis of memory-efficient, clock-memory free, and non-Zeno safety controllers
for timed systems
type: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 228-229
year: '2013'
...
---
_id: '2831'
abstract:
- lang: eng
text: 'We consider Markov decision processes (MDPs) with Büchi (liveness) objectives.
We consider the problem of computing the set of almost-sure winning states from
where the objective can be ensured with probability 1. Our contributions are as
follows: First, we present the first subquadratic symbolic algorithm to compute
the almost-sure winning set for MDPs with Büchi objectives; our algorithm takes
O(n · √ m) symbolic steps as compared to the previous known algorithm that takes
O(n 2) symbolic steps, where n is the number of states and m is the number of
edges of the MDP. In practice MDPs have constant out-degree, and then our symbolic
algorithm takes O(n · √ n) symbolic steps, as compared to the previous known O(n
2) symbolic steps algorithm. Second, we present a new algorithm, namely win-lose
algorithm, with the following two properties: (a) the algorithm iteratively computes
subsets of the almost-sure winning set and its complement, as compared to all
previous algorithms that discover the almost-sure winning set upon termination;
and (b) requires O(n · √ K) symbolic steps, where K is the maximal number of edges
of strongly connected components (scc''s) of the MDP. The win-lose algorithm requires
symbolic computation of scc''s. Third, we improve the algorithm for symbolic scc
computation; the previous known algorithm takes linear symbolic steps, and our
new algorithm improves the constants associated with the linear number of steps.
In the worst case the previous known algorithm takes 5×n symbolic steps, whereas
our new algorithm takes 4×n symbolic steps.'
article_processing_charge: No
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: Monika H
full_name: Henzinger, Monika H
id: 540c9bbd-f2de-11ec-812d-d04a5be85630
last_name: Henzinger
orcid: 0000-0002-5008-6530
- first_name: Manas
full_name: Joglekar, Manas
last_name: Joglekar
- first_name: Nisarg
full_name: Shah, Nisarg
last_name: Shah
citation:
ama: Chatterjee K, Henzinger M, Joglekar M, Shah N. Symbolic algorithms for qualitative
analysis of Markov decision processes with Büchi objectives. Formal Methods
in System Design. 2013;42(3):301-327. doi:10.1007/s10703-012-0180-2
apa: Chatterjee, K., Henzinger, M., Joglekar, M., & Shah, N. (2013). Symbolic
algorithms for qualitative analysis of Markov decision processes with Büchi objectives.
Formal Methods in System Design. Springer. https://doi.org/10.1007/s10703-012-0180-2
chicago: Chatterjee, Krishnendu, Monika Henzinger, Manas Joglekar, and Nisarg Shah.
“Symbolic Algorithms for Qualitative Analysis of Markov Decision Processes with
Büchi Objectives.” Formal Methods in System Design. Springer, 2013. https://doi.org/10.1007/s10703-012-0180-2.
ieee: K. Chatterjee, M. Henzinger, M. Joglekar, and N. Shah, “Symbolic algorithms
for qualitative analysis of Markov decision processes with Büchi objectives,”
Formal Methods in System Design, vol. 42, no. 3. Springer, pp. 301–327,
2013.
ista: Chatterjee K, Henzinger M, Joglekar M, Shah N. 2013. Symbolic algorithms for
qualitative analysis of Markov decision processes with Büchi objectives. Formal
Methods in System Design. 42(3), 301–327.
mla: Chatterjee, Krishnendu, et al. “Symbolic Algorithms for Qualitative Analysis
of Markov Decision Processes with Büchi Objectives.” Formal Methods in System
Design, vol. 42, no. 3, Springer, 2013, pp. 301–27, doi:10.1007/s10703-012-0180-2.
short: K. Chatterjee, M. Henzinger, M. Joglekar, N. Shah, Formal Methods in System
Design 42 (2013) 301–327.
corr_author: '1'
date_created: 2018-12-11T11:59:49Z
date_published: 2013-06-01T00:00:00Z
date_updated: 2025-09-29T13:50:32Z
day: '01'
department:
- _id: KrCh
doi: 10.1007/s10703-012-0180-2
ec_funded: 1
external_id:
arxiv:
- '1104.3348'
isi:
- '000319151400003'
intvolume: ' 42'
isi: 1
issue: '3'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1104.3348
month: '06'
oa: 1
oa_version: Preprint
page: 301 - 327
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: 2587B514-B435-11E9-9278-68D0E5697425
name: Microsoft Research Faculty Fellowship
publication: Formal Methods in System Design
publication_status: published
publisher: Springer
publist_id: '3968'
quality_controlled: '1'
related_material:
record:
- id: '3342'
relation: earlier_version
status: public
scopus_import: '1'
status: public
title: Symbolic algorithms for qualitative analysis of Markov decision processes with
Büchi objectives
type: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 42
year: '2013'
...
---
_id: '2836'
abstract:
- lang: eng
text: 'We study the automatic synthesis of fair non-repudiation protocols, a class
of fair exchange protocols, used for digital contract signing. First, we show
how to specify the objectives of the participating agents and the trusted third
party as path formulas in linear temporal logic and prove that the satisfaction
of these objectives imply fairness; a property required of fair exchange protocols.
We then show that weak (co-operative) co-synthesis and classical (strictly competitive)
co-synthesis fail, whereas assume-guarantee synthesis (AGS) succeeds. We demonstrate
the success of AGS as follows: (a) any solution of AGS is attack-free; no subset
of participants can violate the objectives of the other participants; (b) the
Asokan-Shoup-Waidner certified mail protocol that has known vulnerabilities is
not a solution of AGS; (c) the Kremer-Markowitch non-repudiation protocol is a
solution of AGS; and (d) AGS presents a new and symmetric fair non-repudiation
protocol that is attack-free. To our knowledge this is the first application of
synthesis to fair non-repudiation protocols, and our results show how synthesis
can both automatically discover vulnerabilities in protocols and generate correct
protocols. The solution to AGS can be computed efficiently as the secure equilibrium
solution of three-player graph games. '
article_processing_charge: No
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: Vishwanath
full_name: Raman, Vishwanath
last_name: Raman
citation:
ama: Chatterjee K, Raman V. Assume-guarantee synthesis for digital contract signing.
Formal Aspects of Computing. 2013;26(4):825-859. doi:10.1007/s00165-013-0283-6
apa: Chatterjee, K., & Raman, V. (2013). Assume-guarantee synthesis for digital
contract signing. Formal Aspects of Computing. Springer. https://doi.org/10.1007/s00165-013-0283-6
chicago: Chatterjee, Krishnendu, and Vishwanath Raman. “Assume-Guarantee Synthesis
for Digital Contract Signing.” Formal Aspects of Computing. Springer, 2013.
https://doi.org/10.1007/s00165-013-0283-6.
ieee: K. Chatterjee and V. Raman, “Assume-guarantee synthesis for digital contract
signing,” Formal Aspects of Computing, vol. 26, no. 4. Springer, pp. 825–859,
2013.
ista: Chatterjee K, Raman V. 2013. Assume-guarantee synthesis for digital contract
signing. Formal Aspects of Computing. 26(4), 825–859.
mla: Chatterjee, Krishnendu, and Vishwanath Raman. “Assume-Guarantee Synthesis for
Digital Contract Signing.” Formal Aspects of Computing, vol. 26, no. 4,
Springer, 2013, pp. 825–59, doi:10.1007/s00165-013-0283-6.
short: K. Chatterjee, V. Raman, Formal Aspects of Computing 26 (2013) 825–859.
date_created: 2018-12-11T11:59:51Z
date_published: 2013-07-04T00:00:00Z
date_updated: 2025-09-29T13:47:26Z
day: '04'
department:
- _id: KrCh
doi: 10.1007/s00165-013-0283-6
ec_funded: 1
external_id:
arxiv:
- '1004.2697'
isi:
- '000339105100007'
intvolume: ' 26'
isi: 1
issue: '4'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1004.2697
month: '07'
oa: 1
oa_version: Preprint
page: 825 - 859
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: 2587B514-B435-11E9-9278-68D0E5697425
name: Microsoft Research Faculty Fellowship
publication: Formal Aspects of Computing
publication_status: published
publisher: Springer
publist_id: '3963'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Assume-guarantee synthesis for digital contract signing
type: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 26
year: '2013'
...
---
_id: '2854'
abstract:
- lang: eng
text: We consider concurrent games played on graphs. At every round of a game, each
player simultaneously and independently selects a move; the moves jointly determine
the transition to a successor state. Two basic objectives are the safety objective
to stay forever in a given set of states, and its dual, the reachability objective
to reach a given set of states. First, we present a simple proof of the fact that
in concurrent reachability games, for all ε>0, memoryless ε-optimal strategies
exist. A memoryless strategy is independent of the history of plays, and an ε-optimal
strategy achieves the objective with probability within ε of the value of the
game. In contrast to previous proofs of this fact, our proof is more elementary
and more combinatorial. Second, we present a strategy-improvement (a.k.a. policy-iteration)
algorithm for concurrent games with reachability objectives. Finally, we present
a strategy-improvement algorithm for turn-based stochastic games (where each player
selects moves in turns) with safety objectives. Our algorithms yield sequences
of player-1 strategies which ensure probabilities of winning that converge monotonically
(from below) to the value of the game. © 2012 Elsevier Inc.
acknowledgement: This work was partially supported in part by the NSF grants CCR-0132780,
CNS-0720884, CCR-0225610, by the Swiss National Science Foundation, ERC Start Grant
Graph Games (Project No. 279307), FWF NFN Grant S11407-N23 (RiSE), and a Microsoft
faculty fellows
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: Luca
full_name: De Alfaro, Luca
last_name: De Alfaro
- 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, De Alfaro L, Henzinger TA. Strategy improvement for concurrent
reachability and turn based stochastic safety games. Journal of Computer and
System Sciences. 2013;79(5):640-657. doi:10.1016/j.jcss.2012.12.001
apa: Chatterjee, K., De Alfaro, L., & Henzinger, T. A. (2013). Strategy improvement
for concurrent reachability and turn based stochastic safety games. Journal
of Computer and System Sciences. Elsevier. https://doi.org/10.1016/j.jcss.2012.12.001
chicago: Chatterjee, Krishnendu, Luca De Alfaro, and Thomas A Henzinger. “Strategy
Improvement for Concurrent Reachability and Turn Based Stochastic Safety Games.”
Journal of Computer and System Sciences. Elsevier, 2013. https://doi.org/10.1016/j.jcss.2012.12.001.
ieee: K. Chatterjee, L. De Alfaro, and T. A. Henzinger, “Strategy improvement for
concurrent reachability and turn based stochastic safety games,” Journal of
Computer and System Sciences, vol. 79, no. 5. Elsevier, pp. 640–657, 2013.
ista: Chatterjee K, De Alfaro L, Henzinger TA. 2013. Strategy improvement for concurrent
reachability and turn based stochastic safety games. Journal of Computer and System
Sciences. 79(5), 640–657.
mla: Chatterjee, Krishnendu, et al. “Strategy Improvement for Concurrent Reachability
and Turn Based Stochastic Safety Games.” Journal of Computer and System Sciences,
vol. 79, no. 5, Elsevier, 2013, pp. 640–57, doi:10.1016/j.jcss.2012.12.001.
short: K. Chatterjee, L. De Alfaro, T.A. Henzinger, Journal of Computer and System
Sciences 79 (2013) 640–657.
corr_author: '1'
date_created: 2018-12-11T11:59:57Z
date_published: 2013-08-01T00:00:00Z
date_updated: 2025-09-29T13:40:38Z
day: '01'
ddc:
- '000'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1016/j.jcss.2012.12.001
ec_funded: 1
external_id:
isi:
- '000316837300011'
file:
- access_level: open_access
checksum: 6d3ee12cceb946a0abe69594b6a22409
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:18:48Z
date_updated: 2020-07-14T12:45:51Z
file_id: '5370'
file_name: IST-2015-388-v1+1_1-s2.0-S0022000012001778-main.pdf
file_size: 425488
relation: main_file
file_date_updated: 2020-07-14T12:45:51Z
has_accepted_license: '1'
intvolume: ' 79'
isi: 1
issue: '5'
language:
- iso: eng
license: https://creativecommons.org/licenses/by-nc-nd/4.0/
month: '08'
oa: 1
oa_version: Published Version
page: 640 - 657
project:
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11407
name: Game Theory
- _id: 2587B514-B435-11E9-9278-68D0E5697425
name: Microsoft Research Faculty Fellowship
publication: Journal of Computer and System Sciences
publication_status: published
publisher: Elsevier
publist_id: '3938'
pubrep_id: '388'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Strategy improvement for concurrent reachability and turn based stochastic
safety games
tmp:
image: /images/cc_by_nc_nd.png
legal_code_url: https://creativecommons.org/licenses/by-nc-nd/4.0/legalcode
name: Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International
(CC BY-NC-ND 4.0)
short: CC BY-NC-ND (4.0)
type: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 79
year: '2013'
...
---
_id: '2858'
abstract:
- lang: eng
text: Tumor growth is caused by the acquisition of driver mutations, which enhance
the net reproductive rate of cells. Driver mutations may increase cell division,
reduce cell death, or allow cells to overcome density-limiting effects. We study
the dynamics of tumor growth as one additional driver mutation is acquired. Our
models are based on two-type branching processes that terminate in either tumor
disappearance or tumor detection. In our first model, both cell types grow exponentially,
with a faster rate for cells carrying the additional driver. We find that the
additional driver mutation does not affect the survival probability of the lesion,
but can substantially reduce the time to reach the detectable size if the lesion
is slow growing. In our second model, cells lacking the additional driver cannot
exceed a fixed carrying capacity, due to density limitations. In this case, the
time to detection depends strongly on this carrying capacity. Our model provides
a quantitative framework for studying tumor dynamics during different stages of
progression. We observe that early, small lesions need additional drivers, while
late stage metastases are only marginally affected by them. These results help
to explain why additional driver mutations are typically not detected in fast-growing
metastases.
article_processing_charge: No
author:
- first_name: Johannes
full_name: Reiter, Johannes
id: 4A918E98-F248-11E8-B48F-1D18A9856A87
last_name: Reiter
orcid: 0000-0002-0170-7353
- first_name: Ivana
full_name: Božić, Ivana
last_name: Božić
- first_name: Benjamin
full_name: Allen, Benjamin
id: 135B5B70-E9D2-11E9-BD74-BB415DA2B523
last_name: Allen
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Martin
full_name: Nowak, Martin
last_name: Nowak
citation:
ama: Reiter J, Božić I, Allen B, Chatterjee K, Nowak M. The effect of one additional
driver mutation on tumor progression. Evolutionary Applications. 2013;6(1):34-45.
doi:10.1111/eva.12020
apa: Reiter, J., Božić, I., Allen, B., Chatterjee, K., & Nowak, M. (2013). The
effect of one additional driver mutation on tumor progression. Evolutionary
Applications. Wiley-Blackwell. https://doi.org/10.1111/eva.12020
chicago: Reiter, Johannes, Ivana Božić, Benjamin Allen, Krishnendu Chatterjee, and
Martin Nowak. “The Effect of One Additional Driver Mutation on Tumor Progression.”
Evolutionary Applications. Wiley-Blackwell, 2013. https://doi.org/10.1111/eva.12020.
ieee: J. Reiter, I. Božić, B. Allen, K. Chatterjee, and M. Nowak, “The effect of
one additional driver mutation on tumor progression,” Evolutionary Applications,
vol. 6, no. 1. Wiley-Blackwell, pp. 34–45, 2013.
ista: Reiter J, Božić I, Allen B, Chatterjee K, Nowak M. 2013. The effect of one
additional driver mutation on tumor progression. Evolutionary Applications. 6(1),
34–45.
mla: Reiter, Johannes, et al. “The Effect of One Additional Driver Mutation on Tumor
Progression.” Evolutionary Applications, vol. 6, no. 1, Wiley-Blackwell,
2013, pp. 34–45, doi:10.1111/eva.12020.
short: J. Reiter, I. Božić, B. Allen, K. Chatterjee, M. Nowak, Evolutionary Applications
6 (2013) 34–45.
corr_author: '1'
date_created: 2018-12-11T11:59:58Z
date_published: 2013-01-01T00:00:00Z
date_updated: 2026-04-09T14:26:23Z
day: '01'
ddc:
- '570'
department:
- _id: KrCh
doi: 10.1111/eva.12020
ec_funded: 1
external_id:
isi:
- '000313878800004'
file:
- access_level: open_access
checksum: e2955b3889f8a823c3d5a72cb16f8957
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:15:50Z
date_updated: 2020-07-14T12:45:51Z
file_id: '5173'
file_name: IST-2016-415-v1+1_Reiter_et_al-2013-Evolutionary_Applications.pdf
file_size: 1172037
relation: main_file
file_date_updated: 2020-07-14T12:45:51Z
has_accepted_license: '1'
intvolume: ' 6'
isi: 1
issue: '1'
language:
- iso: eng
month: '01'
oa: 1
oa_version: Published Version
page: 34 - 45
project:
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11407
name: Game Theory
publication: Evolutionary Applications
publication_status: published
publisher: Wiley-Blackwell
publist_id: '3931'
pubrep_id: '415'
quality_controlled: '1'
related_material:
record:
- id: '1400'
relation: dissertation_contains
status: public
scopus_import: '1'
status: public
title: The effect of one additional driver mutation on tumor progression
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: 6
year: '2013'
...