---
_id: '3360'
abstract:
- lang: eng
text: 'A discounted-sum automaton (NDA) is a nondeterministic finite automaton with
edge weights, which values 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 lambda^i,
where the discount factor lambda is a fixed rational number greater than 1. Discounted
summation is a common and useful measuring scheme, especially for infinite sequences,
which reflects the assumption that earlier weights are more important than later
weights. Determinizing automata is often essential, for example, in formal verification,
where there are polynomial algorithms for comparing two deterministic NDAs, while
the equivalence problem for NDAs is not known to be decidable. Unfortunately,
however, discounted-sum automata are, in general, not determinizable: it is currently
known that for every rational discount factor 1 < lambda < 2, there is an
NDA with lambda (denoted lambda-NDA) that cannot be determinized. We provide positive
news, showing that every NDA with an integral factor is determinizable. We also
complete the picture by proving that the integers characterize exactly the discount
factors that guarantee determinizability: we show that for every non-integral
rational factor lambda, there is a nondeterminizable lambda-NDA. Finally, we 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. This shows that for integral discount
factors, the class of NDAs forms an attractive specification formalism in quantitative
formal verification. All our results hold equally for automata over finite words
and for automata over infinite words. '
accept: '1'
alternative_title:
- LIPIcs
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
cc_license: '''https://creativecommons.org/licenses/by-nc-nd/4.0/'''
citation:
ama: 'Boker U, Henzinger TA. Determinizing discounted-sum automata. In: Vol 12.
Springer; 2011:82-96. doi:10.4230/LIPIcs.CSL.2011.82'
apa: 'Boker, U., & Henzinger, T. A. (2011). Determinizing discounted-sum automata
(Vol. 12, pp. 82–96). Presented at the CSL: Computer Science Logic, Bergen, Norway:
Springer. https://doi.org/10.4230/LIPIcs.CSL.2011.82'
chicago: Boker, Udi, and Thomas A Henzinger. “Determinizing Discounted-Sum Automata,”
12:82–96. Springer, 2011. https://doi.org/10.4230/LIPIcs.CSL.2011.82.
ieee: 'U. Boker and T. A. Henzinger, “Determinizing discounted-sum automata,” presented
at the CSL: Computer Science Logic, Bergen, Norway, 2011, vol. 12, pp. 82–96.'
ista: 'Boker U, Henzinger TA. 2011. Determinizing discounted-sum automata. CSL:
Computer Science Logic, LIPIcs, vol. 12. 82–96.'
mla: Boker, Udi, and Thomas A. Henzinger. *Determinizing Discounted-Sum Automata*.
Vol. 12, Springer, 2011, pp. 82–96, doi:10.4230/LIPIcs.CSL.2011.82.
short: U. Boker, T.A. Henzinger, in:, Springer, 2011, pp. 82–96.
conference:
end_date: 2011-09-15
location: Bergen, Norway
name: 'CSL: Computer Science Logic'
start_date: 2011-09-12
date_created: 2018-12-11T12:02:53Z
date_published: 2011-08-31T00:00:00Z
date_updated: 2020-01-21T13:20:22Z
day: '31'
ddc:
- '004'
department:
- _id: ToHe
doi: 10.4230/LIPIcs.CSL.2011.82
file:
- access_level: open_access
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:10:17Z
date_updated: 2018-12-12T10:10:17Z
file_id: '4803'
file_name: IST-2012-82-v1+1_Determinizing_discounted-sum_automata.pdf
file_size: 504270
open_access: 1
relation: main_file
file_date_updated: 2018-12-12T10:10:17Z
intvolume: ' 12'
language:
- iso: eng
month: '08'
oa: 1
oa_version: Published Version
page: 82 - 96
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 25EFB36C-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '215543'
name: COMponent-Based Embedded Systems design Techniques
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _id: 25F1337C-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '214373'
name: Design for Embedded Systems
publication_status: published
publisher: Springer
publist_id: '3255'
pubrep_id: '82'
quality_controlled: '1'
status: public
title: Determinizing discounted-sum automata
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 12
year: '2011'
...