---
_id: '1155'
abstract:
- lang: eng
text: This dissertation concerns the automatic verification of probabilistic systems
and programs with arrays by statistical and logical methods. Although statistical
and logical methods are different in nature, we show that they can be successfully
combined for system analysis. In the first part of the dissertation we present
a new statistical algorithm for the verification of probabilistic systems with
respect to unbounded properties, including linear temporal logic. Our algorithm
often performs faster than the previous approaches, and at the same time requires
less information about the system. In addition, our method can be generalized
to unbounded quantitative properties such as mean-payoff bounds. In the second
part, we introduce two techniques for comparing probabilistic systems. Probabilistic
systems are typically compared using the notion of equivalence, which requires
the systems to have the equal probability of all behaviors. However, this notion
is often too strict, since probabilities are typically only empirically estimated,
and any imprecision may break the relation between processes. On the one hand,
we propose to replace the Boolean notion of equivalence by a quantitative distance
of similarity. For this purpose, we introduce a statistical framework for estimating
distances between Markov chains based on their simulation runs, and we investigate
which distances can be approximated in our framework. On the other hand, we propose
to compare systems with respect to a new qualitative logic, which expresses that
behaviors occur with probability one or a positive probability. This qualitative
analysis is robust with respect to modeling errors and applicable to many domains.
In the last part, we present a new quantifier-free logic for integer arrays, which
allows us to express counting. Counting properties are prevalent in array-manipulating
programs, however they cannot be expressed in the quantified fragments of the
theory of arrays. We present a decision procedure for our logic, and provide several
complexity results.
acknowledgement: ' First of all, I want to thank my advisor, prof. Thomas A. Henzinger,
for his guidance during my PhD program. I am grateful for the freedom I was given
to pursue my research interests, and his continuous support. Working with prof.
Henzinger was a truly inspiring experience and taught me what it means to be a scientist.
I want to express my gratitude to my collaborators: Nikola Beneš, Krishnendu Chatterjee,
Martin Chmelík, Ashutosh Gupta, Willibald Krenn, Jan Kˇretínský, Dejan Nickovic,
Andrey Kupriyanov, and Tatjana Petrov. I have learned a great deal from my collaborators,
and without their help this thesis would not be possible. In addition, I want to
thank the members of my thesis committee: Dirk Beyer, Dejan Nickovic, and Georg
Weissenbacher for their advice and reviewing this dissertation. I would especially
like to acknowledge the late Helmut Veith, who was a member of my committee. I will
remember Helmut for his kindness, enthusiasm, and wit, as well as for being an inspiring
scientist. Finally, I would like to thank my colleagues for making my stay at IST
such a pleasant experience: Guy Avni, Sergiy Bogomolov, Ventsislav Chonev, Rasmus
Ibsen-Jensen, Mirco Giacobbe, Bernhard Kragl, Hui Kong, Petr Novotný, Jan Otop,
Andreas Pavlogiannis, Tantjana Petrov, Arjun Radhakrishna, Jakob Ruess, Thorsten
Tarrach, as well as other members of groups Henzinger and Chatterjee. '
alternative_title:
- ISTA Thesis
article_processing_charge: No
author:
- first_name: Przemyslaw
full_name: Daca, Przemyslaw
id: 49351290-F248-11E8-B48F-1D18A9856A87
last_name: Daca
citation:
ama: Daca P. Statistical and logical methods for property checking. 2017. doi:10.15479/AT:ISTA:TH_730
apa: Daca, P. (2017). Statistical and logical methods for property checking.
Institute of Science and Technology Austria. https://doi.org/10.15479/AT:ISTA:TH_730
chicago: Daca, Przemyslaw. “Statistical and Logical Methods for Property Checking.”
Institute of Science and Technology Austria, 2017. https://doi.org/10.15479/AT:ISTA:TH_730.
ieee: P. Daca, “Statistical and logical methods for property checking,” Institute
of Science and Technology Austria, 2017.
ista: Daca P. 2017. Statistical and logical methods for property checking. Institute
of Science and Technology Austria.
mla: Daca, Przemyslaw. Statistical and Logical Methods for Property Checking.
Institute of Science and Technology Austria, 2017, doi:10.15479/AT:ISTA:TH_730.
short: P. Daca, Statistical and Logical Methods for Property Checking, Institute
of Science and Technology Austria, 2017.
date_created: 2018-12-11T11:50:27Z
date_published: 2017-01-02T00:00:00Z
date_updated: 2023-09-07T11:58:34Z
day: '02'
ddc:
- '004'
- '005'
degree_awarded: PhD
department:
- _id: ToHe
doi: 10.15479/AT:ISTA:TH_730
ec_funded: 1
file:
- access_level: open_access
checksum: 1406a681cb737508234fde34766be2c2
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:11:26Z
date_updated: 2020-07-14T12:44:34Z
file_id: '4880'
file_name: IST-2017-730-v1+1_Statistical_and_Logical_Methods_for_Property_Checking.pdf
file_size: 1028586
relation: main_file
file_date_updated: 2020-07-14T12:44:34Z
has_accepted_license: '1'
language:
- iso: eng
month: '01'
oa: 1
oa_version: Published Version
page: '163'
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: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
publication_identifier:
issn:
- 2663-337X
publication_status: published
publisher: Institute of Science and Technology Austria
publist_id: '6203'
pubrep_id: '730'
related_material:
record:
- id: '1093'
relation: part_of_dissertation
status: public
- id: '1230'
relation: part_of_dissertation
status: public
- id: '1234'
relation: part_of_dissertation
status: public
- id: '1391'
relation: part_of_dissertation
status: public
- id: '1501'
relation: part_of_dissertation
status: public
- id: '1502'
relation: part_of_dissertation
status: public
- id: '2063'
relation: part_of_dissertation
status: public
- id: '2167'
relation: part_of_dissertation
status: public
status: public
supervisor:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
title: Statistical and logical methods for property checking
type: dissertation
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
year: '2017'
...
---
_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: '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: '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: '1391'
abstract:
- lang: eng
text: "We present an extension to the quantifier-free theory of integer arrays which
allows us to express counting. The properties expressible in Array Folds Logic
(AFL) include statements such as "the first array cell contains the array
length," and "the array contains equally many minimal and maximal elements."
These properties cannot be expressed in quantified fragments of the theory of
arrays, nor in the theory of concatenation. Using reduction to counter machines,
we show that the satisfiability problem of AFL is PSPACE-complete, and with a
natural restriction the complexity decreases to NP. We also show that adding either
universal quantifiers or concatenation leads to undecidability.\r\nAFL contains
terms that fold a function over an array. We demonstrate that folding, a well-known
concept from functional languages, allows us to concisely summarize loops that
count over arrays, which occurs frequently in real-life programs. We provide a
tool that can discharge proof obligations in AFL, and we demonstrate on practical
examples that our decision procedure can solve a broad range of problems in symbolic
testing and program verification."
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: Andrey
full_name: Kupriyanov, Andrey
id: 2C311BF8-F248-11E8-B48F-1D18A9856A87
last_name: Kupriyanov
citation:
ama: 'Daca P, Henzinger TA, Kupriyanov A. Array folds logic. In: Vol 9780. Springer;
2016:230-248. doi:10.1007/978-3-319-41540-6_13'
apa: 'Daca, P., Henzinger, T. A., & Kupriyanov, A. (2016). Array folds logic
(Vol. 9780, pp. 230–248). Presented at the CAV: Computer Aided Verification, Toronto,
Canada: Springer. https://doi.org/10.1007/978-3-319-41540-6_13'
chicago: Daca, Przemyslaw, Thomas A Henzinger, and Andrey Kupriyanov. “Array Folds
Logic,” 9780:230–48. Springer, 2016. https://doi.org/10.1007/978-3-319-41540-6_13.
ieee: 'P. Daca, T. A. Henzinger, and A. Kupriyanov, “Array folds logic,” presented
at the CAV: Computer Aided Verification, Toronto, Canada, 2016, vol. 9780, pp.
230–248.'
ista: 'Daca P, Henzinger TA, Kupriyanov A. 2016. Array folds logic. CAV: Computer
Aided Verification, LNCS, vol. 9780, 230–248.'
mla: Daca, Przemyslaw, et al. Array Folds Logic. Vol. 9780, Springer, 2016,
pp. 230–48, doi:10.1007/978-3-319-41540-6_13.
short: P. Daca, T.A. Henzinger, A. Kupriyanov, in:, Springer, 2016, pp. 230–248.
conference:
end_date: 2016-07-23
location: Toronto, Canada
name: 'CAV: Computer Aided Verification'
start_date: 2016-07-17
date_created: 2018-12-11T11:51:45Z
date_published: 2016-07-13T00:00:00Z
date_updated: 2023-09-07T11:58:33Z
day: '13'
department:
- _id: ToHe
doi: 10.1007/978-3-319-41540-6_13
ec_funded: 1
intvolume: ' 9780'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1603.06850
month: '07'
oa: 1
oa_version: Preprint
page: 230 - 248
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: Springer
publist_id: '5818'
quality_controlled: '1'
related_material:
record:
- id: '1155'
relation: dissertation_contains
status: public
scopus_import: 1
status: public
title: Array folds logic
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 9780
year: '2016'
...
---
_id: '1230'
abstract:
- lang: eng
text: Concolic testing is a promising method for generating test suites for large
programs. However, it suffers from the path-explosion problem and often fails
to find tests that cover difficult-to-reach parts of programs. In contrast, model
checkers based on counterexample-guided abstraction refinement explore programs
exhaustively, while failing to scale on large programs with precision. In this
paper, we present a novel method that iteratively combines concolic testing and
model checking to find a test suite for a given coverage criterion. If concolic
testing fails to cover some test goals, then the model checker refines its program
abstraction to prove more paths infeasible, which reduces the search space for
concolic testing. We have implemented our method on top of the concolictesting
tool Crest and the model checker CpaChecker. We evaluated our tool on a collection
of programs and a category of SvComp benchmarks. In our experiments, we observed
an improvement in branch coverage compared to Crest from 48% to 63% in the best
case, and from 66% to 71% on average.
acknowledgement: "We thank Andrey Kupriyanov for feedback on the manuscript,\r\nand
Michael Tautschnig for help with preparing the experiments. This research was supported
in part by the European Research Council (ERC) under grant 267989 (QUAREM) and by
the Austrian Science Fund (FWF) under grants S11402-N23 (RiSE) and Z211-N23 (Wittgenstein
Award)."
alternative_title:
- LNCS
author:
- first_name: Przemyslaw
full_name: Daca, Przemyslaw
id: 49351290-F248-11E8-B48F-1D18A9856A87
last_name: Daca
- first_name: Ashutosh
full_name: Gupta, Ashutosh
id: 335E5684-F248-11E8-B48F-1D18A9856A87
last_name: Gupta
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
citation:
ama: 'Daca P, Gupta A, Henzinger TA. Abstraction-driven concolic testing. In: Vol
9583. Springer; 2016:328-347. doi:10.1007/978-3-662-49122-5_16'
apa: 'Daca, P., Gupta, A., & Henzinger, T. A. (2016). Abstraction-driven concolic
testing (Vol. 9583, pp. 328–347). Presented at the VMCAI: Verification, Model
Checking and Abstract Interpretation, St. Petersburg, FL, USA: Springer. https://doi.org/10.1007/978-3-662-49122-5_16'
chicago: Daca, Przemyslaw, Ashutosh Gupta, and Thomas A Henzinger. “Abstraction-Driven
Concolic Testing,” 9583:328–47. Springer, 2016. https://doi.org/10.1007/978-3-662-49122-5_16.
ieee: 'P. Daca, A. Gupta, and T. A. Henzinger, “Abstraction-driven concolic testing,”
presented at the VMCAI: Verification, Model Checking and Abstract Interpretation,
St. Petersburg, FL, USA, 2016, vol. 9583, pp. 328–347.'
ista: 'Daca P, Gupta A, Henzinger TA. 2016. Abstraction-driven concolic testing.
VMCAI: Verification, Model Checking and Abstract Interpretation, LNCS, vol. 9583,
328–347.'
mla: Daca, Przemyslaw, et al. Abstraction-Driven Concolic Testing. Vol. 9583,
Springer, 2016, pp. 328–47, doi:10.1007/978-3-662-49122-5_16.
short: P. Daca, A. Gupta, T.A. Henzinger, in:, Springer, 2016, pp. 328–347.
conference:
end_date: 2016-01-19
location: St. Petersburg, FL, USA
name: 'VMCAI: Verification, Model Checking and Abstract Interpretation'
start_date: 2016-01-17
date_created: 2018-12-11T11:50:50Z
date_published: 2016-01-01T00:00:00Z
date_updated: 2023-09-07T11:58:33Z
day: '01'
department:
- _id: ToHe
doi: 10.1007/978-3-662-49122-5_16
ec_funded: 1
intvolume: ' 9583'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1511.02615
month: '01'
oa: 1
oa_version: Preprint
page: 328 - 347
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: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
publication_status: published
publisher: Springer
publist_id: '6104'
quality_controlled: '1'
related_material:
record:
- id: '1155'
relation: dissertation_contains
status: public
scopus_import: 1
status: public
title: Abstraction-driven concolic testing
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 9583
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: '1501'
abstract:
- lang: eng
text: 'We consider Markov decision processes (MDPs) which are a standard model for
probabilistic systems. We focus on qualitative properties for MDPs that can express
that desired behaviors of the system arise almost-surely (with probability 1)
or with positive probability. We introduce a new simulation relation to capture
the refinement relation of MDPs with respect to qualitative properties, and present
discrete graph algorithms with quadratic complexity to compute the simulation
relation. We present an automated technique for assume-guarantee style reasoning
for compositional analysis of two-player games by giving a counterexample guided
abstraction-refinement approach to compute our new simulation relation. We show
a tight link between two-player games and MDPs, and as a consequence the results
for games are lifted to MDPs with qualitative properties. We have implemented
our algorithms and show that the compositional analysis leads to significant improvements. '
acknowledgement: 'The research was partly supported by Austrian Science Fund (FWF)
Grant No. P23499- N23, FWF NFN Grant No. S11407-N23, FWF Grant S11403-N23 (RiSE),
and FWF Grant Z211-N23 (Wittgenstein Award), ERC Start Grant (279307: Graph Games),
Microsoft faculty fellows award, the ERC Advanced Grant QUAREM (Quantitative Reactive
Modeling).'
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Martin
full_name: Chmelik, Martin
id: 3624234E-F248-11E8-B48F-1D18A9856A87
last_name: Chmelik
- first_name: Przemyslaw
full_name: Daca, Przemyslaw
id: 49351290-F248-11E8-B48F-1D18A9856A87
last_name: Daca
citation:
ama: Chatterjee K, Chmelik M, Daca P. CEGAR for compositional analysis of qualitative
properties in Markov decision processes. Formal Methods in System Design.
2015;47(2):230-264. doi:10.1007/s10703-015-0235-2
apa: Chatterjee, K., Chmelik, M., & Daca, P. (2015). CEGAR for compositional
analysis of qualitative properties in Markov decision processes. Formal Methods
in System Design. Springer. https://doi.org/10.1007/s10703-015-0235-2
chicago: Chatterjee, Krishnendu, Martin Chmelik, and Przemyslaw Daca. “CEGAR for
Compositional Analysis of Qualitative Properties in Markov Decision Processes.”
Formal Methods in System Design. Springer, 2015. https://doi.org/10.1007/s10703-015-0235-2.
ieee: K. Chatterjee, M. Chmelik, and P. Daca, “CEGAR for compositional analysis
of qualitative properties in Markov decision processes,” Formal Methods in
System Design, vol. 47, no. 2. Springer, pp. 230–264, 2015.
ista: Chatterjee K, Chmelik M, Daca P. 2015. CEGAR for compositional analysis of
qualitative properties in Markov decision processes. Formal Methods in System
Design. 47(2), 230–264.
mla: Chatterjee, Krishnendu, et al. “CEGAR for Compositional Analysis of Qualitative
Properties in Markov Decision Processes.” Formal Methods in System Design,
vol. 47, no. 2, Springer, 2015, pp. 230–64, doi:10.1007/s10703-015-0235-2.
short: K. Chatterjee, M. Chmelik, P. Daca, Formal Methods in System Design 47 (2015)
230–264.
date_created: 2018-12-11T11:52:23Z
date_published: 2015-10-01T00:00:00Z
date_updated: 2023-09-07T11:58:33Z
day: '01'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1007/s10703-015-0235-2
ec_funded: 1
intvolume: ' 47'
issue: '2'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1405.0835
month: '10'
oa: 1
oa_version: Preprint
page: 230 - 264
project:
- _id: 2584A770-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: P 23499-N23
name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 2587B514-B435-11E9-9278-68D0E5697425
name: Microsoft Research Faculty Fellowship
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
publication: Formal Methods in System Design
publication_status: published
publisher: Springer
publist_id: '5677'
quality_controlled: '1'
related_material:
record:
- id: '1155'
relation: dissertation_contains
status: public
scopus_import: 1
status: public
title: CEGAR for compositional analysis of qualitative properties in Markov decision
processes
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 47
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: '2063'
abstract:
- lang: eng
text: We consider Markov decision processes (MDPs) which are a standard model for
probabilistic systems.We focus on qualitative properties forMDPs that can express
that desired behaviors of the system arise almost-surely (with probability 1)
or with positive probability. We introduce a new simulation relation to capture
the refinement relation ofMDPs with respect to qualitative properties, and present
discrete graph theoretic algorithms with quadratic complexity to compute the simulation
relation.We present an automated technique for assume-guarantee style reasoning
for compositional analysis ofMDPs with qualitative properties by giving a counterexample
guided abstraction-refinement approach to compute our new simulation relation.
We have implemented our algorithms and show that the compositional analysis 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: Martin
full_name: Chmelik, Martin
id: 3624234E-F248-11E8-B48F-1D18A9856A87
last_name: Chmelik
- first_name: Przemyslaw
full_name: Daca, Przemyslaw
id: 49351290-F248-11E8-B48F-1D18A9856A87
last_name: Daca
citation:
ama: 'Chatterjee K, Chmelik M, Daca P. CEGAR for qualitative analysis of probabilistic
systems. In: Vol 8559. Springer; 2014:473-490. doi:10.1007/978-3-319-08867-9_31'
apa: 'Chatterjee, K., Chmelik, M., & Daca, P. (2014). CEGAR for qualitative
analysis of probabilistic systems (Vol. 8559, pp. 473–490). Presented at the CAV:
Computer Aided Verification, Vienna, Austria: Springer. https://doi.org/10.1007/978-3-319-08867-9_31'
chicago: Chatterjee, Krishnendu, Martin Chmelik, and Przemyslaw Daca. “CEGAR for
Qualitative Analysis of Probabilistic Systems,” 8559:473–90. Springer, 2014. https://doi.org/10.1007/978-3-319-08867-9_31.
ieee: 'K. Chatterjee, M. Chmelik, and P. Daca, “CEGAR for qualitative analysis of
probabilistic systems,” presented at the CAV: Computer Aided Verification, Vienna,
Austria, 2014, vol. 8559, pp. 473–490.'
ista: 'Chatterjee K, Chmelik M, Daca P. 2014. CEGAR for qualitative analysis of
probabilistic systems. CAV: Computer Aided Verification, LNCS, vol. 8559, 473–490.'
mla: Chatterjee, Krishnendu, et al. CEGAR for Qualitative Analysis of Probabilistic
Systems. Vol. 8559, Springer, 2014, pp. 473–90, doi:10.1007/978-3-319-08867-9_31.
short: K. Chatterjee, M. Chmelik, P. Daca, in:, Springer, 2014, pp. 473–490.
conference:
end_date: 2014-07-22
location: Vienna, Austria
name: 'CAV: Computer Aided Verification'
start_date: 2014-07-18
date_created: 2018-12-11T11:55:30Z
date_published: 2014-07-01T00:00:00Z
date_updated: 2023-09-07T11:58:33Z
day: '01'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1007/978-3-319-08867-9_31
ec_funded: 1
intvolume: ' 8559'
language:
- iso: eng
month: '07'
oa_version: None
page: 473 - 490
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: 25F5A88A-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11402-N23
name: Moderne Concurrency Paradigms
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 2587B514-B435-11E9-9278-68D0E5697425
name: Microsoft Research Faculty Fellowship
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
publication_status: published
publisher: Springer
publist_id: '4978'
quality_controlled: '1'
related_material:
record:
- id: '5412'
relation: earlier_version
status: public
- id: '5413'
relation: earlier_version
status: public
- id: '5414'
relation: earlier_version
status: public
- id: '1155'
relation: dissertation_contains
status: public
status: public
title: CEGAR for qualitative analysis of probabilistic systems
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 8559
year: '2014'
...
---
_id: '2167'
abstract:
- lang: eng
text: Model-based testing is a promising technology for black-box software and hardware
testing, in which test cases are generated automatically from high-level specifications.
Nowadays, systems typically consist of multiple interacting components and, due
to their complexity, testing presents a considerable portion of the effort and
cost in the design process. Exploiting the compositional structure of system specifications
can considerably reduce the effort in model-based testing. Moreover, inferring
properties about the system from testing its individual components allows the
designer to reduce the amount of integration testing. In this paper, we study
compositional properties of the ioco-testing theory. We propose a new approach
to composition and hiding operations, inspired by contract-based design and interface
theories. These operations preserve behaviors that are compatible under composition
and hiding, and prune away incompatible ones. The resulting specification characterizes
the input sequences for which the unit testing of components is sufficient to
infer the correctness of component integration without the need for further tests.
We provide a methodology that uses these results to minimize integration testing
effort, but also to detect potential weaknesses in specifications. While we focus
on asynchronous models and the ioco conformance relation, the resulting methodology
can be applied to a broader class of systems.
article_number: '6823899'
article_processing_charge: No
arxiv: 1
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: Willibald
full_name: Krenn, Willibald
last_name: Krenn
- first_name: Dejan
full_name: Nickovic, Dejan
last_name: Nickovic
citation:
ama: 'Daca P, Henzinger TA, Krenn W, Nickovic D. Compositional specifications for
IOCO testing. In: IEEE 7th International Conference on Software Testing, Verification
and Validation. IEEE; 2014. doi:10.1109/ICST.2014.50'
apa: 'Daca, P., Henzinger, T. A., Krenn, W., & Nickovic, D. (2014). Compositional
specifications for IOCO testing. In IEEE 7th International Conference on Software
Testing, Verification and Validation. Cleveland, USA: IEEE. https://doi.org/10.1109/ICST.2014.50'
chicago: Daca, Przemyslaw, Thomas A Henzinger, Willibald Krenn, and Dejan Nickovic.
“Compositional Specifications for IOCO Testing.” In IEEE 7th International
Conference on Software Testing, Verification and Validation. IEEE, 2014. https://doi.org/10.1109/ICST.2014.50.
ieee: P. Daca, T. A. Henzinger, W. Krenn, and D. Nickovic, “Compositional specifications
for IOCO testing,” in IEEE 7th International Conference on Software Testing,
Verification and Validation, Cleveland, USA, 2014.
ista: 'Daca P, Henzinger TA, Krenn W, Nickovic D. 2014. Compositional specifications
for IOCO testing. IEEE 7th International Conference on Software Testing, Verification
and Validation. ICST: International Conference on Software Testing, Verification
and Validation, 6823899.'
mla: Daca, Przemyslaw, et al. “Compositional Specifications for IOCO Testing.” IEEE
7th International Conference on Software Testing, Verification and Validation,
6823899, IEEE, 2014, doi:10.1109/ICST.2014.50.
short: P. Daca, T.A. Henzinger, W. Krenn, D. Nickovic, in:, IEEE 7th International
Conference on Software Testing, Verification and Validation, IEEE, 2014.
conference:
end_date: 2014-04-04
location: Cleveland, USA
name: 'ICST: International Conference on Software Testing, Verification and Validation'
start_date: 2014-03-31
date_created: 2018-12-11T11:56:06Z
date_published: 2014-03-01T00:00:00Z
date_updated: 2023-09-07T11:58:33Z
day: '01'
department:
- _id: ToHe
doi: 10.1109/ICST.2014.50
ec_funded: 1
external_id:
arxiv:
- '1904.07083'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1904.07083
month: '03'
oa: 1
oa_version: Preprint
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: IEEE 7th International Conference on Software Testing, Verification and
Validation
publication_identifier:
isbn:
- 978-1-4799-2255-0
issn:
- 2159-4848
publication_status: published
publisher: IEEE
publist_id: '4817'
quality_controlled: '1'
related_material:
record:
- id: '5411'
relation: earlier_version
status: public
- id: '1155'
relation: dissertation_contains
status: public
scopus_import: 1
status: public
title: Compositional specifications for IOCO testing
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2014'
...
---
_id: '5411'
abstract:
- lang: eng
text: "Model-based testing is a promising technology for black-box software and
hardware testing, in which test cases are generated automatically from high-level
specifications. Nowadays, systems typically consist of multiple interacting components
and, due to their complexity, testing presents a considerable portion of the effort
and cost in the design process. Exploiting the compositional structure of system
specifications can considerably reduce the effort in model-based testing. Moreover,
inferring properties about the system from testing its individual components allows
the designer to reduce the amount of integration testing.\r\nIn this paper, we
study compositional properties of the IOCO-testing theory. We propose a new approach
to composition and hiding operations, inspired by contract-based design and interface
theories. These operations preserve behaviors that are compatible under composition
and hiding, and prune away incompatible ones. The resulting specification characterizes
the input sequences for which the unit testing of components is sufficient to
infer the correctness of component integration without the need for further tests.
We provide a methodology that uses these results to minimize integration testing
effort, but also to detect potential weaknesses in specifications. While we focus
on asynchronous models and the IOCO conformance relation, the resulting methodology
can be applied to a broader class of systems."
alternative_title:
- IST Austria Technical Report
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: Willibald
full_name: Krenn, Willibald
last_name: Krenn
- first_name: Dejan
full_name: Nickovic, Dejan
id: 41BCEE5C-F248-11E8-B48F-1D18A9856A87
last_name: Nickovic
citation:
ama: Daca P, Henzinger TA, Krenn W, Nickovic D. Compositional Specifications
for IOCO Testing. IST Austria; 2014. doi:10.15479/AT:IST-2014-148-v2-1
apa: Daca, P., Henzinger, T. A., Krenn, W., & Nickovic, D. (2014). Compositional
specifications for IOCO testing. IST Austria. https://doi.org/10.15479/AT:IST-2014-148-v2-1
chicago: Daca, Przemyslaw, Thomas A Henzinger, Willibald Krenn, and Dejan Nickovic.
Compositional Specifications for IOCO Testing. IST Austria, 2014. https://doi.org/10.15479/AT:IST-2014-148-v2-1.
ieee: P. Daca, T. A. Henzinger, W. Krenn, and D. Nickovic, Compositional specifications
for IOCO testing. IST Austria, 2014.
ista: Daca P, Henzinger TA, Krenn W, Nickovic D. 2014. Compositional specifications
for IOCO testing, IST Austria, 20p.
mla: Daca, Przemyslaw, et al. Compositional Specifications for IOCO Testing.
IST Austria, 2014, doi:10.15479/AT:IST-2014-148-v2-1.
short: P. Daca, T.A. Henzinger, W. Krenn, D. Nickovic, Compositional Specifications
for IOCO Testing, IST Austria, 2014.
date_created: 2018-12-12T11:39:11Z
date_published: 2014-01-28T00:00:00Z
date_updated: 2023-02-23T10:31:07Z
day: '28'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.15479/AT:IST-2014-148-v2-1
file:
- access_level: open_access
checksum: 0e03aba625cc334141a3148432aa5760
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:54:21Z
date_updated: 2020-07-14T12:46:46Z
file_id: '5543'
file_name: IST-2014-148-v2+1_main_tr.pdf
file_size: 534732
relation: main_file
file_date_updated: 2020-07-14T12:46:46Z
has_accepted_license: '1'
language:
- iso: eng
month: '01'
oa: 1
oa_version: Published Version
page: '20'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '152'
related_material:
record:
- id: '2167'
relation: later_version
status: public
status: public
title: Compositional specifications for IOCO testing
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2014'
...
---
_id: '5412'
abstract:
- lang: eng
text: "We consider Markov decision processes (MDPs) which are a standard model for
probabilistic systems. We focus on qualitative properties for MDPs that can express
that desired behaviors of the system arise almost-surely (with probability 1)
or with positive probability.\r\nWe introduce a new simulation relation to capture
the refinement relation of MDPs with respect to qualitative properties, and present
discrete graph theoretic algorithms with quadratic complexity to compute the simulation
relation.\r\nWe present an automated technique for assume-guarantee style reasoning
for compositional analysis of MDPs with qualitative properties by giving a counter-example
guided abstraction-refinement approach to compute our new simulation relation.
We have implemented our algorithms and show that the compositional analysis leads
to significant improvements. "
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: Przemyslaw
full_name: Daca, Przemyslaw
id: 49351290-F248-11E8-B48F-1D18A9856A87
last_name: Daca
- first_name: Martin
full_name: Chmelik, Martin
id: 3624234E-F248-11E8-B48F-1D18A9856A87
last_name: Chmelik
citation:
ama: Chatterjee K, Daca P, Chmelik M. CEGAR for Qualitative Analysis of Probabilistic
Systems. IST Austria; 2014. doi:10.15479/AT:IST-2014-153-v1-1
apa: Chatterjee, K., Daca, P., & Chmelik, M. (2014). CEGAR for qualitative
analysis of probabilistic systems. IST Austria. https://doi.org/10.15479/AT:IST-2014-153-v1-1
chicago: Chatterjee, Krishnendu, Przemyslaw Daca, and Martin Chmelik. CEGAR for
Qualitative Analysis of Probabilistic Systems. IST Austria, 2014. https://doi.org/10.15479/AT:IST-2014-153-v1-1.
ieee: K. Chatterjee, P. Daca, and M. Chmelik, CEGAR for qualitative analysis
of probabilistic systems. IST Austria, 2014.
ista: Chatterjee K, Daca P, Chmelik M. 2014. CEGAR for qualitative analysis of probabilistic
systems, IST Austria, 31p.
mla: Chatterjee, Krishnendu, et al. CEGAR for Qualitative Analysis of Probabilistic
Systems. IST Austria, 2014, doi:10.15479/AT:IST-2014-153-v1-1.
short: K. Chatterjee, P. Daca, M. Chmelik, CEGAR for Qualitative Analysis of Probabilistic
Systems, IST Austria, 2014.
date_created: 2018-12-12T11:39:11Z
date_published: 2014-01-29T00:00:00Z
date_updated: 2023-02-23T12:25:18Z
day: '29'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.15479/AT:IST-2014-153-v1-1
file:
- access_level: open_access
checksum: 4d6cda4bebed970926403ad6ad8c745f
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:53:39Z
date_updated: 2020-07-14T12:46:47Z
file_id: '5500'
file_name: IST-2014-153-v1+1_main.pdf
file_size: 423322
relation: main_file
file_date_updated: 2020-07-14T12:46:47Z
has_accepted_license: '1'
language:
- iso: eng
month: '01'
oa: 1
oa_version: Published Version
page: '31'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '153'
related_material:
record:
- id: '2063'
relation: later_version
status: public
- id: '5413'
relation: later_version
status: public
- id: '5414'
relation: later_version
status: public
status: public
title: CEGAR for qualitative analysis of probabilistic systems
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2014'
...
---
_id: '5413'
abstract:
- lang: eng
text: "We consider Markov decision processes (MDPs) which are a standard model for
probabilistic systems. We focus on qualitative properties for MDPs that can express
that desired behaviors of the system arise almost-surely (with probability 1)
or with positive probability.\r\nWe introduce a new simulation relation to capture
the refinement relation of MDPs with respect to qualitative properties, and present
discrete graph theoretic algorithms with quadratic complexity to compute the simulation
relation.\r\nWe present an automated technique for assume-guarantee style reasoning
for compositional analysis of MDPs with qualitative properties by giving a counter-example
guided abstraction-refinement approach to compute our new simulation relation.
We have implemented our algorithms and show that the compositional analysis leads
to significant improvements. "
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: Przemyslaw
full_name: Daca, Przemyslaw
id: 49351290-F248-11E8-B48F-1D18A9856A87
last_name: Daca
- first_name: Martin
full_name: Chmelik, Martin
id: 3624234E-F248-11E8-B48F-1D18A9856A87
last_name: Chmelik
citation:
ama: Chatterjee K, Daca P, Chmelik M. CEGAR for Qualitative Analysis of Probabilistic
Systems. IST Austria; 2014. doi:10.15479/AT:IST-2014-153-v2-2
apa: Chatterjee, K., Daca, P., & Chmelik, M. (2014). CEGAR for qualitative
analysis of probabilistic systems. IST Austria. https://doi.org/10.15479/AT:IST-2014-153-v2-2
chicago: Chatterjee, Krishnendu, Przemyslaw Daca, and Martin Chmelik. CEGAR for
Qualitative Analysis of Probabilistic Systems. IST Austria, 2014. https://doi.org/10.15479/AT:IST-2014-153-v2-2.
ieee: K. Chatterjee, P. Daca, and M. Chmelik, CEGAR for qualitative analysis
of probabilistic systems. IST Austria, 2014.
ista: Chatterjee K, Daca P, Chmelik M. 2014. CEGAR for qualitative analysis of probabilistic
systems, IST Austria, 33p.
mla: Chatterjee, Krishnendu, et al. CEGAR for Qualitative Analysis of Probabilistic
Systems. IST Austria, 2014, doi:10.15479/AT:IST-2014-153-v2-2.
short: K. Chatterjee, P. Daca, M. Chmelik, CEGAR for Qualitative Analysis of Probabilistic
Systems, IST Austria, 2014.
date_created: 2018-12-12T11:39:11Z
date_published: 2014-02-06T00:00:00Z
date_updated: 2023-02-23T12:25:18Z
day: '06'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.15479/AT:IST-2014-153-v2-2
file:
- access_level: open_access
checksum: ce4967a184d84863eec76c66cbac1614
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:54:17Z
date_updated: 2020-07-14T12:46:47Z
file_id: '5539'
file_name: IST-2014-153-v2+2_main.pdf
file_size: 606049
relation: main_file
file_date_updated: 2020-07-14T12:46:47Z
has_accepted_license: '1'
language:
- iso: eng
month: '02'
oa: 1
oa_version: Published Version
page: '33'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '164'
related_material:
record:
- id: '2063'
relation: later_version
status: public
- id: '5412'
relation: earlier_version
status: public
- id: '5414'
relation: later_version
status: public
status: public
title: CEGAR for qualitative analysis of probabilistic systems
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2014'
...
---
_id: '5414'
abstract:
- lang: eng
text: "We consider Markov decision processes (MDPs) which are a standard model for
probabilistic systems. We focus on qualitative properties for MDPs that can express
that desired behaviors of the system arise almost-surely (with probability 1)
or with positive probability.\r\nWe introduce a new simulation relation to capture
the refinement relation of MDPs with respect to qualitative properties, and present
discrete graph theoretic algorithms with quadratic complexity to compute the simulation
relation.\r\nWe present an automated technique for assume-guarantee style reasoning
for compositional analysis of MDPs with qualitative properties by giving a counter-example
guided abstraction-refinement approach to compute our new simulation relation.
\r\nWe have implemented our algorithms and show that the compositional analysis
leads to significant improvements. "
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: Przemyslaw
full_name: Daca, Przemyslaw
id: 49351290-F248-11E8-B48F-1D18A9856A87
last_name: Daca
- first_name: Martin
full_name: Chmelik, Martin
id: 3624234E-F248-11E8-B48F-1D18A9856A87
last_name: Chmelik
citation:
ama: Chatterjee K, Daca P, Chmelik M. CEGAR for Qualitative Analysis of Probabilistic
Systems. IST Austria; 2014. doi:10.15479/AT:IST-2014-153-v3-1
apa: Chatterjee, K., Daca, P., & Chmelik, M. (2014). CEGAR for qualitative
analysis of probabilistic systems. IST Austria. https://doi.org/10.15479/AT:IST-2014-153-v3-1
chicago: Chatterjee, Krishnendu, Przemyslaw Daca, and Martin Chmelik. CEGAR for
Qualitative Analysis of Probabilistic Systems. IST Austria, 2014. https://doi.org/10.15479/AT:IST-2014-153-v3-1.
ieee: K. Chatterjee, P. Daca, and M. Chmelik, CEGAR for qualitative analysis
of probabilistic systems. IST Austria, 2014.
ista: Chatterjee K, Daca P, Chmelik M. 2014. CEGAR for qualitative analysis of probabilistic
systems, IST Austria, 33p.
mla: Chatterjee, Krishnendu, et al. CEGAR for Qualitative Analysis of Probabilistic
Systems. IST Austria, 2014, doi:10.15479/AT:IST-2014-153-v3-1.
short: K. Chatterjee, P. Daca, M. Chmelik, CEGAR for Qualitative Analysis of Probabilistic
Systems, IST Austria, 2014.
date_created: 2018-12-12T11:39:12Z
date_published: 2014-02-07T00:00:00Z
date_updated: 2023-02-23T12:25:15Z
day: '07'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.15479/AT:IST-2014-153-v3-1
file:
- access_level: open_access
checksum: 87b93fe9af71fc5c94b0eb6151537e11
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:53:03Z
date_updated: 2020-07-14T12:46:48Z
file_id: '5464'
file_name: IST-2014-153-v3+1_main.pdf
file_size: 606227
relation: main_file
file_date_updated: 2020-07-14T12:46:48Z
has_accepted_license: '1'
language:
- iso: eng
month: '02'
oa: 1
oa_version: Published Version
page: '33'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '165'
related_material:
record:
- id: '2063'
relation: later_version
status: public
- id: '5412'
relation: earlier_version
status: public
- id: '5413'
relation: earlier_version
status: public
status: public
title: CEGAR for qualitative analysis of probabilistic systems
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2014'
...