conference paper
Determinizing discounted-sum automata
LIPIcs
published
yes
Udi
Boker
author 31E297B6-F248-11E8-B48F-1D18A9856A87
Thomas A
Henzinger
author 40876CD8-F248-11E8-B48F-1D18A9856A870000−0002−2985−7724
ToHe
department
CSL: Computer Science Logic
Rigorous Systems Engineering
project
COMponent-Based Embedded Systems design Techniques
project
Quantitative Reactive Modeling
project
Design for Embedded Systems
project
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.
https://research-explorer.app.ist.ac.at/download/3360/4803/IST-2012-82-v1+1_Determinizing_discounted-sum_automata.pdf
application/pdfno
cc_by_nc_nd
Springer2011Bergen, Norway
eng
10.4230/LIPIcs.CSL.2011.82
1282 - 96
Boker, Udi, and Thomas A. Henzinger. <i>Determinizing Discounted-Sum Automata</i>. Vol. 12, Springer, 2011, pp. 82–96, doi:<a href="https://doi.org/10.4230/LIPIcs.CSL.2011.82">10.4230/LIPIcs.CSL.2011.82</a>.
Boker, Udi, and Thomas A Henzinger. “Determinizing Discounted-Sum Automata,” 12:82–96. Springer, 2011. <a href="https://doi.org/10.4230/LIPIcs.CSL.2011.82">https://doi.org/10.4230/LIPIcs.CSL.2011.82</a>.
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.
Boker U, Henzinger TA. 2011. Determinizing discounted-sum automata. CSL: Computer Science Logic, LIPIcs, vol. 12. 82–96.
Boker U, Henzinger TA. Determinizing discounted-sum automata. In: Vol 12. Springer; 2011:82-96. doi:<a href="https://doi.org/10.4230/LIPIcs.CSL.2011.82">10.4230/LIPIcs.CSL.2011.82</a>
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. <a href="https://doi.org/10.4230/LIPIcs.CSL.2011.82">https://doi.org/10.4230/LIPIcs.CSL.2011.82</a>
U. Boker, T.A. Henzinger, in:, Springer, 2011, pp. 82–96.
33602018-12-11T12:02:53Z2020-01-21T13:20:22Z