---
_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
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: '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.
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: 2021-01-12T06:59:54Z
day: '01'
department:
- _id: KrCh
doi: 10.1142/S0129054113400066
ec_funded: 1
external_id:
arxiv:
- '0804.4525'
intvolume: ' 24'
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: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 24
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.
author:
- first_name: Sebastian
full_name: Novak, Sebastian
id: 461468AE-F248-11E8-B48F-1D18A9856A87
last_name: Novak
- 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.
date_created: 2018-12-11T11:59:45Z
date_published: 2013-10-07T00:00:00Z
date_updated: 2021-01-12T06:59:55Z
day: '07'
ddc:
- '000'
department:
- _id: NiBa
- _id: KrCh
doi: 10.1016/j.jtbi.2013.05.029
ec_funded: 1
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'
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: 2DF688A6-F248-11E8-B48F-1D18A9856A87
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'
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: 2021-01-12T06:59:56Z
day: '01'
department:
- _id: KrCh
doi: 10.1145/2461328.2461370
ec_funded: 1
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: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 1
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.
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: 2021-01-12T06:59:58Z
day: '24'
department:
- _id: KrCh
doi: 10.1016/j.ic.2013.04.003
ec_funded: 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: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 228-229
year: '2013'
...