---
_id: '14259'
abstract:
- lang: eng
text: "We provide a learning-based technique for guessing a winning strategy in
a parity game originating from an LTL synthesis problem. A cheaply obtained guess
can be useful in several applications. Not only can the guessed strategy be applied
as best-effort in cases where the game’s huge size prohibits rigorous approaches,
but it can also increase the scalability of rigorous LTL synthesis in several
ways. Firstly, checking whether a guessed strategy is winning is easier than constructing
one. Secondly, even if the guess is wrong in some places, it can be fixed by strategy
iteration faster than constructing one from scratch. Thirdly, the guess can be
used in on-the-fly approaches to prioritize exploration in the most fruitful directions.\r\nIn
contrast to previous works, we (i) reflect the highly structured logical information
in game’s states, the so-called semantic labelling, coming from the recent LTL-to-automata
translations, and (ii) learn to reflect it properly by learning from previously
solved games, bringing the solving process closer to human-like reasoning."
acknowledgement: This research was funded in part by the German Research Foundation
(DFG) project 427755713 Group-By Objectives in Probabilistic Verification (GOPro).
alternative_title:
- LNCS
article_processing_charge: Yes (in subscription journal)
author:
- first_name: Jan
full_name: Kretinsky, Jan
id: 44CEF464-F248-11E8-B48F-1D18A9856A87
last_name: Kretinsky
orcid: 0000-0002-8122-2881
- first_name: Tobias
full_name: Meggendorfer, Tobias
id: b21b0c15-30a2-11eb-80dc-f13ca25802e1
last_name: Meggendorfer
orcid: 0000-0002-1712-2165
- first_name: Maximilian
full_name: Prokop, Maximilian
last_name: Prokop
- first_name: Sabine
full_name: Rieder, Sabine
last_name: Rieder
citation:
ama: 'Kretinsky J, Meggendorfer T, Prokop M, Rieder S. Guessing winning policies
in LTL synthesis by semantic learning. In: 35th International Conference on
Computer Aided Verification . Vol 13964. Springer Nature; 2023:390-414. doi:10.1007/978-3-031-37706-8_20'
apa: 'Kretinsky, J., Meggendorfer, T., Prokop, M., & Rieder, S. (2023). Guessing
winning policies in LTL synthesis by semantic learning. In 35th International
Conference on Computer Aided Verification (Vol. 13964, pp. 390–414). Paris,
France: Springer Nature. https://doi.org/10.1007/978-3-031-37706-8_20'
chicago: Kretinsky, Jan, Tobias Meggendorfer, Maximilian Prokop, and Sabine Rieder.
“Guessing Winning Policies in LTL Synthesis by Semantic Learning.” In 35th
International Conference on Computer Aided Verification , 13964:390–414. Springer
Nature, 2023. https://doi.org/10.1007/978-3-031-37706-8_20.
ieee: J. Kretinsky, T. Meggendorfer, M. Prokop, and S. Rieder, “Guessing winning
policies in LTL synthesis by semantic learning,” in 35th International Conference
on Computer Aided Verification , Paris, France, 2023, vol. 13964, pp. 390–414.
ista: 'Kretinsky J, Meggendorfer T, Prokop M, Rieder S. 2023. Guessing winning policies
in LTL synthesis by semantic learning. 35th International Conference on Computer
Aided Verification . CAV: Computer Aided Verification, LNCS, vol. 13964, 390–414.'
mla: Kretinsky, Jan, et al. “Guessing Winning Policies in LTL Synthesis by Semantic
Learning.” 35th International Conference on Computer Aided Verification ,
vol. 13964, Springer Nature, 2023, pp. 390–414, doi:10.1007/978-3-031-37706-8_20.
short: J. Kretinsky, T. Meggendorfer, M. Prokop, S. Rieder, in:, 35th International
Conference on Computer Aided Verification , Springer Nature, 2023, pp. 390–414.
conference:
end_date: 2023-07-22
location: Paris, France
name: 'CAV: Computer Aided Verification'
start_date: 2023-07-17
date_created: 2023-09-03T22:01:16Z
date_published: 2023-07-17T00:00:00Z
date_updated: 2023-09-06T08:27:33Z
day: '17'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1007/978-3-031-37706-8_20
file:
- access_level: open_access
checksum: ed66278b61bb869e1baba3d9b9081271
content_type: application/pdf
creator: dernst
date_created: 2023-09-06T08:25:50Z
date_updated: 2023-09-06T08:25:50Z
file_id: '14276'
file_name: 2023_LNCS_CAV_Kretinsky.pdf
file_size: 428354
relation: main_file
success: 1
file_date_updated: 2023-09-06T08:25:50Z
has_accepted_license: '1'
intvolume: ' 13964'
language:
- iso: eng
month: '07'
oa: 1
oa_version: Published Version
page: 390-414
publication: '35th International Conference on Computer Aided Verification '
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031377051'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Guessing winning policies in LTL synthesis by semantic learning
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 13964
year: '2023'
...
---
_id: '13967'
abstract:
- lang: eng
text: 'A classic solution technique for Markov decision processes (MDP) and stochastic
games (SG) is value iteration (VI). Due to its good practical performance, this
approximative approach is typically preferred over exact techniques, even though
no practical bounds on the imprecision of the result could be given until recently.
As a consequence, even the most used model checkers could return arbitrarily wrong
results. Over the past decade, different works derived stopping criteria, indicating
when the precision reaches the desired level, for various settings, in particular
MDP with reachability, total reward, and mean payoff, and SG with reachability.In
this paper, we provide the first stopping criteria for VI on SG with total reward
and mean payoff, yielding the first anytime algorithms in these settings. To this
end, we provide the solution in two flavours: First through a reduction to the
MDP case and second directly on SG. The former is simpler and automatically utilizes
any advances on MDP. The latter allows for more local computations, heading towards
better practical efficiency.Our solution unifies the previously mentioned approaches
for MDP and SG and their underlying ideas. To achieve this, we isolate objective-specific
subroutines as well as identify objective-independent concepts. These structural
concepts, while surprisingly simple, form the very essence of the unified solution.'
acknowledgement: This research was funded in part by DFG projects 383882557 “SUV”
and 427755713 “GOPro”.
article_processing_charge: No
author:
- first_name: Jan
full_name: Kretinsky, Jan
id: 44CEF464-F248-11E8-B48F-1D18A9856A87
last_name: Kretinsky
orcid: 0000-0002-8122-2881
- first_name: Tobias
full_name: Meggendorfer, Tobias
id: b21b0c15-30a2-11eb-80dc-f13ca25802e1
last_name: Meggendorfer
orcid: 0000-0002-1712-2165
- first_name: Maximilian
full_name: Weininger, Maximilian
id: 02ab0197-cc70-11ed-ab61-918e71f56881
last_name: Weininger
citation:
ama: 'Kretinsky J, Meggendorfer T, Weininger M. Stopping criteria for value iteration
on stochastic games with quantitative objectives. In: 38th Annual ACM/IEEE
Symposium on Logic in Computer Science. Vol 2023. Institute of Electrical
and Electronics Engineers; 2023. doi:10.1109/LICS56636.2023.10175771'
apa: 'Kretinsky, J., Meggendorfer, T., & Weininger, M. (2023). Stopping criteria
for value iteration on stochastic games with quantitative objectives. In 38th
Annual ACM/IEEE Symposium on Logic in Computer Science (Vol. 2023). Boston,
MA, United States: Institute of Electrical and Electronics Engineers. https://doi.org/10.1109/LICS56636.2023.10175771'
chicago: Kretinsky, Jan, Tobias Meggendorfer, and Maximilian Weininger. “Stopping
Criteria for Value Iteration on Stochastic Games with Quantitative Objectives.”
In 38th Annual ACM/IEEE Symposium on Logic in Computer Science, Vol. 2023.
Institute of Electrical and Electronics Engineers, 2023. https://doi.org/10.1109/LICS56636.2023.10175771.
ieee: J. Kretinsky, T. Meggendorfer, and M. Weininger, “Stopping criteria for value
iteration on stochastic games with quantitative objectives,” in 38th Annual
ACM/IEEE Symposium on Logic in Computer Science, Boston, MA, United States,
2023, vol. 2023.
ista: 'Kretinsky J, Meggendorfer T, Weininger M. 2023. Stopping criteria for value
iteration on stochastic games with quantitative objectives. 38th Annual ACM/IEEE
Symposium on Logic in Computer Science. LICS: Symposium on Logic in Computer Science
vol. 2023.'
mla: Kretinsky, Jan, et al. “Stopping Criteria for Value Iteration on Stochastic
Games with Quantitative Objectives.” 38th Annual ACM/IEEE Symposium on Logic
in Computer Science, vol. 2023, Institute of Electrical and Electronics Engineers,
2023, doi:10.1109/LICS56636.2023.10175771.
short: J. Kretinsky, T. Meggendorfer, M. Weininger, in:, 38th Annual ACM/IEEE Symposium
on Logic in Computer Science, Institute of Electrical and Electronics Engineers,
2023.
conference:
end_date: 2023-06-29
location: Boston, MA, United States
name: 'LICS: Symposium on Logic in Computer Science'
start_date: 2023-06-26
date_created: 2023-08-06T22:01:10Z
date_published: 2023-07-01T00:00:00Z
date_updated: 2023-12-13T12:06:10Z
day: '01'
department:
- _id: KrCh
doi: 10.1109/LICS56636.2023.10175771
external_id:
arxiv:
- '2304.09930'
isi:
- '001036707700042'
intvolume: ' 2023'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.48550/arXiv.2304.09930
month: '07'
oa: 1
oa_version: Preprint
publication: 38th Annual ACM/IEEE Symposium on Logic in Computer Science
publication_identifier:
isbn:
- '9798350335873'
issn:
- 1043-6871
publication_status: published
publisher: Institute of Electrical and Electronics Engineers
quality_controlled: '1'
scopus_import: '1'
status: public
title: Stopping criteria for value iteration on stochastic games with quantitative
objectives
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 2023
year: '2023'
...
---
_id: '10602'
abstract:
- lang: eng
text: Transforming ω-automata into parity automata is traditionally done using appearance
records. We present an efficient variant of this idea, tailored to Rabin automata,
and several optimizations applicable to all appearance records. We compare the
methods experimentally and show that our method produces significantly smaller
automata than previous approaches.
acknowledgement: This work is partially funded by the German Research Foundation (DFG)
projects Verified Model Checkers (No. 317422601) and Statistical Unbounded Verification
(No. 383882557), and the Alexander von Humboldt Foundation with funds from the German
Federal Ministry of Education and Research. It is an extended version of [21], including
all proofs together with further explanations and examples. Moreover, we provide
a new, more efficient construction based on (total) preorders, unifying previous
optimizations. Experiments are performed with a new, performant implementation,
comparing our approach to the current state of the art.
article_processing_charge: Yes (via OA deal)
article_type: original
author:
- first_name: Jan
full_name: Kretinsky, Jan
id: 44CEF464-F248-11E8-B48F-1D18A9856A87
last_name: Kretinsky
orcid: 0000-0002-8122-2881
- first_name: Tobias
full_name: Meggendorfer, Tobias
id: b21b0c15-30a2-11eb-80dc-f13ca25802e1
last_name: Meggendorfer
orcid: 0000-0002-1712-2165
- first_name: Clara
full_name: Waldmann, Clara
last_name: Waldmann
- first_name: Maximilian
full_name: Weininger, Maximilian
last_name: Weininger
citation:
ama: Kretinsky J, Meggendorfer T, Waldmann C, Weininger M. Index appearance record
with preorders. Acta Informatica. 2022;59:585-618. doi:10.1007/s00236-021-00412-y
apa: Kretinsky, J., Meggendorfer, T., Waldmann, C., & Weininger, M. (2022).
Index appearance record with preorders. Acta Informatica. Springer Nature.
https://doi.org/10.1007/s00236-021-00412-y
chicago: Kretinsky, Jan, Tobias Meggendorfer, Clara Waldmann, and Maximilian Weininger.
“Index Appearance Record with Preorders.” Acta Informatica. Springer Nature,
2022. https://doi.org/10.1007/s00236-021-00412-y.
ieee: J. Kretinsky, T. Meggendorfer, C. Waldmann, and M. Weininger, “Index appearance
record with preorders,” Acta Informatica, vol. 59. Springer Nature, pp.
585–618, 2022.
ista: Kretinsky J, Meggendorfer T, Waldmann C, Weininger M. 2022. Index appearance
record with preorders. Acta Informatica. 59, 585–618.
mla: Kretinsky, Jan, et al. “Index Appearance Record with Preorders.” Acta Informatica,
vol. 59, Springer Nature, 2022, pp. 585–618, doi:10.1007/s00236-021-00412-y.
short: J. Kretinsky, T. Meggendorfer, C. Waldmann, M. Weininger, Acta Informatica
59 (2022) 585–618.
date_created: 2022-01-06T12:37:27Z
date_published: 2022-10-01T00:00:00Z
date_updated: 2023-08-02T13:49:28Z
day: '01'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1007/s00236-021-00412-y
external_id:
isi:
- '000735765500001'
file:
- access_level: open_access
checksum: bf1c195b6aaf59e8530cf9e3a9d731f7
content_type: application/pdf
creator: cchlebak
date_created: 2022-01-07T07:50:31Z
date_updated: 2022-01-07T07:50:31Z
file_id: '10603'
file_name: 2021_ActaInfor_Křetínský.pdf
file_size: 1066082
relation: main_file
success: 1
file_date_updated: 2022-01-07T07:50:31Z
has_accepted_license: '1'
intvolume: ' 59'
isi: 1
keyword:
- computer networks and communications
- information systems
- software
language:
- iso: eng
month: '10'
oa: 1
oa_version: Published Version
page: 585-618
project:
- _id: B67AFEDC-15C9-11EA-A837-991A96BB2854
name: IST Austria Open Access Fund
publication: Acta Informatica
publication_identifier:
eissn:
- 1432-0525
issn:
- 0001-5903
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Index appearance record with preorders
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: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
volume: 59
year: '2022'
...
---
_id: '12775'
abstract:
- lang: eng
text: "We consider the problem of approximating the reachability probabilities in
Markov decision processes (MDP) with uncountable (continuous) state and action
spaces. While there are algorithms that, for special classes of such MDP, provide
a sequence of approximations converging to the true value in the limit, our aim
is to obtain an algorithm with guarantees on the precision of the approximation.\r\nAs
this problem is undecidable in general, assumptions on the MDP are necessary.
Our main contribution is to identify sufficient assumptions that are as weak as
possible, thus approaching the \"boundary\" of which systems can be correctly
and reliably analyzed. To this end, we also argue why each of our assumptions
is necessary for algorithms based on processing finitely many observations.\r\nWe
present two solution variants. The first one provides converging lower bounds
under weaker assumptions than typical ones from previous works concerned with
guarantees. The second one then utilizes stronger assumptions to additionally
provide converging upper bounds. Altogether, we obtain an anytime algorithm, i.e.
yielding a sequence of approximants with known and iteratively improving precision,
converging to the true value in the limit. Besides, due to the generality of our
assumptions, our algorithms are very general templates, readily allowing for various
heuristics from literature in contrast to, e.g., a specific discretization algorithm.
Our theoretical contribution thus paves the way for future practical improvements
without sacrificing correctness guarantees."
acknowledgement: "Kush Grover: The author has been supported by the DFG research training
group GRK\r\n2428 ConVeY.\r\nMaximilian Weininger: The author has been partially
supported by DFG projects 383882557\r\nStatistical Unbounded Verification (SUV)
and 427755713 Group-By Objectives in Probabilistic\r\nVerification (GOPro)"
alternative_title:
- LIPIcs
article_number: '11'
article_processing_charge: No
author:
- first_name: Kush
full_name: Grover, Kush
last_name: Grover
- first_name: Jan
full_name: Kretinsky, Jan
id: 44CEF464-F248-11E8-B48F-1D18A9856A87
last_name: Kretinsky
orcid: 0000-0002-8122-2881
- first_name: Tobias
full_name: Meggendorfer, Tobias
id: b21b0c15-30a2-11eb-80dc-f13ca25802e1
last_name: Meggendorfer
orcid: 0000-0002-1712-2165
- first_name: Maimilian
full_name: Weininger, Maimilian
last_name: Weininger
citation:
ama: 'Grover K, Kretinsky J, Meggendorfer T, Weininger M. Anytime guarantees for
reachability in uncountable Markov decision processes. In: 33rd International
Conference on Concurrency Theory . Vol 243. Schloss Dagstuhl - Leibniz-Zentrum
für Informatik; 2022. doi:10.4230/LIPIcs.CONCUR.2022.11'
apa: 'Grover, K., Kretinsky, J., Meggendorfer, T., & Weininger, M. (2022). Anytime
guarantees for reachability in uncountable Markov decision processes. In 33rd
International Conference on Concurrency Theory (Vol. 243). Warsaw, Poland:
Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2022.11'
chicago: Grover, Kush, Jan Kretinsky, Tobias Meggendorfer, and Maimilian Weininger.
“Anytime Guarantees for Reachability in Uncountable Markov Decision Processes.”
In 33rd International Conference on Concurrency Theory , Vol. 243. Schloss
Dagstuhl - Leibniz-Zentrum für Informatik, 2022. https://doi.org/10.4230/LIPIcs.CONCUR.2022.11.
ieee: K. Grover, J. Kretinsky, T. Meggendorfer, and M. Weininger, “Anytime guarantees
for reachability in uncountable Markov decision processes,” in 33rd International
Conference on Concurrency Theory , Warsaw, Poland, 2022, vol. 243.
ista: 'Grover K, Kretinsky J, Meggendorfer T, Weininger M. 2022. Anytime guarantees
for reachability in uncountable Markov decision processes. 33rd International
Conference on Concurrency Theory . CONCUR: Conference on Concurrency Theory, LIPIcs,
vol. 243, 11.'
mla: Grover, Kush, et al. “Anytime Guarantees for Reachability in Uncountable Markov
Decision Processes.” 33rd International Conference on Concurrency Theory ,
vol. 243, 11, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022, doi:10.4230/LIPIcs.CONCUR.2022.11.
short: K. Grover, J. Kretinsky, T. Meggendorfer, M. Weininger, in:, 33rd International
Conference on Concurrency Theory , Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
2022.
conference:
end_date: 2022-09-16
location: Warsaw, Poland
name: 'CONCUR: Conference on Concurrency Theory'
start_date: 2022-09-13
date_created: 2023-03-28T08:09:32Z
date_published: 2022-09-15T00:00:00Z
date_updated: 2023-09-26T10:43:30Z
day: '15'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.4230/LIPIcs.CONCUR.2022.11
external_id:
arxiv:
- '2008.04824'
file:
- access_level: open_access
checksum: e282e43d3ae0ba6e067b72f4583e13c0
content_type: application/pdf
creator: dernst
date_created: 2023-09-26T10:43:15Z
date_updated: 2023-09-26T10:43:15Z
file_id: '14372'
file_name: 2022_LIPIcS_Grover.pdf
file_size: 960036
relation: main_file
success: 1
file_date_updated: 2023-09-26T10:43:15Z
has_accepted_license: '1'
intvolume: ' 243'
language:
- iso: eng
month: '09'
oa: 1
oa_version: Published Version
publication: '33rd International Conference on Concurrency Theory '
publication_identifier:
issn:
- 1868-8969
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
quality_controlled: '1'
scopus_import: '1'
status: public
title: Anytime guarantees for reachability in uncountable Markov decision processes
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 243
year: '2022'
...
---
_id: '297'
abstract:
- lang: eng
text: Graph games played by two players over finite-state graphs are central in
many problems in computer science. In particular, graph games with ω -regular
winning conditions, specified as parity objectives, which can express properties
such as safety, liveness, fairness, are the basic framework for verification and
synthesis of reactive systems. The decisions for a player at various states of
the graph game are represented as strategies. While the algorithmic problem for
solving graph games with parity objectives has been widely studied, the most prominent
data-structure for strategy representation in graph games has been binary decision
diagrams (BDDs). However, due to the bit-level representation, BDDs do not retain
the inherent flavor of the decisions of strategies, and are notoriously hard to
minimize to obtain succinct representation. In this work we propose decision trees
for strategy representation in graph games. Decision trees retain the flavor of
decisions of strategies and allow entropy-based minimization to obtain succinct
trees. However, decision trees work in settings (e.g., probabilistic models) where
errors are allowed, and overfitting of data is typically avoided. In contrast,
for strategies in graph games no error is allowed, and the decision tree must
represent the entire strategy. We develop new techniques to extend decision trees
to overcome the above obstacles, while retaining the entropy-based techniques
to obtain succinct trees. We have implemented our techniques to extend the existing
decision tree solvers. We present experimental results for problems in reactive
synthesis to show that decision trees provide a much more efficient data-structure
for strategy representation as compared to BDDs.
alternative_title:
- LNCS
article_processing_charge: No
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: Jan
full_name: Kretinsky, Jan
id: 44CEF464-F248-11E8-B48F-1D18A9856A87
last_name: Kretinsky
orcid: 0000-0002-8122-2881
- first_name: Viktor
full_name: Toman, Viktor
id: 3AF3DA7C-F248-11E8-B48F-1D18A9856A87
last_name: Toman
orcid: 0000-0001-9036-063X
citation:
ama: 'Brázdil T, Chatterjee K, Kretinsky J, Toman V. Strategy representation by
decision trees in reactive synthesis. In: Vol 10805. Springer; 2018:385-407. doi:10.1007/978-3-319-89960-2_21'
apa: 'Brázdil, T., Chatterjee, K., Kretinsky, J., & Toman, V. (2018). Strategy
representation by decision trees in reactive synthesis (Vol. 10805, pp. 385–407).
Presented at the TACAS 2018: Tools and Algorithms for the Construction and Analysis
of Systems, Thessaloniki, Greece: Springer. https://doi.org/10.1007/978-3-319-89960-2_21'
chicago: Brázdil, Tomáš, Krishnendu Chatterjee, Jan Kretinsky, and Viktor Toman.
“Strategy Representation by Decision Trees in Reactive Synthesis,” 10805:385–407.
Springer, 2018. https://doi.org/10.1007/978-3-319-89960-2_21.
ieee: 'T. Brázdil, K. Chatterjee, J. Kretinsky, and V. Toman, “Strategy representation
by decision trees in reactive synthesis,” presented at the TACAS 2018: Tools and
Algorithms for the Construction and Analysis of Systems, Thessaloniki, Greece,
2018, vol. 10805, pp. 385–407.'
ista: 'Brázdil T, Chatterjee K, Kretinsky J, Toman V. 2018. Strategy representation
by decision trees in reactive synthesis. TACAS 2018: Tools and Algorithms for
the Construction and Analysis of Systems, LNCS, vol. 10805, 385–407.'
mla: Brázdil, Tomáš, et al. Strategy Representation by Decision Trees in Reactive
Synthesis. Vol. 10805, Springer, 2018, pp. 385–407, doi:10.1007/978-3-319-89960-2_21.
short: T. Brázdil, K. Chatterjee, J. Kretinsky, V. Toman, in:, Springer, 2018, pp.
385–407.
conference:
end_date: 2018-04-20
location: Thessaloniki, Greece
name: 'TACAS 2018: Tools and Algorithms for the Construction and Analysis of Systems'
start_date: 2018-04-14
date_created: 2018-12-11T11:45:41Z
date_published: 2018-04-12T00:00:00Z
date_updated: 2023-09-19T09:57:08Z
day: '12'
ddc:
- '000'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1007/978-3-319-89960-2_21
ec_funded: 1
external_id:
isi:
- '000546326300021'
file:
- access_level: open_access
checksum: b13874ffb114932ad9cc2586b7469db4
content_type: application/pdf
creator: dernst
date_created: 2018-12-17T16:29:08Z
date_updated: 2020-07-14T12:45:57Z
file_id: '5723'
file_name: 2018_LNCS_Brazdil.pdf
file_size: 1829940
relation: main_file
file_date_updated: 2020-07-14T12:45:57Z
has_accepted_license: '1'
intvolume: ' 10805'
isi: 1
language:
- iso: eng
month: '04'
oa: 1
oa_version: Published Version
page: 385 - 407
project:
- _id: 25892FC0-B435-11E9-9278-68D0E5697425
grant_number: ICT15-003
name: Efficient Algorithms for Computer Aided 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: 2564DBCA-B435-11E9-9278-68D0E5697425
call_identifier: H2020
grant_number: '665385'
name: International IST Doctoral Program
publication_status: published
publisher: Springer
publist_id: '7584'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Strategy representation by decision trees in reactive synthesis
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 10805
year: '2018'
...
---
_id: '471'
abstract:
- lang: eng
text: 'We present a new algorithm for the statistical model checking of Markov chains
with respect to unbounded temporal properties, including full linear temporal
logic. The main idea is that we monitor each simulation run on the fly, in order
to detect quickly if a bottom strongly connected component is entered with high
probability, in which case the simulation run can be terminated early. As a result,
our simulation runs are often much shorter than required by termination bounds
that are computed a priori for a desired level of confidence on a large state
space. In comparison to previous algorithms for statistical model checking our
method is not only faster in many cases but also requires less information about
the system, namely, only the minimum transition probability that occurs in the
Markov chain. In addition, our method can be generalised to unbounded quantitative
properties such as mean-payoff bounds. '
article_number: '12'
author:
- first_name: Przemyslaw
full_name: Daca, Przemyslaw
id: 49351290-F248-11E8-B48F-1D18A9856A87
last_name: Daca
- 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: Jan
full_name: Kretinsky, Jan
id: 44CEF464-F248-11E8-B48F-1D18A9856A87
last_name: Kretinsky
orcid: 0000-0002-8122-2881
- first_name: Tatjana
full_name: Petrov, Tatjana
id: 3D5811FC-F248-11E8-B48F-1D18A9856A87
last_name: Petrov
orcid: 0000-0002-9041-0905
citation:
ama: Daca P, Henzinger TA, Kretinsky J, Petrov T. Faster statistical model checking
for unbounded temporal properties. ACM Transactions on Computational Logic
(TOCL). 2017;18(2). doi:10.1145/3060139
apa: Daca, P., Henzinger, T. A., Kretinsky, J., & Petrov, T. (2017). Faster
statistical model checking for unbounded temporal properties. ACM Transactions
on Computational Logic (TOCL). ACM. https://doi.org/10.1145/3060139
chicago: Daca, Przemyslaw, Thomas A Henzinger, Jan Kretinsky, and Tatjana Petrov.
“Faster Statistical Model Checking for Unbounded Temporal Properties.” ACM
Transactions on Computational Logic (TOCL). ACM, 2017. https://doi.org/10.1145/3060139.
ieee: P. Daca, T. A. Henzinger, J. Kretinsky, and T. Petrov, “Faster statistical
model checking for unbounded temporal properties,” ACM Transactions on Computational
Logic (TOCL), vol. 18, no. 2. ACM, 2017.
ista: Daca P, Henzinger TA, Kretinsky J, Petrov T. 2017. Faster statistical model
checking for unbounded temporal properties. ACM Transactions on Computational
Logic (TOCL). 18(2), 12.
mla: Daca, Przemyslaw, et al. “Faster Statistical Model Checking for Unbounded Temporal
Properties.” ACM Transactions on Computational Logic (TOCL), vol. 18, no.
2, 12, ACM, 2017, doi:10.1145/3060139.
short: P. Daca, T.A. Henzinger, J. Kretinsky, T. Petrov, ACM Transactions on Computational
Logic (TOCL) 18 (2017).
date_created: 2018-12-11T11:46:39Z
date_published: 2017-05-01T00:00:00Z
date_updated: 2023-02-21T16:48:11Z
day: '01'
department:
- _id: ToHe
doi: 10.1145/3060139
ec_funded: 1
intvolume: ' 18'
issue: '2'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1504.05739
month: '05'
oa: 1
oa_version: Submitted Version
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _id: 25F5A88A-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11402-N23
name: Moderne Concurrency Paradigms
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
- _id: 25681D80-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '291734'
name: International IST Postdoc Fellowship Programme
publication: ACM Transactions on Computational Logic (TOCL)
publication_identifier:
issn:
- '15293785'
publication_status: published
publisher: ACM
publist_id: '7349'
quality_controlled: '1'
related_material:
record:
- id: '1234'
relation: earlier_version
status: public
scopus_import: 1
status: public
title: Faster statistical model checking for unbounded temporal properties
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 18
year: '2017'
...
---
_id: '466'
abstract:
- lang: eng
text: 'We consider Markov decision processes (MDPs) with multiple limit-average
(or mean-payoff) objectives. There exist two different views: (i) the expectation
semantics, where the goal is to optimize the expected mean-payoff objective, and
(ii) the satisfaction semantics, where the goal is to maximize the probability
of runs such that the mean-payoff value stays above a given vector. We consider
optimization with respect to both objectives at once, thus unifying the existing
semantics. Precisely, the goal is to optimize the expectation while ensuring the
satisfaction constraint. Our problem captures the notion of optimization with
respect to strategies that are risk-averse (i.e., ensure certain probabilistic
guarantee). Our main results are as follows: First, we present algorithms for
the decision problems which are always polynomial in the size of the MDP. We also
show that an approximation of the Pareto-curve can be computed in time polynomial
in the size of the MDP, and the approximation factor, but exponential in the number
of dimensions. Second, we present a complete characterization of the strategy
complexity (in terms of memory bounds and randomization) required to solve our
problem. '
article_number: '15'
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Zuzana
full_name: Křetínská, Zuzana
last_name: Křetínská
- first_name: Jan
full_name: Kretinsky, Jan
id: 44CEF464-F248-11E8-B48F-1D18A9856A87
last_name: Kretinsky
orcid: 0000-0002-8122-2881
citation:
ama: Chatterjee K, Křetínská Z, Kretinsky J. Unifying two views on multiple mean-payoff
objectives in Markov decision processes. Logical Methods in Computer Science.
2017;13(2). doi:10.23638/LMCS-13(2:15)2017
apa: Chatterjee, K., Křetínská, Z., & Kretinsky, J. (2017). Unifying two views
on multiple mean-payoff objectives in Markov decision processes. Logical Methods
in Computer Science. International Federation of Computational Logic. https://doi.org/10.23638/LMCS-13(2:15)2017
chicago: Chatterjee, Krishnendu, Zuzana Křetínská, and Jan Kretinsky. “Unifying
Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes.” Logical
Methods in Computer Science. International Federation of Computational Logic,
2017. https://doi.org/10.23638/LMCS-13(2:15)2017.
ieee: K. Chatterjee, Z. Křetínská, and J. Kretinsky, “Unifying two views on multiple
mean-payoff objectives in Markov decision processes,” Logical Methods in Computer
Science, vol. 13, no. 2. International Federation of Computational Logic,
2017.
ista: Chatterjee K, Křetínská Z, Kretinsky J. 2017. Unifying two views on multiple
mean-payoff objectives in Markov decision processes. Logical Methods in Computer
Science. 13(2), 15.
mla: Chatterjee, Krishnendu, et al. “Unifying Two Views on Multiple Mean-Payoff
Objectives in Markov Decision Processes.” Logical Methods in Computer Science,
vol. 13, no. 2, 15, International Federation of Computational Logic, 2017, doi:10.23638/LMCS-13(2:15)2017.
short: K. Chatterjee, Z. Křetínská, J. Kretinsky, Logical Methods in Computer Science
13 (2017).
date_created: 2018-12-11T11:46:38Z
date_published: 2017-07-03T00:00:00Z
date_updated: 2023-02-23T12:26:16Z
day: '03'
ddc:
- '004'
department:
- _id: KrCh
doi: 10.23638/LMCS-13(2:15)2017
ec_funded: 1
file:
- access_level: open_access
checksum: bfa405385ec6229ad5ead89ab5751639
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:18:32Z
date_updated: 2020-07-14T12:46:33Z
file_id: '5354'
file_name: IST-2018-957-v1+1_2017_Chatterjee_Unifying_two.pdf
file_size: 511832
relation: main_file
file_date_updated: 2020-07-14T12:46:33Z
has_accepted_license: '1'
intvolume: ' 13'
issue: '2'
language:
- iso: eng
license: https://creativecommons.org/licenses/by-nd/4.0/
month: '07'
oa: 1
oa_version: Published Version
project:
- _id: 25681D80-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '291734'
name: International IST Postdoc Fellowship Programme
- _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: 2590DB08-B435-11E9-9278-68D0E5697425
call_identifier: H2020
grant_number: '701309'
name: Atomic-Resolution Structures of Mitochondrial Respiratory Chain Supercomplexes
(H2020)
publication: Logical Methods in Computer Science
publication_identifier:
issn:
- '18605974'
publication_status: published
publisher: International Federation of Computational Logic
publist_id: '7355'
pubrep_id: '957'
quality_controlled: '1'
related_material:
record:
- id: '1657'
relation: earlier_version
status: public
- id: '5429'
relation: earlier_version
status: public
- id: '5435'
relation: earlier_version
status: public
scopus_import: 1
status: public
title: Unifying two views on multiple mean-payoff objectives in Markov decision processes
tmp:
image: /image/cc_by_nd.png
legal_code_url: https://creativecommons.org/licenses/by-nd/4.0/legalcode
name: Creative Commons Attribution-NoDerivatives 4.0 International (CC BY-ND 4.0)
short: CC BY-ND (4.0)
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 13
year: '2017'
...
---
_id: '645'
abstract:
- lang: eng
text: Markov decision processes (MDPs) are standard models for probabilistic systems
with non-deterministic behaviours. Long-run average rewards provide a mathematically
elegant formalism for expressing long term performance. Value iteration (VI) is
one of the simplest and most efficient algorithmic approaches to MDPs with other
properties, such as reachability objectives. Unfortunately, a naive extension
of VI does not work for MDPs with long-run average rewards, as there is no known
stopping criterion. In this work our contributions are threefold. (1) We refute
a conjecture related to stopping criteria for MDPs with long-run average rewards.
(2) We present two practical algorithms for MDPs with long-run average rewards
based on VI. First, we show that a combination of applying VI locally for each
maximal end-component (MEC) and VI for reachability objectives can provide approximation
guarantees. Second, extending the above approach with a simulation-guided on-demand
variant of VI, we present an anytime algorithm that is able to deal with very
large models. (3) Finally, we present experimental results showing that our methods
significantly outperform the standard approaches on several benchmarks.
alternative_title:
- LNCS
author:
- first_name: Pranav
full_name: Ashok, Pranav
last_name: Ashok
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Przemyslaw
full_name: Daca, Przemyslaw
id: 49351290-F248-11E8-B48F-1D18A9856A87
last_name: Daca
- first_name: Jan
full_name: Kretinsky, Jan
id: 44CEF464-F248-11E8-B48F-1D18A9856A87
last_name: Kretinsky
orcid: 0000-0002-8122-2881
- first_name: Tobias
full_name: Meggendorfer, Tobias
last_name: Meggendorfer
citation:
ama: 'Ashok P, Chatterjee K, Daca P, Kretinsky J, Meggendorfer T. Value iteration
for long run average reward in markov decision processes. In: Majumdar R, Kunčak
V, eds. Vol 10426. Springer; 2017:201-221. doi:10.1007/978-3-319-63387-9_10'
apa: 'Ashok, P., Chatterjee, K., Daca, P., Kretinsky, J., & Meggendorfer, T.
(2017). Value iteration for long run average reward in markov decision processes.
In R. Majumdar & V. Kunčak (Eds.) (Vol. 10426, pp. 201–221). Presented at
the CAV: Computer Aided Verification, Heidelberg, Germany: Springer. https://doi.org/10.1007/978-3-319-63387-9_10'
chicago: Ashok, Pranav, Krishnendu Chatterjee, Przemyslaw Daca, Jan Kretinsky, and
Tobias Meggendorfer. “Value Iteration for Long Run Average Reward in Markov Decision
Processes.” edited by Rupak Majumdar and Viktor Kunčak, 10426:201–21. Springer,
2017. https://doi.org/10.1007/978-3-319-63387-9_10.
ieee: 'P. Ashok, K. Chatterjee, P. Daca, J. Kretinsky, and T. Meggendorfer, “Value
iteration for long run average reward in markov decision processes,” presented
at the CAV: Computer Aided Verification, Heidelberg, Germany, 2017, vol. 10426,
pp. 201–221.'
ista: 'Ashok P, Chatterjee K, Daca P, Kretinsky J, Meggendorfer T. 2017. Value iteration
for long run average reward in markov decision processes. CAV: Computer Aided
Verification, LNCS, vol. 10426, 201–221.'
mla: Ashok, Pranav, et al. Value Iteration for Long Run Average Reward in Markov
Decision Processes. Edited by Rupak Majumdar and Viktor Kunčak, vol. 10426,
Springer, 2017, pp. 201–21, doi:10.1007/978-3-319-63387-9_10.
short: P. Ashok, K. Chatterjee, P. Daca, J. Kretinsky, T. Meggendorfer, in:, R.
Majumdar, V. Kunčak (Eds.), Springer, 2017, pp. 201–221.
conference:
end_date: 2017-07-28
location: Heidelberg, Germany
name: 'CAV: Computer Aided Verification'
start_date: 2017-07-24
date_created: 2018-12-11T11:47:41Z
date_published: 2017-07-13T00:00:00Z
date_updated: 2021-01-12T08:07:32Z
day: '13'
department:
- _id: KrCh
doi: 10.1007/978-3-319-63387-9_10
ec_funded: 1
editor:
- first_name: Rupak
full_name: Majumdar, Rupak
last_name: Majumdar
- first_name: Viktor
full_name: Kunčak, Viktor
last_name: Kunčak
intvolume: ' 10426'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1705.02326
month: '07'
oa: 1
oa_version: Submitted Version
page: 201 - 221
project:
- _id: 25892FC0-B435-11E9-9278-68D0E5697425
grant_number: ICT15-003
name: Efficient Algorithms for Computer Aided 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_identifier:
isbn:
- 978-331963386-2
publication_status: published
publisher: Springer
publist_id: '7135'
quality_controlled: '1'
scopus_import: 1
status: public
title: Value iteration for long run average reward in markov decision processes
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 10426
year: '2017'
...
---
_id: '13160'
abstract:
- lang: eng
text: "Transforming deterministic ω\r\n-automata into deterministic parity automata
is traditionally done using variants of appearance records. We present a more
efficient variant of this approach, tailored to Rabin automata, and several optimizations
applicable to all appearance records. We compare the methods experimentally and
find out that our method produces smaller automata than previous approaches. Moreover,
the experiments demonstrate the potential of our method for LTL synthesis, using
LTL-to-Rabin translators. It leads to significantly smaller parity automata when
compared to state-of-the-art approaches on complex formulae."
acknowledgement: This work is partially funded by the DFG project “Verified Model
Checkers” and by the Czech Science Foundation, grant No. P202/12/G061.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Jan
full_name: Kretinsky, Jan
id: 44CEF464-F248-11E8-B48F-1D18A9856A87
last_name: Kretinsky
orcid: 0000-0002-8122-2881
- first_name: Tobias
full_name: Meggendorfer, Tobias
id: b21b0c15-30a2-11eb-80dc-f13ca25802e1
last_name: Meggendorfer
orcid: 0000-0002-1712-2165
- first_name: Clara
full_name: Waldmann, Clara
last_name: Waldmann
- first_name: Maximilian
full_name: Weininger, Maximilian
last_name: Weininger
citation:
ama: 'Kretinsky J, Meggendorfer T, Waldmann C, Weininger M. Index appearance record
for transforming Rabin automata into parity automata. In: Tools and Algorithms
for the Construction and Analysis of Systems. Vol 10205. Springer; 2017:443-460.
doi:10.1007/978-3-662-54577-5_26'
apa: 'Kretinsky, J., Meggendorfer, T., Waldmann, C., & Weininger, M. (2017).
Index appearance record for transforming Rabin automata into parity automata.
In Tools and Algorithms for the Construction and Analysis of Systems (Vol.
10205, pp. 443–460). Uppsala, Sweden: Springer. https://doi.org/10.1007/978-3-662-54577-5_26'
chicago: Kretinsky, Jan, Tobias Meggendorfer, Clara Waldmann, and Maximilian Weininger.
“Index Appearance Record for Transforming Rabin Automata into Parity Automata.”
In Tools and Algorithms for the Construction and Analysis of Systems, 10205:443–60.
Springer, 2017. https://doi.org/10.1007/978-3-662-54577-5_26.
ieee: J. Kretinsky, T. Meggendorfer, C. Waldmann, and M. Weininger, “Index appearance
record for transforming Rabin automata into parity automata,” in Tools and
Algorithms for the Construction and Analysis of Systems, Uppsala, Sweden,
2017, vol. 10205, pp. 443–460.
ista: 'Kretinsky J, Meggendorfer T, Waldmann C, Weininger M. 2017. Index appearance
record for transforming Rabin automata into parity automata. Tools and Algorithms
for the Construction and Analysis of Systems. TACAS: Tools and Algorithms for
the Construction and Analysis of Systems, LNCS, vol. 10205, 443–460.'
mla: Kretinsky, Jan, et al. “Index Appearance Record for Transforming Rabin Automata
into Parity Automata.” Tools and Algorithms for the Construction and Analysis
of Systems, vol. 10205, Springer, 2017, pp. 443–60, doi:10.1007/978-3-662-54577-5_26.
short: J. Kretinsky, T. Meggendorfer, C. Waldmann, M. Weininger, in:, Tools and
Algorithms for the Construction and Analysis of Systems, Springer, 2017, pp. 443–460.
conference:
end_date: 2017-04-29
location: Uppsala, Sweden
name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
start_date: 2017-04-22
date_created: 2023-06-21T13:21:14Z
date_published: 2017-03-31T00:00:00Z
date_updated: 2023-06-21T13:29:46Z
day: '31'
department:
- _id: KrCh
doi: 10.1007/978-3-662-54577-5_26
external_id:
arxiv:
- '1701.05738'
intvolume: ' 10205'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.48550/arXiv.1701.05738
month: '03'
oa: 1
oa_version: Preprint
page: 443-460
publication: Tools and Algorithms for the Construction and Analysis of Systems
publication_identifier:
eisbn:
- '9783662545775'
eissn:
- 1611-3349
isbn:
- '9783662545768'
issn:
- 0302-9743
publication_status: published
publisher: Springer
quality_controlled: '1'
status: public
title: Index appearance record for transforming Rabin automata into parity automata
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 10205
year: '2017'
...
---
_id: '1407'
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 all satisfying initial states. Moreover, for any (partial)
solution our algorithm synthesizes witness control strategies to ensure almost-sure
satisfaction of the temporal logic specification. While the proposed algorithm
guarantees progress and soundness in every iteration, it is computationally demanding.
We offer an alternative, more efficient solution for the reachability properties
that decomposes the problem into a series of smaller problems of the same type.
All algorithms are demonstrated on an illustrative case study.
article_processing_charge: No
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. Nonlinear Analysis: Hybrid Systems. 2017;23(2):230-253. doi:10.1016/j.nahs.2016.04.006'
apa: 'Svoreňová, M., Kretinsky, J., Chmelik, M., Chatterjee, K., Cěrná, I., &
Belta, C. (2017). Temporal logic control for stochastic linear systems using abstraction
refinement of probabilistic games. Nonlinear Analysis: Hybrid Systems.
Elsevier. https://doi.org/10.1016/j.nahs.2016.04.006'
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.” Nonlinear Analysis: Hybrid
Systems. Elsevier, 2017. https://doi.org/10.1016/j.nahs.2016.04.006.'
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,” Nonlinear Analysis: Hybrid Systems, vol. 23, no.
2. Elsevier, pp. 230–253, 2017.'
ista: 'Svoreňová M, Kretinsky J, Chmelik M, Chatterjee K, Cěrná I, Belta C. 2017.
Temporal logic control for stochastic linear systems using abstraction refinement
of probabilistic games. Nonlinear Analysis: Hybrid Systems. 23(2), 230–253.'
mla: 'Svoreňová, Mária, et al. “Temporal Logic Control for Stochastic Linear Systems
Using Abstraction Refinement of Probabilistic Games.” Nonlinear Analysis: Hybrid
Systems, vol. 23, no. 2, Elsevier, 2017, pp. 230–53, doi:10.1016/j.nahs.2016.04.006.'
short: 'M. Svoreňová, J. Kretinsky, M. Chmelik, K. Chatterjee, I. Cěrná, C. Belta,
Nonlinear Analysis: Hybrid Systems 23 (2017) 230–253.'
date_created: 2018-12-11T11:51:50Z
date_published: 2017-02-01T00:00:00Z
date_updated: 2023-09-20T09:43:09Z
day: '01'
department:
- _id: ToHe
- _id: KrCh
doi: 10.1016/j.nahs.2016.04.006
ec_funded: 1
external_id:
arxiv:
- '1410.5387'
isi:
- '000390637000014'
intvolume: ' 23'
isi: 1
issue: '2'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1410.5387
month: '02'
oa: 1
oa_version: Preprint
page: 230 - 253
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: 'Nonlinear Analysis: Hybrid Systems'
publication_status: published
publisher: Elsevier
publist_id: '5800'
quality_controlled: '1'
related_material:
record:
- id: '1689'
relation: earlier_version
status: public
scopus_import: '1'
status: public
title: Temporal logic control for stochastic linear systems using abstraction refinement
of probabilistic games
type: journal_article
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 23
year: '2017'
...
---
_id: '1093'
abstract:
- lang: eng
text: 'We introduce a general class of distances (metrics) between Markov chains,
which are based on linear behaviour. This class encompasses distances given topologically
(such as the total variation distance or trace distance) as well as by temporal
logics or automata. We investigate which of the distances can be approximated
by observing the systems, i.e. by black-box testing or simulation, and we provide
both negative and positive results. '
acknowledgement: "This research was funded in part by the European Research Council
(ERC) under grant agreement 267989\r\n(QUAREM), the Austrian Science Fund (FWF)
under grants project S11402-N23 (RiSE and SHiNE)\r\nand Z211-N23 (Wittgenstein Award),
by the Czech Science Foundation Grant No. P202/12/G061, and\r\nby the SNSF Advanced
Postdoc. Mobility Fellowship – grant number P300P2_161067."
alternative_title:
- LIPIcs
article_number: '20'
author:
- first_name: Przemyslaw
full_name: Daca, Przemyslaw
id: 49351290-F248-11E8-B48F-1D18A9856A87
last_name: Daca
- 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: Jan
full_name: Kretinsky, Jan
id: 44CEF464-F248-11E8-B48F-1D18A9856A87
last_name: Kretinsky
orcid: 0000-0002-8122-2881
- first_name: Tatjana
full_name: Petrov, Tatjana
id: 3D5811FC-F248-11E8-B48F-1D18A9856A87
last_name: Petrov
orcid: 0000-0002-9041-0905
citation:
ama: 'Daca P, Henzinger TA, Kretinsky J, Petrov T. Linear distances between Markov
chains. In: Vol 59. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2016. doi:10.4230/LIPIcs.CONCUR.2016.20'
apa: 'Daca, P., Henzinger, T. A., Kretinsky, J., & Petrov, T. (2016). Linear
distances between Markov chains (Vol. 59). Presented at the CONCUR: Concurrency
Theory, Quebec City; Canada: Schloss Dagstuhl - Leibniz-Zentrum für Informatik.
https://doi.org/10.4230/LIPIcs.CONCUR.2016.20'
chicago: Daca, Przemyslaw, Thomas A Henzinger, Jan Kretinsky, and Tatjana Petrov.
“Linear Distances between Markov Chains,” Vol. 59. Schloss Dagstuhl - Leibniz-Zentrum
für Informatik, 2016. https://doi.org/10.4230/LIPIcs.CONCUR.2016.20.
ieee: 'P. Daca, T. A. Henzinger, J. Kretinsky, and T. Petrov, “Linear distances
between Markov chains,” presented at the CONCUR: Concurrency Theory, Quebec City;
Canada, 2016, vol. 59.'
ista: 'Daca P, Henzinger TA, Kretinsky J, Petrov T. 2016. Linear distances between
Markov chains. CONCUR: Concurrency Theory, LIPIcs, vol. 59, 20.'
mla: Daca, Przemyslaw, et al. Linear Distances between Markov Chains. Vol.
59, 20, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016, doi:10.4230/LIPIcs.CONCUR.2016.20.
short: P. Daca, T.A. Henzinger, J. Kretinsky, T. Petrov, in:, Schloss Dagstuhl -
Leibniz-Zentrum für Informatik, 2016.
conference:
end_date: 2016-08-26
location: Quebec City; Canada
name: 'CONCUR: Concurrency Theory'
start_date: 2016-08-23
date_created: 2018-12-11T11:50:06Z
date_published: 2016-08-01T00:00:00Z
date_updated: 2023-09-07T11:58:33Z
day: '01'
ddc:
- '004'
department:
- _id: ToHe
- _id: KrCh
- _id: CaGu
doi: 10.4230/LIPIcs.CONCUR.2016.20
ec_funded: 1
file:
- access_level: open_access
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:11:39Z
date_updated: 2018-12-12T10:11:39Z
file_id: '4895'
file_name: IST-2017-794-v1+1_LIPIcs-CONCUR-2016-20.pdf
file_size: 501827
relation: main_file
file_date_updated: 2018-12-12T10:11:39Z
has_accepted_license: '1'
intvolume: ' 59'
language:
- iso: eng
month: '08'
oa: 1
oa_version: Published Version
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: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '6283'
pubrep_id: '794'
quality_controlled: '1'
related_material:
record:
- id: '1155'
relation: dissertation_contains
status: public
scopus_import: 1
status: public
title: Linear distances between Markov chains
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 59
year: '2016'
...
---
_id: '1234'
abstract:
- lang: eng
text: We present a new algorithm for the statistical model checking of Markov chains
with respect to unbounded temporal properties, including full linear temporal
logic. The main idea is that we monitor each simulation run on the fly, in order
to detect quickly if a bottom strongly connected component is entered with high
probability, in which case the simulation run can be terminated early. As a result,
our simulation runs are often much shorter than required by termination bounds
that are computed a priori for a desired level of confidence on a large state
space. In comparison to previous algorithms for statistical model checking our
method is not only faster in many cases but also requires less information about
the system, namely, only the minimum transition probability that occurs in the
Markov chain. In addition, our method can be generalised to unbounded quantitative
properties such as mean-payoff bounds.
acknowledgement: "This research was funded in part by the European Research Council
(ERC) under\r\ngrant agreement 267989 (QUAREM), the Austrian Science Fund
\ (FWF) under\r\ngrants project S11402-N23 (RiSE) and Z211-N23 (Wittgenstein Award),
the Peo-\r\nple Programme (Marie Curie Actions) of the European Union’s Seventh
Framework\r\nProgramme (FP7/2007-2013) REA Grant No 291734, the SNSF Advanced Postdoc.\r\nMobility
Fellowship – grant number P300P2\r\n161067, and the Czech Science Foun-\r\ndation
under grant agreement P202/12/G061."
alternative_title:
- LNCS
author:
- first_name: Przemyslaw
full_name: Daca, Przemyslaw
id: 49351290-F248-11E8-B48F-1D18A9856A87
last_name: Daca
- 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: Jan
full_name: Kretinsky, Jan
id: 44CEF464-F248-11E8-B48F-1D18A9856A87
last_name: Kretinsky
orcid: 0000-0002-8122-2881
- first_name: Tatjana
full_name: Petrov, Tatjana
id: 3D5811FC-F248-11E8-B48F-1D18A9856A87
last_name: Petrov
orcid: 0000-0002-9041-0905
citation:
ama: 'Daca P, Henzinger TA, Kretinsky J, Petrov T. Faster statistical model checking
for unbounded temporal properties. In: Vol 9636. Springer; 2016:112-129. doi:10.1007/978-3-662-49674-9_7'
apa: 'Daca, P., Henzinger, T. A., Kretinsky, J., & Petrov, T. (2016). Faster
statistical model checking for unbounded temporal properties (Vol. 9636, pp. 112–129).
Presented at the TACAS: Tools and Algorithms for the Construction and Analysis
of Systems, Eindhoven, The Netherlands: Springer. https://doi.org/10.1007/978-3-662-49674-9_7'
chicago: Daca, Przemyslaw, Thomas A Henzinger, Jan Kretinsky, and Tatjana Petrov.
“Faster Statistical Model Checking for Unbounded Temporal Properties,” 9636:112–29.
Springer, 2016. https://doi.org/10.1007/978-3-662-49674-9_7.
ieee: 'P. Daca, T. A. Henzinger, J. Kretinsky, and T. Petrov, “Faster statistical
model checking for unbounded temporal properties,” presented at the TACAS: Tools
and Algorithms for the Construction and Analysis of Systems, Eindhoven, The Netherlands,
2016, vol. 9636, pp. 112–129.'
ista: 'Daca P, Henzinger TA, Kretinsky J, Petrov T. 2016. Faster statistical model
checking for unbounded temporal properties. TACAS: Tools and Algorithms for the
Construction and Analysis of Systems, LNCS, vol. 9636, 112–129.'
mla: Daca, Przemyslaw, et al. Faster Statistical Model Checking for Unbounded
Temporal Properties. Vol. 9636, Springer, 2016, pp. 112–29, doi:10.1007/978-3-662-49674-9_7.
short: P. Daca, T.A. Henzinger, J. Kretinsky, T. Petrov, in:, Springer, 2016, pp.
112–129.
conference:
end_date: 2016-04-08
location: Eindhoven, The Netherlands
name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
start_date: 2016-04-02
date_created: 2018-12-11T11:50:51Z
date_published: 2016-01-01T00:00:00Z
date_updated: 2023-09-07T11:58:33Z
day: '01'
department:
- _id: ToHe
- _id: CaGu
doi: 10.1007/978-3-662-49674-9_7
ec_funded: 1
intvolume: ' 9636'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1504.05739
month: '01'
oa: 1
oa_version: Preprint
page: 112 - 129
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: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
- _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: '6099'
quality_controlled: '1'
related_material:
record:
- id: '471'
relation: later_version
status: public
- id: '1155'
relation: dissertation_contains
status: public
scopus_import: 1
status: public
title: Faster statistical model checking for unbounded temporal properties
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 9636
year: '2016'
...
---
_id: '1499'
abstract:
- lang: eng
text: "We consider weighted automata with both positive and negative integer weights
on edges and\r\nstudy the problem of synchronization using adaptive strategies
that may only observe whether\r\nthe current weight-level is negative or nonnegative.
We show that the synchronization problem is decidable in polynomial time for deterministic
weighted automata."
acknowledgement: "The research leading to these results has received funding from
the European Union Seventh Framework Programme (FP7/2007-2013) under grant agreement
601148 (CASSTING), EU FP7 FET project SENSATION, Sino-Danish Basic Research Center
IDAE4CPS, the European Research Council (ERC) under grant agreement 267989 (QUAREM),
the Austrian Science Fund (FWF) project S11402-N23 (RiSE) and Z211-N23 (Wittgenstein
Award), the Czech Science Foundation under grant agreement P202/12/G061, and People
Programme (Marie Curie Actions) of the European Union’s Seventh Framework\r\nProgramme
(FP7/2007-2013) REA Grant No 291734."
alternative_title:
- LIPIcs
author:
- 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: Simon
full_name: Laursen, Simon
last_name: Laursen
- first_name: Jiří
full_name: Srba, Jiří
last_name: Srba
citation:
ama: 'Kretinsky J, Larsen K, Laursen S, Srba J. Polynomial time decidability of
weighted synchronization under partial observability. In: Vol 42. Schloss Dagstuhl
- Leibniz-Zentrum für Informatik; 2015:142-154. doi:10.4230/LIPIcs.CONCUR.2015.142'
apa: 'Kretinsky, J., Larsen, K., Laursen, S., & Srba, J. (2015). Polynomial
time decidability of weighted synchronization under partial observability (Vol.
42, pp. 142–154). Presented at the CONCUR: Concurrency Theory, Madrid, Spain:
Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2015.142'
chicago: Kretinsky, Jan, Kim Larsen, Simon Laursen, and Jiří Srba. “Polynomial Time
Decidability of Weighted Synchronization under Partial Observability,” 42:142–54.
Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015. https://doi.org/10.4230/LIPIcs.CONCUR.2015.142.
ieee: 'J. Kretinsky, K. Larsen, S. Laursen, and J. Srba, “Polynomial time decidability
of weighted synchronization under partial observability,” presented at the CONCUR:
Concurrency Theory, Madrid, Spain, 2015, vol. 42, pp. 142–154.'
ista: 'Kretinsky J, Larsen K, Laursen S, Srba J. 2015. Polynomial time decidability
of weighted synchronization under partial observability. CONCUR: Concurrency Theory,
LIPIcs, vol. 42, 142–154.'
mla: Kretinsky, Jan, et al. Polynomial Time Decidability of Weighted Synchronization
under Partial Observability. Vol. 42, Schloss Dagstuhl - Leibniz-Zentrum für
Informatik, 2015, pp. 142–54, doi:10.4230/LIPIcs.CONCUR.2015.142.
short: J. Kretinsky, K. Larsen, S. Laursen, J. Srba, in:, Schloss Dagstuhl - Leibniz-Zentrum
für Informatik, 2015, pp. 142–154.
conference:
end_date: 2015-09-04
location: Madrid, Spain
name: 'CONCUR: Concurrency Theory'
start_date: 2015-09-01
date_created: 2018-12-11T11:52:22Z
date_published: 2015-01-01T00:00:00Z
date_updated: 2021-01-12T06:51:10Z
day: '01'
ddc:
- '000'
- '003'
department:
- _id: ToHe
- _id: KrCh
doi: 10.4230/LIPIcs.CONCUR.2015.142
ec_funded: 1
file:
- access_level: open_access
checksum: 49eb5021caafaabe5356c65b9c5f8c9c
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:08:12Z
date_updated: 2020-07-14T12:44:58Z
file_id: '4672'
file_name: IST-2016-498-v1+1_32.pdf
file_size: 623563
relation: main_file
file_date_updated: 2020-07-14T12:44:58Z
has_accepted_license: '1'
intvolume: ' 42'
language:
- iso: eng
month: '01'
oa: 1
oa_version: Published Version
page: 142 - 154
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: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
- _id: 25681D80-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '291734'
name: International IST Postdoc Fellowship Programme
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '5680'
pubrep_id: '498'
quality_controlled: '1'
scopus_import: 1
status: public
title: Polynomial time decidability of weighted synchronization under partial observability
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 42
year: '2015'
...
---
_id: '1594'
abstract:
- lang: eng
text: Quantitative extensions of temporal logics have recently attracted significant
attention. In this work, we study frequency LTL (fLTL), an extension of LTL which
allows to speak about frequencies of events along an execution. Such an extension
is particularly useful for probabilistic systems that often cannot fulfil strict
qualitative guarantees on the behaviour. It has been recently shown that controller
synthesis for Markov decision processes and fLTL is decidable when all the bounds
on frequencies are 1. As a step towards a complete quantitative solution, we show
that the problem is decidable for the fragment fLTL\GU, where U does not occur
in the scope of G (but still F can). Our solution is based on a novel translation
of such quantitative formulae into equivalent deterministic automata.
acknowledgement: "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 Czech Science Foundation under grant agreement P202/12/G061, by the EU 7th Framework
Programme under grant agreement no. 295261 (MEALS) and 318490 (SENSATION), by the
CDZ project 1023 (CAP), by the CAS/SAFEA International Partnership Program for Creative
Research Teams, by the EPSRC grant EP/M023656/1, by the People Programme (Marie
Curie Actions) of the European Union’s Seventh Framework Programme (FP7/2007–2013)
REA Grant No 291734, by the Austrian Science Fund (FWF) S11407-N23 (RiSE/SHiNE),
and by the ERC Start Grant (279307: Graph Games).\r\n"
alternative_title:
- LNCS
author:
- first_name: Vojtěch
full_name: Forejt, Vojtěch
last_name: Forejt
- first_name: Jan
full_name: Krčál, Jan
last_name: Krčál
- first_name: Jan
full_name: Kretinsky, Jan
id: 44CEF464-F248-11E8-B48F-1D18A9856A87
last_name: Kretinsky
orcid: 0000-0002-8122-2881
citation:
ama: 'Forejt V, Krčál J, Kretinsky J. Controller synthesis for MDPs and frequency
LTL\GU. In: Vol 9450. Springer; 2015:162-177. doi:10.1007/978-3-662-48899-7_12'
apa: 'Forejt, V., Krčál, J., & Kretinsky, J. (2015). Controller synthesis for
MDPs and frequency LTL\GU (Vol. 9450, pp. 162–177). Presented at the LPAR: Logic
for Programming, Artificial Intelligence, and Reasoning, Suva, Fiji: Springer.
https://doi.org/10.1007/978-3-662-48899-7_12'
chicago: Forejt, Vojtěch, Jan Krčál, and Jan Kretinsky. “Controller Synthesis for
MDPs and Frequency LTL\GU,” 9450:162–77. Springer, 2015. https://doi.org/10.1007/978-3-662-48899-7_12.
ieee: 'V. Forejt, J. Krčál, and J. Kretinsky, “Controller synthesis for MDPs and
frequency LTL\GU,” presented at the LPAR: Logic for Programming, Artificial Intelligence,
and Reasoning, Suva, Fiji, 2015, vol. 9450, pp. 162–177.'
ista: 'Forejt V, Krčál J, Kretinsky J. 2015. Controller synthesis for MDPs and frequency
LTL\GU. LPAR: Logic for Programming, Artificial Intelligence, and Reasoning, LNCS,
vol. 9450, 162–177.'
mla: Forejt, Vojtěch, et al. Controller Synthesis for MDPs and Frequency LTL\GU.
Vol. 9450, Springer, 2015, pp. 162–77, doi:10.1007/978-3-662-48899-7_12.
short: V. Forejt, J. Krčál, J. Kretinsky, in:, Springer, 2015, pp. 162–177.
conference:
end_date: 2015-11-28
location: Suva, Fiji
name: 'LPAR: Logic for Programming, Artificial Intelligence, and Reasoning'
start_date: 2015-11-24
date_created: 2018-12-11T11:52:55Z
date_published: 2015-11-22T00:00:00Z
date_updated: 2021-01-12T06:51:50Z
day: '22'
department:
- _id: ToHe
- _id: KrCh
doi: 10.1007/978-3-662-48899-7_12
ec_funded: 1
intvolume: ' 9450'
language:
- iso: eng
month: '11'
oa_version: None
page: 162 - 177
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_status: published
publisher: Springer
publist_id: '5577'
quality_controlled: '1'
scopus_import: 1
status: public
title: Controller synthesis for MDPs and frequency LTL\GU
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 9450
year: '2015'
...
---
_id: '1601'
abstract:
- lang: eng
text: We propose a flexible exchange format for ω-automata, as typically used in
formal verification, and implement support for it in a range of established tools.
Our aim is to simplify the interaction of tools, helping the research community
to build upon other people’s work. A key feature of the format is the use of very
generic acceptance conditions, specified by Boolean combinations of acceptance
primitives, rather than being limited to common cases such as Büchi, Streett,
or Rabin. Such flexibility in the choice of acceptance conditions can be exploited
in applications, for example in probabilistic model checking, and furthermore
encourages the development of acceptance-agnostic tools for automata manipulations.
The format allows acceptance conditions that are either state-based or transition-based,
and also supports alternating automata.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Tomáš
full_name: Babiak, Tomáš
last_name: Babiak
- first_name: František
full_name: Blahoudek, František
last_name: Blahoudek
- first_name: Alexandre
full_name: Duret Lutz, Alexandre
last_name: Duret Lutz
- first_name: Joachim
full_name: Klein, Joachim
last_name: Klein
- first_name: Jan
full_name: Kretinsky, Jan
id: 44CEF464-F248-11E8-B48F-1D18A9856A87
last_name: Kretinsky
orcid: 0000-0002-8122-2881
- first_name: Daniel
full_name: Mueller, Daniel
last_name: Mueller
- first_name: David
full_name: Parker, David
last_name: Parker
- first_name: Jan
full_name: Strejček, Jan
last_name: Strejček
citation:
ama: 'Babiak T, Blahoudek F, Duret Lutz A, et al. The Hanoi omega-automata format.
In: Vol 9206. Springer; 2015:479-486. doi:10.1007/978-3-319-21690-4_31'
apa: 'Babiak, T., Blahoudek, F., Duret Lutz, A., Klein, J., Kretinsky, J., Mueller,
D., … Strejček, J. (2015). The Hanoi omega-automata format (Vol. 9206, pp. 479–486).
Presented at the CAV: Computer Aided Verification, San Francisco, CA, United States:
Springer. https://doi.org/10.1007/978-3-319-21690-4_31'
chicago: Babiak, Tomáš, František Blahoudek, Alexandre Duret Lutz, Joachim Klein,
Jan Kretinsky, Daniel Mueller, David Parker, and Jan Strejček. “The Hanoi Omega-Automata
Format,” 9206:479–86. Springer, 2015. https://doi.org/10.1007/978-3-319-21690-4_31.
ieee: 'T. Babiak et al., “The Hanoi omega-automata format,” presented at
the CAV: Computer Aided Verification, San Francisco, CA, United States, 2015,
vol. 9206, pp. 479–486.'
ista: 'Babiak T, Blahoudek F, Duret Lutz A, Klein J, Kretinsky J, Mueller D, Parker
D, Strejček J. 2015. The Hanoi omega-automata format. CAV: Computer Aided Verification,
LNCS, vol. 9206, 479–486.'
mla: Babiak, Tomáš, et al. The Hanoi Omega-Automata Format. Vol. 9206, Springer,
2015, pp. 479–86, doi:10.1007/978-3-319-21690-4_31.
short: T. Babiak, F. Blahoudek, A. Duret Lutz, J. Klein, J. Kretinsky, D. Mueller,
D. Parker, J. Strejček, in:, Springer, 2015, pp. 479–486.
conference:
end_date: 2015-07-24
location: San Francisco, CA, United States
name: 'CAV: Computer Aided Verification'
start_date: 2015-07-18
date_created: 2018-12-11T11:52:57Z
date_published: 2015-07-16T00:00:00Z
date_updated: 2021-01-12T06:51:54Z
day: '16'
ddc:
- '000'
department:
- _id: ToHe
- _id: KrCh
doi: 10.1007/978-3-319-21690-4_31
ec_funded: 1
file:
- access_level: open_access
checksum: 5885236fa88a439baba9ac6f3e801e93
content_type: application/pdf
creator: dernst
date_created: 2020-05-15T08:38:12Z
date_updated: 2020-07-14T12:45:04Z
file_id: '7850'
file_name: 2015_CAV_Babiak.pdf
file_size: 1651779
relation: main_file
file_date_updated: 2020-07-14T12:45:04Z
has_accepted_license: '1'
intvolume: ' 9206'
language:
- iso: eng
month: '07'
oa: 1
oa_version: Submitted Version
page: 479 - 486
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
- _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
publication_status: published
publisher: Springer
publist_id: '5566'
quality_controlled: '1'
scopus_import: 1
status: public
title: The Hanoi omega-automata format
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 9206
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: '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: '1657'
abstract:
- lang: eng
text: 'We consider Markov decision processes (MDPs) with multiple limit-average
(or mean-payoff) objectives. There exist two different views: (i) ~the expectation
semantics, where the goal is to optimize the expected mean-payoff objective, and
(ii) ~the satisfaction semantics, where the goal is to maximize the probability
of runs such that the mean-payoff value stays above a given vector. We consider
optimization with respect to both objectives at once, thus unifying the existing
semantics. Precisely, the goal is to optimize the expectation while ensuring the
satisfaction constraint. Our problem captures the notion of optimization with
respect to strategies that are risk-averse (i.e., Ensure certain probabilistic
guarantee). Our main results are as follows: First, we present algorithms for
the decision problems, which are always polynomial in the size of the MDP. We
also show that an approximation of the Pareto curve can be computed in time polynomial
in the size of the MDP, and the approximation factor, but exponential in the number
of dimensions. Second, we present a complete characterization of the strategy
complexity (in terms of memory bounds and randomization) required to solve our
problem. '
acknowledgement: "A Technical Report of this paper is available at: https://repository.ist.ac.at/327\r\n"
alternative_title:
- LICS
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Zuzana
full_name: Komárková, Zuzana
last_name: Komárková
- first_name: Jan
full_name: Kretinsky, Jan
id: 44CEF464-F248-11E8-B48F-1D18A9856A87
last_name: Kretinsky
orcid: 0000-0002-8122-2881
citation:
ama: Chatterjee K, Komárková Z, Kretinsky J. Unifying two views on multiple mean-payoff
objectives in Markov decision processes. 2015:244-256. doi:10.1109/LICS.2015.32
apa: 'Chatterjee, K., Komárková, Z., & Kretinsky, J. (2015). Unifying two views
on multiple mean-payoff objectives in Markov decision processes. Presented at
the LICS: Logic in Computer Science, Kyoto, Japan: IEEE. https://doi.org/10.1109/LICS.2015.32'
chicago: Chatterjee, Krishnendu, Zuzana Komárková, and Jan Kretinsky. “Unifying
Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes.” LICS.
IEEE, 2015. https://doi.org/10.1109/LICS.2015.32.
ieee: K. Chatterjee, Z. Komárková, and J. Kretinsky, “Unifying two views on multiple
mean-payoff objectives in Markov decision processes.” IEEE, pp. 244–256, 2015.
ista: Chatterjee K, Komárková Z, Kretinsky J. 2015. Unifying two views on multiple
mean-payoff objectives in Markov decision processes. , 244–256.
mla: Chatterjee, Krishnendu, et al. Unifying Two Views on Multiple Mean-Payoff
Objectives in Markov Decision Processes. IEEE, 2015, pp. 244–56, doi:10.1109/LICS.2015.32.
short: K. Chatterjee, Z. Komárková, J. Kretinsky, (2015) 244–256.
conference:
end_date: 2015-07-10
location: Kyoto, Japan
name: 'LICS: Logic in Computer Science'
start_date: 2015-07-06
date_created: 2018-12-11T11:53:18Z
date_published: 2015-07-01T00:00:00Z
date_updated: 2023-02-23T12:26:16Z
day: '01'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1109/LICS.2015.32
ec_funded: 1
language:
- iso: eng
month: '07'
oa_version: None
page: 244 - 256
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: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _id: 25681D80-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '291734'
name: International IST Postdoc Fellowship Programme
publication_status: published
publisher: IEEE
publist_id: '5493'
quality_controlled: '1'
related_material:
record:
- id: '466'
relation: later_version
status: public
- id: '5429'
relation: earlier_version
status: public
- id: '5435'
relation: earlier_version
status: public
scopus_import: 1
series_title: LICS
status: public
title: Unifying two views on multiple mean-payoff objectives in Markov decision processes
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2015'
...
---
_id: '5429'
abstract:
- lang: eng
text: "We consider Markov decision processes (MDPs) with multiple limit-average
(or mean-payoff) objectives. \r\nThere have been two different views: (i) the
expectation semantics, where the goal is to optimize the expected mean-payoff
objective, and (ii) the satisfaction semantics, where the goal is to maximize
the probability of runs such that the mean-payoff value stays above a given vector.
\ \r\nWe consider the problem where the goal is to optimize the expectation under
the constraint that the satisfaction semantics is ensured, and thus consider a
generalization that unifies the existing semantics.\r\nOur problem captures the
notion of optimization with respect to strategies that are risk-averse (i.e.,
ensures certain probabilistic guarantee).\r\nOur main results are algorithms for
the decision problem which are always polynomial in the size of the MDP. We also
show that an approximation of the Pareto-curve can be computed in time polynomial
in the size of the MDP, and the approximation factor, but exponential in the number
of dimensions.\r\nFinally, we present a complete characterization of the strategy
complexity (in terms of memory bounds and randomization) required to solve our
problem."
alternative_title:
- IST Austria Technical Report
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Zuzana
full_name: Komarkova, Zuzana
last_name: Komarkova
- first_name: Jan
full_name: Kretinsky, Jan
id: 44CEF464-F248-11E8-B48F-1D18A9856A87
last_name: Kretinsky
orcid: 0000-0002-8122-2881
citation:
ama: Chatterjee K, Komarkova Z, Kretinsky J. Unifying Two Views on Multiple Mean-Payoff
Objectives in Markov Decision Processes. IST Austria; 2015. doi:10.15479/AT:IST-2015-318-v1-1
apa: Chatterjee, K., Komarkova, Z., & Kretinsky, J. (2015). Unifying two
views on multiple mean-payoff objectives in Markov decision processes. IST
Austria. https://doi.org/10.15479/AT:IST-2015-318-v1-1
chicago: Chatterjee, Krishnendu, Zuzana Komarkova, and Jan Kretinsky. Unifying
Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes.
IST Austria, 2015. https://doi.org/10.15479/AT:IST-2015-318-v1-1.
ieee: K. Chatterjee, Z. Komarkova, and J. Kretinsky, Unifying two views on multiple
mean-payoff objectives in Markov decision processes. IST Austria, 2015.
ista: Chatterjee K, Komarkova Z, Kretinsky J. 2015. Unifying two views on multiple
mean-payoff objectives in Markov decision processes, IST Austria, 41p.
mla: Chatterjee, Krishnendu, et al. Unifying Two Views on Multiple Mean-Payoff
Objectives in Markov Decision Processes. IST Austria, 2015, doi:10.15479/AT:IST-2015-318-v1-1.
short: K. Chatterjee, Z. Komarkova, J. Kretinsky, Unifying Two Views on Multiple
Mean-Payoff Objectives in Markov Decision Processes, IST Austria, 2015.
date_created: 2018-12-12T11:39:17Z
date_published: 2015-01-12T00:00:00Z
date_updated: 2023-02-23T12:26:16Z
day: '12'
ddc:
- '004'
department:
- _id: KrCh
doi: 10.15479/AT:IST-2015-318-v1-1
file:
- access_level: open_access
checksum: e4869a584567c506349abda9c8ec7db3
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:54:11Z
date_updated: 2020-07-14T12:46:52Z
file_id: '5533'
file_name: IST-2015-318-v1+1_main.pdf
file_size: 689863
relation: main_file
file_date_updated: 2020-07-14T12:46:52Z
has_accepted_license: '1'
language:
- iso: eng
month: '01'
oa: 1
oa_version: Published Version
page: '41'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '318'
related_material:
record:
- id: '1657'
relation: later_version
status: public
- id: '466'
relation: later_version
status: public
- id: '5435'
relation: later_version
status: public
status: public
title: Unifying two views on multiple mean-payoff objectives in Markov decision processes
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2015'
...
---
_id: '5435'
abstract:
- lang: eng
text: "We consider Markov decision processes (MDPs) with multiple limit-average
(or mean-payoff) objectives. \r\nThere have been two different views: (i) the
expectation semantics, where the goal is to optimize the expected mean-payoff
objective, and (ii) the satisfaction semantics, where the goal is to maximize
the probability of runs such that the mean-payoff value stays above a given vector.
\ \r\nWe consider the problem where the goal is to optimize the expectation under
the constraint that the satisfaction semantics is ensured, and thus consider a
generalization that unifies the existing semantics. Our problem captures the notion
of optimization with respect to strategies that are risk-averse (i.e., ensures
certain probabilistic guarantee).\r\nOur main results are algorithms for the decision
problem which are always polynomial in the size of the MDP.\r\nWe also show that
an approximation of the Pareto-curve can be computed in time polynomial in the
size of the MDP, and the approximation factor, but exponential in the number of
dimensions. Finally, we present a complete characterization of the strategy complexity
(in terms of memory bounds and randomization) required to solve our problem."
alternative_title:
- IST Austria Technical Report
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Zuzana
full_name: Komarkova, Zuzana
last_name: Komarkova
- first_name: Jan
full_name: Kretinsky, Jan
id: 44CEF464-F248-11E8-B48F-1D18A9856A87
last_name: Kretinsky
orcid: 0000-0002-8122-2881
citation:
ama: Chatterjee K, Komarkova Z, Kretinsky J. Unifying Two Views on Multiple Mean-Payoff
Objectives in Markov Decision Processes. IST Austria; 2015. doi:10.15479/AT:IST-2015-318-v2-1
apa: Chatterjee, K., Komarkova, Z., & Kretinsky, J. (2015). Unifying two
views on multiple mean-payoff objectives in Markov decision processes. IST
Austria. https://doi.org/10.15479/AT:IST-2015-318-v2-1
chicago: Chatterjee, Krishnendu, Zuzana Komarkova, and Jan Kretinsky. Unifying
Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes.
IST Austria, 2015. https://doi.org/10.15479/AT:IST-2015-318-v2-1.
ieee: K. Chatterjee, Z. Komarkova, and J. Kretinsky, Unifying two views on multiple
mean-payoff objectives in Markov decision processes. IST Austria, 2015.
ista: Chatterjee K, Komarkova Z, Kretinsky J. 2015. Unifying two views on multiple
mean-payoff objectives in Markov decision processes, IST Austria, 51p.
mla: Chatterjee, Krishnendu, et al. Unifying Two Views on Multiple Mean-Payoff
Objectives in Markov Decision Processes. IST Austria, 2015, doi:10.15479/AT:IST-2015-318-v2-1.
short: K. Chatterjee, Z. Komarkova, J. Kretinsky, Unifying Two Views on Multiple
Mean-Payoff Objectives in Markov Decision Processes, IST Austria, 2015.
date_created: 2018-12-12T11:39:19Z
date_published: 2015-02-23T00:00:00Z
date_updated: 2023-02-23T12:26:00Z
day: '23'
ddc:
- '004'
department:
- _id: KrCh
doi: 10.15479/AT:IST-2015-318-v2-1
file:
- access_level: open_access
checksum: 75284adec80baabdfe71ff9ebbc27445
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:54:03Z
date_updated: 2020-07-14T12:46:53Z
file_id: '5525'
file_name: IST-2015-318-v2+1_main.pdf
file_size: 717630
relation: main_file
file_date_updated: 2020-07-14T12:46:53Z
has_accepted_license: '1'
language:
- iso: eng
month: '02'
oa: 1
oa_version: Published Version
page: '51'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '327'
related_material:
record:
- id: '1657'
relation: later_version
status: public
- id: '466'
relation: later_version
status: public
- id: '5429'
relation: earlier_version
status: public
status: public
title: Unifying two views on multiple mean-payoff objectives in Markov decision processes
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2015'
...
---
_id: '1502'
abstract:
- lang: eng
text: We extend the theory of input-output conformance with operators for merge
and quotient. The former is useful when testing against multiple requirements
or views. The latter can be used to generate tests for patches of an already tested
system. Both operators can combine systems with different action alphabets, which
is usually the case when constructing complex systems and specifications from
parts, for instance different views as well as newly defined functionality of
a~previous version of the system.
acknowledgement: "This research was funded in part by the European Research Council
(ERC) under grant agreement 267989 (QUAREM), by the Austrian Science Fund (FWF)
projects S11402-N23(RiSE) and Z211-N23 (Wittgestein Award), by People Programme
(Marie Curie Actions) of the European Union's Seventh Framework Programme (FP7/2007-2013)
under REA grant agreement 291734, and by the ARTEMIS JU under grant agreement 295373
(nSafeCer). Jan Křetínský has been partially supported by the Czech Science Foundation,
grant No. P202/12/G061. Nikola Beneš has been supported by the\r\nMEYS project
No. CZ.1.07/2.3.00/30.0009 Employment of Newly Graduated Doctors of Science for
Scientific Excellence."
alternative_title:
- 'Proceedings of the 18th International ACM SIGSOFT Symposium on Component-Based
Software Engineering '
author:
- first_name: Nikola
full_name: Beneš, Nikola
last_name: Beneš
- first_name: Przemyslaw
full_name: Daca, Przemyslaw
id: 49351290-F248-11E8-B48F-1D18A9856A87
last_name: Daca
- 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: Jan
full_name: Kretinsky, Jan
id: 44CEF464-F248-11E8-B48F-1D18A9856A87
last_name: Kretinsky
orcid: 0000-0002-8122-2881
- first_name: Dejan
full_name: Nickovic, Dejan
last_name: Nickovic
citation:
ama: 'Beneš N, Daca P, Henzinger TA, Kretinsky J, Nickovic D. Complete composition
operators for IOCO-testing theory. In: ACM; 2015:101-110. doi:10.1145/2737166.2737175'
apa: 'Beneš, N., Daca, P., Henzinger, T. A., Kretinsky, J., & Nickovic, D. (2015).
Complete composition operators for IOCO-testing theory (pp. 101–110). Presented
at the CBSE: Component-Based Software Engineering , Montreal, QC, Canada: ACM.
https://doi.org/10.1145/2737166.2737175'
chicago: Beneš, Nikola, Przemyslaw Daca, Thomas A Henzinger, Jan Kretinsky, and
Dejan Nickovic. “Complete Composition Operators for IOCO-Testing Theory,” 101–10.
ACM, 2015. https://doi.org/10.1145/2737166.2737175.
ieee: 'N. Beneš, P. Daca, T. A. Henzinger, J. Kretinsky, and D. Nickovic, “Complete
composition operators for IOCO-testing theory,” presented at the CBSE: Component-Based
Software Engineering , Montreal, QC, Canada, 2015, pp. 101–110.'
ista: 'Beneš N, Daca P, Henzinger TA, Kretinsky J, Nickovic D. 2015. Complete composition
operators for IOCO-testing theory. CBSE: Component-Based Software Engineering
, Proceedings of the 18th International ACM SIGSOFT Symposium on Component-Based
Software Engineering , , 101–110.'
mla: Beneš, Nikola, et al. Complete Composition Operators for IOCO-Testing Theory.
ACM, 2015, pp. 101–10, doi:10.1145/2737166.2737175.
short: N. Beneš, P. Daca, T.A. Henzinger, J. Kretinsky, D. Nickovic, in:, ACM, 2015,
pp. 101–110.
conference:
end_date: 2015-05-08
location: Montreal, QC, Canada
name: 'CBSE: Component-Based Software Engineering '
start_date: 2015-05-04
date_created: 2018-12-11T11:52:24Z
date_published: 2015-05-01T00:00:00Z
date_updated: 2023-09-07T11:58:33Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
- _id: KrCh
doi: 10.1145/2737166.2737175
ec_funded: 1
file:
- access_level: open_access
checksum: c6ce681035c163a158751f240cb7d389
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:17:46Z
date_updated: 2020-07-14T12:44:59Z
file_id: '5303'
file_name: IST-2016-625-v1+1_conf-cbse-BenesDHKN15.pdf
file_size: 467561
relation: main_file
file_date_updated: 2020-07-14T12:44:59Z
has_accepted_license: '1'
language:
- iso: eng
month: '05'
oa: 1
oa_version: Submitted Version
page: 101 - 110
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: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
- _id: 25681D80-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '291734'
name: International IST Postdoc Fellowship Programme
publication_identifier:
isbn:
- 978-1-4503-3471-6
publication_status: published
publisher: ACM
publist_id: '5676'
pubrep_id: '625'
quality_controlled: '1'
related_material:
record:
- id: '1155'
relation: dissertation_contains
status: public
scopus_import: 1
status: public
title: Complete composition operators for IOCO-testing theory
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
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: '1603'
abstract:
- lang: eng
text: "For deterministic systems, a counterexample to a property can simply be an
error trace, whereas counterexamples in probabilistic systems are necessarily
more complex. For instance, a set of erroneous traces with a sufficient cumulative
probability mass can be used. Since these are too large objects to understand
and manipulate, compact representations such as subchains have been considered.
In the case of probabilistic systems with non-determinism, the situation is even
more complex. While a subchain for a given strategy (or scheduler, resolving non-determinism)
is a straightforward choice, we take a different approach. Instead, we focus on
the strategy itself, and extract the most important decisions it makes, and present
its succinct representation.\r\nThe key tools we employ to achieve this are (1)
introducing a concept of importance of a state w.r.t. the strategy, and (2) learning
using decision trees. There are three main consequent advantages of our approach.
Firstly, it exploits the quantitative information on states, stressing the more
important decisions. Secondly, it leads to a greater variability and degree of
freedom in representing the strategies. Thirdly, the representation uses a self-explanatory
data structure. In summary, our approach produces more succinct and more explainable
strategies, as opposed to e.g. binary decision diagrams. Finally, our experimental
results show that we can extract several rules describing the strategy even for
very large systems that do not fit in memory, and based on the rules explain the
erroneous behaviour."
acknowledgement: This research was funded in part by Austrian Science Fund (FWF) Grant
No P 23499-N23, FWF NFN Grant No S11407-N23 (RiSE) and Z211-N23 (Wittgenstein Award),
European Research Council (ERC) Grant No 279307 (Graph Games), ERC Grant No 267989
(QUAREM), the Czech Science Foundation Grant No P202/12/G061, and People Programme
(Marie Curie Actions) of the European Union’s Seventh Framework Programme (FP7/2007–2013)
REA Grant No 291734.
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: Martin
full_name: Chmelik, Martin
id: 3624234E-F248-11E8-B48F-1D18A9856A87
last_name: Chmelik
- first_name: Andreas
full_name: Fellner, Andreas
id: 42BABFB4-F248-11E8-B48F-1D18A9856A87
last_name: Fellner
- first_name: Jan
full_name: Kretinsky, Jan
id: 44CEF464-F248-11E8-B48F-1D18A9856A87
last_name: Kretinsky
orcid: 0000-0002-8122-2881
citation:
ama: 'Brázdil T, Chatterjee K, Chmelik M, Fellner A, Kretinsky J. Counterexample
explanation by learning small strategies in Markov decision processes. In: Vol
9206. Springer; 2015:158-177. doi:10.1007/978-3-319-21690-4_10'
apa: 'Brázdil, T., Chatterjee, K., Chmelik, M., Fellner, A., & Kretinsky, J.
(2015). Counterexample explanation by learning small strategies in Markov decision
processes (Vol. 9206, pp. 158–177). Presented at the CAV: Computer Aided Verification,
San Francisco, CA, United States: Springer. https://doi.org/10.1007/978-3-319-21690-4_10'
chicago: Brázdil, Tomáš, Krishnendu Chatterjee, Martin Chmelik, Andreas Fellner,
and Jan Kretinsky. “Counterexample Explanation by Learning Small Strategies in
Markov Decision Processes,” 9206:158–77. Springer, 2015. https://doi.org/10.1007/978-3-319-21690-4_10.
ieee: 'T. Brázdil, K. Chatterjee, M. Chmelik, A. Fellner, and J. Kretinsky, “Counterexample
explanation by learning small strategies in Markov decision processes,” presented
at the CAV: Computer Aided Verification, San Francisco, CA, United States, 2015,
vol. 9206, pp. 158–177.'
ista: 'Brázdil T, Chatterjee K, Chmelik M, Fellner A, Kretinsky J. 2015. Counterexample
explanation by learning small strategies in Markov decision processes. CAV: Computer
Aided Verification, LNCS, vol. 9206, 158–177.'
mla: Brázdil, Tomáš, et al. Counterexample Explanation by Learning Small Strategies
in Markov Decision Processes. Vol. 9206, Springer, 2015, pp. 158–77, doi:10.1007/978-3-319-21690-4_10.
short: T. Brázdil, K. Chatterjee, M. Chmelik, A. Fellner, J. Kretinsky, in:, Springer,
2015, pp. 158–177.
conference:
end_date: 2015-07-24
location: San Francisco, CA, United States
name: 'CAV: Computer Aided Verification'
start_date: 2015-07-18
date_created: 2018-12-11T11:52:58Z
date_published: 2015-07-16T00:00:00Z
date_updated: 2024-02-21T13:52:07Z
day: '16'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1007/978-3-319-21690-4_10
ec_funded: 1
intvolume: ' 9206'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1502.02834
month: '07'
oa: 1
oa_version: Preprint
page: 158 - 177
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: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _id: 25681D80-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '291734'
name: International IST Postdoc Fellowship Programme
publication_identifier:
eisbn:
- 978-3-319-21690-4
publication_status: published
publisher: Springer
publist_id: '5564'
quality_controlled: '1'
related_material:
record:
- id: '5549'
relation: research_paper
status: public
scopus_import: 1
status: public
title: Counterexample explanation by learning small strategies in Markov decision
processes
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 9206
year: '2015'
...
---
_id: '2027'
abstract:
- lang: eng
text: We present a general framework for applying machine-learning algorithms to
the verification of Markov decision processes (MDPs). The primary goal of these
techniques is to improve performance by avoiding an exhaustive exploration of
the state space. Our framework focuses on probabilistic reachability, which is
a core property for verification, and is illustrated through two distinct instantiations.
The first assumes that full knowledge of the MDP is available, and performs a
heuristic-driven partial exploration of the model, yielding precise lower and
upper bounds on the required probability. The second tackles the case where we
may only sample the MDP, and yields probabilistic guarantees, again in terms of
both the lower and upper bounds, which provides efficient stopping criteria for
the approximation. The latter is the first extension of statistical model checking
for unbounded properties inMDPs. In contrast with other related techniques, our
approach is not restricted to time-bounded (finite-horizon) or discounted properties,
nor does it assume any particular properties of the MDP. We also show how our
methods extend to LTL objectives. We present experimental results showing the
performance of our framework on several examples.
acknowledgement: This research was funded in part by the European Research Council
(ERC) under grant agreement 246967 (VERIWARE), by the EU FP7 project HIERATIC, by
the Czech Science Foundation grant No P202/12/P612, by EPSRC project EP/K038575/1.
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: Martin
full_name: Chmelik, Martin
id: 3624234E-F248-11E8-B48F-1D18A9856A87
last_name: Chmelik
- first_name: Vojtěch
full_name: Forejt, Vojtěch
last_name: Forejt
- first_name: Jan
full_name: Kretinsky, Jan
id: 44CEF464-F248-11E8-B48F-1D18A9856A87
last_name: Kretinsky
orcid: 0000-0002-8122-2881
- first_name: Marta
full_name: Kwiatkowska, Marta
last_name: Kwiatkowska
- first_name: David
full_name: Parker, David
last_name: Parker
- first_name: Mateusz
full_name: Ujma, Mateusz
last_name: Ujma
citation:
ama: 'Brázdil T, Chatterjee K, Chmelik M, et al. Verification of markov decision
processes using learning algorithms. In: Cassez F, Raskin J-F, eds. Lecture
Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence
and Lecture Notes in Bioinformatics). Vol 8837. Society of Industrial and
Applied Mathematics; 2014:98-114. doi:10.1007/978-3-319-11936-6_8'
apa: 'Brázdil, T., Chatterjee, K., Chmelik, M., Forejt, V., Kretinsky, J., Kwiatkowska,
M., … Ujma, M. (2014). Verification of markov decision processes using learning
algorithms. In F. Cassez & J.-F. Raskin (Eds.), Lecture Notes in Computer
Science (including subseries Lecture Notes in Artificial Intelligence and Lecture
Notes in Bioinformatics) (Vol. 8837, pp. 98–114). Sydney, Australia: Society
of Industrial and Applied Mathematics. https://doi.org/10.1007/978-3-319-11936-6_8'
chicago: Brázdil, Tomáš, Krishnendu Chatterjee, Martin Chmelik, Vojtěch Forejt,
Jan Kretinsky, Marta Kwiatkowska, David Parker, and Mateusz Ujma. “Verification
of Markov Decision Processes Using Learning Algorithms.” In Lecture Notes
in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence
and Lecture Notes in Bioinformatics), edited by Franck Cassez and Jean-François
Raskin, 8837:98–114. Society of Industrial and Applied Mathematics, 2014. https://doi.org/10.1007/978-3-319-11936-6_8.
ieee: T. Brázdil et al., “Verification of markov decision processes using
learning algorithms,” in Lecture Notes in Computer Science (including subseries
Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics),
Sydney, Australia, 2014, vol. 8837, pp. 98–114.
ista: 'Brázdil T, Chatterjee K, Chmelik M, Forejt V, Kretinsky J, Kwiatkowska M,
Parker D, Ujma M. 2014. Verification of markov decision processes using learning
algorithms. Lecture Notes in Computer Science (including subseries Lecture Notes
in Artificial Intelligence and Lecture Notes in Bioinformatics). ALENEX: Algorithm
Engineering and Experiments, LNCS, vol. 8837, 98–114.'
mla: Brázdil, Tomáš, et al. “Verification of Markov Decision Processes Using Learning
Algorithms.” Lecture Notes in Computer Science (Including Subseries Lecture
Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), edited
by Franck Cassez and Jean-François Raskin, vol. 8837, Society of Industrial and
Applied Mathematics, 2014, pp. 98–114, doi:10.1007/978-3-319-11936-6_8.
short: T. Brázdil, K. Chatterjee, M. Chmelik, V. Forejt, J. Kretinsky, M. Kwiatkowska,
D. Parker, M. Ujma, in:, F. Cassez, J.-F. Raskin (Eds.), Lecture Notes in Computer
Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture
Notes in Bioinformatics), Society of Industrial and Applied Mathematics, 2014,
pp. 98–114.
conference:
end_date: 2014-11-07
location: Sydney, Australia
name: 'ALENEX: Algorithm Engineering and Experiments'
start_date: 2014-11-03
date_created: 2018-12-11T11:55:17Z
date_published: 2014-11-01T00:00:00Z
date_updated: 2021-01-12T06:54:49Z
day: '01'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1007/978-3-319-11936-6_8
ec_funded: 1
editor:
- first_name: Franck
full_name: Cassez, Franck
last_name: Cassez
- first_name: Jean-François
full_name: Raskin, Jean-François
last_name: Raskin
intvolume: ' 8837'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1402.2967
month: '11'
oa: 1
oa_version: Submitted Version
page: 98 - 114
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _id: 26241A12-B435-11E9-9278-68D0E5697425
grant_number: '24696'
name: LIGHT-REGULATED LIGAND TRAPS FOR SPATIO-TEMPORAL INHIBITION OF CELL SIGNALING
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 25F5A88A-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11402-N23
name: Moderne Concurrency Paradigms
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11407
name: Game Theory
- _id: 2584A770-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: P 23499-N23
name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 2587B514-B435-11E9-9278-68D0E5697425
name: Microsoft Research Faculty Fellowship
publication: ' Lecture Notes in Computer Science (including subseries Lecture Notes
in Artificial Intelligence and Lecture Notes in Bioinformatics)'
publication_status: published
publisher: Society of Industrial and Applied Mathematics
publist_id: '5046'
quality_controlled: '1'
status: public
title: Verification of markov decision processes using learning algorithms
type: conference
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
volume: 8837
year: '2014'
...
---
_id: '2026'
abstract:
- lang: eng
text: 'We present a tool for translating LTL formulae into deterministic ω-automata.
It is the first tool that covers the whole LTL that does not use Safra’s determinization
or any of its variants. This leads to smaller automata. There are several outputs
of the tool: firstly, deterministic Rabin automata, which are the standard input
for probabilistic model checking, e.g. for the probabilistic model-checker PRISM;
secondly, deterministic generalized Rabin automata, which can also be used for
probabilistic model checking and are sometimes by orders of magnitude smaller.
We also link our tool to PRISM and show that this leads to a significant speed-up
of probabilistic LTL model checking, especially with the generalized Rabin automata.'
acknowledgement: "Sponsor: P202/12/G061; GACR; Czech Science Foundation\r\n\r\n"
alternative_title:
- LNCS
author:
- first_name: Zuzana
full_name: Komárková, Zuzana
last_name: Komárková
- first_name: Jan
full_name: Kretinsky, Jan
id: 44CEF464-F248-11E8-B48F-1D18A9856A87
last_name: Kretinsky
orcid: 0000-0002-8122-2881
citation:
ama: 'Komárková Z, Kretinsky J. Rabinizer 3: Safraless translation of ltl to small
deterministic automata. In: Cassez F, Raskin J-F, eds. Lecture Notes in Computer
Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture
Notes in Bioinformatics). Vol 8837. Springer; 2014:235-241. doi:10.1007/978-3-319-11936-6_17'
apa: 'Komárková, Z., & Kretinsky, J. (2014). Rabinizer 3: Safraless translation
of ltl to small deterministic automata. In F. Cassez & J.-F. Raskin (Eds.),
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial
Intelligence and Lecture Notes in Bioinformatics) (Vol. 8837, pp. 235–241).
Sydney, Australia: Springer. https://doi.org/10.1007/978-3-319-11936-6_17'
chicago: 'Komárková, Zuzana, and Jan Kretinsky. “Rabinizer 3: Safraless Translation
of Ltl to Small Deterministic Automata.” In Lecture Notes in Computer Science
(Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes
in Bioinformatics), edited by Franck Cassez and Jean-François Raskin, 8837:235–41.
Springer, 2014. https://doi.org/10.1007/978-3-319-11936-6_17.'
ieee: 'Z. Komárková and J. Kretinsky, “Rabinizer 3: Safraless translation of ltl
to small deterministic automata,” in Lecture Notes in Computer Science (including
subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics),
Sydney, Australia, 2014, vol. 8837, pp. 235–241.'
ista: 'Komárková Z, Kretinsky J. 2014. Rabinizer 3: Safraless translation of ltl
to small deterministic automata. Lecture Notes in Computer Science (including
subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics).
ATVA: Automated Technology for Verification and Analysis, LNCS, vol. 8837, 235–241.'
mla: 'Komárková, Zuzana, and Jan Kretinsky. “Rabinizer 3: Safraless Translation
of Ltl to Small Deterministic Automata.” Lecture Notes in Computer Science
(Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes
in Bioinformatics), edited by Franck Cassez and Jean-François Raskin, vol.
8837, Springer, 2014, pp. 235–41, doi:10.1007/978-3-319-11936-6_17.'
short: Z. Komárková, J. Kretinsky, in:, F. Cassez, J.-F. Raskin (Eds.), Lecture
Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence
and Lecture Notes in Bioinformatics), Springer, 2014, pp. 235–241.
conference:
end_date: 2014-11-07
location: Sydney, Australia
name: 'ATVA: Automated Technology for Verification and Analysis'
start_date: 2014-11-03
date_created: 2018-12-11T11:55:17Z
date_published: 2014-01-01T00:00:00Z
date_updated: 2021-01-12T06:54:49Z
day: '01'
department:
- _id: ToHe
doi: 10.1007/978-3-319-11936-6_17
ec_funded: 1
editor:
- first_name: Franck
full_name: Cassez, Franck
last_name: Cassez
- first_name: Jean-François
full_name: Raskin, Jean-François
last_name: Raskin
intvolume: ' 8837'
language:
- iso: eng
month: '01'
oa_version: None
page: 235 - 241
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _id: 25F5A88A-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11402-N23
name: Moderne Concurrency Paradigms
publication: Lecture Notes in Computer Science (including subseries Lecture Notes
in Artificial Intelligence and Lecture Notes in Bioinformatics)
publication_status: published
publisher: Springer
publist_id: '5045'
quality_controlled: '1'
status: public
title: 'Rabinizer 3: Safraless translation of ltl to small deterministic automata'
type: conference
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
volume: 8837
year: '2014'
...
---
_id: '2053'
abstract:
- lang: eng
text: In contrast to the usual understanding of probabilistic systems as stochastic
processes, recently these systems have also been regarded as transformers of probabilities.
In this paper, we give a natural definition of strong bisimulation for probabilistic
systems corresponding to this view that treats probability distributions as first-class
citizens. Our definition applies in the same way to discrete systems as well as
to systems with uncountable state and action spaces. Several examples demonstrate
that our definition refines the understanding of behavioural equivalences of probabilistic
systems. In particular, it solves a longstanding open problem concerning the representation
of memoryless continuous time by memoryfull continuous time. Finally, we give
algorithms for computing this bisimulation not only for finite but also for classes
of uncountably infinite systems.
acknowledgement: This work is supported by the EU 7th Framework Programme under grant
agreements 295261 (MEALS) and 318490 (SENSATION), Czech Science Foundation under
grant agreement P202/12/G061, the DFG Transregional Collaborative Research Centre
SFB/TR 14 AVACS, and by the CAS/SAFEA International Partnership Program for Creative
Research Teams.
alternative_title:
- LNCS
author:
- first_name: Holger
full_name: Hermanns, Holger
last_name: Hermanns
- first_name: Jan
full_name: Krčál, Jan
last_name: Krčál
- first_name: Jan
full_name: Kretinsky, Jan
id: 44CEF464-F248-11E8-B48F-1D18A9856A87
last_name: Kretinsky
orcid: 0000-0002-8122-2881
citation:
ama: 'Hermanns H, Krčál J, Kretinsky J. Probabilistic bisimulation: Naturally on
distributions. In: Baldan P, Gorla D, eds. Lecture Notes in Computer Science
(Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes
in Bioinformatics). Vol 8704. Schloss Dagstuhl - Leibniz-Zentrum für Informatik;
2014:249-265. doi:10.1007/978-3-662-44584-6_18'
apa: 'Hermanns, H., Krčál, J., & Kretinsky, J. (2014). Probabilistic bisimulation:
Naturally on distributions. In P. Baldan & D. Gorla (Eds.), Lecture Notes
in Computer Science (including subseries Lecture Notes in Artificial Intelligence
and Lecture Notes in Bioinformatics) (Vol. 8704, pp. 249–265). Rome, Italy:
Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.1007/978-3-662-44584-6_18'
chicago: 'Hermanns, Holger, Jan Krčál, and Jan Kretinsky. “Probabilistic Bisimulation:
Naturally on Distributions.” In Lecture Notes in Computer Science (Including
Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics),
edited by Paolo Baldan and Daniele Gorla, 8704:249–65. Schloss Dagstuhl - Leibniz-Zentrum
für Informatik, 2014. https://doi.org/10.1007/978-3-662-44584-6_18.'
ieee: 'H. Hermanns, J. Krčál, and J. Kretinsky, “Probabilistic bisimulation: Naturally
on distributions,” in Lecture Notes in Computer Science (including subseries
Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics),
Rome, Italy, 2014, vol. 8704, pp. 249–265.'
ista: 'Hermanns H, Krčál J, Kretinsky J. 2014. Probabilistic bisimulation: Naturally
on distributions. Lecture Notes in Computer Science (including subseries Lecture
Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). CONCUR:
Concurrency Theory, LNCS, vol. 8704, 249–265.'
mla: 'Hermanns, Holger, et al. “Probabilistic Bisimulation: Naturally on Distributions.”
Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial
Intelligence and Lecture Notes in Bioinformatics), edited by Paolo Baldan
and Daniele Gorla, vol. 8704, Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
2014, pp. 249–65, doi:10.1007/978-3-662-44584-6_18.'
short: H. Hermanns, J. Krčál, J. Kretinsky, in:, P. Baldan, D. Gorla (Eds.), Lecture
Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence
and Lecture Notes in Bioinformatics), Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
2014, pp. 249–265.
conference:
end_date: 2014-09-05
location: Rome, Italy
name: 'CONCUR: Concurrency Theory'
start_date: 2014-09-02
date_created: 2018-12-11T11:55:27Z
date_published: 2014-09-01T00:00:00Z
date_updated: 2021-01-12T06:55:00Z
day: '01'
department:
- _id: ToHe
- _id: KrCh
doi: 10.1007/978-3-662-44584-6_18
ec_funded: 1
editor:
- first_name: Paolo
full_name: Baldan, Paolo
last_name: Baldan
- first_name: Daniele
full_name: Gorla, Daniele
last_name: Gorla
intvolume: ' 8704'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1404.5084
month: '09'
oa: 1
oa_version: Submitted Version
page: 249 - 265
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _id: 25F5A88A-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11402-N23
name: Moderne Concurrency Paradigms
publication: Lecture Notes in Computer Science (including subseries Lecture Notes
in Artificial Intelligence and Lecture Notes in Bioinformatics)
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '4993'
status: public
title: 'Probabilistic bisimulation: Naturally on distributions'
type: conference
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
volume: 8704
year: '2014'
...
---
_id: '2190'
abstract:
- lang: eng
text: We present a new algorithm to construct a (generalized) deterministic Rabin
automaton for an LTL formula φ. The automaton is the product of a master automaton
and an array of slave automata, one for each G-subformula of φ. The slave automaton
for G ψ is in charge of recognizing whether FG ψ holds. As opposed to standard
determinization procedures, the states of all our automata have a clear logical
structure, which allows for various optimizations. Our construction subsumes former
algorithms for fragments of LTL. Experimental results show improvement in the
sizes of the resulting automata compared to existing methods.
acknowledgement: The author is on leave from Faculty of Informatics, Masaryk University,
Czech Republic, and partially supported by the Czech Science Foundation, grant No.
P202/12/G061.
alternative_title:
- LNCS
author:
- first_name: Javier
full_name: Esparza, Javier
last_name: Esparza
- first_name: Jan
full_name: Kretinsky, Jan
id: 44CEF464-F248-11E8-B48F-1D18A9856A87
last_name: Kretinsky
orcid: 0000-0002-8122-2881
citation:
ama: 'Esparza J, Kretinsky J. From LTL to deterministic automata: A safraless compositional
approach. In: Vol 8559. Springer; 2014:192-208. doi:10.1007/978-3-319-08867-9_13'
apa: 'Esparza, J., & Kretinsky, J. (2014). From LTL to deterministic automata:
A safraless compositional approach (Vol. 8559, pp. 192–208). Presented at the
CAV: Computer Aided Verification, Springer. https://doi.org/10.1007/978-3-319-08867-9_13'
chicago: 'Esparza, Javier, and Jan Kretinsky. “From LTL to Deterministic Automata:
A Safraless Compositional Approach,” 8559:192–208. Springer, 2014. https://doi.org/10.1007/978-3-319-08867-9_13.'
ieee: 'J. Esparza and J. Kretinsky, “From LTL to deterministic automata: A safraless
compositional approach,” presented at the CAV: Computer Aided Verification, 2014,
vol. 8559, pp. 192–208.'
ista: 'Esparza J, Kretinsky J. 2014. From LTL to deterministic automata: A safraless
compositional approach. CAV: Computer Aided Verification, LNCS, vol. 8559, 192–208.'
mla: 'Esparza, Javier, and Jan Kretinsky. From LTL to Deterministic Automata:
A Safraless Compositional Approach. Vol. 8559, Springer, 2014, pp. 192–208,
doi:10.1007/978-3-319-08867-9_13.'
short: J. Esparza, J. Kretinsky, in:, Springer, 2014, pp. 192–208.
conference:
name: 'CAV: Computer Aided Verification'
date_created: 2018-12-11T11:56:14Z
date_published: 2014-01-01T00:00:00Z
date_updated: 2021-01-12T06:55:53Z
day: '01'
department:
- _id: ToHe
- _id: KrCh
doi: 10.1007/978-3-319-08867-9_13
ec_funded: 1
intvolume: ' 8559'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1402.3388
month: '01'
oa: 1
oa_version: Submitted Version
page: 192 - 208
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _id: 25F5A88A-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11402-N23
name: Moderne Concurrency Paradigms
publication_status: published
publisher: Springer
publist_id: '4784'
quality_controlled: '1'
status: public
title: 'From LTL to deterministic automata: A safraless compositional approach'
type: conference
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
volume: 8559
year: '2014'
...
---
_id: '2446'
abstract:
- lang: eng
text: The model-checking problem for probabilistic systems crucially relies on the
translation of LTL to deterministic Rabin automata (DRW). Our recent Safraless
translation [KE12, GKE12] for the LTL(F,G) fragment produces smaller automata
as compared to the traditional approach. In this work, instead of DRW we consider
deterministic automata with acceptance condition given as disjunction of generalized
Rabin pairs (DGRW). The Safraless translation of LTL(F,G) formulas to DGRW results
in smaller automata as compared to DRW. We present algorithms for probabilistic
model-checking as well as game solving for DGRW conditions. Our new algorithms
lead to improvement both in terms of theoretical bounds as well as practical evaluation.
We compare PRISM with and without our new translation, and show that the new translation
leads to significant improvements.
alternative_title:
- LNCS
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Andreas
full_name: Gaiser, Andreas
last_name: Gaiser
- first_name: Jan
full_name: Kretinsky, Jan
id: 44CEF464-F248-11E8-B48F-1D18A9856A87
last_name: Kretinsky
orcid: 0000-0002-8122-2881
citation:
ama: Chatterjee K, Gaiser A, Kretinsky J. Automata with generalized Rabin pairs
for probabilistic model checking and LTL synthesis. 2013;8044:559-575. doi:10.1007/978-3-642-39799-8_37
apa: 'Chatterjee, K., Gaiser, A., & Kretinsky, J. (2013). Automata with generalized
Rabin pairs for probabilistic model checking and LTL synthesis. Presented at the
CAV: Computer Aided Verification, St. Petersburg, Russia: Springer. https://doi.org/10.1007/978-3-642-39799-8_37'
chicago: Chatterjee, Krishnendu, Andreas Gaiser, and Jan Kretinsky. “Automata with
Generalized Rabin Pairs for Probabilistic Model Checking and LTL Synthesis.” Lecture
Notes in Computer Science. Springer, 2013. https://doi.org/10.1007/978-3-642-39799-8_37.
ieee: K. Chatterjee, A. Gaiser, and J. Kretinsky, “Automata with generalized Rabin
pairs for probabilistic model checking and LTL synthesis,” vol. 8044. Springer,
pp. 559–575, 2013.
ista: Chatterjee K, Gaiser A, Kretinsky J. 2013. Automata with generalized Rabin
pairs for probabilistic model checking and LTL synthesis. 8044, 559–575.
mla: Chatterjee, Krishnendu, et al. Automata with Generalized Rabin Pairs for
Probabilistic Model Checking and LTL Synthesis. Vol. 8044, Springer, 2013,
pp. 559–75, doi:10.1007/978-3-642-39799-8_37.
short: K. Chatterjee, A. Gaiser, J. Kretinsky, 8044 (2013) 559–575.
conference:
end_date: 2013-07-19
location: St. Petersburg, Russia
name: 'CAV: Computer Aided Verification'
start_date: 2013-07-13
date_created: 2018-12-11T11:57:42Z
date_published: 2013-07-01T00:00:00Z
date_updated: 2020-08-11T10:09:47Z
day: '01'
department:
- _id: KrCh
doi: 10.1007/978-3-642-39799-8_37
ec_funded: 1
external_id:
arxiv:
- '1304.5281'
intvolume: ' 8044'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1304.5281
month: '07'
oa: 1
oa_version: Preprint
page: 559 - 575
project:
- _id: 2584A770-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: P 23499-N23
name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11407
name: Game Theory
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 2587B514-B435-11E9-9278-68D0E5697425
name: Microsoft Research Faculty Fellowship
publication_status: published
publisher: Springer
publist_id: '4457'
quality_controlled: '1'
scopus_import: 1
series_title: Lecture Notes in Computer Science
status: public
title: Automata with generalized Rabin pairs for probabilistic model checking and
LTL synthesis
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 8044
year: '2013'
...