---
_id: '1667'
abstract:
- lang: eng
text: We consider parametric version of fixed-delay continuoustime Markov chains
(or equivalently deterministic and stochastic Petri nets, DSPN) where fixed-delay
transitions are specified by parameters, rather than concrete values. Our goal
is to synthesize values of these parameters that, for a given cost function, minimise
expected total cost incurred before reaching a given set of target states. We
show that under mild assumptions, optimal values of parameters can be effectively
approximated using translation to a Markov decision process (MDP) whose actions
correspond to discretized values of these parameters. To this end we identify
and overcome several interesting phenomena arising in systems with fixed delays.
acknowledgement: The research leading to these results has received funding from the
People Programme (Marie Curie Actions) of the European Union’s Seventh Framework
Programme (FP7/2007-2013) under REA grant agreement n∘ [291734]. This work is partly
supported by the German Research Council (DFG) as part of the Transregional Collaborative
Research Center AVACS (SFB/TR 14), by the EU 7th Framework Programme under grant
agreement no. 295261 (MEALS) and 318490 (SENSATION), by the Czech Science Foundation,
grant No. 15-17564S, and by the CAS/SAFEA International Partnership Program for
Creative Research Teams.
alternative_title:
- LNCS
author:
- first_name: Tomáš
full_name: Brázdil, Tomáš
last_name: Brázdil
- first_name: L'Uboš
full_name: Korenčiak, L'Uboš
last_name: Korenčiak
- first_name: Jan
full_name: Krčál, Jan
last_name: Krčál
- first_name: Petr
full_name: Novotny, Petr
id: 3CC3B868-F248-11E8-B48F-1D18A9856A87
last_name: Novotny
- first_name: Vojtěch
full_name: Řehák, Vojtěch
last_name: Řehák
citation:
ama: Brázdil T, Korenčiak L, Krčál J, Novotný P, Řehák V. Optimizing performance
of continuous-time stochastic systems using timeout synthesis. 2015;9259:141-159.
doi:10.1007/978-3-319-22264-6_10
apa: 'Brázdil, T., Korenčiak, L., Krčál, J., Novotný, P., & Řehák, V. (2015).
Optimizing performance of continuous-time stochastic systems using timeout synthesis.
Presented at the QEST: Quantitative Evaluation of Systems, Madrid, Spain: Springer.
https://doi.org/10.1007/978-3-319-22264-6_10'
chicago: Brázdil, Tomáš, L’Uboš Korenčiak, Jan Krčál, Petr Novotný, and Vojtěch
Řehák. “Optimizing Performance of Continuous-Time Stochastic Systems Using Timeout
Synthesis.” Lecture Notes in Computer Science. Springer, 2015. https://doi.org/10.1007/978-3-319-22264-6_10.
ieee: T. Brázdil, L. Korenčiak, J. Krčál, P. Novotný, and V. Řehák, “Optimizing
performance of continuous-time stochastic systems using timeout synthesis,” vol.
9259. Springer, pp. 141–159, 2015.
ista: Brázdil T, Korenčiak L, Krčál J, Novotný P, Řehák V. 2015. Optimizing performance
of continuous-time stochastic systems using timeout synthesis. 9259, 141–159.
mla: Brázdil, Tomáš, et al. Optimizing Performance of Continuous-Time Stochastic
Systems Using Timeout Synthesis. Vol. 9259, Springer, 2015, pp. 141–59, doi:10.1007/978-3-319-22264-6_10.
short: T. Brázdil, L. Korenčiak, J. Krčál, P. Novotný, V. Řehák, 9259 (2015) 141–159.
conference:
end_date: 2015-09-03
location: Madrid, Spain
name: 'QEST: Quantitative Evaluation of Systems'
start_date: 2015-09-01
date_created: 2018-12-11T11:53:22Z
date_published: 2015-08-22T00:00:00Z
date_updated: 2021-01-12T06:52:24Z
day: '22'
department:
- _id: KrCh
doi: 10.1007/978-3-319-22264-6_10
ec_funded: 1
intvolume: ' 9259'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1407.4777
month: '08'
oa: 1
oa_version: Preprint
page: 141 - 159
project:
- _id: 25681D80-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '291734'
name: International IST Postdoc Fellowship Programme
publication_status: published
publisher: Springer
publist_id: '5482'
quality_controlled: '1'
scopus_import: 1
series_title: Lecture Notes in Computer Science
status: public
title: Optimizing performance of continuous-time stochastic systems using timeout
synthesis
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 9259
year: '2015'
...
---
_id: '1673'
abstract:
- lang: eng
text: 'When a new mutant arises in a population, there is a probability it outcompetes
the residents and fixes. The structure of the population can affect this fixation
probability. Suppressing population structures reduce the difference between two
competing variants, while amplifying population structures enhance the difference.
Suppressors are ubiquitous and easy to construct, but amplifiers for the large
population limit are more elusive and only a few examples have been discovered.
Whether or not a population structure is an amplifier of selection depends on
the probability distribution for the placement of the invading mutant. First,
we prove that there exist only bounded amplifiers for adversarial placement-that
is, for arbitrary initial conditions. Next, we show that the Star population structure,
which is known to amplify for mutants placed uniformly at random, does not amplify
for mutants that arise through reproduction and are therefore placed proportional
to the temperatures of the vertices. Finally, we construct population structures
that amplify for all mutational events that arise through reproduction, uniformly
at random, or through some combination of the two. '
acknowledgement: 'K.C. gratefully acknowledges support from ERC Start grant no. (279307:
Graph Games), Austrian Science Fund (FWF) grant no. P23499-N23, and FWF NFN grant
no. S11407-N23 (RiSE). '
article_number: '20150114'
author:
- first_name: Ben
full_name: Adlam, Ben
last_name: Adlam
- 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: 'Adlam B, Chatterjee K, Nowak M. Amplifiers of selection. Proceedings of
the Royal Society A: Mathematical, Physical and Engineering Sciences. 2015;471(2181).
doi:10.1098/rspa.2015.0114'
apa: 'Adlam, B., Chatterjee, K., & Nowak, M. (2015). Amplifiers of selection.
Proceedings of the Royal Society A: Mathematical, Physical and Engineering
Sciences. Royal Society of London. https://doi.org/10.1098/rspa.2015.0114'
chicago: 'Adlam, Ben, Krishnendu Chatterjee, and Martin Nowak. “Amplifiers of Selection.”
Proceedings of the Royal Society A: Mathematical, Physical and Engineering
Sciences. Royal Society of London, 2015. https://doi.org/10.1098/rspa.2015.0114.'
ieee: 'B. Adlam, K. Chatterjee, and M. Nowak, “Amplifiers of selection,” Proceedings
of the Royal Society A: Mathematical, Physical and Engineering Sciences, vol.
471, no. 2181. Royal Society of London, 2015.'
ista: 'Adlam B, Chatterjee K, Nowak M. 2015. Amplifiers of selection. Proceedings
of the Royal Society A: Mathematical, Physical and Engineering Sciences. 471(2181),
20150114.'
mla: 'Adlam, Ben, et al. “Amplifiers of Selection.” Proceedings of the Royal
Society A: Mathematical, Physical and Engineering Sciences, vol. 471, no.
2181, 20150114, Royal Society of London, 2015, doi:10.1098/rspa.2015.0114.'
short: 'B. Adlam, K. Chatterjee, M. Nowak, Proceedings of the Royal Society A: Mathematical,
Physical and Engineering Sciences 471 (2015).'
date_created: 2018-12-11T11:53:24Z
date_published: 2015-09-08T00:00:00Z
date_updated: 2021-01-12T06:52:26Z
day: '08'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1098/rspa.2015.0114
ec_funded: 1
file:
- access_level: open_access
checksum: e613d94d283c776322403a28aad11bdd
content_type: application/pdf
creator: kschuh
date_created: 2019-04-18T12:39:56Z
date_updated: 2020-07-14T12:45:11Z
file_id: '6342'
file_name: 2015_rspa_Adlam.pdf
file_size: 391466
relation: main_file
file_date_updated: 2020-07-14T12:45:11Z
has_accepted_license: '1'
intvolume: ' 471'
issue: '2181'
language:
- iso: eng
month: '09'
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: 2584A770-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: P 23499-N23
name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
publication: 'Proceedings of the Royal Society A: Mathematical, Physical and Engineering
Sciences'
publication_status: published
publisher: Royal Society of London
publist_id: '5477'
quality_controlled: '1'
scopus_import: 1
status: public
title: Amplifiers of selection
type: journal_article
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 471
year: '2015'
...
---
_id: '1681'
abstract:
- lang: eng
text: In many social situations, individuals endeavor to find the single best possible
partner, but are constrained to evaluate the candidates in sequence. Examples
include the search for mates, economic partnerships, or any other long-term ties
where the choice to interact involves two parties. Surprisingly, however, previous
theoretical work on mutual choice problems focuses on finding equilibrium solutions,
while ignoring the evolutionary dynamics of decisions. Empirically, this may be
of high importance, as some equilibrium solutions can never be reached unless
the population undergoes radical changes and a sufficient number of individuals
change their decisions simultaneously. To address this question, we apply a mutual
choice sequential search problem in an evolutionary game-theoretical model that
allows one to find solutions that are favored by evolution. As an example, we
study the influence of sequential search on the evolutionary dynamics of cooperation.
For this, we focus on the classic snowdrift game and the prisoner’s dilemma game.
article_processing_charge: No
article_type: original
author:
- first_name: Tadeas
full_name: Priklopil, Tadeas
id: 3C869AA0-F248-11E8-B48F-1D18A9856A87
last_name: Priklopil
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
citation:
ama: Priklopil T, Chatterjee K. Evolution of decisions in population games with
sequentially searching individuals. Games. 2015;6(4):413-437. doi:10.3390/g6040413
apa: Priklopil, T., & Chatterjee, K. (2015). Evolution of decisions in population
games with sequentially searching individuals. Games. MDPI. https://doi.org/10.3390/g6040413
chicago: Priklopil, Tadeas, and Krishnendu Chatterjee. “Evolution of Decisions in
Population Games with Sequentially Searching Individuals.” Games. MDPI,
2015. https://doi.org/10.3390/g6040413.
ieee: T. Priklopil and K. Chatterjee, “Evolution of decisions in population games
with sequentially searching individuals,” Games, vol. 6, no. 4. MDPI, pp.
413–437, 2015.
ista: Priklopil T, Chatterjee K. 2015. Evolution of decisions in population games
with sequentially searching individuals. Games. 6(4), 413–437.
mla: Priklopil, Tadeas, and Krishnendu Chatterjee. “Evolution of Decisions in Population
Games with Sequentially Searching Individuals.” Games, vol. 6, no. 4, MDPI,
2015, pp. 413–37, doi:10.3390/g6040413.
short: T. Priklopil, K. Chatterjee, Games 6 (2015) 413–437.
date_created: 2018-12-11T11:53:26Z
date_published: 2015-09-29T00:00:00Z
date_updated: 2023-10-17T11:42:52Z
day: '29'
ddc:
- '000'
department:
- _id: NiBa
- _id: KrCh
doi: 10.3390/g6040413
ec_funded: 1
file:
- access_level: open_access
checksum: 912e1acbaf201100f447a43e4d5958bd
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:12:41Z
date_updated: 2020-07-14T12:45:12Z
file_id: '4959'
file_name: IST-2016-448-v1+1_games-06-00413.pdf
file_size: 518832
relation: main_file
file_date_updated: 2020-07-14T12:45:12Z
has_accepted_license: '1'
intvolume: ' 6'
issue: '4'
language:
- iso: eng
license: https://creativecommons.org/licenses/by/4.0/
month: '09'
oa: 1
oa_version: Published Version
page: 413 - 437
project:
- _id: 25681D80-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '291734'
name: International IST Postdoc Fellowship Programme
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
publication: Games
publication_identifier:
eissn:
- 2073-4336
publication_status: published
publisher: MDPI
publist_id: '5467'
pubrep_id: '448'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Evolution of decisions in population games with sequentially searching individuals
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: 6
year: '2015'
...
---
_id: '1689'
abstract:
- lang: eng
text: We consider the problem of computing the set of initial states of a dynamical
system such that there exists a control strategy to ensure that the trajectories
satisfy a temporal logic specification with probability 1 (almost-surely). We
focus on discrete-time, stochastic linear dynamics and specifications given as
formulas of the Generalized Reactivity(1) fragment of Linear Temporal Logic over
linear predicates in the states of the system. We propose a solution based on
iterative abstraction-refinement, and turn-based 2-player probabilistic games.
While the theoretical guarantee of our algorithm after any finite number of iterations
is only a partial solution, we show that if our algorithm terminates, then the
result is the set of satisfying initial states. Moreover, for any (partial) solution
our algorithm synthesizes witness control strategies to ensure almost-sure satisfaction
of the temporal logic specification. We demonstrate our approach on an illustrative
case study.
author:
- first_name: Mária
full_name: Svoreňová, Mária
last_name: Svoreňová
- first_name: Jan
full_name: Kretinsky, Jan
id: 44CEF464-F248-11E8-B48F-1D18A9856A87
last_name: Kretinsky
orcid: 0000-0002-8122-2881
- first_name: Martin
full_name: Chmelik, Martin
id: 3624234E-F248-11E8-B48F-1D18A9856A87
last_name: Chmelik
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Ivana
full_name: Cěrná, Ivana
last_name: Cěrná
- first_name: Cǎlin
full_name: Belta, Cǎlin
last_name: Belta
citation:
ama: 'Svoreňová M, Kretinsky J, Chmelik M, Chatterjee K, Cěrná I, Belta C. Temporal
logic control for stochastic linear systems using abstraction refinement of probabilistic
games. In: Proceedings of the 18th International Conference on Hybrid Systems:
Computation and Control. ACM; 2015:259-268. doi:10.1145/2728606.2728608'
apa: 'Svoreňová, M., Kretinsky, J., Chmelik, M., Chatterjee, K., Cěrná, I., &
Belta, C. (2015). Temporal logic control for stochastic linear systems using abstraction
refinement of probabilistic games. In Proceedings of the 18th International
Conference on Hybrid Systems: Computation and Control (pp. 259–268). Seattle,
WA, United States: ACM. https://doi.org/10.1145/2728606.2728608'
chicago: 'Svoreňová, Mária, Jan Kretinsky, Martin Chmelik, Krishnendu Chatterjee,
Ivana Cěrná, and Cǎlin Belta. “Temporal Logic Control for Stochastic Linear Systems
Using Abstraction Refinement of Probabilistic Games.” In Proceedings of the
18th International Conference on Hybrid Systems: Computation and Control,
259–68. ACM, 2015. https://doi.org/10.1145/2728606.2728608.'
ieee: 'M. Svoreňová, J. Kretinsky, M. Chmelik, K. Chatterjee, I. Cěrná, and C. Belta,
“Temporal logic control for stochastic linear systems using abstraction refinement
of probabilistic games,” in Proceedings of the 18th International Conference
on Hybrid Systems: Computation and Control, Seattle, WA, United States, 2015,
pp. 259–268.'
ista: 'Svoreňová M, Kretinsky J, Chmelik M, Chatterjee K, Cěrná I, Belta C. 2015.
Temporal logic control for stochastic linear systems using abstraction refinement
of probabilistic games. Proceedings of the 18th International Conference on Hybrid
Systems: Computation and Control. HSCC: Hybrid Systems - Computation and Control,
259–268.'
mla: 'Svoreňová, Mária, et al. “Temporal Logic Control for Stochastic Linear Systems
Using Abstraction Refinement of Probabilistic Games.” Proceedings of the 18th
International Conference on Hybrid Systems: Computation and Control, ACM,
2015, pp. 259–68, doi:10.1145/2728606.2728608.'
short: 'M. Svoreňová, J. Kretinsky, M. Chmelik, K. Chatterjee, I. Cěrná, C. Belta,
in:, Proceedings of the 18th International Conference on Hybrid Systems: Computation
and Control, ACM, 2015, pp. 259–268.'
conference:
end_date: 2015-04-16
location: Seattle, WA, United States
name: 'HSCC: Hybrid Systems - Computation and Control'
start_date: 2015-04-14
date_created: 2018-12-11T11:53:29Z
date_published: 2015-04-14T00:00:00Z
date_updated: 2023-09-20T09:43:09Z
day: '14'
department:
- _id: ToHe
- _id: KrCh
doi: 10.1145/2728606.2728608
ec_funded: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1410.5387
month: '04'
oa: 1
oa_version: Preprint
page: 259 - 268
project:
- _id: 25681D80-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '291734'
name: International IST Postdoc Fellowship Programme
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _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: 25863FF4-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11407
name: Game Theory
publication: 'Proceedings of the 18th International Conference on Hybrid Systems:
Computation and Control'
publication_status: published
publisher: ACM
publist_id: '5456'
related_material:
record:
- id: '1407'
relation: later_version
status: public
scopus_import: 1
status: public
title: Temporal logic control for stochastic linear systems using abstraction refinement
of probabilistic games
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2015'
...
---
_id: '1691'
abstract:
- lang: eng
text: We consider a case study of the problem of deploying an autonomous air vehicle
in a partially observable, dynamic, indoor environment from a specification given
as a linear temporal logic (LTL) formula over regions of interest. We model the
motion and sensing capabilities of the vehicle as a partially observable Markov
decision process (POMDP). We adapt recent results for solving POMDPs with parity
objectives to generate a control policy. We also extend the existing framework
with a policy minimization technique to obtain a better implementable policy,
while preserving its correctness. The proposed techniques are illustrated in an
experimental setup involving an autonomous quadrotor performing surveillance in
a dynamic environment.
author:
- first_name: Mária
full_name: Svoreňová, Mária
last_name: Svoreňová
- first_name: Martin
full_name: Chmelik, Martin
id: 3624234E-F248-11E8-B48F-1D18A9856A87
last_name: Chmelik
- first_name: Kevin
full_name: Leahy, Kevin
last_name: Leahy
- first_name: Hasan
full_name: Eniser, Hasan
last_name: Eniser
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Ivana
full_name: Cěrná, Ivana
last_name: Cěrná
- first_name: Cǎlin
full_name: Belta, Cǎlin
last_name: Belta
citation:
ama: 'Svoreňová M, Chmelik M, Leahy K, et al. Temporal logic motion planning using
POMDPs with parity objectives: Case study paper. In: Proceedings of the 18th
International Conference on Hybrid Systems: Computation and Control. ACM;
2015:233-238. doi:10.1145/2728606.2728617'
apa: 'Svoreňová, M., Chmelik, M., Leahy, K., Eniser, H., Chatterjee, K., Cěrná,
I., & Belta, C. (2015). Temporal logic motion planning using POMDPs with parity
objectives: Case study paper. In Proceedings of the 18th International Conference
on Hybrid Systems: Computation and Control (pp. 233–238). Seattle, WA, United
States: ACM. https://doi.org/10.1145/2728606.2728617'
chicago: 'Svoreňová, Mária, Martin Chmelik, Kevin Leahy, Hasan Eniser, Krishnendu
Chatterjee, Ivana Cěrná, and Cǎlin Belta. “Temporal Logic Motion Planning Using
POMDPs with Parity Objectives: Case Study Paper.” In Proceedings of the 18th
International Conference on Hybrid Systems: Computation and Control, 233–38.
ACM, 2015. https://doi.org/10.1145/2728606.2728617.'
ieee: 'M. Svoreňová et al., “Temporal logic motion planning using POMDPs
with parity objectives: Case study paper,” in Proceedings of the 18th International
Conference on Hybrid Systems: Computation and Control, Seattle, WA, United
States, 2015, pp. 233–238.'
ista: 'Svoreňová M, Chmelik M, Leahy K, Eniser H, Chatterjee K, Cěrná I, Belta C.
2015. Temporal logic motion planning using POMDPs with parity objectives: Case
study paper. Proceedings of the 18th International Conference on Hybrid Systems:
Computation and Control. HSCC: Hybrid Systems - Computation and Control, 233–238.'
mla: 'Svoreňová, Mária, et al. “Temporal Logic Motion Planning Using POMDPs with
Parity Objectives: Case Study Paper.” Proceedings of the 18th International
Conference on Hybrid Systems: Computation and Control, ACM, 2015, pp. 233–38,
doi:10.1145/2728606.2728617.'
short: 'M. Svoreňová, M. Chmelik, K. Leahy, H. Eniser, K. Chatterjee, I. Cěrná,
C. Belta, in:, Proceedings of the 18th International Conference on Hybrid Systems:
Computation and Control, ACM, 2015, pp. 233–238.'
conference:
end_date: 2015-04-16
location: Seattle, WA, United States
name: 'HSCC: Hybrid Systems - Computation and Control'
start_date: 2015-04-14
date_created: 2018-12-11T11:53:29Z
date_published: 2015-04-14T00:00:00Z
date_updated: 2021-01-12T06:52:33Z
day: '14'
department:
- _id: KrCh
doi: 10.1145/2728606.2728617
ec_funded: 1
language:
- iso: eng
month: '04'
oa_version: None
page: 233 - 238
project:
- _id: 2584A770-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: P 23499-N23
name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
publication: 'Proceedings of the 18th International Conference on Hybrid Systems:
Computation and Control'
publication_status: published
publisher: ACM
publist_id: '5453'
scopus_import: 1
status: public
title: 'Temporal logic motion planning using POMDPs with parity objectives: Case study
paper'
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2015'
...
---
_id: '1694'
abstract:
- lang: eng
text: "\r\nWe introduce quantitative timed refinement and timed simulation (directed)
metrics, incorporating zenoness checks, for timed systems. These metrics assign
positive real numbers which quantify the timing mismatches between two timed systems,
amongst non-zeno runs. We quantify timing mismatches in three ways: (1) the maximal
timing mismatch that can arise, (2) the “steady-state” maximal 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 distances to within any desired degree of accuracy.
In order to compute the values of the quantitative simulation distances, 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 in graph games, and then use these algorithms
to compute the values of the timed simulation distances over timed automata.\r\n"
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 temporal simulation and refinement distances
for timed systems. IEEE Transactions on Automatic Control. 2015;60(9):2291-2306.
doi:10.1109/TAC.2015.2404612
apa: Chatterjee, K., & Prabhu, V. (2015). Quantitative temporal simulation and
refinement distances for timed systems. IEEE Transactions on Automatic Control.
IEEE. https://doi.org/10.1109/TAC.2015.2404612
chicago: Chatterjee, Krishnendu, and Vinayak Prabhu. “Quantitative Temporal Simulation
and Refinement Distances for Timed Systems.” IEEE Transactions on Automatic
Control. IEEE, 2015. https://doi.org/10.1109/TAC.2015.2404612.
ieee: K. Chatterjee and V. Prabhu, “Quantitative temporal simulation and refinement
distances for timed systems,” IEEE Transactions on Automatic Control, vol.
60, no. 9. IEEE, pp. 2291–2306, 2015.
ista: Chatterjee K, Prabhu V. 2015. Quantitative temporal simulation and refinement
distances for timed systems. IEEE Transactions on Automatic Control. 60(9), 2291–2306.
mla: Chatterjee, Krishnendu, and Vinayak Prabhu. “Quantitative Temporal Simulation
and Refinement Distances for Timed Systems.” IEEE Transactions on Automatic
Control, vol. 60, no. 9, IEEE, 2015, pp. 2291–306, doi:10.1109/TAC.2015.2404612.
short: K. Chatterjee, V. Prabhu, IEEE Transactions on Automatic Control 60 (2015)
2291–2306.
date_created: 2018-12-11T11:53:30Z
date_published: 2015-02-24T00:00:00Z
date_updated: 2021-01-12T06:52:34Z
day: '24'
department:
- _id: KrCh
doi: 10.1109/TAC.2015.2404612
ec_funded: 1
intvolume: ' 60'
issue: '9'
language:
- iso: eng
month: '02'
oa_version: None
page: 2291 - 2306
project:
- _id: 2584A770-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: P 23499-N23
name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _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: IEEE Transactions on Automatic Control
publication_status: published
publisher: IEEE
publist_id: '5450'
quality_controlled: '1'
scopus_import: 1
status: public
title: Quantitative temporal simulation and refinement distances for timed systems
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 60
year: '2015'
...
---
_id: '1698'
abstract:
- lang: eng
text: 'In mean-payoff games, the objective of the protagonist is to ensure that
the limit average of an infinite sequence of numeric weights is nonnegative. In
energy games, the objective is to ensure that the running sum of weights is always
nonnegative. Multi-mean-payoff and multi-energy games replace individual weights
by tuples, and the limit average (resp., running sum) of each coordinate must
be (resp., remain) nonnegative. We prove finite-memory determinacy of multi-energy
games and show inter-reducibility of multi-mean-payoff and multi-energy games
for finite-memory strategies. We improve the computational complexity for solving
both classes with finite-memory strategies: we prove coNP-completeness improving
the previous known EXPSPACE bound. For memoryless strategies, we show that deciding
the existence of a winning strategy for the protagonist is NP-complete. We present
the first solution of multi-mean-payoff games with infinite-memory strategies:
we show that mean-payoff-sup objectives can be decided in NP∩coNP, whereas mean-payoff-inf
objectives are coNP-complete.'
acknowledgement: 'The research was partly supported by Austrian Science Fund (FWF)
Grant No P23499-N23, FWF NFN Grant No S11407-N23 and S11402-N23 (RiSE), ERC Start
grant (279307: Graph Games), Microsoft faculty fellows award, the ERC Advanced Grant
QUAREM (267989: Quantitative Reactive Modeling), European project Cassting (FP7-601148),
ERC Start grant (279499: inVEST).'
author:
- first_name: Yaron
full_name: Velner, Yaron
last_name: Velner
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Laurent
full_name: Doyen, Laurent
last_name: Doyen
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Alexander
full_name: Rabinovich, Alexander
last_name: Rabinovich
- first_name: Jean
full_name: Raskin, Jean
last_name: Raskin
citation:
ama: Velner Y, Chatterjee K, Doyen L, Henzinger TA, Rabinovich A, Raskin J. The
complexity of multi-mean-payoff and multi-energy games. Information and Computation.
2015;241(4):177-196. doi:10.1016/j.ic.2015.03.001
apa: Velner, Y., Chatterjee, K., Doyen, L., Henzinger, T. A., Rabinovich, A., &
Raskin, J. (2015). The complexity of multi-mean-payoff and multi-energy games.
Information and Computation. Elsevier. https://doi.org/10.1016/j.ic.2015.03.001
chicago: Velner, Yaron, Krishnendu Chatterjee, Laurent Doyen, Thomas A Henzinger,
Alexander Rabinovich, and Jean Raskin. “The Complexity of Multi-Mean-Payoff and
Multi-Energy Games.” Information and Computation. Elsevier, 2015. https://doi.org/10.1016/j.ic.2015.03.001.
ieee: Y. Velner, K. Chatterjee, L. Doyen, T. A. Henzinger, A. Rabinovich, and J.
Raskin, “The complexity of multi-mean-payoff and multi-energy games,” Information
and Computation, vol. 241, no. 4. Elsevier, pp. 177–196, 2015.
ista: Velner Y, Chatterjee K, Doyen L, Henzinger TA, Rabinovich A, Raskin J. 2015.
The complexity of multi-mean-payoff and multi-energy games. Information and Computation.
241(4), 177–196.
mla: Velner, Yaron, et al. “The Complexity of Multi-Mean-Payoff and Multi-Energy
Games.” Information and Computation, vol. 241, no. 4, Elsevier, 2015, pp.
177–96, doi:10.1016/j.ic.2015.03.001.
short: Y. Velner, K. Chatterjee, L. Doyen, T.A. Henzinger, A. Rabinovich, J. Raskin,
Information and Computation 241 (2015) 177–196.
date_created: 2018-12-11T11:53:32Z
date_published: 2015-04-01T00:00:00Z
date_updated: 2021-01-12T06:52:36Z
day: '01'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1016/j.ic.2015.03.001
ec_funded: 1
intvolume: ' 241'
issue: '4'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1209.3234
month: '04'
oa: 1
oa_version: Preprint
page: 177 - 196
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: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _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
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
publication: Information and Computation
publication_status: published
publisher: Elsevier
publist_id: '5443'
quality_controlled: '1'
scopus_import: 1
status: public
title: The complexity of multi-mean-payoff and multi-energy games
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 241
year: '2015'
...
---
_id: '1709'
abstract:
- lang: eng
text: The competition for resources among cells, individuals or species is a fundamental
characteristic of evolution. Biological all-pay auctions have been used to model
situations where multiple individuals compete for a single resource. However,
in many situations multiple resources with various values exist and single reward
auctions are not applicable. We generalize the model to multiple rewards and study
the evolution of strategies. In biological all-pay auctions the bid of an individual
corresponds to its strategy and is equivalent to its payment in the auction. The
decreasingly ordered rewards are distributed according to the decreasingly ordered
bids of the participating individuals. The reproductive success of an individual
is proportional to its fitness given by the sum of the rewards won minus its payments.
Hence, successful bidding strategies spread in the population. We find that the
results for the multiple reward case are very different from the single reward
case. While the mixed strategy equilibrium in the single reward case with more
than two players consists of mostly low-bidding individuals, we show that the
equilibrium can convert to many high-bidding individuals and a few low-bidding
individuals in the multiple reward case. Some reward values lead to a specialization
among the individuals where one subpopulation competes for the rewards and the
other subpopulation largely avoids costly competitions. Whether the mixed strategy
equilibrium is an evolutionarily stable strategy (ESS) depends on the specific
values of the rewards.
acknowledgement: 'This work was supported by grants from the John Templeton Foundation,
ERC Start Grant (279307: Graph Games), FWF NFN Grant (No S11407N23 RiSE/SHiNE),
FWF Grant (No P23499N23) and a Microsoft faculty fellows award.'
article_processing_charge: No
article_type: original
author:
- first_name: Johannes
full_name: Reiter, Johannes
id: 4A918E98-F248-11E8-B48F-1D18A9856A87
last_name: Reiter
orcid: 0000-0002-0170-7353
- first_name: Ayush
full_name: Kanodia, Ayush
last_name: Kanodia
- first_name: Raghav
full_name: Gupta, Raghav
last_name: Gupta
- first_name: Martin
full_name: Nowak, Martin
last_name: Nowak
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
citation:
ama: Reiter J, Kanodia A, Gupta R, Nowak M, Chatterjee K. Biological auctions with
multiple rewards. Proceedings of the Royal Society of London Series B Biological
Sciences. 2015;282(1812). doi:10.1098/rspb.2015.1041
apa: Reiter, J., Kanodia, A., Gupta, R., Nowak, M., & Chatterjee, K. (2015).
Biological auctions with multiple rewards. Proceedings of the Royal Society
of London Series B Biological Sciences. Royal Society. https://doi.org/10.1098/rspb.2015.1041
chicago: Reiter, Johannes, Ayush Kanodia, Raghav Gupta, Martin Nowak, and Krishnendu
Chatterjee. “Biological Auctions with Multiple Rewards.” Proceedings of the
Royal Society of London Series B Biological Sciences. Royal Society, 2015.
https://doi.org/10.1098/rspb.2015.1041.
ieee: J. Reiter, A. Kanodia, R. Gupta, M. Nowak, and K. Chatterjee, “Biological
auctions with multiple rewards,” Proceedings of the Royal Society of London
Series B Biological Sciences, vol. 282, no. 1812. Royal Society, 2015.
ista: Reiter J, Kanodia A, Gupta R, Nowak M, Chatterjee K. 2015. Biological auctions
with multiple rewards. Proceedings of the Royal Society of London Series B Biological
Sciences. 282(1812).
mla: Reiter, Johannes, et al. “Biological Auctions with Multiple Rewards.” Proceedings
of the Royal Society of London Series B Biological Sciences, vol. 282, no.
1812, Royal Society, 2015, doi:10.1098/rspb.2015.1041.
short: J. Reiter, A. Kanodia, R. Gupta, M. Nowak, K. Chatterjee, Proceedings of
the Royal Society of London Series B Biological Sciences 282 (2015).
date_created: 2018-12-11T11:53:35Z
date_published: 2015-07-15T00:00:00Z
date_updated: 2023-09-07T11:40:43Z
day: '15'
department:
- _id: KrCh
doi: 10.1098/rspb.2015.1041
external_id:
pmid:
- '26180069'
intvolume: ' 282'
issue: '1812'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://www.ncbi.nlm.nih.gov/pmc/articles/PMC4528522/
month: '07'
oa: 1
oa_version: Submitted Version
pmid: 1
project:
- _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: Proceedings of the Royal Society of London Series B Biological Sciences
publication_status: published
publisher: Royal Society
publist_id: '5425'
quality_controlled: '1'
related_material:
record:
- id: '1400'
relation: dissertation_contains
status: public
scopus_import: 1
status: public
title: Biological auctions with multiple rewards
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 282
year: '2015'
...
---
_id: '1714'
abstract:
- lang: eng
text: 'We present a flexible framework for the automated competitive analysis of
on-line scheduling algorithms for firm-deadline real-time tasks based on multi-objective
graphs: Given a task set and an on-line scheduling algorithm specified as a labeled
transition system, along with some optional safety, liveness, and/or limit-average
constraints for the adversary, we automatically compute the competitive ratio
of the algorithm w.r.t. A clairvoyant scheduler. We demonstrate the flexibility
and power of our approach by comparing the competitive ratio of several on-line
algorithms, including Dover, that have been proposed in the past, for various
task sets. Our experimental results reveal that none of these algorithms is universally
optimal, in the sense that there are task sets where other schedulers provide
better performance. Our framework is hence a very useful design tool for selecting
optimal algorithms for a given application.'
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: Andreas
full_name: Pavlogiannis, Andreas
id: 49704004-F248-11E8-B48F-1D18A9856A87
last_name: Pavlogiannis
orcid: 0000-0002-8943-0722
- 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, Pavlogiannis A, Kößler A, Schmid U. A framework for automated
competitive analysis of on-line scheduling of firm-deadline tasks. In: Real-Time
Systems Symposium. Vol 2015. IEEE; 2015:118-127. doi:10.1109/RTSS.2014.9'
apa: 'Chatterjee, K., Pavlogiannis, A., Kößler, A., & Schmid, U. (2015). A framework
for automated competitive analysis of on-line scheduling of firm-deadline tasks.
In Real-Time Systems Symposium (Vol. 2015, pp. 118–127). Rome, Italy: IEEE.
https://doi.org/10.1109/RTSS.2014.9'
chicago: Chatterjee, Krishnendu, Andreas Pavlogiannis, Alexander Kößler, and Ulrich
Schmid. “A Framework for Automated Competitive Analysis of On-Line Scheduling
of Firm-Deadline Tasks.” In Real-Time Systems Symposium, 2015:118–27. IEEE,
2015. https://doi.org/10.1109/RTSS.2014.9.
ieee: K. Chatterjee, A. Pavlogiannis, A. Kößler, and U. Schmid, “A framework for
automated competitive analysis of on-line scheduling of firm-deadline tasks,”
in Real-Time Systems Symposium, Rome, Italy, 2015, vol. 2015, no. January,
pp. 118–127.
ista: 'Chatterjee K, Pavlogiannis A, Kößler A, Schmid U. 2015. A framework for automated
competitive analysis of on-line scheduling of firm-deadline tasks. Real-Time Systems
Symposium. RTSS: Real-Time Systems Symposium vol. 2015, 118–127.'
mla: Chatterjee, Krishnendu, et al. “A Framework for Automated Competitive Analysis
of On-Line Scheduling of Firm-Deadline Tasks.” Real-Time Systems Symposium,
vol. 2015, no. January, IEEE, 2015, pp. 118–27, doi:10.1109/RTSS.2014.9.
short: K. Chatterjee, A. Pavlogiannis, A. Kößler, U. Schmid, in:, Real-Time Systems
Symposium, IEEE, 2015, pp. 118–127.
conference:
end_date: 2014-12-05
location: Rome, Italy
name: 'RTSS: Real-Time Systems Symposium'
start_date: 2014-12-02
date_created: 2018-12-11T11:53:37Z
date_published: 2015-01-15T00:00:00Z
date_updated: 2023-09-07T12:01:59Z
day: '15'
department:
- _id: KrCh
doi: 10.1109/RTSS.2014.9
intvolume: ' 2015'
issue: January
language:
- iso: eng
month: '01'
oa_version: None
page: 118 - 127
publication: Real-Time Systems Symposium
publication_status: published
publisher: IEEE
publist_id: '5417'
quality_controlled: '1'
related_material:
record:
- id: '5423'
relation: earlier_version
status: public
- id: '821'
relation: dissertation_contains
status: public
scopus_import: 1
status: public
title: A framework for automated competitive analysis of on-line scheduling of firm-deadline
tasks
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 2015
year: '2015'
...
---
_id: '1731'
abstract:
- lang: eng
text: 'We consider two-player zero-sum games on graphs. These games can be classified
on the basis of the information of the players and on the mode of interaction
between them. On the basis of information the classification is as follows: (a)
partial-observation (both players have partial view of the game); (b) one-sided
complete-observation (one player has complete observation); and (c) complete-observation
(both players have complete view of the game). On the basis of mode of interaction
we have the following classification: (a) concurrent (both players interact simultaneously);
and (b) turn-based (both players interact in turn). The two sources of randomness
in these games are randomness in transition function and randomness in strategies.
In general, randomized strategies are more powerful than deterministic strategies,
and randomness in transitions gives more general classes of games. In this work
we present a complete characterization for the classes of games where randomness
is not helpful in: (a) the transition function probabilistic transition can be
simulated by deterministic transition); and (b) strategies (pure strategies are
as powerful as randomized strategies). As consequence of our characterization
we obtain new undecidability results for these 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: Laurent
full_name: Doyen, Laurent
last_name: Doyen
- first_name: Hugo
full_name: Gimbert, Hugo
last_name: Gimbert
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
citation:
ama: Chatterjee K, Doyen L, Gimbert H, Henzinger TA. Randomness for free. Information
and Computation. 2015;245(12):3-16. doi:10.1016/j.ic.2015.06.003
apa: Chatterjee, K., Doyen, L., Gimbert, H., & Henzinger, T. A. (2015). Randomness
for free. Information and Computation. Elsevier. https://doi.org/10.1016/j.ic.2015.06.003
chicago: Chatterjee, Krishnendu, Laurent Doyen, Hugo Gimbert, and Thomas A Henzinger.
“Randomness for Free.” Information and Computation. Elsevier, 2015. https://doi.org/10.1016/j.ic.2015.06.003.
ieee: K. Chatterjee, L. Doyen, H. Gimbert, and T. A. Henzinger, “Randomness for
free,” Information and Computation, vol. 245, no. 12. Elsevier, pp. 3–16,
2015.
ista: Chatterjee K, Doyen L, Gimbert H, Henzinger TA. 2015. Randomness for free.
Information and Computation. 245(12), 3–16.
mla: Chatterjee, Krishnendu, et al. “Randomness for Free.” Information and Computation,
vol. 245, no. 12, Elsevier, 2015, pp. 3–16, doi:10.1016/j.ic.2015.06.003.
short: K. Chatterjee, L. Doyen, H. Gimbert, T.A. Henzinger, Information and Computation
245 (2015) 3–16.
date_created: 2018-12-11T11:53:42Z
date_published: 2015-12-01T00:00:00Z
date_updated: 2023-02-23T11:45:42Z
day: '01'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1016/j.ic.2015.06.003
ec_funded: 1
intvolume: ' 245'
issue: '12'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1006.0673
month: '12'
oa: 1
oa_version: Preprint
page: 3 - 16
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
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _id: 25EFB36C-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '215543'
name: COMponent-Based Embedded Systems design Techniques
- _id: 25F1337C-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '214373'
name: Design for Embedded Systems
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
publication: Information and Computation
publication_status: published
publisher: Elsevier
publist_id: '5395'
quality_controlled: '1'
related_material:
record:
- id: '3856'
relation: earlier_version
status: public
scopus_import: 1
status: public
title: Randomness for free
type: journal_article
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 245
year: '2015'
...
---
_id: '1732'
abstract:
- lang: eng
text: We consider partially observable Markov decision processes (POMDPs), that
are a standard framework for robotics applications to model uncertainties present
in the real world, with temporal logic specifications. All temporal logic specifications
in linear-time temporal logic (LTL) can be expressed as parity objectives. We
study the qualitative analysis problem for POMDPs with parity objectives that
asks whether there is a controller (policy) to ensure that the objective holds
with probability 1 (almost-surely). While the qualitative analysis of POMDPs with
parity objectives is undecidable, recent results show that when restricted to
finite-memory policies the problem is EXPTIME-complete. While the problem is intractable
in theory, we present a practical approach to solve the qualitative analysis problem.
We designed several heuristics to deal with the exponential complexity, and have
used our implementation on a number of well-known POMDP examples for robotics
applications. Our results provide the first practical approach to solve the qualitative
analysis of robot motion planning with LTL properties in the presence of uncertainty.
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: Martin
full_name: Chmelik, Martin
id: 3624234E-F248-11E8-B48F-1D18A9856A87
last_name: Chmelik
- first_name: Raghav
full_name: Gupta, Raghav
last_name: Gupta
- first_name: Ayush
full_name: Kanodia, Ayush
last_name: Kanodia
citation:
ama: 'Chatterjee K, Chmelik M, Gupta R, Kanodia A. Qualitative analysis of POMDPs
with temporal logic specifications for robotics applications. In: IEEE; 2015:325-330.
doi:10.1109/ICRA.2015.7139019'
apa: 'Chatterjee, K., Chmelik, M., Gupta, R., & Kanodia, A. (2015). Qualitative
analysis of POMDPs with temporal logic specifications for robotics applications
(pp. 325–330). Presented at the ICRA: International Conference on Robotics and
Automation, Seattle, WA, United States: IEEE. https://doi.org/10.1109/ICRA.2015.7139019'
chicago: Chatterjee, Krishnendu, Martin Chmelik, Raghav Gupta, and Ayush Kanodia.
“Qualitative Analysis of POMDPs with Temporal Logic Specifications for Robotics
Applications,” 325–30. IEEE, 2015. https://doi.org/10.1109/ICRA.2015.7139019.
ieee: 'K. Chatterjee, M. Chmelik, R. Gupta, and A. Kanodia, “Qualitative analysis
of POMDPs with temporal logic specifications for robotics applications,” presented
at the ICRA: International Conference on Robotics and Automation, Seattle, WA,
United States, 2015, pp. 325–330.'
ista: 'Chatterjee K, Chmelik M, Gupta R, Kanodia A. 2015. Qualitative analysis of
POMDPs with temporal logic specifications for robotics applications. ICRA: International
Conference on Robotics and Automation, 325–330.'
mla: Chatterjee, Krishnendu, et al. Qualitative Analysis of POMDPs with Temporal
Logic Specifications for Robotics Applications. IEEE, 2015, pp. 325–30, doi:10.1109/ICRA.2015.7139019.
short: K. Chatterjee, M. Chmelik, R. Gupta, A. Kanodia, in:, IEEE, 2015, pp. 325–330.
conference:
end_date: 2015-05-30
location: Seattle, WA, United States
name: 'ICRA: International Conference on Robotics and Automation'
start_date: 2015-05-26
date_created: 2018-12-11T11:53:43Z
date_published: 2015-01-01T00:00:00Z
date_updated: 2023-02-23T12:25:52Z
day: '01'
department:
- _id: KrCh
doi: 10.1109/ICRA.2015.7139019
ec_funded: 1
external_id:
arxiv:
- '1409.3360'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1409.3360
month: '01'
oa: 1
oa_version: Preprint
page: 325 - 330
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'
publication_status: published
publisher: IEEE
publist_id: '5394'
quality_controlled: '1'
related_material:
record:
- id: '5424'
relation: earlier_version
status: public
- id: '5426'
relation: earlier_version
status: public
scopus_import: 1
status: public
title: Qualitative analysis of POMDPs with temporal logic specifications for robotics
applications
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2015'
...
---
_id: '1820'
abstract:
- lang: eng
text: 'We consider partially observable Markov decision processes (POMDPs) with
a set of target states and every transition is associated with an integer cost.
The optimization objec- tive we study asks to minimize the expected total cost
till the target set is reached, while ensuring that the target set is reached
almost-surely (with probability 1). We show that for integer costs approximating
the optimal cost is undecidable. For positive costs, our results are as follows:
(i) we establish matching lower and upper bounds for the optimal cost and the
bound is double exponential; (ii) we show that the problem of approximating the
optimal cost is decidable and present ap- proximation algorithms developing on
the existing algorithms for POMDPs with finite-horizon objectives. While the worst-
case running time of our algorithm is double exponential, we present efficient
stopping criteria for the algorithm and show experimentally that it performs well
in many examples.'
acknowledgement: ' The research was partly supported by Austrian Science Fund (FWF)
Grant No P23499-N23, FWF NFN Grant No S11407-N23 (RiSE), ERC Start grant (279307:
Graph Games), and Microsoft faculty fellows award.'
alternative_title:
- Artifical Intelligence
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: Martin
full_name: Chmelik, Martin
id: 3624234E-F248-11E8-B48F-1D18A9856A87
last_name: Chmelik
- first_name: Raghav
full_name: Gupta, Raghav
last_name: Gupta
- first_name: Ayush
full_name: Kanodia, Ayush
last_name: Kanodia
citation:
ama: 'Chatterjee K, Chmelik M, Gupta R, Kanodia A. Optimal cost almost-sure reachability
in POMDPs. In: Proceedings of the Twenty-Ninth AAAI Conference on Artificial
Intelligence . Vol 5. AAAI Press; 2015:3496-3502.'
apa: 'Chatterjee, K., Chmelik, M., Gupta, R., & Kanodia, A. (2015). Optimal
cost almost-sure reachability in POMDPs. In Proceedings of the Twenty-Ninth
AAAI Conference on Artificial Intelligence (Vol. 5, pp. 3496–3502). Austin,
TX, USA: AAAI Press.'
chicago: Chatterjee, Krishnendu, Martin Chmelik, Raghav Gupta, and Ayush Kanodia.
“Optimal Cost Almost-Sure Reachability in POMDPs.” In Proceedings of the Twenty-Ninth
AAAI Conference on Artificial Intelligence , 5:3496–3502. AAAI Press, 2015.
ieee: K. Chatterjee, M. Chmelik, R. Gupta, and A. Kanodia, “Optimal cost almost-sure
reachability in POMDPs,” in Proceedings of the Twenty-Ninth AAAI Conference
on Artificial Intelligence , Austin, TX, USA, 2015, vol. 5, pp. 3496–3502.
ista: 'Chatterjee K, Chmelik M, Gupta R, Kanodia A. 2015. Optimal cost almost-sure
reachability in POMDPs. Proceedings of the Twenty-Ninth AAAI Conference on Artificial
Intelligence . IAAI: Innovative Applications of Artificial Intelligence, Artifical
Intelligence, vol. 5, 3496–3502.'
mla: Chatterjee, Krishnendu, et al. “Optimal Cost Almost-Sure Reachability in POMDPs.”
Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence
, vol. 5, AAAI Press, 2015, pp. 3496–502.
short: K. Chatterjee, M. Chmelik, R. Gupta, A. Kanodia, in:, Proceedings of the
Twenty-Ninth AAAI Conference on Artificial Intelligence , AAAI Press, 2015, pp.
3496–3502.
conference:
end_date: 2015-01-30
location: Austin, TX, USA
name: 'IAAI: Innovative Applications of Artificial Intelligence'
start_date: 2015-01-25
date_created: 2018-12-11T11:54:11Z
date_published: 2015-06-01T00:00:00Z
date_updated: 2023-02-23T10:02:57Z
day: '01'
department:
- _id: KrCh
ec_funded: 1
external_id:
arxiv:
- '1411.3880'
intvolume: ' 5'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1411.3880
month: '06'
oa: 1
oa_version: Preprint
page: 3496-3502
project:
- _id: 2584A770-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: P 23499-N23
name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
publication: 'Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence '
publication_status: published
publisher: AAAI Press
publist_id: '5286'
quality_controlled: '1'
related_material:
record:
- id: '1529'
relation: later_version
status: public
scopus_import: 1
status: public
title: Optimal cost almost-sure reachability in POMDPs
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 5
year: '2015'
...
---
_id: '1838'
abstract:
- lang: eng
text: Synthesis of program parts is particularly useful for concurrent systems.
However, most approaches do not support common design tasks, like modifying a
single process without having to re-synthesize or verify the whole system. Assume-guarantee
synthesis (AGS) provides robustness against modifications of system parts, but
thus far has been limited to the perfect information setting. This means that
local variables cannot be hidden from other processes, which renders synthesis
results cumbersome or even impossible to realize.We resolve this shortcoming by
defining AGS under partial information. We analyze the complexity and decidability
in different settings, showing that the problem has a high worstcase complexity
and is undecidable in many interesting cases. Based on these observations, we
present a pragmatic algorithm based on bounded synthesis, and demonstrate its
practical applicability on several examples.
acknowledgement: 'This work was supported by the Austrian Science Fund (FWF) through
the research network RiSE (S11406-N23, S11407-N23) and grant nr. P23499-N23, by
the European Commission through an ERC Start grant (279307: Graph Games) and project
STANCE (317753), as well as by the German Research Foundation (DFG) through SFB/TR
14 AVACS and project ASDPS(JA 2357/2-1).'
alternative_title:
- LNCS
author:
- first_name: Roderick
full_name: Bloem, Roderick
last_name: Bloem
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Swen
full_name: Jacobs, Swen
last_name: Jacobs
- first_name: Robert
full_name: Könighofer, Robert
last_name: Könighofer
citation:
ama: 'Bloem R, Chatterjee K, Jacobs S, Könighofer R. Assume-guarantee synthesis
for concurrent reactive programs with partial information. In: Vol 9035. Springer;
2015:517-532. doi:10.1007/978-3-662-46681-0_50'
apa: 'Bloem, R., Chatterjee, K., Jacobs, S., & Könighofer, R. (2015). Assume-guarantee
synthesis for concurrent reactive programs with partial information (Vol. 9035,
pp. 517–532). Presented at the TACAS: Tools and Algorithms for the Construction
and Analysis of Systems, London, United Kingdom: Springer. https://doi.org/10.1007/978-3-662-46681-0_50'
chicago: Bloem, Roderick, Krishnendu Chatterjee, Swen Jacobs, and Robert Könighofer.
“Assume-Guarantee Synthesis for Concurrent Reactive Programs with Partial Information,”
9035:517–32. Springer, 2015. https://doi.org/10.1007/978-3-662-46681-0_50.
ieee: 'R. Bloem, K. Chatterjee, S. Jacobs, and R. Könighofer, “Assume-guarantee
synthesis for concurrent reactive programs with partial information,” presented
at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems,
London, United Kingdom, 2015, vol. 9035, pp. 517–532.'
ista: 'Bloem R, Chatterjee K, Jacobs S, Könighofer R. 2015. Assume-guarantee synthesis
for concurrent reactive programs with partial information. TACAS: Tools and Algorithms
for the Construction and Analysis of Systems, LNCS, vol. 9035, 517–532.'
mla: Bloem, Roderick, et al. Assume-Guarantee Synthesis for Concurrent Reactive
Programs with Partial Information. Vol. 9035, Springer, 2015, pp. 517–32,
doi:10.1007/978-3-662-46681-0_50.
short: R. Bloem, K. Chatterjee, S. Jacobs, R. Könighofer, in:, Springer, 2015, pp.
517–532.
conference:
end_date: 2015-04-18
location: London, United Kingdom
name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
start_date: 2015-04-11
date_created: 2018-12-11T11:54:17Z
date_published: 2015-01-01T00:00:00Z
date_updated: 2021-01-12T06:53:32Z
day: '01'
department:
- _id: KrCh
doi: 10.1007/978-3-662-46681-0_50
ec_funded: 1
intvolume: ' 9035'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1411.4604
month: '01'
oa: 1
oa_version: Preprint
page: 517 - 532
project:
- _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: 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: '5264'
scopus_import: 1
status: public
title: Assume-guarantee synthesis for concurrent reactive programs with partial information
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 9035
year: '2015'
...
---
_id: '1839'
abstract:
- lang: eng
text: We present MultiGain, a tool to synthesize strategies for Markov decision
processes (MDPs) with multiple mean-payoff objectives. Our models are described
in PRISM, and our tool uses the existing interface and simulator of PRISM. Our
tool extends PRISM by adding novel algorithms for multiple mean-payoff objectives,
and also provides features such as (i) generating strategies and exploring them
for simulation, and checking them with respect to other properties; and (ii) generating
an approximate Pareto curve for two mean-payoff objectives. In addition, we present
a new practical algorithm for the analysis of MDPs with multiple mean-payoff objectives
under memoryless strategies.
alternative_title:
- LNCS
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. Multigain: A controller synthesis
tool for MDPs with multiple mean-payoff objectives. 2015;9035:181-187. doi:10.1007/978-3-662-46681-0_12'
apa: 'Brázdil, T., Chatterjee, K., Forejt, V., & Kučera, A. (2015). Multigain:
A controller synthesis tool for MDPs with multiple mean-payoff objectives. Presented
at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems,
London, United Kingdom: Springer. https://doi.org/10.1007/978-3-662-46681-0_12'
chicago: 'Brázdil, Tomáš, Krishnendu Chatterjee, Vojtěch Forejt, and Antonín Kučera.
“Multigain: A Controller Synthesis Tool for MDPs with Multiple Mean-Payoff Objectives.”
Lecture Notes in Computer Science. Springer, 2015. https://doi.org/10.1007/978-3-662-46681-0_12.'
ieee: 'T. Brázdil, K. Chatterjee, V. Forejt, and A. Kučera, “Multigain: A controller
synthesis tool for MDPs with multiple mean-payoff objectives,” vol. 9035. Springer,
pp. 181–187, 2015.'
ista: 'Brázdil T, Chatterjee K, Forejt V, Kučera A. 2015. Multigain: A controller
synthesis tool for MDPs with multiple mean-payoff objectives. 9035, 181–187.'
mla: 'Brázdil, Tomáš, et al. Multigain: A Controller Synthesis Tool for MDPs
with Multiple Mean-Payoff Objectives. Vol. 9035, Springer, 2015, pp. 181–87,
doi:10.1007/978-3-662-46681-0_12.'
short: T. Brázdil, K. Chatterjee, V. Forejt, A. Kučera, 9035 (2015) 181–187.
conference:
end_date: 2015-04-18
location: London, United Kingdom
name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
start_date: 2015-04-11
date_created: 2018-12-11T11:54:18Z
date_published: 2015-01-01T00:00:00Z
date_updated: 2020-01-21T13:18:52Z
day: '01'
department:
- _id: KrCh
doi: 10.1007/978-3-662-46681-0_12
ec_funded: 1
intvolume: ' 9035'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1501.03093
month: '01'
oa: 1
oa_version: Preprint
page: 181 - 187
project:
- _id: 2584A770-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: P 23499-N23
name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _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: '5263'
quality_controlled: '1'
series_title: Lecture Notes in Computer Science
status: public
title: 'Multigain: A controller synthesis tool for MDPs with multiple mean-payoff
objectives'
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 9035
year: '2015'
...
---
_id: '1846'
abstract:
- lang: eng
text: Modal transition systems (MTS) is a well-studied specification formalism of
reactive systems supporting a step-wise refinement methodology. Despite its many
advantages, the formalism as well as its currently known extensions are incapable
of expressing some practically needed aspects in the refinement process like exclusive,
conditional and persistent choices. We introduce a new model called parametric
modal transition systems (PMTS) together with a general modal refinement notion
that overcomes many of the limitations. We investigate the computational complexity
of modal and thorough refinement checking on PMTS and its subclasses and provide
a direct encoding of the modal refinement problem into quantified Boolean formulae,
allowing us to employ state-of-the-art QBF solvers for modal refinement checking.
The experiments we report on show that the feasibility of refinement checking
is more influenced by the degree of nondeterminism rather than by the syntactic
restrictions on the types of formulae allowed in the description of the PMTS.
article_processing_charge: No
article_type: original
author:
- first_name: Nikola
full_name: Beneš, Nikola
last_name: Beneš
- first_name: Jan
full_name: Kretinsky, Jan
id: 44CEF464-F248-11E8-B48F-1D18A9856A87
last_name: Kretinsky
orcid: 0000-0002-8122-2881
- first_name: Kim
full_name: Larsen, Kim
last_name: Larsen
- first_name: Mikael
full_name: Möller, Mikael
last_name: Möller
- first_name: Salomon
full_name: Sickert, Salomon
last_name: Sickert
- first_name: Jiří
full_name: Srba, Jiří
last_name: Srba
citation:
ama: Beneš N, Kretinsky J, Larsen K, Möller M, Sickert S, Srba J. Refinement checking
on parametric modal transition systems. Acta Informatica. 2015;52(2-3):269-297.
doi:10.1007/s00236-015-0215-4
apa: Beneš, N., Kretinsky, J., Larsen, K., Möller, M., Sickert, S., & Srba,
J. (2015). Refinement checking on parametric modal transition systems. Acta
Informatica. Springer. https://doi.org/10.1007/s00236-015-0215-4
chicago: Beneš, Nikola, Jan Kretinsky, Kim Larsen, Mikael Möller, Salomon Sickert,
and Jiří Srba. “Refinement Checking on Parametric Modal Transition Systems.” Acta
Informatica. Springer, 2015. https://doi.org/10.1007/s00236-015-0215-4.
ieee: N. Beneš, J. Kretinsky, K. Larsen, M. Möller, S. Sickert, and J. Srba, “Refinement
checking on parametric modal transition systems,” Acta Informatica, vol.
52, no. 2–3. Springer, pp. 269–297, 2015.
ista: Beneš N, Kretinsky J, Larsen K, Möller M, Sickert S, Srba J. 2015. Refinement
checking on parametric modal transition systems. Acta Informatica. 52(2–3), 269–297.
mla: Beneš, Nikola, et al. “Refinement Checking on Parametric Modal Transition Systems.”
Acta Informatica, vol. 52, no. 2–3, Springer, 2015, pp. 269–97, doi:10.1007/s00236-015-0215-4.
short: N. Beneš, J. Kretinsky, K. Larsen, M. Möller, S. Sickert, J. Srba, Acta Informatica
52 (2015) 269–297.
date_created: 2018-12-11T11:54:20Z
date_published: 2015-04-01T00:00:00Z
date_updated: 2021-01-12T06:53:35Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
- _id: KrCh
doi: 10.1007/s00236-015-0215-4
ec_funded: 1
file:
- access_level: open_access
checksum: fb4037ddc4fc05f33080dd3547ede350
content_type: application/pdf
creator: dernst
date_created: 2020-05-15T08:57:44Z
date_updated: 2020-07-14T12:45:19Z
file_id: '7854'
file_name: 2015_ActaInfo_Benes.pdf
file_size: 488482
relation: main_file
file_date_updated: 2020-07-14T12:45:19Z
has_accepted_license: '1'
intvolume: ' 52'
issue: 2-3
language:
- iso: eng
month: '04'
oa: 1
oa_version: Submitted Version
page: 269 - 297
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
publication: Acta Informatica
publication_status: published
publisher: Springer
publist_id: '5255'
quality_controlled: '1'
scopus_import: 1
status: public
title: Refinement checking on parametric modal transition systems
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 52
year: '2015'
...
---
_id: '1851'
abstract:
- lang: eng
text: We consider mating strategies for females who search for males sequentially
during a season of limited length. We show that the best strategy rejects a given
male type if encountered before a time-threshold but accepts him after. For frequency-independent
benefits, we obtain the optimal time-thresholds explicitly for both discrete and
continuous distributions of males, and allow for mistakes being made in assessing
the correct male type. When the benefits are indirect (genes for the offspring)
and the population is under frequency-dependent ecological selection, the benefits
depend on the mating strategy of other females as well. This case is particularly
relevant to speciation models that seek to explore the stability of reproductive
isolation by assortative mating under frequency-dependent ecological selection.
We show that the indirect benefits are to be quantified by the reproductive values
of couples, and describe how the evolutionarily stable time-thresholds can be
found. We conclude with an example based on the Levene model, in which we analyze
the evolutionarily stable assortative mating strategies and the strength of reproductive
isolation provided by them.
article_processing_charge: No
article_type: original
author:
- first_name: Tadeas
full_name: Priklopil, Tadeas
id: 3C869AA0-F248-11E8-B48F-1D18A9856A87
last_name: Priklopil
- first_name: Eva
full_name: Kisdi, Eva
last_name: Kisdi
- first_name: Mats
full_name: Gyllenberg, Mats
last_name: Gyllenberg
citation:
ama: Priklopil T, Kisdi E, Gyllenberg M. Evolutionarily stable mating decisions
for sequentially searching females and the stability of reproductive isolation
by assortative mating. Evolution. 2015;69(4):1015-1026. doi:10.1111/evo.12618
apa: Priklopil, T., Kisdi, E., & Gyllenberg, M. (2015). Evolutionarily stable
mating decisions for sequentially searching females and the stability of reproductive
isolation by assortative mating. Evolution. Wiley. https://doi.org/10.1111/evo.12618
chicago: Priklopil, Tadeas, Eva Kisdi, and Mats Gyllenberg. “Evolutionarily Stable
Mating Decisions for Sequentially Searching Females and the Stability of Reproductive
Isolation by Assortative Mating.” Evolution. Wiley, 2015. https://doi.org/10.1111/evo.12618.
ieee: T. Priklopil, E. Kisdi, and M. Gyllenberg, “Evolutionarily stable mating decisions
for sequentially searching females and the stability of reproductive isolation
by assortative mating,” Evolution, vol. 69, no. 4. Wiley, pp. 1015–1026,
2015.
ista: Priklopil T, Kisdi E, Gyllenberg M. 2015. Evolutionarily stable mating decisions
for sequentially searching females and the stability of reproductive isolation
by assortative mating. Evolution. 69(4), 1015–1026.
mla: Priklopil, Tadeas, et al. “Evolutionarily Stable Mating Decisions for Sequentially
Searching Females and the Stability of Reproductive Isolation by Assortative Mating.”
Evolution, vol. 69, no. 4, Wiley, 2015, pp. 1015–26, doi:10.1111/evo.12618.
short: T. Priklopil, E. Kisdi, M. Gyllenberg, Evolution 69 (2015) 1015–1026.
date_created: 2018-12-11T11:54:21Z
date_published: 2015-02-09T00:00:00Z
date_updated: 2022-06-07T10:52:37Z
day: '09'
ddc:
- '570'
department:
- _id: NiBa
- _id: KrCh
doi: 10.1111/evo.12618
ec_funded: 1
external_id:
pmid:
- '25662095'
file:
- access_level: open_access
checksum: 1e8be0b1d7598a78cd2623d8ee8e7798
content_type: application/pdf
creator: dernst
date_created: 2020-05-15T09:05:34Z
date_updated: 2020-07-14T12:45:19Z
file_id: '7855'
file_name: 2015_Evolution_Priklopil.pdf
file_size: 967214
relation: main_file
file_date_updated: 2020-07-14T12:45:19Z
has_accepted_license: '1'
intvolume: ' 69'
issue: '4'
language:
- iso: eng
month: '02'
oa: 1
oa_version: Submitted Version
page: 1015 - 1026
pmid: 1
project:
- _id: 25681D80-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '291734'
name: International IST Postdoc Fellowship Programme
publication: Evolution
publication_identifier:
eissn:
- 1558-5646
issn:
- 0014-3820
publication_status: published
publisher: Wiley
publist_id: '5249'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Evolutionarily stable mating decisions for sequentially searching females and
the stability of reproductive isolation by assortative mating
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 69
year: '2015'
...
---
_id: '1856'
abstract:
- lang: eng
text: 'The traditional synthesis question given a specification asks for the automatic
construction of a system that satisfies the specification, whereas often there
exists a preference order among the different systems that satisfy the given specification.
Under a probabilistic assumption about the possible inputs, such a preference
order is naturally expressed by a weighted automaton, which assigns to each word
a value, such that a system is preferred if it generates a higher expected value.
We solve the following optimal synthesis problem: given an omega-regular specification,
a Markov chain that describes the distribution of inputs, and a weighted automaton
that measures how well a system satisfies the given specification under the input
assumption, synthesize a system that optimizes the measured value. For safety
specifications and quantitative measures that are defined by mean-payoff automata,
the optimal synthesis problem reduces to finding a strategy in a Markov decision
process (MDP) that is optimal for a long-run average reward objective, which can
be achieved in polynomial time. For general omega-regular specifications along
with mean-payoff automata, the solution rests on a new, polynomial-time algorithm
for computing optimal strategies in MDPs with mean-payoff parity objectives. Our
algorithm constructs optimal strategies that consist of two memoryless strategies
and a counter. The counter is in general not bounded. To obtain a finite-state
system, we show how to construct an ε-optimal strategy with a bounded counter,
for all ε > 0. Furthermore, we show how to decide in polynomial time if it
is possible to construct an optimal finite-state system (i.e., a system without
a counter) for a given specification. We have implemented our approach and the
underlying algorithms in a tool that takes qualitative and quantitative specifications
and automatically constructs a system that satisfies the qualitative specification
and optimizes the quantitative specification, if such a system exists. We present
some experimental results showing optimal systems that were automatically generated
in this way.'
article_number: '9'
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Barbara
full_name: Jobstmann, Barbara
last_name: Jobstmann
- first_name: Rohit
full_name: Singh, Rohit
last_name: Singh
citation:
ama: Chatterjee K, Henzinger TA, Jobstmann B, Singh R. Measuring and synthesizing
systems in probabilistic environments. Journal of the ACM. 2015;62(1).
doi:10.1145/2699430
apa: Chatterjee, K., Henzinger, T. A., Jobstmann, B., & Singh, R. (2015). Measuring
and synthesizing systems in probabilistic environments. Journal of the ACM.
ACM. https://doi.org/10.1145/2699430
chicago: Chatterjee, Krishnendu, Thomas A Henzinger, Barbara Jobstmann, and Rohit
Singh. “Measuring and Synthesizing Systems in Probabilistic Environments.” Journal
of the ACM. ACM, 2015. https://doi.org/10.1145/2699430.
ieee: K. Chatterjee, T. A. Henzinger, B. Jobstmann, and R. Singh, “Measuring and
synthesizing systems in probabilistic environments,” Journal of the ACM,
vol. 62, no. 1. ACM, 2015.
ista: Chatterjee K, Henzinger TA, Jobstmann B, Singh R. 2015. Measuring and synthesizing
systems in probabilistic environments. Journal of the ACM. 62(1), 9.
mla: Chatterjee, Krishnendu, et al. “Measuring and Synthesizing Systems in Probabilistic
Environments.” Journal of the ACM, vol. 62, no. 1, 9, ACM, 2015, doi:10.1145/2699430.
short: K. Chatterjee, T.A. Henzinger, B. Jobstmann, R. Singh, Journal of the ACM
62 (2015).
date_created: 2018-12-11T11:54:23Z
date_published: 2015-02-01T00:00:00Z
date_updated: 2023-02-23T11:46:04Z
day: '01'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1145/2699430
ec_funded: 1
intvolume: ' 62'
issue: '1'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1004.0739
month: '02'
oa: 1
oa_version: Preprint
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _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 the ACM
publication_status: published
publisher: ACM
publist_id: '5244'
quality_controlled: '1'
related_material:
record:
- id: '3864'
relation: earlier_version
status: public
scopus_import: 1
status: public
title: Measuring and synthesizing systems in probabilistic environments
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 62
year: '2015'
...
---
_id: '1873'
abstract:
- lang: eng
text: 'We consider partially observable Markov decision processes (POMDPs) with
limit-average payoff, where a reward value in the interval [0,1] is associated
with every transition, and the payoff of an infinite path is the long-run average
of the rewards. We consider two types of path constraints: (i) a quantitative
constraint defines the set of paths where the payoff is at least a given threshold
λ1ε(0,1]; and (ii) a qualitative constraint which is a special case of the quantitative
constraint with λ1=1. We consider the computation of the almost-sure winning set,
where the controller needs to ensure that the path constraint is satisfied with
probability 1. Our main results for qualitative path constraints are as follows:
(i) the problem of deciding the existence of a finite-memory controller is EXPTIME-complete;
and (ii) the problem of deciding the existence of an infinite-memory controller
is undecidable. For quantitative path constraints we show that the problem of
deciding the existence of a finite-memory controller is undecidable. We also present
a prototype implementation of our EXPTIME algorithm and experimental results on
several examples.'
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: Martin
full_name: Chmelik, Martin
id: 3624234E-F248-11E8-B48F-1D18A9856A87
last_name: Chmelik
citation:
ama: Chatterjee K, Chmelik M. POMDPs under probabilistic semantics. Artificial
Intelligence. 2015;221:46-72. doi:10.1016/j.artint.2014.12.009
apa: Chatterjee, K., & Chmelik, M. (2015). POMDPs under probabilistic semantics.
Artificial Intelligence. Elsevier. https://doi.org/10.1016/j.artint.2014.12.009
chicago: Chatterjee, Krishnendu, and Martin Chmelik. “POMDPs under Probabilistic
Semantics.” Artificial Intelligence. Elsevier, 2015. https://doi.org/10.1016/j.artint.2014.12.009.
ieee: K. Chatterjee and M. Chmelik, “POMDPs under probabilistic semantics,” Artificial
Intelligence, vol. 221. Elsevier, pp. 46–72, 2015.
ista: Chatterjee K, Chmelik M. 2015. POMDPs under probabilistic semantics. Artificial
Intelligence. 221, 46–72.
mla: Chatterjee, Krishnendu, and Martin Chmelik. “POMDPs under Probabilistic Semantics.”
Artificial Intelligence, vol. 221, Elsevier, 2015, pp. 46–72, doi:10.1016/j.artint.2014.12.009.
short: K. Chatterjee, M. Chmelik, Artificial Intelligence 221 (2015) 46–72.
date_created: 2018-12-11T11:54:28Z
date_published: 2015-04-01T00:00:00Z
date_updated: 2021-01-12T06:53:46Z
day: '01'
department:
- _id: KrCh
doi: 10.1016/j.artint.2014.12.009
external_id:
arxiv:
- '1408.2058'
intvolume: ' 221'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1408.2058
month: '04'
oa: 1
oa_version: Preprint
page: 46 - 72
publication: Artificial Intelligence
publication_status: published
publisher: Elsevier
publist_id: '5224'
quality_controlled: '1'
scopus_import: 1
status: public
title: POMDPs under probabilistic semantics
type: journal_article
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 221
year: '2015'
...
---
_id: '1882'
abstract:
- lang: eng
text: We provide a framework for compositional and iterative design and verification
of systems with quantitative information, such as rewards, time or energy. It
is based on disjunctive modal transition systems where we allow actions to bear
various types of quantitative information. Throughout the design process the actions
can be further refined and the information made more precise. We show how to compute
the results of standard operations on the systems, including the quotient (residual),
which has not been previously considered for quantitative non-deterministic systems.
Our quantitative framework has close connections to the modal nu-calculus and
is compositional with respect to general notions of distances between systems
and the standard operations.
acknowledgement: This research was funded in part by the European Research Council
(ERC) under grant agreement 267989 (QUAREM), by the Austrian Science Fund (FWF)
project S11402-N23 (RiSE), and by the Czech Science Foundation, grant No. P202/12/G061.
alternative_title:
- LNCS
author:
- first_name: Uli
full_name: Fahrenberg, Uli
last_name: Fahrenberg
- first_name: Jan
full_name: Kretinsky, Jan
id: 44CEF464-F248-11E8-B48F-1D18A9856A87
last_name: Kretinsky
orcid: 0000-0002-8122-2881
- first_name: Axel
full_name: Legay, Axel
last_name: Legay
- first_name: Louis
full_name: Traonouez, Louis
last_name: Traonouez
citation:
ama: 'Fahrenberg U, Kretinsky J, Legay A, Traonouez L. Compositionality for quantitative
specifications. In: Vol 8997. Springer; 2015:306-324. doi:10.1007/978-3-319-15317-9_19'
apa: 'Fahrenberg, U., Kretinsky, J., Legay, A., & Traonouez, L. (2015). Compositionality
for quantitative specifications (Vol. 8997, pp. 306–324). Presented at the FACS:
Formal Aspects of Component Software, Bertinoro, Italy: Springer. https://doi.org/10.1007/978-3-319-15317-9_19'
chicago: Fahrenberg, Uli, Jan Kretinsky, Axel Legay, and Louis Traonouez. “Compositionality
for Quantitative Specifications,” 8997:306–24. Springer, 2015. https://doi.org/10.1007/978-3-319-15317-9_19.
ieee: 'U. Fahrenberg, J. Kretinsky, A. Legay, and L. Traonouez, “Compositionality
for quantitative specifications,” presented at the FACS: Formal Aspects of Component
Software, Bertinoro, Italy, 2015, vol. 8997, pp. 306–324.'
ista: 'Fahrenberg U, Kretinsky J, Legay A, Traonouez L. 2015. Compositionality for
quantitative specifications. FACS: Formal Aspects of Component Software, LNCS,
vol. 8997, 306–324.'
mla: Fahrenberg, Uli, et al. Compositionality for Quantitative Specifications.
Vol. 8997, Springer, 2015, pp. 306–24, doi:10.1007/978-3-319-15317-9_19.
short: U. Fahrenberg, J. Kretinsky, A. Legay, L. Traonouez, in:, Springer, 2015,
pp. 306–324.
conference:
end_date: 2014-09-12
location: Bertinoro, Italy
name: 'FACS: Formal Aspects of Component Software'
start_date: 2014-09-10
date_created: 2018-12-11T11:54:31Z
date_published: 2015-01-30T00:00:00Z
date_updated: 2021-01-12T06:53:49Z
day: '30'
department:
- _id: ToHe
- _id: KrCh
doi: 10.1007/978-3-319-15317-9_19
ec_funded: 1
intvolume: ' 8997'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1408.1256
month: '01'
oa: 1
oa_version: Preprint
page: 306 - 324
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
publication_status: published
publisher: Springer
publist_id: '5216'
quality_controlled: '1'
scopus_import: 1
status: public
title: Compositionality for quantitative specifications
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 8997
year: '2015'
...
---
_id: '2034'
abstract:
- lang: eng
text: Opacity is a generic security property, that has been defined on (non-probabilistic)
transition systems and later on Markov chains with labels. For a secret predicate,
given as a subset of runs, and a function describing the view of an external observer,
the value of interest for opacity is a measure of the set of runs disclosing the
secret. We extend this definition to the richer framework of Markov decision processes,
where non-deterministicchoice is combined with probabilistic transitions, and
we study related decidability problems with partial or complete observation hypotheses
for the schedulers. We prove that all questions are decidable with complete observation
and ω-regular secrets. With partial observation, we prove that all quantitative
questions are undecidable but the question whether a system is almost surely non-opaquebecomes
decidable for a restricted class of ω-regular secrets, as well as for all ω-regular
secrets under finite-memory schedulers.
author:
- first_name: Béatrice
full_name: Bérard, Béatrice
last_name: Bérard
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Nathalie
full_name: Sznajder, Nathalie
last_name: Sznajder
citation:
ama: Bérard B, Chatterjee K, Sznajder N. Probabilistic opacity for Markov decision
processes. Information Processing Letters. 2015;115(1):52-59. doi:10.1016/j.ipl.2014.09.001
apa: Bérard, B., Chatterjee, K., & Sznajder, N. (2015). Probabilistic opacity
for Markov decision processes. Information Processing Letters. Elsevier.
https://doi.org/10.1016/j.ipl.2014.09.001
chicago: Bérard, Béatrice, Krishnendu Chatterjee, and Nathalie Sznajder. “Probabilistic
Opacity for Markov Decision Processes.” Information Processing Letters.
Elsevier, 2015. https://doi.org/10.1016/j.ipl.2014.09.001.
ieee: B. Bérard, K. Chatterjee, and N. Sznajder, “Probabilistic opacity for Markov
decision processes,” Information Processing Letters, vol. 115, no. 1.
Elsevier, pp. 52–59, 2015.
ista: Bérard B, Chatterjee K, Sznajder N. 2015. Probabilistic opacity for Markov
decision processes. Information Processing Letters. 115(1), 52–59.
mla: Bérard, Béatrice, et al. “Probabilistic Opacity for Markov Decision Processes.”
Information Processing Letters, vol. 115, no. 1, Elsevier, 2015, pp. 52–59,
doi:10.1016/j.ipl.2014.09.001.
short: B. Bérard, K. Chatterjee, N. Sznajder, Information Processing Letters 115
(2015) 52–59.
date_created: 2018-12-11T11:55:20Z
date_published: 2015-01-01T00:00:00Z
date_updated: 2021-01-12T06:54:52Z
day: '01'
department:
- _id: KrCh
doi: 10.1016/j.ipl.2014.09.001
ec_funded: 1
intvolume: ' 115'
issue: '1'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1407.4225
month: '01'
oa: 1
oa_version: Preprint
page: 52 - 59
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 Processing Letters'
publication_status: published
publisher: Elsevier
publist_id: '5025'
quality_controlled: '1'
scopus_import: 1
status: public
title: Probabilistic opacity for Markov decision processes
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 115
year: '2015'
...