---
_id: '8600'
abstract:
- lang: eng
text: 'A vector addition system with states (VASS) consists of a finite set of states
and counters. A transition changes the current state to the next state, and every
counter is either incremented, or decremented, or left unchanged. A state and
value for each counter is a configuration; and a computation is an infinite sequence
of configurations with transitions between successive configurations. A probabilistic
VASS consists of a VASS along with a probability distribution over the transitions
for each state. Qualitative properties such as state and configuration reachability
have been widely studied for VASS. In this work we consider multi-dimensional
long-run average objectives for VASS and probabilistic VASS. For a counter, the
cost of a configuration is the value of the counter; and the long-run average
value of a computation for the counter is the long-run average of the costs of
the configurations in the computation. The multi-dimensional long-run average
problem given a VASS and a threshold value for each counter, asks whether there
is a computation such that for each counter the long-run average value for the
counter does not exceed the respective threshold. For probabilistic VASS, instead
of the existence of a computation, we consider whether the expected long-run average
value for each counter does not exceed the respective threshold. Our main results
are as follows: we show that the multi-dimensional long-run average problem (a)
is NP-complete for integer-valued VASS; (b) is undecidable for natural-valued
VASS (i.e., nonnegative counters); and (c) can be solved in polynomial time for
probabilistic integer-valued VASS, and probabilistic natural-valued VASS when
all computations are non-terminating.'
alternative_title:
- LIPIcs
article_number: '23'
article_processing_charge: No
arxiv: 1
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: 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. Multi-dimensional long-run average problems
for vector addition systems with states. In: 31st International Conference
on Concurrency Theory. Vol 171. Schloss Dagstuhl - Leibniz-Zentrum für Informatik;
2020. doi:10.4230/LIPIcs.CONCUR.2020.23'
apa: 'Chatterjee, K., Henzinger, T. A., & Otop, J. (2020). Multi-dimensional
long-run average problems for vector addition systems with states. In 31st
International Conference on Concurrency Theory (Vol. 171). Virtual: Schloss
Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2020.23'
chicago: Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. “Multi-Dimensional
Long-Run Average Problems for Vector Addition Systems with States.” In 31st
International Conference on Concurrency Theory, Vol. 171. Schloss Dagstuhl
- Leibniz-Zentrum für Informatik, 2020. https://doi.org/10.4230/LIPIcs.CONCUR.2020.23.
ieee: K. Chatterjee, T. A. Henzinger, and J. Otop, “Multi-dimensional long-run average
problems for vector addition systems with states,” in 31st International Conference
on Concurrency Theory, Virtual, 2020, vol. 171.
ista: 'Chatterjee K, Henzinger TA, Otop J. 2020. Multi-dimensional long-run average
problems for vector addition systems with states. 31st International Conference
on Concurrency Theory. CONCUR: Conference on Concurrency Theory, LIPIcs, vol.
171, 23.'
mla: Chatterjee, Krishnendu, et al. “Multi-Dimensional Long-Run Average Problems
for Vector Addition Systems with States.” 31st International Conference on
Concurrency Theory, vol. 171, 23, Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
2020, doi:10.4230/LIPIcs.CONCUR.2020.23.
short: K. Chatterjee, T.A. Henzinger, J. Otop, in:, 31st International Conference
on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020.
conference:
end_date: 2020-09-04
location: Virtual
name: 'CONCUR: Conference on Concurrency Theory'
start_date: 2020-09-01
date_created: 2020-10-04T22:01:36Z
date_published: 2020-08-06T00:00:00Z
date_updated: 2021-01-12T08:20:15Z
day: '06'
ddc:
- '000'
department:
- _id: KrCh
- _id: ToHe
doi: 10.4230/LIPIcs.CONCUR.2020.23
external_id:
arxiv:
- '2007.08917'
file:
- access_level: open_access
checksum: 5039752f644c4b72b9361d21a5e31baf
content_type: application/pdf
creator: dernst
date_created: 2020-10-05T14:04:25Z
date_updated: 2020-10-05T14:04:25Z
file_id: '8610'
file_name: 2020_LIPIcsCONCUR_Chatterjee.pdf
file_size: 601231
relation: main_file
success: 1
file_date_updated: 2020-10-05T14:04:25Z
has_accepted_license: '1'
intvolume: ' 171'
language:
- iso: eng
month: '08'
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: 25F2ACDE-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11402-N23
name: Rigorous Systems Engineering
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
publication: 31st International Conference on Concurrency Theory
publication_identifier:
isbn:
- '9783959771603'
issn:
- '18688969'
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
quality_controlled: '1'
scopus_import: '1'
status: public
title: Multi-dimensional long-run average problems for vector addition systems with
states
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/3.0/legalcode
name: Creative Commons Attribution 3.0 Unported (CC BY 3.0)
short: CC BY (3.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 171
year: '2020'
...
---
_id: '86'
abstract:
- lang: eng
text: Responsiveness—the requirement that every request to a system be eventually
handled—is one of the fundamental liveness properties of a reactive system. Average
response time is a quantitative measure for the responsiveness requirement used
commonly in performance evaluation. We show how average response time can be computed
on state-transition graphs, on Markov chains, and on game graphs. In all three
cases, we give polynomial-time algorithms.
acknowledgement: 'This research was supported in part by the Austrian Science Fund
(FWF) under grants S11402-N23, S11407-N23 (RiSE/SHiNE) and Z211-N23 (Wittgenstein
Award), ERC Start grant (279307: Graph Games), Vienna Science and Technology Fund
(WWTF) through project ICT15-003 and by the National Science Centre (NCN), Poland
under grant 2014/15/D/ST6/04543.'
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: 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. Computing average response time. In: Lohstroh
M, Derler P, Sirjani M, eds. Principles of Modeling. Vol 10760. Springer;
2018:143-161. doi:10.1007/978-3-319-95246-8_9'
apa: Chatterjee, K., Henzinger, T. A., & Otop, J. (2018). Computing average
response time. In M. Lohstroh, P. Derler, & M. Sirjani (Eds.), Principles
of Modeling (Vol. 10760, pp. 143–161). Springer. https://doi.org/10.1007/978-3-319-95246-8_9
chicago: Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. “Computing Average
Response Time.” In Principles of Modeling, edited by Marten Lohstroh, Patricia
Derler, and Marjan Sirjani, 10760:143–61. Springer, 2018. https://doi.org/10.1007/978-3-319-95246-8_9.
ieee: K. Chatterjee, T. A. Henzinger, and J. Otop, “Computing average response time,”
in Principles of Modeling, vol. 10760, M. Lohstroh, P. Derler, and M. Sirjani,
Eds. Springer, 2018, pp. 143–161.
ista: 'Chatterjee K, Henzinger TA, Otop J. 2018.Computing average response time.
In: Principles of Modeling. LNCS, vol. 10760, 143–161.'
mla: Chatterjee, Krishnendu, et al. “Computing Average Response Time.” Principles
of Modeling, edited by Marten Lohstroh et al., vol. 10760, Springer, 2018,
pp. 143–61, doi:10.1007/978-3-319-95246-8_9.
short: K. Chatterjee, T.A. Henzinger, J. Otop, in:, M. Lohstroh, P. Derler, M. Sirjani
(Eds.), Principles of Modeling, Springer, 2018, pp. 143–161.
date_created: 2018-12-11T11:44:33Z
date_published: 2018-07-20T00:00:00Z
date_updated: 2021-01-12T08:20:14Z
day: '20'
ddc:
- '000'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1007/978-3-319-95246-8_9
ec_funded: 1
editor:
- first_name: Marten
full_name: Lohstroh, Marten
last_name: Lohstroh
- first_name: Patricia
full_name: Derler, Patricia
last_name: Derler
- first_name: Marjan
full_name: Sirjani, Marjan
last_name: Sirjani
file:
- access_level: open_access
checksum: 9995c6ce6957333baf616fc4f20be597
content_type: application/pdf
creator: dernst
date_created: 2019-11-19T08:22:18Z
date_updated: 2020-07-14T12:48:14Z
file_id: '7053'
file_name: 2018_PrinciplesModeling_Chatterjee.pdf
file_size: 516307
relation: main_file
file_date_updated: 2020-07-14T12:48:14Z
has_accepted_license: '1'
intvolume: ' 10760'
language:
- iso: eng
month: '07'
oa: 1
oa_version: Submitted Version
page: 143 - 161
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11407
name: Game Theory
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 25892FC0-B435-11E9-9278-68D0E5697425
grant_number: ICT15-003
name: Efficient Algorithms for Computer Aided Verification
publication: Principles of Modeling
publication_status: published
publisher: Springer
publist_id: '7968'
quality_controlled: '1'
scopus_import: 1
status: public
title: Computing average response time
type: book_chapter
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 10760
year: '2018'
...
---
_id: '1066'
abstract:
- lang: eng
text: "Simulation is an attractive alternative to language inclusion for automata
as it is an under-approximation of language inclusion, but usually has much lower
complexity. 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. 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 in general, whereas the (quantitative) simulation reduces to quantitative
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, yet they still admit pseudo-polynomial
time algorithms."
article_processing_charge: No
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: 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. Information and Computation. 2017;254(2):143-166. doi:10.1016/j.ic.2016.10.006
apa: Chatterjee, K., Henzinger, T. A., Otop, J., & Velner, Y. (2017). Quantitative
fair simulation games. Information and Computation. Elsevier. https://doi.org/10.1016/j.ic.2016.10.006
chicago: Chatterjee, Krishnendu, Thomas A Henzinger, Jan Otop, and Yaron Velner.
“Quantitative Fair Simulation Games.” Information and Computation. Elsevier,
2017. https://doi.org/10.1016/j.ic.2016.10.006.
ieee: K. Chatterjee, T. A. Henzinger, J. Otop, and Y. Velner, “Quantitative fair
simulation games,” Information and Computation, vol. 254, no. 2. Elsevier,
pp. 143–166, 2017.
ista: Chatterjee K, Henzinger TA, Otop J, Velner Y. 2017. Quantitative fair simulation
games. Information and Computation. 254(2), 143–166.
mla: Chatterjee, Krishnendu, et al. “Quantitative Fair Simulation Games.” Information
and Computation, vol. 254, no. 2, Elsevier, 2017, pp. 143–66, doi:10.1016/j.ic.2016.10.006.
short: K. Chatterjee, T.A. Henzinger, J. Otop, Y. Velner, Information and Computation
254 (2017) 143–166.
date_created: 2018-12-11T11:49:58Z
date_published: 2017-06-01T00:00:00Z
date_updated: 2023-09-20T12:07:48Z
day: '01'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1016/j.ic.2016.10.006
ec_funded: 1
external_id:
isi:
- '000402025600002'
intvolume: ' 254'
isi: 1
issue: '2'
language:
- iso: eng
month: '06'
oa_version: None
page: 143 - 166
project:
- _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: 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: 2587B514-B435-11E9-9278-68D0E5697425
name: Microsoft Research Faculty Fellowship
publication: Information and Computation
publication_status: published
publisher: Elsevier
publist_id: '6322'
quality_controlled: '1'
related_material:
record:
- id: '5428'
relation: earlier_version
status: public
scopus_import: '1'
status: public
title: Quantitative fair simulation games
type: journal_article
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 254
year: '2017'
...
---
_id: '467'
abstract:
- lang: eng
text: Recently there has been a significant effort to handle 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, some basic system properties such as average
response time cannot be expressed using weighted automata or in any other known
decidable formalism. In this work, we introduce nested weighted automata as a
natural extension of weighted automata, which makes it possible to express important
quantitative properties such as average response time. In nested weighted automata,
a master automaton spins off and collects results from weighted slave automata,
each of which computes a quantity along a finite portion of an infinite word.
Nested weighted automata can be viewed as the quantitative analogue of monitor
automata, which are used in runtime verification. We establish an almost-complete
decidability picture for the basic decision problems about nested weighted automata
and illustrate their applicability in several domains. In particular, nested weighted
automata can be used to decide average response time properties.
article_number: '31'
arxiv: 1
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: 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. ACM Transactions
on Computational Logic (TOCL). 2017;18(4). doi:10.1145/3152769
apa: Chatterjee, K., Henzinger, T. A., & Otop, J. (2017). Nested weighted automata.
ACM Transactions on Computational Logic (TOCL). ACM. https://doi.org/10.1145/3152769
chicago: Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. “Nested Weighted
Automata.” ACM Transactions on Computational Logic (TOCL). ACM, 2017. https://doi.org/10.1145/3152769.
ieee: K. Chatterjee, T. A. Henzinger, and J. Otop, “Nested weighted automata,” ACM
Transactions on Computational Logic (TOCL), vol. 18, no. 4. ACM, 2017.
ista: Chatterjee K, Henzinger TA, Otop J. 2017. Nested weighted automata. ACM Transactions
on Computational Logic (TOCL). 18(4), 31.
mla: Chatterjee, Krishnendu, et al. “Nested Weighted Automata.” ACM Transactions
on Computational Logic (TOCL), vol. 18, no. 4, 31, ACM, 2017, doi:10.1145/3152769.
short: K. Chatterjee, T.A. Henzinger, J. Otop, ACM Transactions on Computational
Logic (TOCL) 18 (2017).
date_created: 2018-12-11T11:46:38Z
date_published: 2017-12-01T00:00:00Z
date_updated: 2023-02-23T12:26:19Z
day: '01'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1145/3152769
ec_funded: 1
external_id:
arxiv:
- '1606.03598'
intvolume: ' 18'
issue: '4'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1606.03598
month: '12'
oa: 1
oa_version: Preprint
project:
- _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: 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
publication: ACM Transactions on Computational Logic (TOCL)
publication_identifier:
issn:
- '15293785'
publication_status: published
publisher: ACM
publist_id: '7354'
quality_controlled: '1'
related_material:
record:
- id: '1656'
relation: earlier_version
status: public
- id: '5415'
relation: earlier_version
status: public
- id: '5436'
relation: earlier_version
status: public
scopus_import: 1
status: public
title: Nested weighted automata
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 18
year: '2017'
...
---
_id: '1196'
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. The 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;
robustness problems that measure how much a model can be perturbed without violating
the specification; and parameter synthesis for hybrid systems. We show that for
automatic distance functions, and (a) . ω-regular linear-time, (b) . ω-regular
branching-time, and (c) hybrid specifications, the model-measuring problem can
be solved.We use automata-theoretic model-checking methods for model measuring,
replacing the emptiness question for word, tree, and hybrid automata by the .
optimal-value question for the weighted versions of these automata. For automata
over words and trees, we consider weighted automata that accumulate weights by
maximizing, summing, discounting, and limit averaging. For hybrid automata, we
consider monotonic (parametric) hybrid automata, a hybrid counterpart of (discrete)
weighted automata.We give several examples of using the model-measuring problem
to compute various notions of robustness and quantitative satisfaction for temporal
specifications. Further, we propose the modeling framework for model measuring
to ease the specification and reduce the likelihood of errors in modeling.Finally,
we present a variant of the model-measuring problem, called the . model-repair
problem. The model-repair problem applies to models that do not satisfy the specification;
it can be used to derive restrictions, under which the model satisfies the specification,
i.e., to repair the model.'
acknowledgement: "This research was supported in part by the European Research Council
(ERC) under grant 267989 (QUAREM), by the Austrian Science Fund1 (FWF) under grants
S11402-N23 (RiSE) and Z211-N23 (Wittgenstein Award), and by the National Science
Centre (NCN), Poland under grant 2014/15/D/ST6/04543.\r\nA Technical Report of this
article is available via: https://repository.ist.ac.at/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 discrete and hybrid systems. Nonlinear
Analysis: Hybrid Systems. 2017;23:166-190. doi:10.1016/j.nahs.2016.09.001'
apa: 'Henzinger, T. A., & Otop, J. (2017). Model measuring for discrete and
hybrid systems. Nonlinear Analysis: Hybrid Systems. Elsevier. https://doi.org/10.1016/j.nahs.2016.09.001'
chicago: 'Henzinger, Thomas A, and Jan Otop. “Model Measuring for Discrete and Hybrid
Systems.” Nonlinear Analysis: Hybrid Systems. Elsevier, 2017. https://doi.org/10.1016/j.nahs.2016.09.001.'
ieee: 'T. A. Henzinger and J. Otop, “Model measuring for discrete and hybrid systems,”
Nonlinear Analysis: Hybrid Systems, vol. 23. Elsevier, pp. 166–190, 2017.'
ista: 'Henzinger TA, Otop J. 2017. Model measuring for discrete and hybrid systems.
Nonlinear Analysis: Hybrid Systems. 23, 166–190.'
mla: 'Henzinger, Thomas A., and Jan Otop. “Model Measuring for Discrete and Hybrid
Systems.” Nonlinear Analysis: Hybrid Systems, vol. 23, Elsevier, 2017,
pp. 166–90, doi:10.1016/j.nahs.2016.09.001.'
short: 'T.A. Henzinger, J. Otop, Nonlinear Analysis: Hybrid Systems 23 (2017) 166–190.'
date_created: 2018-12-11T11:50:39Z
date_published: 2017-02-01T00:00:00Z
date_updated: 2023-09-20T11:18:50Z
day: '01'
department:
- _id: ToHe
doi: 10.1016/j.nahs.2016.09.001
ec_funded: 1
external_id:
isi:
- '000390637000011'
intvolume: ' 23'
isi: 1
language:
- iso: eng
month: '02'
oa_version: None
page: 166 - 190
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: 'Nonlinear Analysis: Hybrid Systems'
publication_status: published
publisher: Elsevier
publist_id: '6154'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Model measuring for discrete and hybrid systems
type: journal_article
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 23
year: '2017'
...
---
_id: '1090'
abstract:
- lang: eng
text: ' While weighted automata provide a natural framework to express quantitative
properties, many basic properties like average response time cannot be expressed
with weighted automata. Nested weighted automata extend weighted automata and
consist of a master automaton and a set of slave automata that are invoked by
the master automaton. Nested weighted automata are strictly more expressive than
weighted automata (e.g., average response time can be expressed with nested weighted
automata), but the basic decision questions have higher complexity (e.g., for
deterministic automata, the emptiness question for nested weighted automata is
PSPACE-hard, whereas the corresponding complexity for weighted automata is PTIME).
We consider a natural subclass of nested weighted automata where at any point
at most a bounded number k of slave automata can be active. We focus on automata
whose master value function is the limit average. We show that these nested weighted
automata with bounded width are strictly more expressive than weighted automata
(e.g., average response time with no overlapping requests can be expressed with
bound k=1, but not with non-nested weighted automata). We show that the complexity
of the basic decision problems (i.e., emptiness and universality) for the subclass
with k constant matches the complexity for weighted automata. Moreover, when k
is part of the input given in unary we establish PSPACE-completeness.'
acknowledgement: "This research was supported in part by the Austrian Science Fund
(FWF) under grants S11402-N23\r\n(RiSE/SHiNE) and Z211-N23 (Wittgenstein Award),
ERC Start grant (279307: Graph Games), Vienna\r\nScience and Technology Fund (WWTF)
through project ICT15-003 and by the National Science Centre\r\n(NCN), Poland under
grant 2014/15/D/ST6/04543."
alternative_title:
- LIPIcs
article_number: '24'
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 limit-average automata
of bounded width. In: Vol 58. Schloss Dagstuhl - Leibniz-Zentrum für Informatik;
2016. doi:10.4230/LIPIcs.MFCS.2016.24'
apa: 'Chatterjee, K., Henzinger, T. A., & Otop, J. (2016). Nested weighted limit-average
automata of bounded width (Vol. 58). Presented at the MFCS: Mathematical Foundations
of Computer Science (SG), Krakow; Poland: Schloss Dagstuhl - Leibniz-Zentrum für
Informatik. https://doi.org/10.4230/LIPIcs.MFCS.2016.24'
chicago: Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. “Nested Weighted
Limit-Average Automata of Bounded Width,” Vol. 58. Schloss Dagstuhl - Leibniz-Zentrum
für Informatik, 2016. https://doi.org/10.4230/LIPIcs.MFCS.2016.24.
ieee: 'K. Chatterjee, T. A. Henzinger, and J. Otop, “Nested weighted limit-average
automata of bounded width,” presented at the MFCS: Mathematical Foundations of
Computer Science (SG), Krakow; Poland, 2016, vol. 58.'
ista: 'Chatterjee K, Henzinger TA, Otop J. 2016. Nested weighted limit-average automata
of bounded width. MFCS: Mathematical Foundations of Computer Science (SG), LIPIcs,
vol. 58, 24.'
mla: Chatterjee, Krishnendu, et al. Nested Weighted Limit-Average Automata of
Bounded Width. Vol. 58, 24, Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
2016, doi:10.4230/LIPIcs.MFCS.2016.24.
short: K. Chatterjee, T.A. Henzinger, J. Otop, in:, Schloss Dagstuhl - Leibniz-Zentrum
für Informatik, 2016.
conference:
end_date: 2016-08-26
location: Krakow; Poland
name: 'MFCS: Mathematical Foundations of Computer Science (SG)'
start_date: 2016-08-22
date_created: 2018-12-11T11:50:05Z
date_published: 2016-08-01T00:00:00Z
date_updated: 2021-01-12T06:48:12Z
day: '01'
ddc:
- '004'
department:
- _id: KrCh
- _id: ToHe
doi: 10.4230/LIPIcs.MFCS.2016.24
ec_funded: 1
file:
- access_level: open_access
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:17:31Z
date_updated: 2018-12-12T10:17:31Z
file_id: '5286'
file_name: IST-2017-795-v1+1_LIPIcs-MFCS-2016-24.pdf
file_size: 564560
relation: main_file
file_date_updated: 2018-12-12T10:17:31Z
has_accepted_license: '1'
intvolume: ' 58'
language:
- iso: eng
month: '08'
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: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 25892FC0-B435-11E9-9278-68D0E5697425
grant_number: ICT15-003
name: Efficient Algorithms for Computer Aided Verification
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '6286'
pubrep_id: '795'
quality_controlled: '1'
scopus_import: 1
status: public
title: Nested weighted limit-average automata of bounded width
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: 58
year: '2016'
...
---
_id: '1138'
abstract:
- lang: eng
text: Automata with monitor counters, where the transitions do not depend on counter
values, and nested weighted automata are two expressive automata-theoretic frameworks
for quantitative properties. For a well-studied and wide class of quantitative
functions, we establish that automata with monitor counters and nested weighted
automata are equivalent. We study for the first time such quantitative automata
under probabilistic semantics. We show that several problems that are undecidable
for the classical questions of emptiness and universality become decidable under
the probabilistic semantics. We present a complete picture of decidability for
such automata, and even an almost-complete picture of computational complexity,
for the probabilistic questions we consider. © 2016 ACM.
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 (Wittgenstein Award), FWF Grant No P23499-
N23, FWF NFN Grant No S114
arxiv: 1
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: 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. Quantitative automata under probabilistic
semantics. In: Proceedings of the 31st Annual ACM/IEEE Symposium. IEEE;
2016:76-85. doi:10.1145/2933575.2933588'
apa: 'Chatterjee, K., Henzinger, T. A., & Otop, J. (2016). Quantitative automata
under probabilistic semantics. In Proceedings of the 31st Annual ACM/IEEE Symposium
(pp. 76–85). New York, NY, USA: IEEE. https://doi.org/10.1145/2933575.2933588'
chicago: Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. “Quantitative
Automata under Probabilistic Semantics.” In Proceedings of the 31st Annual
ACM/IEEE Symposium, 76–85. IEEE, 2016. https://doi.org/10.1145/2933575.2933588.
ieee: K. Chatterjee, T. A. Henzinger, and J. Otop, “Quantitative automata under
probabilistic semantics,” in Proceedings of the 31st Annual ACM/IEEE Symposium,
New York, NY, USA, 2016, pp. 76–85.
ista: 'Chatterjee K, Henzinger TA, Otop J. 2016. Quantitative automata under probabilistic
semantics. Proceedings of the 31st Annual ACM/IEEE Symposium. LICS: Logic in Computer
Science, 76–85.'
mla: Chatterjee, Krishnendu, et al. “Quantitative Automata under Probabilistic Semantics.”
Proceedings of the 31st Annual ACM/IEEE Symposium, IEEE, 2016, pp. 76–85,
doi:10.1145/2933575.2933588.
short: K. Chatterjee, T.A. Henzinger, J. Otop, in:, Proceedings of the 31st Annual
ACM/IEEE Symposium, IEEE, 2016, pp. 76–85.
conference:
end_date: 2016-07-08
location: New York, NY, USA
name: 'LICS: Logic in Computer Science'
start_date: 2016-07-05
date_created: 2018-12-11T11:50:21Z
date_published: 2016-07-05T00:00:00Z
date_updated: 2021-01-12T06:48:34Z
day: '05'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1145/2933575.2933588
ec_funded: 1
external_id:
arxiv:
- '1604.06764'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1604.06764
month: '07'
oa: 1
oa_version: Preprint
page: 76 - 85
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: 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: 25892FC0-B435-11E9-9278-68D0E5697425
grant_number: ICT15-003
name: Efficient Algorithms for Computer Aided Verification
publication: Proceedings of the 31st Annual ACM/IEEE Symposium
publication_status: published
publisher: IEEE
publist_id: '6220'
quality_controlled: '1'
scopus_import: 1
status: public
title: Quantitative automata under probabilistic semantics
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2016'
...
---
_id: '1526'
abstract:
- lang: eng
text: 'We present the first study of robustness of systems that are both timed as
well as reactive (I/O). We study the behavior of such timed I/O systems in the
presence of uncertain inputs and formalize their robustness using the analytic
notion of Lipschitz continuity: a timed I/O system is K-(Lipschitz) robust if
the perturbation in its output is at most K times the perturbation in its input.
We quantify input and output perturbation using similarity functions over timed
words such as the timed version of the Manhattan distance and the Skorokhod distance.
We consider two models of timed I/O systems — timed transducers and asynchronous
sequential circuits. We show that K-robustness of timed transducers can be decided
in polynomial space under certain conditions. For asynchronous sequential circuits,
we reduce K-robustness w.r.t. timed Manhattan distances to K-robustness of discrete
letter-to-letter transducers and show PSpace-completeness of the problem.'
acknowledgement: This research was supported in part by the European Research Council
(ERC) under grant 267989 (QUAREM), by the Austrian Science Fund (FWF) under grants
S11402-N23 (RiSE) and Z211-N23 (Wittgenstein Award), and by the National Science
Centre (NCN), Poland under grant 2014/15/D/ST6/04543.
alternative_title:
- LNCS
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
- first_name: Roopsha
full_name: Samanta, Roopsha
id: 3D2AAC08-F248-11E8-B48F-1D18A9856A87
last_name: Samanta
citation:
ama: 'Henzinger TA, Otop J, Samanta R. Lipschitz robustness of timed I/O systems.
In: Vol 9583. Springer; 2016:250-267. doi:10.1007/978-3-662-49122-5_12'
apa: 'Henzinger, T. A., Otop, J., & Samanta, R. (2016). Lipschitz robustness
of timed I/O systems (Vol. 9583, pp. 250–267). 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_12'
chicago: Henzinger, Thomas A, Jan Otop, and Roopsha Samanta. “Lipschitz Robustness
of Timed I/O Systems,” 9583:250–67. Springer, 2016. https://doi.org/10.1007/978-3-662-49122-5_12.
ieee: 'T. A. Henzinger, J. Otop, and R. Samanta, “Lipschitz robustness of timed
I/O systems,” presented at the VMCAI: Verification, Model Checking and Abstract
Interpretation, St. Petersburg, FL, USA, 2016, vol. 9583, pp. 250–267.'
ista: 'Henzinger TA, Otop J, Samanta R. 2016. Lipschitz robustness of timed I/O
systems. VMCAI: Verification, Model Checking and Abstract Interpretation, LNCS,
vol. 9583, 250–267.'
mla: Henzinger, Thomas A., et al. Lipschitz Robustness of Timed I/O Systems.
Vol. 9583, Springer, 2016, pp. 250–67, doi:10.1007/978-3-662-49122-5_12.
short: T.A. Henzinger, J. Otop, R. Samanta, in:, Springer, 2016, pp. 250–267.
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:52:32Z
date_published: 2016-01-01T00:00:00Z
date_updated: 2021-01-12T06:51:23Z
day: '01'
department:
- _id: ToHe
doi: 10.1007/978-3-662-49122-5_12
ec_funded: 1
intvolume: ' 9583'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1506.01233
month: '01'
oa: 1
oa_version: Preprint
page: 250 - 267
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: '5647'
quality_controlled: '1'
scopus_import: 1
status: public
title: Lipschitz robustness of timed I/O systems
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 9583
year: '2016'
...
---
_id: '1335'
abstract:
- lang: eng
text: In this paper we review various automata-theoretic formalisms for expressing
quantitative properties. We start with finite-state Boolean automata that express
the traditional regular properties. We then consider weighted ω-automata that
can measure the average density of events, which finite-state Boolean automata
cannot. However, even weighted ω-automata cannot express basic performance properties
like average response time. We finally consider two formalisms of weighted ω-automata
with monitors, where the monitors are either (a) counters or (b) weighted automata
themselves. We present a translation result to establish that these two formalisms
are equivalent. Weighted ω-automata with monitors generalize weighted ω-automata,
and can express average response time property. They present a natural, robust,
and expressive framework for quantitative specifications, with important decidable
properties.
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: 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. Quantitative monitor automata. In: Vol
9837. Springer; 2016:23-38. doi:10.1007/978-3-662-53413-7_2'
apa: 'Chatterjee, K., Henzinger, T. A., & Otop, J. (2016). Quantitative monitor
automata (Vol. 9837, pp. 23–38). Presented at the SAS: Static Analysis Symposium,
Edinburgh, United Kingdom: Springer. https://doi.org/10.1007/978-3-662-53413-7_2'
chicago: Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. “Quantitative
Monitor Automata,” 9837:23–38. Springer, 2016. https://doi.org/10.1007/978-3-662-53413-7_2.
ieee: 'K. Chatterjee, T. A. Henzinger, and J. Otop, “Quantitative monitor automata,”
presented at the SAS: Static Analysis Symposium, Edinburgh, United Kingdom, 2016,
vol. 9837, pp. 23–38.'
ista: 'Chatterjee K, Henzinger TA, Otop J. 2016. Quantitative monitor automata.
SAS: Static Analysis Symposium, LNCS, vol. 9837, 23–38.'
mla: Chatterjee, Krishnendu, et al. Quantitative Monitor Automata. Vol. 9837,
Springer, 2016, pp. 23–38, doi:10.1007/978-3-662-53413-7_2.
short: K. Chatterjee, T.A. Henzinger, J. Otop, in:, Springer, 2016, pp. 23–38.
conference:
end_date: 2016-09-10
location: Edinburgh, United Kingdom
name: 'SAS: Static Analysis Symposium'
start_date: 2016-09-08
date_created: 2018-12-11T11:51:26Z
date_published: 2016-08-31T00:00:00Z
date_updated: 2021-01-12T06:49:58Z
day: '31'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1007/978-3-662-53413-7_2
ec_funded: 1
intvolume: ' 9837'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1604.06764
month: '08'
oa: 1
oa_version: Preprint
page: 23 - 38
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 25892FC0-B435-11E9-9278-68D0E5697425
grant_number: ICT15-003
name: Efficient Algorithms for Computer Aided Verification
publication_status: published
publisher: Springer
publist_id: '5932'
quality_controlled: '1'
scopus_import: 1
status: public
title: Quantitative monitor automata
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 9837
year: '2016'
...
---
_id: '1656'
abstract:
- lang: eng
text: Recently there has been a significant effort to handle 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, some basic system properties such as average
response time cannot be expressed using weighted automata, nor in any other know
decidable formalism. In this work, we introduce nested weighted automata as a
natural extension of weighted automata which makes it possible to express important
quantitative properties such as average response time. In nested weighted automata,
a master automaton spins off and collects results from weighted slave automata,
each of which computes a quantity along a finite portion of an infinite word.
Nested weighted automata can be viewed as the quantitative analogue of monitor
automata, which are used in run-time verification. We establish an almost complete
decidability picture for the basic decision problems about nested weighted automata,
and illustrate their applicability in several domains. In particular, nested weighted
automata can be used to decide average response time properties.
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), Z211-N23 (Wittgenstein Award), FWF Grant No P23499-
N23, FWF NFN Grant No S11407-N23 (RiSE), ERC Start grant (279307: Graph Games),
and Microsoft faculty fellows award.\r\nA Technical Report of the paper is available
at: \r\nhttps://repository.ist.ac.at/331/\r\n"
article_number: '7174926'
arxiv: 1
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: 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. In: Proceedings
- Symposium on Logic in Computer Science. Vol 2015-July. IEEE; 2015. doi:10.1109/LICS.2015.72'
apa: 'Chatterjee, K., Henzinger, T. A., & Otop, J. (2015). Nested weighted automata.
In Proceedings - Symposium on Logic in Computer Science (Vol. 2015–July).
Kyoto, Japan: IEEE. https://doi.org/10.1109/LICS.2015.72'
chicago: Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. “Nested Weighted
Automata.” In Proceedings - Symposium on Logic in Computer Science, Vol.
2015–July. IEEE, 2015. https://doi.org/10.1109/LICS.2015.72.
ieee: K. Chatterjee, T. A. Henzinger, and J. Otop, “Nested weighted automata,” in
Proceedings - Symposium on Logic in Computer Science, Kyoto, Japan, 2015,
vol. 2015–July.
ista: 'Chatterjee K, Henzinger TA, Otop J. 2015. Nested weighted automata. Proceedings
- Symposium on Logic in Computer Science. LICS: Logic in Computer Science vol.
2015–July, 7174926.'
mla: Chatterjee, Krishnendu, et al. “Nested Weighted Automata.” Proceedings -
Symposium on Logic in Computer Science, vol. 2015–July, 7174926, IEEE, 2015,
doi:10.1109/LICS.2015.72.
short: K. Chatterjee, T.A. Henzinger, J. Otop, in:, Proceedings - Symposium on Logic
in Computer Science, IEEE, 2015.
conference:
end_date: 2015-07-10
location: Kyoto, Japan
name: 'LICS: Logic in Computer Science'
start_date: 2015-07-06
date_created: 2018-12-11T11:53:17Z
date_published: 2015-07-31T00:00:00Z
date_updated: 2023-02-23T12:26:19Z
day: '31'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1109/LICS.2015.72
ec_funded: 1
external_id:
arxiv:
- '1606.03598'
language:
- iso: eng
month: '07'
oa_version: None
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: 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
publication: Proceedings - Symposium on Logic in Computer Science
publication_status: published
publisher: IEEE
publist_id: '5494'
quality_controlled: '1'
related_material:
record:
- id: '467'
relation: later_version
status: public
- id: '5415'
relation: earlier_version
status: public
- id: '5436'
relation: earlier_version
status: public
scopus_import: 1
status: public
title: Nested weighted automata
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 2015-July
year: '2015'
...
---
_id: '1659'
abstract:
- lang: eng
text: 'The target discounted-sum problem is the following: Given a rational discount
factor 0 < λ < 1 and three rational values a, b, and t, does there exist
a finite or an infinite sequence w ε(a, b)∗ or w ε(a, b)w, such that Σ|w| i=0
w(i)λi equals t? The problem turns out to relate to many fields of mathematics
and computer science, and its decidability question is surprisingly hard to solve.
We solve the finite version of the problem, and show the hardness of the infinite
version, linking it to various areas and open problems in mathematics and computer
science: β-expansions, discounted-sum automata, piecewise affine maps, and generalizations
of the Cantor set. We provide some partial results to the infinite version, among
which are solutions to its restriction to eventually-periodic sequences and to
the cases that λ λ 1/2 or λ = 1/n, for every n ε N. We use our results for solving
some open problems on discounted-sum automata, among which are the exact-value
problem for nondeterministic automata over finite words and the universality and
inclusion problems for functional automata.'
acknowledgement: 'A technical report of the article is available at: https://research-explorer.app.ist.ac.at/record/5439'
article_processing_charge: No
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: Jan
full_name: Otop, Jan
id: 2FC5DA74-F248-11E8-B48F-1D18A9856A87
last_name: Otop
citation:
ama: 'Boker U, Henzinger TA, Otop J. The target discounted-sum problem. In: LICS.
Logic in Computer Science. IEEE; 2015:750-761. doi:10.1109/LICS.2015.74'
apa: 'Boker, U., Henzinger, T. A., & Otop, J. (2015). The target discounted-sum
problem. In LICS (pp. 750–761). Kyoto, Japan: IEEE. https://doi.org/10.1109/LICS.2015.74'
chicago: Boker, Udi, Thomas A Henzinger, and Jan Otop. “The Target Discounted-Sum
Problem.” In LICS, 750–61. Logic in Computer Science. IEEE, 2015. https://doi.org/10.1109/LICS.2015.74.
ieee: U. Boker, T. A. Henzinger, and J. Otop, “The target discounted-sum problem,”
in LICS, Kyoto, Japan, 2015, pp. 750–761.
ista: 'Boker U, Henzinger TA, Otop J. 2015. The target discounted-sum problem. LICS.
LICS: Logic in Computer ScienceLogic in Computer Science, 750–761.'
mla: Boker, Udi, et al. “The Target Discounted-Sum Problem.” LICS, IEEE,
2015, pp. 750–61, doi:10.1109/LICS.2015.74.
short: U. Boker, T.A. Henzinger, J. Otop, in:, LICS, IEEE, 2015, pp. 750–761.
conference:
end_date: 2015-07-10
location: Kyoto, Japan
name: 'LICS: Logic in Computer Science'
start_date: 2015-007-06
date_created: 2018-12-11T11:53:19Z
date_published: 2015-07-01T00:00:00Z
date_updated: 2023-02-23T12:26:27Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1109/LICS.2015.74
ec_funded: 1
file:
- access_level: open_access
checksum: 6abebca9c1a620e9e103a8f9222befac
content_type: application/pdf
creator: dernst
date_created: 2020-05-15T08:53:29Z
date_updated: 2020-07-14T12:45:10Z
file_id: '7852'
file_name: 2015_LICS_Boker.pdf
file_size: 340215
relation: main_file
file_date_updated: 2020-07-14T12:45:10Z
has_accepted_license: '1'
language:
- iso: eng
month: '07'
oa: 1
oa_version: Submitted Version
page: 750 - 761
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: LICS
publication_identifier:
eisbn:
- '978-1-4799-8875-4 '
issn:
- '1043-6871 '
publication_status: published
publisher: IEEE
publist_id: '5491'
quality_controlled: '1'
related_material:
record:
- id: '5439'
relation: earlier_version
status: public
scopus_import: 1
series_title: Logic in Computer Science
status: public
title: The target discounted-sum problem
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2015'
...
---
_id: '1680'
abstract:
- lang: eng
text: We consider the satisfiability problem for modal logic over first-order definable
classes of frames.We confirm the conjecture from Hemaspaandra and Schnoor [2008]
that modal logic is decidable over classes definable by universal Horn formulae.
We provide a full classification of Horn formulae with respect to the complexity
of the corresponding satisfiability problem. It turns out, that except for the
trivial case of inconsistent formulae, local satisfiability is eitherNP-complete
or PSPACE-complete, and global satisfiability is NP-complete, PSPACE-complete,
or ExpTime-complete. We also show that the finite satisfiability problem for modal
logic over Horn definable classes of frames is decidable. On the negative side,
we show undecidability of two related problems. First, we exhibit a simple universal
three-variable formula defining the class of frames over which modal logic is
undecidable. Second, we consider the satisfiability problem of bimodal logic over
Horn definable classes of frames, and also present a formula leading to undecidability.
article_number: '2'
author:
- first_name: Jakub
full_name: Michaliszyn, Jakub
last_name: Michaliszyn
- first_name: Jan
full_name: Otop, Jan
id: 2FC5DA74-F248-11E8-B48F-1D18A9856A87
last_name: Otop
- first_name: Emanuel
full_name: Kieroňski, Emanuel
last_name: Kieroňski
citation:
ama: Michaliszyn J, Otop J, Kieroňski E. On the decidability of elementary modal
logics. ACM Transactions on Computational Logic. 2015;17(1). doi:10.1145/2817825
apa: Michaliszyn, J., Otop, J., & Kieroňski, E. (2015). On the decidability
of elementary modal logics. ACM Transactions on Computational Logic. ACM.
https://doi.org/10.1145/2817825
chicago: Michaliszyn, Jakub, Jan Otop, and Emanuel Kieroňski. “On the Decidability
of Elementary Modal Logics.” ACM Transactions on Computational Logic. ACM,
2015. https://doi.org/10.1145/2817825.
ieee: J. Michaliszyn, J. Otop, and E. Kieroňski, “On the decidability of elementary
modal logics,” ACM Transactions on Computational Logic, vol. 17, no. 1.
ACM, 2015.
ista: Michaliszyn J, Otop J, Kieroňski E. 2015. On the decidability of elementary
modal logics. ACM Transactions on Computational Logic. 17(1), 2.
mla: Michaliszyn, Jakub, et al. “On the Decidability of Elementary Modal Logics.”
ACM Transactions on Computational Logic, vol. 17, no. 1, 2, ACM, 2015,
doi:10.1145/2817825.
short: J. Michaliszyn, J. Otop, E. Kieroňski, ACM Transactions on Computational
Logic 17 (2015).
date_created: 2018-12-11T11:53:26Z
date_published: 2015-09-01T00:00:00Z
date_updated: 2021-01-12T06:52:29Z
day: '01'
department:
- _id: ToHe
doi: 10.1145/2817825
ec_funded: 1
intvolume: ' 17'
issue: '1'
language:
- iso: eng
month: '09'
oa_version: None
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: ACM Transactions on Computational Logic
publication_status: published
publisher: ACM
publist_id: '5468'
quality_controlled: '1'
status: public
title: On the decidability of elementary modal logics
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 17
year: '2015'
...
---
_id: '5436'
abstract:
- lang: eng
text: "Recently there has been a significant effort to handle 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, some basic system properties such as average
response time cannot be expressed using weighted automata, nor in any other know
decidable formalism. In this work, we introduce nested weighted automata as a
natural extension of weighted automata which makes it possible to express important
quantitative properties such as average response time.\r\nIn nested weighted automata,
a master automaton spins off and collects results from weighted slave automata,
each of which computes a quantity along a finite portion of an infinite word.
Nested weighted automata can be viewed as the quantitative analogue of monitor
automata, which are used in run-time verification. We establish an almost complete
decidability picture for the basic decision problems about nested weighted automata,
and illustrate their applicability in several domains. In particular, nested weighted
automata can be used to decide average response time properties."
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;
2015. doi:10.15479/AT:IST-2015-170-v2-2
apa: Chatterjee, K., Henzinger, T. A., & Otop, J. (2015). Nested weighted
automata. IST Austria. https://doi.org/10.15479/AT:IST-2015-170-v2-2
chicago: Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. Nested Weighted
Automata. IST Austria, 2015. https://doi.org/10.15479/AT:IST-2015-170-v2-2.
ieee: K. Chatterjee, T. A. Henzinger, and J. Otop, Nested weighted automata.
IST Austria, 2015.
ista: Chatterjee K, Henzinger TA, Otop J. 2015. Nested weighted automata, IST Austria,
29p.
mla: Chatterjee, Krishnendu, et al. Nested Weighted Automata. IST Austria,
2015, doi:10.15479/AT:IST-2015-170-v2-2.
short: K. Chatterjee, T.A. Henzinger, J. Otop, Nested Weighted Automata, IST Austria,
2015.
date_created: 2018-12-12T11:39:19Z
date_published: 2015-04-24T00:00:00Z
date_updated: 2023-02-23T12:25:21Z
day: '24'
ddc:
- '000'
department:
- _id: KrCh
- _id: ToHe
doi: 10.15479/AT:IST-2015-170-v2-2
file:
- access_level: open_access
checksum: 3c402f47d3669c28d04d1af405a08e3f
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:54:19Z
date_updated: 2020-07-14T12:46:54Z
file_id: '5541'
file_name: IST-2015-170-v2+2_report.pdf
file_size: 569991
relation: main_file
file_date_updated: 2020-07-14T12:46:54Z
has_accepted_license: '1'
language:
- iso: eng
month: '04'
oa: 1
oa_version: Published Version
page: '29'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '331'
related_material:
record:
- id: '1656'
relation: later_version
status: public
- id: '467'
relation: later_version
status: public
- id: '5415'
relation: earlier_version
status: public
status: public
title: Nested weighted automata
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2015'
...
---
_id: '5438'
abstract:
- lang: eng
text: "The edit distance between two words w1, w2 is the minimal number of word
operations (letter insertions, deletions, and substitutions) necessary to transform
w1 to w2. The edit distance generalizes to languages L1, L2, where the edit distance
is the minimal number k such that for every word from L1 there exists a word in
L2 with edit distance at most k. We study the edit distance computation problem
between pushdown automata and their subclasses.\r\nThe problem of computing edit
distance to a pushdown automaton is undecidable, and in practice, the interesting
question is to compute the edit distance from a pushdown automaton (the implementation,
a standard model for programs with recursion) to a regular language (the specification).
In this work, we present a complete picture of decidability and complexity for
deciding whether, for a given threshold k, the edit distance from a pushdown automaton
to a finite automaton is at most k. "
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: Rasmus
full_name: Ibsen-Jensen, Rasmus
id: 3B699956-F248-11E8-B48F-1D18A9856A87
last_name: Ibsen-Jensen
orcid: 0000-0003-4783-0389
- first_name: Jan
full_name: Otop, Jan
id: 2FC5DA74-F248-11E8-B48F-1D18A9856A87
last_name: Otop
citation:
ama: Chatterjee K, Henzinger TA, Ibsen-Jensen R, Otop J. Edit Distance for Pushdown
Automata. IST Austria; 2015. doi:10.15479/AT:IST-2015-334-v1-1
apa: Chatterjee, K., Henzinger, T. A., Ibsen-Jensen, R., & Otop, J. (2015).
Edit distance for pushdown automata. IST Austria. https://doi.org/10.15479/AT:IST-2015-334-v1-1
chicago: Chatterjee, Krishnendu, Thomas A Henzinger, Rasmus Ibsen-Jensen, and Jan
Otop. Edit Distance for Pushdown Automata. IST Austria, 2015. https://doi.org/10.15479/AT:IST-2015-334-v1-1.
ieee: K. Chatterjee, T. A. Henzinger, R. Ibsen-Jensen, and J. Otop, Edit distance
for pushdown automata. IST Austria, 2015.
ista: Chatterjee K, Henzinger TA, Ibsen-Jensen R, Otop J. 2015. Edit distance for
pushdown automata, IST Austria, 15p.
mla: Chatterjee, Krishnendu, et al. Edit Distance for Pushdown Automata.
IST Austria, 2015, doi:10.15479/AT:IST-2015-334-v1-1.
short: K. Chatterjee, T.A. Henzinger, R. Ibsen-Jensen, J. Otop, Edit Distance for
Pushdown Automata, IST Austria, 2015.
date_created: 2018-12-12T11:39:20Z
date_published: 2015-05-05T00:00:00Z
date_updated: 2023-02-23T12:20:08Z
day: '05'
ddc:
- '004'
department:
- _id: KrCh
doi: 10.15479/AT:IST-2015-334-v1-1
file:
- access_level: open_access
checksum: 8a5f2d77560e552af87eb1982437a43b
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:53:56Z
date_updated: 2020-07-14T12:46:55Z
file_id: '5518'
file_name: IST-2015-334-v1+1_report.pdf
file_size: 422573
relation: main_file
file_date_updated: 2020-07-14T12:46:55Z
has_accepted_license: '1'
language:
- iso: eng
month: '05'
oa: 1
oa_version: Published Version
page: '15'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '334'
related_material:
record:
- id: '1610'
relation: later_version
status: public
- id: '465'
relation: later_version
status: public
status: public
title: Edit distance for pushdown automata
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2015'
...
---
_id: '5439'
abstract:
- lang: eng
text: 'The target discounted-sum problem is the following: Given a rational discount
factor 0 < λ < 1 and three rational values a, b, and t, does there exist a finite
or an infinite sequence w ε(a, b)∗ or w ε(a, b)w, such that Σ|w| i=0 w(i)λi equals
t? The problem turns out to relate to many fields of mathematics and computer
science, and its decidability question is surprisingly hard to solve. We solve
the finite version of the problem, and show the hardness of the infinite version,
linking it to various areas and open problems in mathematics and computer science:
β-expansions, discounted-sum automata, piecewise affine maps, and generalizations
of the Cantor set. We provide some partial results to the infinite version, among
which are solutions to its restriction to eventually-periodic sequences and to
the cases that λ λ 1/2 or λ = 1/n, for every n ε N. We use our results for solving
some open problems on discounted-sum automata, among which are the exact-value
problem for nondeterministic automata over finite words and the universality and
inclusion problems for functional automata. '
alternative_title:
- IST Austria Technical Report
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: Jan
full_name: Otop, Jan
id: 2FC5DA74-F248-11E8-B48F-1D18A9856A87
last_name: Otop
citation:
ama: Boker U, Henzinger TA, Otop J. The Target Discounted-Sum Problem. IST
Austria; 2015. doi:10.15479/AT:IST-2015-335-v1-1
apa: Boker, U., Henzinger, T. A., & Otop, J. (2015). The target discounted-sum
problem. IST Austria. https://doi.org/10.15479/AT:IST-2015-335-v1-1
chicago: Boker, Udi, Thomas A Henzinger, and Jan Otop. The Target Discounted-Sum
Problem. IST Austria, 2015. https://doi.org/10.15479/AT:IST-2015-335-v1-1.
ieee: U. Boker, T. A. Henzinger, and J. Otop, The target discounted-sum problem.
IST Austria, 2015.
ista: Boker U, Henzinger TA, Otop J. 2015. The target discounted-sum problem, IST
Austria, 20p.
mla: Boker, Udi, et al. The Target Discounted-Sum Problem. IST Austria, 2015,
doi:10.15479/AT:IST-2015-335-v1-1.
short: U. Boker, T.A. Henzinger, J. Otop, The Target Discounted-Sum Problem, IST
Austria, 2015.
date_created: 2018-12-12T11:39:20Z
date_published: 2015-05-18T00:00:00Z
date_updated: 2023-02-23T10:08:48Z
day: '18'
ddc:
- '004'
- '512'
- '513'
department:
- _id: ToHe
doi: 10.15479/AT:IST-2015-335-v1-1
file:
- access_level: open_access
checksum: 40405907aa012acece1bc26cf0be554d
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:53:55Z
date_updated: 2020-07-14T12:46:55Z
file_id: '5517'
file_name: IST-2015-335-v1+1_report.pdf
file_size: 589619
relation: main_file
file_date_updated: 2020-07-14T12:46:55Z
has_accepted_license: '1'
language:
- iso: eng
month: '05'
oa: 1
oa_version: Published Version
page: '20'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '335'
related_material:
record:
- id: '1659'
relation: later_version
status: public
status: public
title: The target discounted-sum problem
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2015'
...
---
_id: '1610'
abstract:
- lang: eng
text: The edit distance between two words w1, w2 is the minimal number of word operations
(letter insertions, deletions, and substitutions) necessary to transform w1 to
w2. The edit distance generalizes to languages L1,L2, where the edit distance
is the minimal number k such that for every word from L1 there exists a word in
L2 with edit distance at most k. We study the edit distance computation problem
between pushdown automata and their subclasses. The problem of computing edit
distance to pushdown automata is undecidable, and in practice, the interesting
question is to compute the edit distance from a pushdown automaton (the implementation,
a standard model for programs with recursion) to a regular language (the specification).
In this work, we present a complete picture of decidability and complexity for
deciding whether, for a given threshold k, the edit distance from a pushdown automaton
to a finite automaton is at most k.
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Rasmus
full_name: Ibsen-Jensen, Rasmus
id: 3B699956-F248-11E8-B48F-1D18A9856A87
last_name: Ibsen-Jensen
orcid: 0000-0003-4783-0389
- first_name: Jan
full_name: Otop, Jan
id: 2FC5DA74-F248-11E8-B48F-1D18A9856A87
last_name: Otop
citation:
ama: 'Chatterjee K, Henzinger TA, Ibsen-Jensen R, Otop J. Edit distance for pushdown
automata. In: 42nd International Colloquium. Vol 9135. Springer Nature;
2015:121-133. doi:10.1007/978-3-662-47666-6_10'
apa: 'Chatterjee, K., Henzinger, T. A., Ibsen-Jensen, R., & Otop, J. (2015).
Edit distance for pushdown automata. In 42nd International Colloquium (Vol.
9135, pp. 121–133). Kyoto, Japan: Springer Nature. https://doi.org/10.1007/978-3-662-47666-6_10'
chicago: Chatterjee, Krishnendu, Thomas A Henzinger, Rasmus Ibsen-Jensen, and Jan
Otop. “Edit Distance for Pushdown Automata.” In 42nd International Colloquium,
9135:121–33. Springer Nature, 2015. https://doi.org/10.1007/978-3-662-47666-6_10.
ieee: K. Chatterjee, T. A. Henzinger, R. Ibsen-Jensen, and J. Otop, “Edit distance
for pushdown automata,” in 42nd International Colloquium, Kyoto, Japan,
2015, vol. 9135, no. Part II, pp. 121–133.
ista: 'Chatterjee K, Henzinger TA, Ibsen-Jensen R, Otop J. 2015. Edit distance for
pushdown automata. 42nd International Colloquium. ICALP: Automata, Languages and
Programming, LNCS, vol. 9135, 121–133.'
mla: Chatterjee, Krishnendu, et al. “Edit Distance for Pushdown Automata.” 42nd
International Colloquium, vol. 9135, no. Part II, Springer Nature, 2015, pp.
121–33, doi:10.1007/978-3-662-47666-6_10.
short: K. Chatterjee, T.A. Henzinger, R. Ibsen-Jensen, J. Otop, in:, 42nd International
Colloquium, Springer Nature, 2015, pp. 121–133.
conference:
end_date: 2015-07-10
location: Kyoto, Japan
name: 'ICALP: Automata, Languages and Programming'
start_date: 2015-07-06
date_created: 2018-12-11T11:53:01Z
date_published: 2015-07-01T00:00:00Z
date_updated: 2023-02-23T12:26:24Z
day: '01'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1007/978-3-662-47666-6_10
ec_funded: 1
external_id:
arxiv:
- '1504.08259'
intvolume: ' 9135'
issue: Part II
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1504.08259
month: '07'
oa: 1
oa_version: None
page: 121 - 133
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: 2584A770-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: P 23499-N23
name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11407
name: Game Theory
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 2587B514-B435-11E9-9278-68D0E5697425
name: Microsoft Research Faculty Fellowship
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
publication: 42nd International Colloquium
publication_identifier:
isbn:
- 978-3-662-47665-9
publication_status: published
publisher: Springer Nature
publist_id: '5556'
pubrep_id: '321'
quality_controlled: '1'
related_material:
record:
- id: '465'
relation: later_version
status: public
- id: '5438'
relation: earlier_version
status: public
scopus_import: '1'
status: public
title: Edit distance for pushdown automata
type: conference
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
volume: 9135
year: '2015'
...
---
_id: '1870'
abstract:
- lang: eng
text: We investigate the problem of checking if a finite-state transducer is robust
to uncertainty in its input. Our notion of robustness is based on the analytic
notion of Lipschitz continuity - a transducer is K-(Lipschitz) robust if the perturbation
in its output is at most K times the perturbation in its input. We quantify input
and output perturbation using similarity functions. We show that K-robustness
is undecidable even for deterministic transducers. We identify a class of functional
transducers, which admits a polynomial time automata-theoretic decision procedure
for K-robustness. This class includes Mealy machines and functional letter-to-letter
transducers. We also study K-robustness of nondeterministic transducers. Since
a nondeterministic transducer generates a set of output words for each input word,
we quantify output perturbation using setsimilarity functions. We show that K-robustness
of nondeterministic transducers is undecidable, even for letter-to-letter transducers.
We identify a class of set-similarity functions which admit decidable K-robustness
of letter-to-letter transducers.
alternative_title:
- LIPIcs
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
- first_name: Roopsha
full_name: Samanta, Roopsha
id: 3D2AAC08-F248-11E8-B48F-1D18A9856A87
last_name: Samanta
citation:
ama: 'Henzinger TA, Otop J, Samanta R. Lipschitz robustness of finite-state transducers.
In: Leibniz International Proceedings in Informatics, LIPIcs. Vol 29. Schloss
Dagstuhl - Leibniz-Zentrum für Informatik; 2014:431-443. doi:10.4230/LIPIcs.FSTTCS.2014.431'
apa: 'Henzinger, T. A., Otop, J., & Samanta, R. (2014). Lipschitz robustness
of finite-state transducers. In Leibniz International Proceedings in Informatics,
LIPIcs (Vol. 29, pp. 431–443). Delhi, India: Schloss Dagstuhl - Leibniz-Zentrum
für Informatik. https://doi.org/10.4230/LIPIcs.FSTTCS.2014.431'
chicago: Henzinger, Thomas A, Jan Otop, and Roopsha Samanta. “Lipschitz Robustness
of Finite-State Transducers.” In Leibniz International Proceedings in Informatics,
LIPIcs, 29:431–43. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2014.
https://doi.org/10.4230/LIPIcs.FSTTCS.2014.431.
ieee: T. A. Henzinger, J. Otop, and R. Samanta, “Lipschitz robustness of finite-state
transducers,” in Leibniz International Proceedings in Informatics, LIPIcs,
Delhi, India, 2014, vol. 29, pp. 431–443.
ista: 'Henzinger TA, Otop J, Samanta R. 2014. Lipschitz robustness of finite-state
transducers. Leibniz International Proceedings in Informatics, LIPIcs. FSTTCS:
Foundations of Software Technology and Theoretical Computer Science, LIPIcs, vol.
29, 431–443.'
mla: Henzinger, Thomas A., et al. “Lipschitz Robustness of Finite-State Transducers.”
Leibniz International Proceedings in Informatics, LIPIcs, vol. 29, Schloss
Dagstuhl - Leibniz-Zentrum für Informatik, 2014, pp. 431–43, doi:10.4230/LIPIcs.FSTTCS.2014.431.
short: T.A. Henzinger, J. Otop, R. Samanta, in:, Leibniz International Proceedings
in Informatics, LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2014,
pp. 431–443.
conference:
end_date: 2014-12-17
location: Delhi, India
name: 'FSTTCS: Foundations of Software Technology and Theoretical Computer Science'
start_date: 2014-12-15
date_created: 2018-12-11T11:54:27Z
date_published: 2014-12-01T00:00:00Z
date_updated: 2021-01-12T06:53:45Z
day: '01'
ddc:
- '004'
department:
- _id: ToHe
doi: 10.4230/LIPIcs.FSTTCS.2014.431
file:
- access_level: open_access
checksum: 7b1aff1710a8bffb7080ec07f62d9a17
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:09:11Z
date_updated: 2020-07-14T12:45:19Z
file_id: '4734'
file_name: IST-2017-804-v1+1_37.pdf
file_size: 562151
relation: main_file
file_date_updated: 2020-07-14T12:45:19Z
has_accepted_license: '1'
intvolume: ' 29'
language:
- iso: eng
month: '12'
oa: 1
oa_version: Published Version
page: 431 - 443
publication: Leibniz International Proceedings in Informatics, LIPIcs
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '5227'
pubrep_id: '804'
quality_controlled: '1'
status: public
title: Lipschitz robustness of finite-state transducers
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: 4435EBFC-F248-11E8-B48F-1D18A9856A87
volume: 29
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: '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'
...