---
_id: '1875'
abstract:
- lang: eng
text: We present a formal framework for repairing infinite-state, imperative, sequential
programs, with (possibly recursive) procedures and multiple assertions; the framework
can generate repaired programs by modifying the original erroneous program in
multiple program locations, and can ensure the readability of the repaired program
using user-defined expression templates; the framework also generates a set of
inductive assertions that serve as a proof of correctness of the repaired program.
As a step toward integrating programmer intent and intuition in automated program
repair, we present a cost-aware formulation - given a cost function associated
with permissible statement modifications, the goal is to ensure that the total
program modification cost does not exceed a given repair budget. As part of our
predicate abstractionbased solution framework, we present a sound and complete
algorithm for repair of Boolean programs. We have developed a prototype tool based
on SMT solving and used it successfully to repair diverse errors in benchmark
C programs.
alternative_title:
- LNCS
author:
- first_name: Roopsha
full_name: Samanta, Roopsha
id: 3D2AAC08-F248-11E8-B48F-1D18A9856A87
last_name: Samanta
- first_name: Oswaldo
full_name: Olivo, Oswaldo
last_name: Olivo
- first_name: Emerson
full_name: Allen, Emerson
last_name: Allen
citation:
ama: 'Samanta R, Olivo O, Allen E. Cost-aware automatic program repair. In: Müller-Olm
M, Seidl H, eds. Vol 8723. Springer; 2014:268-284. doi:10.1007/978-3-319-10936-7_17'
apa: 'Samanta, R., Olivo, O., & Allen, E. (2014). Cost-aware automatic program
repair. In M. Müller-Olm & H. Seidl (Eds.) (Vol. 8723, pp. 268–284). Presented
at the SAS: Static Analysis Symposium, Munich, Germany: Springer. https://doi.org/10.1007/978-3-319-10936-7_17'
chicago: Samanta, Roopsha, Oswaldo Olivo, and Emerson Allen. “Cost-Aware Automatic
Program Repair.” edited by Markus Müller-Olm and Helmut Seidl, 8723:268–84. Springer,
2014. https://doi.org/10.1007/978-3-319-10936-7_17.
ieee: 'R. Samanta, O. Olivo, and E. Allen, “Cost-aware automatic program repair,”
presented at the SAS: Static Analysis Symposium, Munich, Germany, 2014, vol. 8723,
pp. 268–284.'
ista: 'Samanta R, Olivo O, Allen E. 2014. Cost-aware automatic program repair. SAS:
Static Analysis Symposium, LNCS, vol. 8723, 268–284.'
mla: Samanta, Roopsha, et al. Cost-Aware Automatic Program Repair. Edited
by Markus Müller-Olm and Helmut Seidl, vol. 8723, Springer, 2014, pp. 268–84,
doi:10.1007/978-3-319-10936-7_17.
short: R. Samanta, O. Olivo, E. Allen, in:, M. Müller-Olm, H. Seidl (Eds.), Springer,
2014, pp. 268–284.
conference:
end_date: 2014-09-14
location: Munich, Germany
name: 'SAS: Static Analysis Symposium'
start_date: 2014-09-11
date_created: 2018-12-11T11:54:29Z
date_published: 2014-09-01T00:00:00Z
date_updated: 2021-01-12T06:53:46Z
day: '01'
ddc:
- '000'
- '005'
department:
- _id: ToHe
doi: 10.1007/978-3-319-10936-7_17
editor:
- first_name: Markus
full_name: Müller-Olm, Markus
last_name: Müller-Olm
- first_name: Helmut
full_name: Seidl, Helmut
last_name: Seidl
file:
- access_level: open_access
checksum: 78ec4ea1bdecc676cd3e8cad35c6182c
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:07:51Z
date_updated: 2020-07-14T12:45:19Z
file_id: '4650'
file_name: IST-2014-313-v1+1_SOE.SAS14.pdf
file_size: 409485
relation: main_file
file_date_updated: 2020-07-14T12:45:19Z
has_accepted_license: '1'
intvolume: ' 8723'
language:
- iso: eng
month: '09'
oa: 1
oa_version: Submitted Version
page: 268 - 284
publication_status: published
publisher: Springer
publist_id: '5221'
pubrep_id: '313'
quality_controlled: '1'
scopus_import: 1
status: public
title: Cost-aware automatic program repair
type: conference
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
volume: 8723
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: '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: '2038'
abstract:
- lang: eng
text: Recently, there has been an effort to add quantitative objectives to formal
verification and synthesis. We introduce and investigate the extension of temporal
logics with quantitative atomic assertions. At the heart of quantitative objectives
lies the accumulation of values along a computation. It is often the accumulated
sum, as with energy objectives, or the accumulated average, as with mean-payoff
objectives. We investigate the extension of temporal logics with the prefix-accumulation
assertions Sum(v) ≥ c and Avg(v) ≥ c, where v is a numeric (or Boolean) variable
of the system, c is a constant rational number, and Sum(v) and Avg(v) denote the
accumulated sum and average of the values of v from the beginning of the computation
up to the current point in time. We also allow the path-accumulation assertions
LimInfAvg(v) ≥ c and LimSupAvg(v) ≥ c, referring to the average value along an
entire infinite computation. We study the border of decidability for such quantitative
extensions of various temporal logics. In particular, we show that extending the
fragment of CTL that has only the EX, EF, AX, and AG temporal modalities with
both prefix-accumulation assertions, or extending LTL with both path-accumulation
assertions, results in temporal logics whose model-checking problem is decidable.
Moreover, the prefix-accumulation assertions may be generalized with "controlled
accumulation," allowing, for example, to specify constraints on the average
waiting time between a request and a grant. On the negative side, we show that
this branching-time logic is, in a sense, the maximal logic with one or both of
the prefix-accumulation assertions that permits a decidable model-checking procedure.
Extending a temporal logic that has the EG or EU modalities, such as CTL or LTL,
makes the problem undecidable.
acknowledgement: The research was supported in part by ERC Starting grant 278410 (QUALITY).
article_number: '27'
article_processing_charge: No
article_type: original
author:
- first_name: Udi
full_name: Boker, Udi
id: 31E297B6-F248-11E8-B48F-1D18A9856A87
last_name: Boker
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Orna
full_name: Kupferman, Orna
last_name: Kupferman
citation:
ama: Boker U, Chatterjee K, Henzinger TA, Kupferman O. Temporal specifications with
accumulative values. ACM Transactions on Computational Logic (TOCL). 2014;15(4).
doi:10.1145/2629686
apa: Boker, U., Chatterjee, K., Henzinger, T. A., & Kupferman, O. (2014). Temporal
specifications with accumulative values. ACM Transactions on Computational
Logic (TOCL). ACM. https://doi.org/10.1145/2629686
chicago: Boker, Udi, Krishnendu Chatterjee, Thomas A Henzinger, and Orna Kupferman.
“Temporal Specifications with Accumulative Values.” ACM Transactions on Computational
Logic (TOCL). ACM, 2014. https://doi.org/10.1145/2629686.
ieee: U. Boker, K. Chatterjee, T. A. Henzinger, and O. Kupferman, “Temporal specifications
with accumulative values,” ACM Transactions on Computational Logic (TOCL),
vol. 15, no. 4. ACM, 2014.
ista: Boker U, Chatterjee K, Henzinger TA, Kupferman O. 2014. Temporal specifications
with accumulative values. ACM Transactions on Computational Logic (TOCL). 15(4),
27.
mla: Boker, Udi, et al. “Temporal Specifications with Accumulative Values.” ACM
Transactions on Computational Logic (TOCL), vol. 15, no. 4, 27, ACM, 2014,
doi:10.1145/2629686.
short: U. Boker, K. Chatterjee, T.A. Henzinger, O. Kupferman, ACM Transactions on
Computational Logic (TOCL) 15 (2014).
date_created: 2018-12-11T11:55:21Z
date_published: 2014-09-16T00:00:00Z
date_updated: 2023-02-23T12:23:54Z
day: '16'
ddc:
- '000'
- '004'
department:
- _id: ToHe
- _id: KrCh
doi: 10.1145/2629686
ec_funded: 1
file:
- access_level: open_access
checksum: 354c41d37500b56320afce94cf9a99c2
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:10:59Z
date_updated: 2020-07-14T12:45:26Z
file_id: '4851'
file_name: IST-2014-192-v1+1_AccumulativeValues.pdf
file_size: 346184
relation: main_file
file_date_updated: 2020-07-14T12:45:26Z
has_accepted_license: '1'
intvolume: ' 15'
issue: '4'
language:
- iso: eng
month: '09'
oa: 1
oa_version: Submitted Version
project:
- _id: 2584A770-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: P 23499-N23
name: Modern Graph Algorithmic Techniques in Formal Verification
- _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: 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: 2587B514-B435-11E9-9278-68D0E5697425
name: Microsoft Research Faculty Fellowship
publication: ACM Transactions on Computational Logic (TOCL)
publication_status: published
publisher: ACM
publist_id: '5013'
pubrep_id: '192'
quality_controlled: '1'
related_material:
record:
- id: '3356'
relation: earlier_version
status: public
- id: '5385'
relation: earlier_version
status: public
scopus_import: 1
status: public
title: Temporal specifications with accumulative values
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 15
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: '2056'
abstract:
- lang: eng
text: 'We consider a continuous-time Markov chain (CTMC) whose state space is partitioned
into aggregates, and each aggregate is assigned a probability measure. A sufficient
condition for defining a CTMC over the aggregates is presented as a variant of
weak lumpability, which also characterizes that the measure over the original
process can be recovered from that of the aggregated one. We show how the applicability
of de-aggregation depends on the initial distribution. The application section
is devoted to illustrate how the developed theory aids in reducing CTMC models
of biochemical systems particularly in connection to protein-protein interactions.
We assume that the model is written by a biologist in form of site-graph-rewrite
rules. Site-graph-rewrite rules compactly express that, often, only a local context
of a protein (instead of a full molecular species) needs to be in a certain configuration
in order to trigger a reaction event. This observation leads to suitable aggregate
Markov chains with smaller state spaces, thereby providing sufficient reduction
in computational complexity. This is further exemplified in two case studies:
simple unbounded polymerization and early EGFR/insulin crosstalk.'
acknowledgement: T. Petrov is supported by SystemsX.ch—the Swiss Inititative for Systems
Biology.
author:
- first_name: Arnab
full_name: Ganguly, Arnab
last_name: Ganguly
- first_name: Tatjana
full_name: Petrov, Tatjana
id: 3D5811FC-F248-11E8-B48F-1D18A9856A87
last_name: Petrov
orcid: 0000-0002-9041-0905
- first_name: Heinz
full_name: Koeppl, Heinz
last_name: Koeppl
citation:
ama: Ganguly A, Petrov T, Koeppl H. Markov chain aggregation and its applications
to combinatorial reaction networks. Journal of Mathematical Biology. 2014;69(3):767-797.
doi:10.1007/s00285-013-0738-7
apa: Ganguly, A., Petrov, T., & Koeppl, H. (2014). Markov chain aggregation
and its applications to combinatorial reaction networks. Journal of Mathematical
Biology. Springer. https://doi.org/10.1007/s00285-013-0738-7
chicago: Ganguly, Arnab, Tatjana Petrov, and Heinz Koeppl. “Markov Chain Aggregation
and Its Applications to Combinatorial Reaction Networks.” Journal of Mathematical
Biology. Springer, 2014. https://doi.org/10.1007/s00285-013-0738-7.
ieee: A. Ganguly, T. Petrov, and H. Koeppl, “Markov chain aggregation and its applications
to combinatorial reaction networks,” Journal of Mathematical Biology, vol.
69, no. 3. Springer, pp. 767–797, 2014.
ista: Ganguly A, Petrov T, Koeppl H. 2014. Markov chain aggregation and its applications
to combinatorial reaction networks. Journal of Mathematical Biology. 69(3), 767–797.
mla: Ganguly, Arnab, et al. “Markov Chain Aggregation and Its Applications to Combinatorial
Reaction Networks.” Journal of Mathematical Biology, vol. 69, no. 3, Springer,
2014, pp. 767–97, doi:10.1007/s00285-013-0738-7.
short: A. Ganguly, T. Petrov, H. Koeppl, Journal of Mathematical Biology 69 (2014)
767–797.
date_created: 2018-12-11T11:55:28Z
date_published: 2014-11-20T00:00:00Z
date_updated: 2021-01-12T06:55:01Z
day: '20'
department:
- _id: CaGu
- _id: ToHe
doi: 10.1007/s00285-013-0738-7
intvolume: ' 69'
issue: '3'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1303.4532
month: '11'
oa: 1
oa_version: Submitted Version
page: 767 - 797
publication: Journal of Mathematical Biology
publication_status: published
publisher: Springer
publist_id: '4990'
quality_controlled: '1'
scopus_import: 1
status: public
title: Markov chain aggregation and its applications to combinatorial reaction networks
type: journal_article
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
volume: 69
year: '2014'
...
---
_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: '2187'
abstract:
- lang: eng
text: 'Systems should not only be correct but also robust in the sense that they
behave reasonably in unexpected situations. This article addresses synthesis of
robust reactive systems from temporal specifications. Existing methods allow arbitrary
behavior if assumptions in the specification are violated. To overcome this, we
define two robustness notions, combine them, and show how to enforce them in synthesis.
The first notion applies to safety properties: If safety assumptions are violated
temporarily, we require that the system recovers to normal operation with as few
errors as possible. The second notion requires that, if liveness assumptions are
violated, as many guarantees as possible should be fulfilled nevertheless. We
present a synthesis procedure achieving this for the important class of GR(1)
specifications, and establish complexity bounds. We also present an implementation
of a special case of robustness, and show experimental results.'
article_processing_charge: No
article_type: original
author:
- first_name: Roderick
full_name: Bloem, Roderick
last_name: Bloem
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Karin
full_name: Greimel, Karin
last_name: Greimel
- 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: Georg
full_name: Hofferek, Georg
last_name: Hofferek
- first_name: Barbara
full_name: Jobstmann, Barbara
last_name: Jobstmann
- first_name: Bettina
full_name: Könighofer, Bettina
last_name: Könighofer
- first_name: Robert
full_name: Könighofer, Robert
last_name: Könighofer
citation:
ama: Bloem R, Chatterjee K, Greimel K, et al. Synthesizing robust systems. Acta
Informatica. 2014;51(3-4):193-220. doi:10.1007/s00236-013-0191-5
apa: Bloem, R., Chatterjee, K., Greimel, K., Henzinger, T. A., Hofferek, G., Jobstmann,
B., … Könighofer, R. (2014). Synthesizing robust systems. Acta Informatica.
Springer. https://doi.org/10.1007/s00236-013-0191-5
chicago: Bloem, Roderick, Krishnendu Chatterjee, Karin Greimel, Thomas A Henzinger,
Georg Hofferek, Barbara Jobstmann, Bettina Könighofer, and Robert Könighofer.
“Synthesizing Robust Systems.” Acta Informatica. Springer, 2014. https://doi.org/10.1007/s00236-013-0191-5.
ieee: R. Bloem et al., “Synthesizing robust systems,” Acta Informatica,
vol. 51, no. 3–4. Springer, pp. 193–220, 2014.
ista: Bloem R, Chatterjee K, Greimel K, Henzinger TA, Hofferek G, Jobstmann B, Könighofer
B, Könighofer R. 2014. Synthesizing robust systems. Acta Informatica. 51(3–4),
193–220.
mla: Bloem, Roderick, et al. “Synthesizing Robust Systems.” Acta Informatica,
vol. 51, no. 3–4, Springer, 2014, pp. 193–220, doi:10.1007/s00236-013-0191-5.
short: R. Bloem, K. Chatterjee, K. Greimel, T.A. Henzinger, G. Hofferek, B. Jobstmann,
B. Könighofer, R. Könighofer, Acta Informatica 51 (2014) 193–220.
date_created: 2018-12-11T11:56:13Z
date_published: 2014-06-01T00:00:00Z
date_updated: 2021-01-12T06:55:51Z
day: '01'
ddc:
- '621'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1007/s00236-013-0191-5
ec_funded: 1
file:
- access_level: open_access
checksum: d7f560f3d923f0f00aa10a0652f83273
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:16:44Z
date_updated: 2020-07-14T12:45:31Z
file_id: '5234'
file_name: IST-2012-71-v1+1_Synthesizing_robust_systems.pdf
file_size: 169523
relation: main_file
file_date_updated: 2020-07-14T12:45:31Z
has_accepted_license: '1'
intvolume: ' 51'
issue: 3-4
language:
- iso: eng
month: '06'
oa: 1
oa_version: Submitted Version
page: 193 - 220
project:
- _id: 25F5A88A-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11402-N23
name: Moderne Concurrency Paradigms
- _id: 2584A770-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: P 23499-N23
name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 2587B514-B435-11E9-9278-68D0E5697425
name: Microsoft Research Faculty Fellowship
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
publication: Acta Informatica
publication_status: published
publisher: Springer
publist_id: '4787'
pubrep_id: '71'
quality_controlled: '1'
scopus_import: 1
status: public
title: Synthesizing robust systems
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 51
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: '2217'
abstract:
- lang: eng
text: "As hybrid systems involve continuous behaviors, they should be evaluated
by quantitative methods, rather than qualitative methods. In this paper we adapt
a quantitative framework, called model measuring, to the hybrid systems domain.
The model-measuring problem asks, given a model M and a specification, what is
the maximal distance such that all models within that distance from M satisfy
(or violate) the specification. A distance function on models is given as part
of the input of the problem. Distances, especially related to continuous behaviors
are more natural in the hybrid case than the discrete case. We are interested
in distances represented by monotonic hybrid automata, a hybrid counterpart of
(discrete) weighted automata, whose recognized timed languages are monotone (w.r.t.
inclusion) in the values of parameters.\r\n\r\nThe contributions of this paper
are twofold. First, we give sufficient conditions under which the model-measuring
problem can be solved. Second, we discuss the modeling of distances and applications
of the model-measuring problem."
acknowledgement: "This work was supported in part by the Austrian Science
Fund NFN RiSE (Rigorous Systems Engineering) and by the ERC Advanced Grant
QUAREM (Quantitative Reactive Modeling).\r\nA Technical Report of this paper is
available at: \r\nhttps://repository.ist.ac.at/id/eprint/171"
article_processing_charge: No
author:
- 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: Otop, Jan
id: 2FC5DA74-F248-11E8-B48F-1D18A9856A87
last_name: Otop
citation:
ama: 'Henzinger TA, Otop J. Model measuring for hybrid systems. In: Proceedings
of the 17th International Conference on Hybrid Systems: Computation and Control.
Springer; 2014:213-222. doi:10.1145/2562059.2562130'
apa: 'Henzinger, T. A., & Otop, J. (2014). Model measuring for hybrid systems.
In Proceedings of the 17th international conference on Hybrid systems: computation
and control (pp. 213–222). Berlin, Germany: Springer. https://doi.org/10.1145/2562059.2562130'
chicago: 'Henzinger, Thomas A, and Jan Otop. “Model Measuring for Hybrid Systems.”
In Proceedings of the 17th International Conference on Hybrid Systems: Computation
and Control, 213–22. Springer, 2014. https://doi.org/10.1145/2562059.2562130.'
ieee: 'T. A. Henzinger and J. Otop, “Model measuring for hybrid systems,” in Proceedings
of the 17th international conference on Hybrid systems: computation and control,
Berlin, Germany, 2014, pp. 213–222.'
ista: 'Henzinger TA, Otop J. 2014. Model measuring for hybrid systems. Proceedings
of the 17th international conference on Hybrid systems: computation and control.
HSCC: Hybrid Systems - Computation and Control, 213–222.'
mla: 'Henzinger, Thomas A., and Jan Otop. “Model Measuring for Hybrid Systems.”
Proceedings of the 17th International Conference on Hybrid Systems: Computation
and Control, Springer, 2014, pp. 213–22, doi:10.1145/2562059.2562130.'
short: 'T.A. Henzinger, J. Otop, in:, Proceedings of the 17th International Conference
on Hybrid Systems: Computation and Control, Springer, 2014, pp. 213–222.'
conference:
end_date: 2014-04-17
location: Berlin, Germany
name: 'HSCC: Hybrid Systems - Computation and Control'
start_date: 2014-04-15
date_created: 2018-12-11T11:56:23Z
date_published: 2014-04-01T00:00:00Z
date_updated: 2023-02-23T12:25:23Z
day: '01'
department:
- _id: ToHe
doi: 10.1145/2562059.2562130
ec_funded: 1
language:
- iso: eng
month: '04'
oa_version: None
page: 213 - 222
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: 'Proceedings of the 17th international conference on Hybrid systems:
computation and control'
publication_status: published
publisher: Springer
publist_id: '4751'
quality_controlled: '1'
related_material:
record:
- id: '5416'
relation: earlier_version
status: public
scopus_import: 1
status: public
title: Model measuring for hybrid systems
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2014'
...
---
_id: '2218'
abstract:
- lang: eng
text: While fixing concurrency bugs, program repair algorithms may introduce new
concurrency bugs. We present an algorithm that avoids such regressions. The solution
space is given by a set of program transformations we consider in the repair process.
These include reordering of instructions within a thread and inserting atomic
sections. The new algorithm learns a constraint on the space of candidate solutions,
from both positive examples (error-free traces) and counterexamples (error traces).
From each counterexample, the algorithm learns a constraint necessary to remove
the errors. From each positive examples, it learns a constraint that is necessary
in order to prevent the repair from turning the trace into an error trace. We
implemented the algorithm and evaluated it on simplified Linux device drivers
with known bugs.
alternative_title:
- LNCS
author:
- first_name: Pavol
full_name: Cerny, Pavol
last_name: Cerny
- 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: Arjun
full_name: Radhakrishna, Arjun
id: 3B51CAC4-F248-11E8-B48F-1D18A9856A87
last_name: Radhakrishna
- first_name: Leonid
full_name: Ryzhyk, Leonid
last_name: Ryzhyk
- first_name: Thorsten
full_name: Tarrach, Thorsten
id: 3D6E8F2C-F248-11E8-B48F-1D18A9856A87
last_name: Tarrach
orcid: 0000-0003-4409-8487
citation:
ama: 'Cerny P, Henzinger TA, Radhakrishna A, Ryzhyk L, Tarrach T. Regression-free
synthesis for concurrency. In: Vol 8559. Springer; 2014:568-584. doi:10.1007/978-3-319-08867-9_38'
apa: 'Cerny, P., Henzinger, T. A., Radhakrishna, A., Ryzhyk, L., & Tarrach,
T. (2014). Regression-free synthesis for concurrency (Vol. 8559, pp. 568–584).
Presented at the CAV: Computer Aided Verification, Vienna, Austria: Springer.
https://doi.org/10.1007/978-3-319-08867-9_38'
chicago: Cerny, Pavol, Thomas A Henzinger, Arjun Radhakrishna, Leonid Ryzhyk, and
Thorsten Tarrach. “Regression-Free Synthesis for Concurrency,” 8559:568–84. Springer,
2014. https://doi.org/10.1007/978-3-319-08867-9_38.
ieee: 'P. Cerny, T. A. Henzinger, A. Radhakrishna, L. Ryzhyk, and T. Tarrach, “Regression-free
synthesis for concurrency,” presented at the CAV: Computer Aided Verification,
Vienna, Austria, 2014, vol. 8559, pp. 568–584.'
ista: 'Cerny P, Henzinger TA, Radhakrishna A, Ryzhyk L, Tarrach T. 2014. Regression-free
synthesis for concurrency. CAV: Computer Aided Verification, LNCS, vol. 8559,
568–584.'
mla: Cerny, Pavol, et al. Regression-Free Synthesis for Concurrency. Vol.
8559, Springer, 2014, pp. 568–84, doi:10.1007/978-3-319-08867-9_38.
short: P. Cerny, T.A. Henzinger, A. Radhakrishna, L. Ryzhyk, T. Tarrach, in:, Springer,
2014, pp. 568–584.
conference:
end_date: 2014-07-22
location: Vienna, Austria
name: 'CAV: Computer Aided Verification'
start_date: 2014-07-18
date_created: 2018-12-11T11:56:23Z
date_published: 2014-07-22T00:00:00Z
date_updated: 2023-09-07T11:57:01Z
day: '22'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-319-08867-9_38
ec_funded: 1
file:
- access_level: open_access
checksum: a631d3105509f239724644e77a1212e2
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:13:14Z
date_updated: 2020-07-14T12:45:33Z
file_id: '4995'
file_name: IST-2014-297-v1+1_cav14-final.pdf
file_size: 416732
relation: main_file
- access_level: open_access
checksum: f8b0f748cc9fa697ca992cc56c87bc4e
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:13:15Z
date_updated: 2020-07-14T12:45:33Z
file_id: '4996'
file_name: IST-2014-297-v2+1_cav14-final2.pdf
file_size: 616293
relation: main_file
file_date_updated: 2020-07-14T12:45:33Z
has_accepted_license: '1'
intvolume: ' 8559'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://link.springer.com/chapter/10.1007%2F978-3-319-08867-9_38
month: '07'
oa: 1
oa_version: Submitted Version
page: 568 - 584
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_identifier:
isbn:
- 978-331908866-2
publication_status: published
publisher: Springer
publist_id: '4749'
pubrep_id: '297'
quality_controlled: '1'
related_material:
record:
- id: '1130'
relation: dissertation_contains
status: public
status: public
title: Regression-free synthesis for concurrency
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 8559
year: '2014'
...
---
_id: '2233'
abstract:
- lang: eng
text: ' A discounted-sum automaton (NDA) is a nondeterministic finite automaton
with edge weights, valuing a run by the discounted sum of visited edge weights.
More precisely, the weight in the i-th position of the run is divided by λi, where
the discount factor λ is a fixed rational number greater than 1. The value of
a word is the minimal value of the automaton runs on it. Discounted summation
is a common and useful measuring scheme, especially for infinite sequences, reflecting
the assumption that earlier weights are more important than later weights. Unfortunately,
determinization of NDAs, which is often essential in formal verification, is,
in general, not possible. We provide positive news, showing that every NDA with
an integral discount factor is determinizable. We complete the picture by proving
that the integers characterize exactly the discount factors that guarantee determinizability:
for every nonintegral rational discount factor λ, there is a nondeterminizable
λ-NDA. We also prove that the class of NDAs with integral discount factors enjoys
closure under the algebraic operations min, max, addition, and subtraction, which
is not the case for general NDAs nor for deterministic NDAs. For general NDAs,
we look into approximate determinization, which is always possible as the influence
of a word''s suffix decays. We show that the naive approach, of unfolding the
automaton computations up to a sufficient level, is doubly exponential in the
discount factor. We provide an alternative construction for approximate determinization,
which is singly exponential in the discount factor, in the precision, and in the
number of states. We also prove matching lower bounds, showing that the exponential
dependency on each of these three parameters cannot be avoided. All our results
hold equally for automata over finite words and for automata over infinite words. '
author:
- first_name: Udi
full_name: Boker, Udi
last_name: Boker
- 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: Boker U, Henzinger TA. Exact and approximate determinization of discounted-sum
automata. Logical Methods in Computer Science. 2014;10(1). doi:10.2168/LMCS-10(1:10)2014
apa: Boker, U., & Henzinger, T. A. (2014). Exact and approximate determinization
of discounted-sum automata. Logical Methods in Computer Science. International
Federation of Computational Logic. https://doi.org/10.2168/LMCS-10(1:10)2014
chicago: Boker, Udi, and Thomas A Henzinger. “Exact and Approximate Determinization
of Discounted-Sum Automata.” Logical Methods in Computer Science. International
Federation of Computational Logic, 2014. https://doi.org/10.2168/LMCS-10(1:10)2014.
ieee: U. Boker and T. A. Henzinger, “Exact and approximate determinization of discounted-sum
automata,” Logical Methods in Computer Science, vol. 10, no. 1. International
Federation of Computational Logic, 2014.
ista: Boker U, Henzinger TA. 2014. Exact and approximate determinization of discounted-sum
automata. Logical Methods in Computer Science. 10(1).
mla: Boker, Udi, and Thomas A. Henzinger. “Exact and Approximate Determinization
of Discounted-Sum Automata.” Logical Methods in Computer Science, vol.
10, no. 1, International Federation of Computational Logic, 2014, doi:10.2168/LMCS-10(1:10)2014.
short: U. Boker, T.A. Henzinger, Logical Methods in Computer Science 10 (2014).
date_created: 2018-12-11T11:56:28Z
date_published: 2014-02-13T00:00:00Z
date_updated: 2021-01-12T06:56:11Z
day: '13'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.2168/LMCS-10(1:10)2014
ec_funded: 1
file:
- access_level: open_access
checksum: 9f6ea2e2d8d4a32ff0becc29d835bbf8
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:07:45Z
date_updated: 2020-07-14T12:45:34Z
file_id: '4643'
file_name: IST-2015-389-v1+1_1401.3957.pdf
file_size: 550936
relation: main_file
file_date_updated: 2020-07-14T12:45:34Z
has_accepted_license: '1'
intvolume: ' 10'
issue: '1'
language:
- iso: eng
month: '02'
oa: 1
oa_version: Published Version
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
publication: Logical Methods in Computer Science
publication_identifier:
issn:
- '18605974'
publication_status: published
publisher: International Federation of Computational Logic
publist_id: '4728'
pubrep_id: '389'
quality_controlled: '1'
scopus_import: 1
status: public
title: Exact and approximate determinization of discounted-sum automata
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: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 10
year: '2014'
...
---
_id: '2239'
abstract:
- lang: eng
text: The analysis of the energy consumption of software is an important goal for
quantitative formal methods. Current methods, using weighted transition systems
or energy games, model the energy source as an ideal resource whose status is
characterized by one number, namely the amount of remaining energy. Real batteries,
however, exhibit behaviors that can deviate substantially from an ideal energy
resource. Based on a discretization of a standard continuous battery model, we
introduce battery transition systems. In this model, a battery is viewed as consisting
of two parts-the available-charge tank and the bound-charge tank. Any charge or
discharge is applied to the available-charge tank. Over time, the energy from
each tank diffuses to the other tank. Battery transition systems are infinite
state systems that, being not well-structured, fall into no decidable class that
is known to us. Nonetheless, we are able to prove that the !-regular modelchecking
problem is decidable for battery transition systems. We also present a case study
on the verification of control programs for energy-constrained semi-autonomous
robots.
author:
- first_name: Udi
full_name: Boker, Udi
id: 31E297B6-F248-11E8-B48F-1D18A9856A87
last_name: Boker
- 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: Arjun
full_name: Radhakrishna, Arjun
id: 3B51CAC4-F248-11E8-B48F-1D18A9856A87
last_name: Radhakrishna
citation:
ama: 'Boker U, Henzinger TA, Radhakrishna A. Battery transition systems. In: Vol
49. ACM; 2014:595-606. doi:10.1145/2535838.2535875'
apa: 'Boker, U., Henzinger, T. A., & Radhakrishna, A. (2014). Battery transition
systems (Vol. 49, pp. 595–606). Presented at the POPL: Principles of Programming
Languages, San Diego, USA: ACM. https://doi.org/10.1145/2535838.2535875'
chicago: Boker, Udi, Thomas A Henzinger, and Arjun Radhakrishna. “Battery Transition
Systems,” 49:595–606. ACM, 2014. https://doi.org/10.1145/2535838.2535875.
ieee: 'U. Boker, T. A. Henzinger, and A. Radhakrishna, “Battery transition systems,”
presented at the POPL: Principles of Programming Languages, San Diego, USA, 2014,
vol. 49, no. 1, pp. 595–606.'
ista: 'Boker U, Henzinger TA, Radhakrishna A. 2014. Battery transition systems.
POPL: Principles of Programming Languages vol. 49, 595–606.'
mla: Boker, Udi, et al. Battery Transition Systems. Vol. 49, no. 1, ACM,
2014, pp. 595–606, doi:10.1145/2535838.2535875.
short: U. Boker, T.A. Henzinger, A. Radhakrishna, in:, ACM, 2014, pp. 595–606.
conference:
end_date: 2014-01-24
location: San Diego, USA
name: 'POPL: Principles of Programming Languages'
start_date: 2014-01-22
date_created: 2018-12-11T11:56:30Z
date_published: 2014-01-13T00:00:00Z
date_updated: 2021-01-12T06:56:13Z
day: '13'
department:
- _id: ToHe
doi: 10.1145/2535838.2535875
ec_funded: 1
intvolume: ' 49'
issue: '1'
language:
- iso: eng
month: '01'
oa_version: None
page: 595 - 606
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
publication_identifier:
isbn:
- 978-145032544-8
publication_status: published
publisher: ACM
publist_id: '4722'
quality_controlled: '1'
scopus_import: 1
status: public
title: Battery transition systems
type: conference
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
volume: 49
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: '5415'
abstract:
- lang: eng
text: 'Recently there has been a significant effort to add quantitative properties
in formal verification and synthesis. While weighted automata over finite and
infinite words provide a natural and flexible framework to express quantitative
properties, perhaps surprisingly, several basic system properties such as average
response time cannot be expressed with weighted automata. In this work, we introduce
nested weighted automata as a new formalism for expressing important quantitative
properties such as average response time. We establish an almost complete decidability
picture for the basic decision problems for nested weighted automata, and illustrate
its applicability in several domains. '
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: 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: Otop, Jan
id: 2FC5DA74-F248-11E8-B48F-1D18A9856A87
last_name: Otop
citation:
ama: Chatterjee K, Henzinger TA, Otop J. Nested Weighted Automata. IST Austria;
2014. doi:10.15479/AT:IST-2014-170-v1-1
apa: Chatterjee, K., Henzinger, T. A., & Otop, J. (2014). Nested weighted
automata. IST Austria. https://doi.org/10.15479/AT:IST-2014-170-v1-1
chicago: Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. Nested Weighted
Automata. IST Austria, 2014. https://doi.org/10.15479/AT:IST-2014-170-v1-1.
ieee: K. Chatterjee, T. A. Henzinger, and J. Otop, Nested weighted automata.
IST Austria, 2014.
ista: Chatterjee K, Henzinger TA, Otop J. 2014. Nested weighted automata, IST Austria,
27p.
mla: Chatterjee, Krishnendu, et al. Nested Weighted Automata. IST Austria,
2014, doi:10.15479/AT:IST-2014-170-v1-1.
short: K. Chatterjee, T.A. Henzinger, J. Otop, Nested Weighted Automata, IST Austria,
2014.
date_created: 2018-12-12T11:39:12Z
date_published: 2014-02-19T00:00:00Z
date_updated: 2023-02-23T12:26:19Z
day: '19'
ddc:
- '004'
department:
- _id: KrCh
- _id: ToHe
doi: 10.15479/AT:IST-2014-170-v1-1
file:
- access_level: open_access
checksum: 31f90dcf2cf899c3f8c6427cfcc2b3c7
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:53:36Z
date_updated: 2020-07-14T12:46:48Z
file_id: '5497'
file_name: IST-2014-170-v1+1_main.pdf
file_size: 573457
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: '27'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '170'
related_material:
record:
- id: '1656'
relation: later_version
status: public
- id: '467'
relation: later_version
status: public
- id: '5436'
relation: later_version
status: public
status: public
title: Nested weighted automata
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2014'
...
---
_id: '5416'
abstract:
- lang: eng
text: As hybrid systems involve continuous behaviors, they should be evaluated by
quantitative methods, rather than qualitative methods. In this paper we adapt
a quantitative framework, called model measuring, to the hybrid systems domain.
The model-measuring problem asks, given a model M and a specification, what is
the maximal distance such that all models within that distance from M satisfy
(or violate) the specification. A distance function on models is given as part
of the input of the problem. Distances, especially related to continuous behaviors
are more natural in the hybrid case than the discrete case. We are interested
in distances represented by monotonic hybrid automata, a hybrid counterpart of
(discrete) weighted automata, whose recognized timed languages are monotone (w.r.t.
inclusion) in the values of parameters.The contributions of this paper are twofold.
First, we give sufficient conditions under which the model-measuring problem can
be solved. Second, we discuss the modeling of distances and applications of the
model-measuring problem.
alternative_title:
- IST Austria Technical Report
author:
- 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: Otop, Jan
id: 2FC5DA74-F248-11E8-B48F-1D18A9856A87
last_name: Otop
citation:
ama: Henzinger TA, Otop J. Model Measuring for Hybrid Systems. IST Austria;
2014. doi:10.15479/AT:IST-2014-171-v1-1
apa: Henzinger, T. A., & Otop, J. (2014). Model measuring for hybrid systems.
IST Austria. https://doi.org/10.15479/AT:IST-2014-171-v1-1
chicago: Henzinger, Thomas A, and Jan Otop. Model Measuring for Hybrid Systems.
IST Austria, 2014. https://doi.org/10.15479/AT:IST-2014-171-v1-1.
ieee: T. A. Henzinger and J. Otop, Model measuring for hybrid systems. IST
Austria, 2014.
ista: Henzinger TA, Otop J. 2014. Model measuring for hybrid systems, IST Austria,
22p.
mla: Henzinger, Thomas A., and Jan Otop. Model Measuring for Hybrid Systems.
IST Austria, 2014, doi:10.15479/AT:IST-2014-171-v1-1.
short: T.A. Henzinger, J. Otop, Model Measuring for Hybrid Systems, IST Austria,
2014.
date_created: 2018-12-12T11:39:12Z
date_published: 2014-02-19T00:00:00Z
date_updated: 2023-02-23T10:33:21Z
day: '19'
ddc:
- '005'
department:
- _id: ToHe
doi: 10.15479/AT:IST-2014-171-v1-1
file:
- access_level: open_access
checksum: 445456d22371e4e49aad2b9a0c13bf80
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:53:32Z
date_updated: 2020-07-14T12:46:49Z
file_id: '5492'
file_name: IST-2014-171-v1+1_report.pdf
file_size: 712077
relation: main_file
file_date_updated: 2020-07-14T12:46:49Z
has_accepted_license: '1'
language:
- iso: eng
month: '02'
oa: 1
oa_version: Published Version
page: '22'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '171'
related_material:
record:
- id: '2217'
relation: later_version
status: public
status: public
title: Model measuring for hybrid systems
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2014'
...
---
_id: '5417'
abstract:
- lang: eng
text: "We define the model-measuring problem: given a model M and specification
φ, what is the maximal distance ρ such that all models M'within distance ρ from
M satisfy (or violate)φ. The model measuring problem presupposes a distance function
on models. We concentrate on automatic distance functions, which are defined by
weighted automata.\r\nThe model-measuring problem subsumes several generalizations
of the classical model-checking problem, in particular, quantitative model-checking
problems that measure the degree of satisfaction of a specification, and robustness
problems that measure how much a model can be perturbed without violating the
specification.\r\nWe show that for automatic distance functions, and ω-regular
linear-time and branching-time specifications, the model-measuring problem can
be solved.\r\nWe use automata-theoretic model-checking methods for model measuring,
replacing the emptiness question for standard word and tree automata by the optimal-weight
question for the weighted versions of these automata. We consider weighted automata
that accumulate weights by maximizing, summing, discounting, and limit averaging.
\r\nWe give several examples of using the model-measuring problem to compute various
notions of robustness and quantitative satisfaction for temporal specifications."
alternative_title:
- IST Austria Technical Report
author:
- 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: Otop, Jan
id: 2FC5DA74-F248-11E8-B48F-1D18A9856A87
last_name: Otop
citation:
ama: Henzinger TA, Otop J. From Model Checking to Model Measuring. IST Austria;
2014. doi:10.15479/AT:IST-2014-172-v1-1
apa: Henzinger, T. A., & Otop, J. (2014). From model checking to model measuring.
IST Austria. https://doi.org/10.15479/AT:IST-2014-172-v1-1
chicago: Henzinger, Thomas A, and Jan Otop. From Model Checking to Model Measuring.
IST Austria, 2014. https://doi.org/10.15479/AT:IST-2014-172-v1-1.
ieee: T. A. Henzinger and J. Otop, From model checking to model measuring.
IST Austria, 2014.
ista: Henzinger TA, Otop J. 2014. From model checking to model measuring, IST Austria,
14p.
mla: Henzinger, Thomas A., and Jan Otop. From Model Checking to Model Measuring.
IST Austria, 2014, doi:10.15479/AT:IST-2014-172-v1-1.
short: T.A. Henzinger, J. Otop, From Model Checking to Model Measuring, IST Austria,
2014.
date_created: 2018-12-12T11:39:13Z
date_published: 2014-02-19T00:00:00Z
date_updated: 2023-02-23T10:38:10Z
day: '19'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.15479/AT:IST-2014-172-v1-1
file:
- access_level: open_access
checksum: fcc3eab903cfcd3778b338d2d0d44d18
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:53:20Z
date_updated: 2020-07-14T12:46:49Z
file_id: '5481'
file_name: IST-2014-172-v1+1_report.pdf
file_size: 383052
relation: main_file
file_date_updated: 2020-07-14T12:46:49Z
has_accepted_license: '1'
language:
- iso: eng
month: '02'
oa: 1
oa_version: Published Version
page: '14'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '175'
related_material:
record:
- id: '2327'
relation: later_version
status: public
status: public
title: From model checking to model measuring
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2014'
...
---
_id: '5428'
abstract:
- lang: eng
text: "Simulation is an attractive alternative for language inclusion for automata
as it is an under-approximation of language inclusion, but usually has much lower
complexity. For non-deterministic automata, while language inclusion is PSPACE-complete,
simulation can be computed in polynomial time. Simulation has also been extended
in two orthogonal directions, namely, (1) fair simulation, for simulation over
specified set of infinite runs; and (2) quantitative simulation, for simulation
between weighted automata. Again, while fair trace inclusion is PSPACE-complete,
fair simulation can be computed in polynomial time. For weighted automata, the
(quantitative) language inclusion problem is undecidable for mean-payoff automata
and the decidability is open for discounted-sum automata, whereas the (quantitative)
simulation reduce to mean-payoff games and discounted-sum games, which admit pseudo-polynomial
time algorithms.\r\n\r\nIn this work, we study (quantitative) simulation for weighted
automata with Büchi acceptance conditions, i.e., we generalize fair simulation
from non-weighted automata to weighted automata. We show that imposing Büchi acceptance
conditions on weighted automata changes many fundamental properties of the simulation
games. For example, whereas for mean-payoff and discounted-sum games, the players
do not need memory to play optimally; we show in contrast that for simulation
games with Büchi acceptance conditions, (i) for mean-payoff objectives, optimal
strategies for both players require infinite memory in general, and (ii) for discounted-sum
objectives, optimal strategies need not exist for both players. While the simulation
games with Büchi acceptance conditions are more complicated (e.g., due to infinite-memory
requirements for mean-payoff objectives) as compared to their counterpart without
Büchi acceptance conditions, we still present pseudo-polynomial time algorithms
to solve simulation games with Büchi acceptance conditions for both weighted mean-payoff
and weighted discounted-sum automata."
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: 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: Otop, Jan
id: 2FC5DA74-F248-11E8-B48F-1D18A9856A87
last_name: Otop
- first_name: Yaron
full_name: Velner, Yaron
last_name: Velner
citation:
ama: Chatterjee K, Henzinger TA, Otop J, Velner Y. Quantitative Fair Simulation
Games. IST Austria; 2014. doi:10.15479/AT:IST-2014-315-v1-1
apa: Chatterjee, K., Henzinger, T. A., Otop, J., & Velner, Y. (2014). Quantitative
fair simulation games. IST Austria. https://doi.org/10.15479/AT:IST-2014-315-v1-1
chicago: Chatterjee, Krishnendu, Thomas A Henzinger, Jan Otop, and Yaron Velner.
Quantitative Fair Simulation Games. IST Austria, 2014. https://doi.org/10.15479/AT:IST-2014-315-v1-1.
ieee: K. Chatterjee, T. A. Henzinger, J. Otop, and Y. Velner, Quantitative fair
simulation games. IST Austria, 2014.
ista: Chatterjee K, Henzinger TA, Otop J, Velner Y. 2014. Quantitative fair simulation
games, IST Austria, 26p.
mla: Chatterjee, Krishnendu, et al. Quantitative Fair Simulation Games. IST
Austria, 2014, doi:10.15479/AT:IST-2014-315-v1-1.
short: K. Chatterjee, T.A. Henzinger, J. Otop, Y. Velner, Quantitative Fair Simulation
Games, IST Austria, 2014.
date_created: 2018-12-12T11:39:16Z
date_published: 2014-12-05T00:00:00Z
date_updated: 2023-09-20T12:07:48Z
day: '05'
ddc:
- '004'
department:
- _id: ToHe
- _id: KrCh
doi: 10.15479/AT:IST-2014-315-v1-1
file:
- access_level: open_access
checksum: b1d573bc04365625ff9974880c0aa807
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:53:59Z
date_updated: 2020-07-14T12:46:52Z
file_id: '5521'
file_name: IST-2014-315-v1+1_report.pdf
file_size: 531046
relation: main_file
file_date_updated: 2020-07-14T12:46:52Z
has_accepted_license: '1'
language:
- iso: eng
month: '12'
oa: 1
oa_version: Published Version
page: '26'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '315'
related_material:
record:
- id: '1066'
relation: later_version
status: public
status: public
title: Quantitative fair simulation games
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2014'
...
---
_id: '1392'
abstract:
- lang: eng
text: Fault-tolerant distributed algorithms play an important role in ensuring the
reliability of many software applications. In this paper we consider distributed
algorithms whose computations are organized in rounds. To verify the correctness
of such algorithms, we reason about (i) properties (such as invariants) of the
state, (ii) the transitions controlled by the algorithm, and (iii) the communication
graph. We introduce a logic that addresses these points, and contains set comprehensions
with cardinality constraints, function symbols to describe the local states of
each process, and a limited form of quantifier alternation to express the verification
conditions. We show its use in automating the verification of consensus algorithms.
In particular, we give a semi-decision procedure for the unsatisfiability problem
of the logic and identify a decidable fragment. We successfully applied our framework
to verify the correctness of a variety of consensus algorithms tolerant to both
benign faults (message loss, process crashes) and value faults (message corruption).
acknowledgement: Supported by the Vienna Science and Technology Fund (WWTF) through
grant PROSEED.
alternative_title:
- LNCS
author:
- first_name: Cezara
full_name: Dragoi, Cezara
id: 2B2B5ED0-F248-11E8-B48F-1D18A9856A87
last_name: Dragoi
- 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: Helmut
full_name: Veith, Helmut
last_name: Veith
- first_name: Josef
full_name: Widder, Josef
last_name: Widder
- first_name: Damien
full_name: Zufferey, Damien
id: 4397AC76-F248-11E8-B48F-1D18A9856A87
last_name: Zufferey
orcid: 0000-0002-3197-8736
citation:
ama: 'Dragoi C, Henzinger TA, Veith H, Widder J, Zufferey D. A logic-based framework
for verifying consensus algorithms. In: Vol 8318. Springer; 2014:161-181. doi:10.1007/978-3-642-54013-4_10'
apa: 'Dragoi, C., Henzinger, T. A., Veith, H., Widder, J., & Zufferey, D. (2014).
A logic-based framework for verifying consensus algorithms (Vol. 8318, pp. 161–181).
Presented at the VMCAI: Verification, Model Checking and Abstract Interpretation,
San Diego, USA: Springer. https://doi.org/10.1007/978-3-642-54013-4_10'
chicago: Dragoi, Cezara, Thomas A Henzinger, Helmut Veith, Josef Widder, and Damien
Zufferey. “A Logic-Based Framework for Verifying Consensus Algorithms,” 8318:161–81.
Springer, 2014. https://doi.org/10.1007/978-3-642-54013-4_10.
ieee: 'C. Dragoi, T. A. Henzinger, H. Veith, J. Widder, and D. Zufferey, “A logic-based
framework for verifying consensus algorithms,” presented at the VMCAI: Verification,
Model Checking and Abstract Interpretation, San Diego, USA, 2014, vol. 8318, pp.
161–181.'
ista: 'Dragoi C, Henzinger TA, Veith H, Widder J, Zufferey D. 2014. A logic-based
framework for verifying consensus algorithms. VMCAI: Verification, Model Checking
and Abstract Interpretation, LNCS, vol. 8318, 161–181.'
mla: Dragoi, Cezara, et al. A Logic-Based Framework for Verifying Consensus Algorithms.
Vol. 8318, Springer, 2014, pp. 161–81, doi:10.1007/978-3-642-54013-4_10.
short: C. Dragoi, T.A. Henzinger, H. Veith, J. Widder, D. Zufferey, in:, Springer,
2014, pp. 161–181.
conference:
end_date: 2014-01-21
location: San Diego, USA
name: 'VMCAI: Verification, Model Checking and Abstract Interpretation'
start_date: 2014-01-19
date_created: 2018-12-11T11:51:45Z
date_published: 2014-01-01T00:00:00Z
date_updated: 2021-01-12T06:50:22Z
day: '01'
ddc:
- '000'
- '005'
department:
- _id: ToHe
doi: 10.1007/978-3-642-54013-4_10
ec_funded: 1
file:
- access_level: open_access
checksum: bffa33d39be77df0da39defe97eabf84
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:11:06Z
date_updated: 2020-07-14T12:44:48Z
file_id: '4859'
file_name: IST-2014-179-v1+1_vmcai14.pdf
file_size: 444138
relation: main_file
file_date_updated: 2020-07-14T12:44:48Z
has_accepted_license: '1'
intvolume: ' 8318'
language:
- iso: eng
month: '01'
oa: 1
oa_version: Submitted Version
page: 161 - 181
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
publication_status: published
publisher: Springer
publist_id: '5817'
pubrep_id: '179'
quality_controlled: '1'
scopus_import: 1
status: public
title: A logic-based framework for verifying consensus algorithms
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 8318
year: '2014'
...