[{"has_accepted_license":"1","article_processing_charge":"No","day":"01","date_published":"2023-09-01T00:00:00Z","citation":{"short":"U. Boker, T.A. Henzinger, N.A. Mazzocchi, N.E. Sarac, in:, 34th International Conference on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023.","mla":"Boker, Udi, et al. “Safety and Liveness of Quantitative Automata.” 34th International Conference on Concurrency Theory, vol. 279, 17, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023, doi:10.4230/LIPIcs.CONCUR.2023.17.","chicago":"Boker, Udi, Thomas A Henzinger, Nicolas Adrien Mazzocchi, and Naci E Sarac. “Safety and Liveness of Quantitative Automata.” In 34th International Conference on Concurrency Theory, Vol. 279. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. https://doi.org/10.4230/LIPIcs.CONCUR.2023.17.","ama":"Boker U, Henzinger TA, Mazzocchi NA, Sarac NE. Safety and liveness of quantitative automata. In: 34th International Conference on Concurrency Theory. Vol 279. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2023. doi:10.4230/LIPIcs.CONCUR.2023.17","apa":"Boker, U., Henzinger, T. A., Mazzocchi, N. A., & Sarac, N. E. (2023). Safety and liveness of quantitative automata. In 34th International Conference on Concurrency Theory (Vol. 279). Antwerp, Belgium: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2023.17","ieee":"U. Boker, T. A. Henzinger, N. A. Mazzocchi, and N. E. Sarac, “Safety and liveness of quantitative automata,” in 34th International Conference on Concurrency Theory, Antwerp, Belgium, 2023, vol. 279.","ista":"Boker U, Henzinger TA, Mazzocchi NA, Sarac NE. 2023. Safety and liveness of quantitative automata. 34th International Conference on Concurrency Theory. CONCUR: Conference on Concurrency Theory, LIPIcs, vol. 279, 17."},"publication":"34th International Conference on Concurrency Theory","abstract":[{"lang":"eng","text":"The safety-liveness dichotomy is a fundamental concept in formal languages which plays a key role in verification. Recently, this dichotomy has been lifted to quantitative properties, which are arbitrary functions from infinite words to partially-ordered domains. We look into harnessing the dichotomy for the specific classes of quantitative properties expressed by quantitative automata. These automata contain finitely many states and rational-valued transition weights, and their common value functions Inf, Sup, LimInf, LimSup, LimInfAvg, LimSupAvg, and DSum map infinite words into the totallyordered domain of real numbers. In this automata-theoretic setting, we establish a connection between quantitative safety and topological continuity and provide an alternative characterization of quantitative safety and liveness in terms of their boolean counterparts. For all common value functions, we show how the safety closure of a quantitative automaton can be constructed in PTime, and we provide PSpace-complete checks of whether a given quantitative automaton is safe or live, with the exception of LimInfAvg and LimSupAvg automata, for which the safety check is in ExpSpace. Moreover, for deterministic Sup, LimInf, and LimSup automata, we give PTime decompositions into safe and live automata. These decompositions enable the separation of techniques for safety and liveness verification for quantitative specifications."}],"alternative_title":["LIPIcs"],"type":"conference","oa_version":"Published Version","file":[{"file_id":"13224","relation":"main_file","success":1,"checksum":"d40e57a04448ea5c77d7e1cfb9590a81","date_created":"2023-07-14T12:03:48Z","date_updated":"2023-07-14T12:03:48Z","access_level":"open_access","file_name":"CONCUR23.pdf","creator":"esarac","file_size":755529,"content_type":"application/pdf"}],"intvolume":" 279","ddc":["000"],"title":"Safety and liveness of quantitative automata","status":"public","_id":"13221","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publication_identifier":{"isbn":["9783959772990"],"eissn":["1868-8969"]},"month":"09","language":[{"iso":"eng"}],"doi":"10.4230/LIPIcs.CONCUR.2023.17","conference":{"end_date":"2023-09-23","start_date":"2023-09-18","location":"Antwerp, Belgium","name":"CONCUR: Conference on Concurrency Theory"},"project":[{"call_identifier":"H2020","name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"}],"quality_controlled":"1","oa":1,"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"external_id":{"arxiv":["2307.06016"]},"license":"https://creativecommons.org/licenses/by/4.0/","ec_funded":1,"file_date_updated":"2023-07-14T12:03:48Z","article_number":"17","volume":279,"date_created":"2023-07-14T10:00:15Z","date_updated":"2023-10-09T07:14:03Z","author":[{"full_name":"Boker, Udi","last_name":"Boker","first_name":"Udi","id":"31E297B6-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-2985-7724","first_name":"Thomas A","last_name":"Henzinger"},{"full_name":"Mazzocchi, Nicolas Adrien","first_name":"Nicolas Adrien","last_name":"Mazzocchi","id":"b26baa86-3308-11ec-87b0-8990f34baa85"},{"full_name":"Sarac, Naci E","id":"8C6B42F8-C8E6-11E9-A03A-F2DCE5697425","first_name":"Naci E","last_name":"Sarac"}],"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","department":[{"_id":"GradSch"},{"_id":"ToHe"}],"publication_status":"published","year":"2023","acknowledgement":"We thank Christof Löding for pointing us to some results on PSpace-hardess of universality problems and the anonymous reviewers for their helpful comments. This work was supported in part by the ERC-2020-AdG 101020093 and the Israel Science Foundation grant 2410/22."},{"date_updated":"2023-02-23T12:26:27Z","date_created":"2018-12-11T11:53:19Z","author":[{"first_name":"Udi","last_name":"Boker","id":"31E297B6-F248-11E8-B48F-1D18A9856A87","full_name":"Boker, Udi"},{"last_name":"Henzinger","first_name":"Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A"},{"full_name":"Otop, Jan","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","last_name":"Otop","first_name":"Jan"}],"related_material":{"record":[{"status":"public","relation":"earlier_version","id":"5439"}]},"publication_status":"published","department":[{"_id":"ToHe"}],"publisher":"IEEE","acknowledgement":"A technical report of the article is available at: https://research-explorer.app.ist.ac.at/record/5439","year":"2015","file_date_updated":"2020-07-14T12:45:10Z","publist_id":"5491","ec_funded":1,"language":[{"iso":"eng"}],"conference":{"end_date":"2015-07-10","start_date":"2015-007-06","location":"Kyoto, Japan","name":"LICS: Logic in Computer Science"},"doi":"10.1109/LICS.2015.74","quality_controlled":"1","project":[{"grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling","call_identifier":"FP7"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","call_identifier":"FWF","name":"Rigorous Systems Engineering"},{"grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"The Wittgenstein Prize"}],"oa":1,"month":"07","publication_identifier":{"eisbn":["978-1-4799-8875-4 "],"issn":["1043-6871 "]},"oa_version":"Submitted Version","file":[{"checksum":"6abebca9c1a620e9e103a8f9222befac","date_created":"2020-05-15T08:53:29Z","date_updated":"2020-07-14T12:45:10Z","file_id":"7852","relation":"main_file","creator":"dernst","file_size":340215,"content_type":"application/pdf","access_level":"open_access","file_name":"2015_LICS_Boker.pdf"}],"ddc":["000"],"status":"public","title":"The target discounted-sum problem","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_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."}],"type":"conference","date_published":"2015-07-01T00:00:00Z","page":"750 - 761","publication":"LICS","citation":{"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","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.","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","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.","short":"U. Boker, T.A. Henzinger, J. Otop, in:, LICS, IEEE, 2015, pp. 750–761.","mla":"Boker, Udi, et al. “The Target Discounted-Sum Problem.” LICS, IEEE, 2015, pp. 750–61, doi:10.1109/LICS.2015.74."},"day":"01","has_accepted_license":"1","article_processing_charge":"No","series_title":"Logic in Computer Science","scopus_import":1},{"type":"technical_report","alternative_title":["IST Austria Technical Report"],"file_date_updated":"2020-07-14T12:46:55Z","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. "}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"5439","year":"2015","status":"public","publication_status":"published","ddc":["004","512","513"],"title":"The target discounted-sum problem","publisher":"IST Austria","department":[{"_id":"ToHe"}],"author":[{"full_name":"Boker, Udi","first_name":"Udi","last_name":"Boker","id":"31E297B6-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A"},{"full_name":"Otop, Jan","first_name":"Jan","last_name":"Otop","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87"}],"related_material":{"record":[{"id":"1659","status":"public","relation":"later_version"}]},"pubrep_id":"335","date_updated":"2023-02-23T10:08:48Z","date_created":"2018-12-12T11:39:20Z","file":[{"content_type":"application/pdf","file_size":589619,"creator":"system","file_name":"IST-2015-335-v1+1_report.pdf","access_level":"open_access","date_updated":"2020-07-14T12:46:55Z","date_created":"2018-12-12T11:53:55Z","checksum":"40405907aa012acece1bc26cf0be554d","relation":"main_file","file_id":"5517"}],"oa_version":"Published Version","month":"05","day":"18","publication_identifier":{"issn":["2664-1690"]},"has_accepted_license":"1","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","ista":"Boker U, Henzinger TA, Otop J. 2015. The target discounted-sum problem, IST Austria, 20p.","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","ieee":"U. Boker, T. A. Henzinger, and J. Otop, The target discounted-sum problem. IST Austria, 2015.","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.","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."},"oa":1,"page":"20","doi":"10.15479/AT:IST-2015-335-v1-1","date_published":"2015-05-18T00:00:00Z","language":[{"iso":"eng"}]},{"day":"13","scopus_import":1,"date_published":"2014-01-13T00:00:00Z","citation":{"chicago":"Boker, Udi, Thomas A Henzinger, and Arjun Radhakrishna. “Battery Transition Systems,” 49:595–606. ACM, 2014. https://doi.org/10.1145/2535838.2535875.","short":"U. Boker, T.A. Henzinger, A. Radhakrishna, in:, ACM, 2014, pp. 595–606.","mla":"Boker, Udi, et al. Battery Transition Systems. Vol. 49, no. 1, ACM, 2014, pp. 595–606, doi:10.1145/2535838.2535875.","apa":"Boker, U., Henzinger, T. A., & Radhakrishna, A. (2014). Battery transition systems (Vol. 49, pp. 595–606). Presented at the POPL: Principles of Programming Languages, San Diego, USA: ACM. https://doi.org/10.1145/2535838.2535875","ieee":"U. Boker, T. A. Henzinger, and A. Radhakrishna, “Battery transition systems,” presented at the POPL: Principles of Programming Languages, San Diego, USA, 2014, vol. 49, no. 1, pp. 595–606.","ista":"Boker U, Henzinger TA, Radhakrishna A. 2014. Battery transition systems. POPL: Principles of Programming Languages vol. 49, 595–606.","ama":"Boker U, Henzinger TA, Radhakrishna A. Battery transition systems. In: Vol 49. ACM; 2014:595-606. doi:10.1145/2535838.2535875"},"page":"595 - 606","abstract":[{"lang":"eng","text":"The analysis of the energy consumption of software is an important goal for quantitative formal methods. Current methods, using weighted transition systems or energy games, model the energy source as an ideal resource whose status is characterized by one number, namely the amount of remaining energy. Real batteries, however, exhibit behaviors that can deviate substantially from an ideal energy resource. Based on a discretization of a standard continuous battery model, we introduce battery transition systems. In this model, a battery is viewed as consisting of two parts-the available-charge tank and the bound-charge tank. Any charge or discharge is applied to the available-charge tank. Over time, the energy from each tank diffuses to the other tank. Battery transition systems are infinite state systems that, being not well-structured, fall into no decidable class that is known to us. Nonetheless, we are able to prove that the !-regular modelchecking problem is decidable for battery transition systems. We also present a case study on the verification of control programs for energy-constrained semi-autonomous robots."}],"issue":"1","type":"conference","oa_version":"None","user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","_id":"2239","title":"Battery transition systems","status":"public","intvolume":" 49","month":"01","publication_identifier":{"isbn":["978-145032544-8"]},"conference":{"start_date":"2014-01-22","location":"San Diego, USA","end_date":"2014-01-24","name":"POPL: Principles of Programming Languages"},"doi":"10.1145/2535838.2535875","language":[{"iso":"eng"}],"quality_controlled":"1","project":[{"call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FP7","name":"Quantitative Reactive Modeling","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425"}],"publist_id":"4722","ec_funded":1,"author":[{"last_name":"Boker","first_name":"Udi","id":"31E297B6-F248-11E8-B48F-1D18A9856A87","full_name":"Boker, Udi"},{"last_name":"Henzinger","first_name":"Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A"},{"full_name":"Radhakrishna, Arjun","last_name":"Radhakrishna","first_name":"Arjun","id":"3B51CAC4-F248-11E8-B48F-1D18A9856A87"}],"date_updated":"2021-01-12T06:56:13Z","date_created":"2018-12-11T11:56:30Z","volume":49,"year":"2014","publication_status":"published","department":[{"_id":"ToHe"}],"publisher":"ACM"},{"oa":1,"project":[{"_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF"},{"grant_number":"S11402-N23","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Moderne Concurrency Paradigms"},{"name":"Game Theory","call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications"},{"name":"Quantitative Reactive Modeling","call_identifier":"FP7","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"quality_controlled":"1","doi":"10.1145/2629686","language":[{"iso":"eng"}],"month":"09","year":"2014","acknowledgement":"The research was supported in part by ERC Starting grant 278410 (QUALITY).","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"publisher":"ACM","publication_status":"published","related_material":{"record":[{"status":"public","relation":"earlier_version","id":"3356"},{"status":"public","relation":"earlier_version","id":"5385"}]},"author":[{"id":"31E297B6-F248-11E8-B48F-1D18A9856A87","first_name":"Udi","last_name":"Boker","full_name":"Boker, Udi"},{"full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A","last_name":"Henzinger","full_name":"Henzinger, Thomas A"},{"last_name":"Kupferman","first_name":"Orna","full_name":"Kupferman, Orna"}],"volume":15,"date_updated":"2023-02-23T12:23:54Z","date_created":"2018-12-11T11:55:21Z","article_number":"27","ec_funded":1,"publist_id":"5013","file_date_updated":"2020-07-14T12:45:26Z","citation":{"mla":"Boker, Udi, et al. “Temporal Specifications with Accumulative Values.” ACM Transactions on Computational Logic (TOCL), vol. 15, no. 4, 27, ACM, 2014, doi:10.1145/2629686.","short":"U. Boker, K. Chatterjee, T.A. Henzinger, O. Kupferman, ACM Transactions on Computational Logic (TOCL) 15 (2014).","chicago":"Boker, Udi, Krishnendu Chatterjee, Thomas A Henzinger, and Orna Kupferman. “Temporal Specifications with Accumulative Values.” ACM Transactions on Computational Logic (TOCL). ACM, 2014. https://doi.org/10.1145/2629686.","ama":"Boker U, Chatterjee K, Henzinger TA, Kupferman O. Temporal specifications with accumulative values. ACM Transactions on Computational Logic (TOCL). 2014;15(4). doi:10.1145/2629686","ista":"Boker U, Chatterjee K, Henzinger TA, Kupferman O. 2014. Temporal specifications with accumulative values. ACM Transactions on Computational Logic (TOCL). 15(4), 27.","apa":"Boker, U., Chatterjee, K., Henzinger, T. A., & Kupferman, O. (2014). Temporal specifications with accumulative values. ACM Transactions on Computational Logic (TOCL). ACM. https://doi.org/10.1145/2629686","ieee":"U. Boker, K. Chatterjee, T. A. Henzinger, and O. Kupferman, “Temporal specifications with accumulative values,” ACM Transactions on Computational Logic (TOCL), vol. 15, no. 4. ACM, 2014."},"publication":"ACM Transactions on Computational Logic (TOCL)","article_type":"original","date_published":"2014-09-16T00:00:00Z","scopus_import":1,"article_processing_charge":"No","has_accepted_license":"1","day":"16","_id":"2038","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","intvolume":" 15","status":"public","ddc":["000","004"],"title":"Temporal specifications with accumulative values","pubrep_id":"192","file":[{"relation":"main_file","file_id":"4851","date_updated":"2020-07-14T12:45:26Z","date_created":"2018-12-12T10:10:59Z","checksum":"354c41d37500b56320afce94cf9a99c2","file_name":"IST-2014-192-v1+1_AccumulativeValues.pdf","access_level":"open_access","content_type":"application/pdf","file_size":346184,"creator":"system"}],"oa_version":"Submitted Version","type":"journal_article","issue":"4","abstract":[{"lang":"eng","text":"Recently, there has been an effort to add quantitative objectives to formal verification and synthesis. We introduce and investigate the extension of temporal logics with quantitative atomic assertions. At the heart of quantitative objectives lies the accumulation of values along a computation. It is often the accumulated sum, as with energy objectives, or the accumulated average, as with mean-payoff objectives. We investigate the extension of temporal logics with the prefix-accumulation assertions Sum(v) ≥ c and Avg(v) ≥ c, where v is a numeric (or Boolean) variable of the system, c is a constant rational number, and Sum(v) and Avg(v) denote the accumulated sum and average of the values of v from the beginning of the computation up to the current point in time. We also allow the path-accumulation assertions LimInfAvg(v) ≥ c and LimSupAvg(v) ≥ c, referring to the average value along an entire infinite computation. We study the border of decidability for such quantitative extensions of various temporal logics. In particular, we show that extending the fragment of CTL that has only the EX, EF, AX, and AG temporal modalities with both prefix-accumulation assertions, or extending LTL with both path-accumulation assertions, results in temporal logics whose model-checking problem is decidable. Moreover, the prefix-accumulation assertions may be generalized with "controlled accumulation," allowing, for example, to specify constraints on the average waiting time between a request and a grant. On the negative side, we show that this branching-time logic is, in a sense, the maximal logic with one or both of the prefix-accumulation assertions that permits a decidable model-checking procedure. Extending a temporal logic that has the EG or EU modalities, such as CTL or LTL, makes the problem undecidable."}]},{"oa":1,"project":[{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF"},{"grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Reactive Modeling"}],"quality_controlled":"1","doi":"10.1007/978-3-642-39212-2_11","conference":{"name":"ICALP: Automata, Languages and Programming","end_date":"2013-07-12","start_date":"2013-07-08","location":"Riga, Latvia"},"language":[{"iso":"eng"}],"month":"07","acknowledgement":"and ERC Grant QUALITY.","year":"2013","department":[{"_id":"ToHe"}],"publisher":"Springer","publication_status":"published","author":[{"full_name":"Boker, Udi","id":"31E297B6-F248-11E8-B48F-1D18A9856A87","first_name":"Udi","last_name":"Boker"},{"first_name":"Denis","last_name":"Kuperberg","full_name":"Kuperberg, Denis"},{"first_name":"Orna","last_name":"Kupferman","full_name":"Kupferman, Orna"},{"first_name":"Michał","last_name":"Skrzypczak","full_name":"Skrzypczak, Michał"}],"volume":7966,"date_updated":"2020-08-11T10:09:09Z","date_created":"2018-12-11T11:51:44Z","publist_id":"5823","ec_funded":1,"file_date_updated":"2020-07-14T12:44:48Z","citation":{"short":"U. Boker, D. Kuperberg, O. Kupferman, M. Skrzypczak, 7966 (2013) 89–100.","mla":"Boker, Udi, et al. Nondeterminism in the Presence of a Diverse or Unknown Future. Vol. 7966, no. PART 2, Springer, 2013, pp. 89–100, doi:10.1007/978-3-642-39212-2_11.","chicago":"Boker, Udi, Denis Kuperberg, Orna Kupferman, and Michał Skrzypczak. “Nondeterminism in the Presence of a Diverse or Unknown Future.” Lecture Notes in Computer Science. Springer, 2013. https://doi.org/10.1007/978-3-642-39212-2_11.","ama":"Boker U, Kuperberg D, Kupferman O, Skrzypczak M. Nondeterminism in the presence of a diverse or unknown future. 2013;7966(PART 2):89-100. doi:10.1007/978-3-642-39212-2_11","apa":"Boker, U., Kuperberg, D., Kupferman, O., & Skrzypczak, M. (2013). Nondeterminism in the presence of a diverse or unknown future. Presented at the ICALP: Automata, Languages and Programming, Riga, Latvia: Springer. https://doi.org/10.1007/978-3-642-39212-2_11","ieee":"U. Boker, D. Kuperberg, O. Kupferman, and M. Skrzypczak, “Nondeterminism in the presence of a diverse or unknown future,” vol. 7966, no. PART 2. Springer, pp. 89–100, 2013.","ista":"Boker U, Kuperberg D, Kupferman O, Skrzypczak M. 2013. Nondeterminism in the presence of a diverse or unknown future. 7966(PART 2), 89–100."},"page":"89 - 100","date_published":"2013-07-01T00:00:00Z","scopus_import":1,"series_title":"Lecture Notes in Computer Science","article_processing_charge":"No","has_accepted_license":"1","day":"01","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"1387","intvolume":" 7966","title":"Nondeterminism in the presence of a diverse or unknown future","ddc":["000"],"status":"public","file":[{"file_name":"2013_ICALP_Boker.pdf","access_level":"open_access","content_type":"application/pdf","file_size":276982,"creator":"dernst","relation":"main_file","file_id":"7857","date_created":"2020-05-15T11:05:50Z","date_updated":"2020-07-14T12:44:48Z","checksum":"98bc02e3793072e279ec8d364b381ff3"}],"oa_version":"Submitted Version","type":"conference","alternative_title":["LNCS"],"issue":"PART 2","abstract":[{"text":"Choices made by nondeterministic word automata depend on both the past (the prefix of the word read so far) and the future (the suffix yet to be read). In several applications, most notably synthesis, the future is diverse or unknown, leading to algorithms that are based on deterministic automata. Hoping to retain some of the advantages of nondeterministic automata, researchers have studied restricted classes of nondeterministic automata. Three such classes are nondeterministic automata that are good for trees (GFT; i.e., ones that can be expanded to tree automata accepting the derived tree languages, thus whose choices should satisfy diverse futures), good for games (GFG; i.e., ones whose choices depend only on the past), and determinizable by pruning (DBP; i.e., ones that embody equivalent deterministic automata). The theoretical properties and relative merits of the different classes are still open, having vagueness on whether they really differ from deterministic automata. In particular, while DBP ⊆ GFG ⊆ GFT, it is not known whether every GFT automaton is GFG and whether every GFG automaton is DBP. Also open is the possible succinctness of GFG and GFT automata compared to deterministic automata. We study these problems for ω-regular automata with all common acceptance conditions. We show that GFT=GFG⊃DBP, and describe a determinization construction for GFG automata.","lang":"eng"}]},{"scopus_import":1,"series_title":"Lecture Notes in Computer Science","article_processing_charge":"No","has_accepted_license":"1","day":"01","citation":{"chicago":"Almagor, Shaull, Udi Boker, and Orna Kupferman. “Formalizing and Reasoning about Quality.” Lecture Notes in Computer Science. Springer, 2013. https://doi.org/10.1007/978-3-642-39212-2_3.","short":"S. Almagor, U. Boker, O. Kupferman, 7966 (2013) 15–27.","mla":"Almagor, Shaull, et al. Formalizing and Reasoning about Quality. Vol. 7966, no. Part 2, Springer, 2013, pp. 15–27, doi:10.1007/978-3-642-39212-2_3.","ieee":"S. Almagor, U. Boker, and O. Kupferman, “Formalizing and reasoning about quality,” vol. 7966, no. Part 2. Springer, pp. 15–27, 2013.","apa":"Almagor, S., Boker, U., & Kupferman, O. (2013). Formalizing and reasoning about quality. Presented at the ICALP: Automata, Languages and Programming, Riga, Latvia: Springer. https://doi.org/10.1007/978-3-642-39212-2_3","ista":"Almagor S, Boker U, Kupferman O. 2013. Formalizing and reasoning about quality. 7966(Part 2), 15–27.","ama":"Almagor S, Boker U, Kupferman O. Formalizing and reasoning about quality. 2013;7966(Part 2):15-27. doi:10.1007/978-3-642-39212-2_3"},"page":"15 - 27","date_published":"2013-07-01T00:00:00Z","type":"conference","alternative_title":["LNCS"],"issue":"Part 2","abstract":[{"text":"Traditional formal methods are based on a Boolean satisfaction notion: a reactive system satisfies, or not, a given specification. We generalize formal methods to also address the quality of systems. As an adequate specification formalism we introduce the linear temporal logic LTL[F]. The satisfaction value of an LTL[F] formula is a number between 0 and 1, describing the quality of the satisfaction. The logic generalizes traditional LTL by augmenting it with a (parameterized) set F of arbitrary functions over the interval [0,1]. For example, F may contain the maximum or minimum between the satisfaction values of subformulas, their product, and their average. The classical decision problems in formal methods, such as satisfiability, model checking, and synthesis, are generalized to search and optimization problems in the quantitative setting. For example, model checking asks for the quality in which a specification is satisfied, and synthesis returns a system satisfying the specification with the highest quality. Reasoning about quality gives rise to other natural questions, like the distance between specifications. We formalize these basic questions and study them for LTL[F]. By extending the automata-theoretic approach for LTL to a setting that takes quality into an account, we are able to solve the above problems and show that reasoning about LTL[F] has roughly the same complexity as reasoning about traditional LTL.","lang":"eng"}],"_id":"2517","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","intvolume":" 7966","status":"public","ddc":["000"],"title":"Formalizing and reasoning about quality","oa_version":"Submitted Version","file":[{"file_name":"2013_ICALP_Almagor.pdf","access_level":"open_access","content_type":"application/pdf","file_size":363031,"creator":"dernst","relation":"main_file","file_id":"7860","date_updated":"2020-07-14T12:45:42Z","date_created":"2020-05-15T11:16:12Z","checksum":"85afbf6c18a2c7e377c52c9410e2d824"}],"month":"07","oa":1,"project":[{"name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"},{"call_identifier":"FP7","name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989"}],"quality_controlled":"1","doi":"10.1007/978-3-642-39212-2_3","conference":{"end_date":"2013-07-12","start_date":"2013-07-08","location":"Riga, Latvia","name":"ICALP: Automata, Languages and Programming"},"language":[{"iso":"eng"}],"ec_funded":1,"publist_id":"4384","file_date_updated":"2020-07-14T12:45:42Z","year":"2013","acknowledgement":"ERC Grant QUALITY. ","department":[{"_id":"ToHe"}],"publisher":"Springer","publication_status":"published","author":[{"last_name":"Almagor","first_name":"Shaull","full_name":"Almagor, Shaull"},{"last_name":"Boker","first_name":"Udi","id":"31E297B6-F248-11E8-B48F-1D18A9856A87","full_name":"Boker, Udi"},{"full_name":"Kupferman, Orna","first_name":"Orna","last_name":"Kupferman"}],"volume":7966,"date_created":"2018-12-11T11:58:08Z","date_updated":"2020-08-11T10:09:47Z"},{"language":[{"iso":"eng"}],"conference":{"name":"FSTTCS: Foundations of Software Technology and Theoretical Computer Science","location":"Hyderabad, India","start_date":"2012-12-15","end_date":"2012-12-17"},"doi":"10.4230/LIPIcs.FSTTCS.2012.362","quality_controlled":"1","project":[{"call_identifier":"FWF","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"},{"name":"Quantitative Reactive Modeling","call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989"}],"oa":1,"tmp":{"name":"Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International (CC BY-NC-ND 4.0)","legal_code_url":"https://creativecommons.org/licenses/by-nc-nd/4.0/legalcode","short":"CC BY-NC-ND (4.0)","image":"/images/cc_by_nc_nd.png"},"month":"12","date_updated":"2021-01-12T07:00:31Z","date_created":"2018-12-11T12:00:10Z","volume":18,"author":[{"id":"31E297B6-F248-11E8-B48F-1D18A9856A87","last_name":"Boker","first_name":"Udi","full_name":"Boker, Udi"},{"last_name":"Henzinger","first_name":"Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A"}],"publication_status":"published","department":[{"_id":"ToHe"}],"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","acknowledgement":"We thank Laurent Doyen for great ideas and valuable help in analyzing discounted-sum automata.","year":"2012","license":"https://creativecommons.org/licenses/by-nc-nd/4.0/","file_date_updated":"2020-07-14T12:45:52Z","ec_funded":1,"publist_id":"3867","date_published":"2012-12-01T00:00:00Z","page":"362 - 373","publication":"Leibniz International Proceedings in Informatics","citation":{"ieee":"U. Boker and T. A. Henzinger, “Approximate determinization of quantitative automata,” in Leibniz International Proceedings in Informatics, Hyderabad, India, 2012, vol. 18, pp. 362–373.","apa":"Boker, U., & Henzinger, T. A. (2012). Approximate determinization of quantitative automata. In Leibniz International Proceedings in Informatics (Vol. 18, pp. 362–373). Hyderabad, India: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.FSTTCS.2012.362","ista":"Boker U, Henzinger TA. 2012. Approximate determinization of quantitative automata. Leibniz International Proceedings in Informatics. FSTTCS: Foundations of Software Technology and Theoretical Computer Science, LIPIcs, vol. 18, 362–373.","ama":"Boker U, Henzinger TA. Approximate determinization of quantitative automata. In: Leibniz International Proceedings in Informatics. Vol 18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2012:362-373. doi:10.4230/LIPIcs.FSTTCS.2012.362","chicago":"Boker, Udi, and Thomas A Henzinger. “Approximate Determinization of Quantitative Automata.” In Leibniz International Proceedings in Informatics, 18:362–73. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2012. https://doi.org/10.4230/LIPIcs.FSTTCS.2012.362.","short":"U. Boker, T.A. Henzinger, in:, Leibniz International Proceedings in Informatics, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2012, pp. 362–373.","mla":"Boker, Udi, and Thomas A. Henzinger. “Approximate Determinization of Quantitative Automata.” Leibniz International Proceedings in Informatics, vol. 18, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2012, pp. 362–73, doi:10.4230/LIPIcs.FSTTCS.2012.362."},"day":"01","has_accepted_license":"1","scopus_import":1,"oa_version":"Published Version","file":[{"checksum":"88da18d3e2cb2e5011d7d10ce38a3864","date_created":"2018-12-12T10:10:37Z","date_updated":"2020-07-14T12:45:52Z","file_id":"4826","relation":"main_file","creator":"system","file_size":559069,"content_type":"application/pdf","access_level":"open_access","file_name":"IST-2017-805-v1+1_34.pdf"}],"pubrep_id":"805","ddc":["004"],"title":"Approximate determinization of quantitative automata","status":"public","intvolume":" 18","_id":"2891","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","abstract":[{"lang":"eng","text":"Quantitative automata are nondeterministic finite automata with edge weights. They value a\r\nrun by some function from the sequence of visited weights to the reals, and value a word by its\r\nminimal/maximal run. They generalize boolean automata, and have gained much attention in\r\nrecent years. Unfortunately, important automaton classes, such as sum, discounted-sum, and\r\nlimit-average automata, cannot be determinized. Yet, the quantitative setting provides the potential\r\nof approximate determinization. We define approximate determinization with respect to\r\na distance function, and investigate this potential.\r\nWe show that sum automata cannot be determinized approximately with respect to any\r\ndistance function. However, restricting to nonnegative weights allows for approximate determinization\r\nwith respect to some distance functions.\r\nDiscounted-sum automata allow for approximate determinization, as the influence of a word’s\r\nsuffix is decaying. However, the naive approach, of unfolding the automaton computations up\r\nto a sufficient level, is shown to be doubly exponential in the discount factor. We provide an\r\nalternative construction that is singly exponential in the discount factor, in the precision, and\r\nin the number of states. We prove matching lower bounds, showing exponential dependency on\r\neach of these three parameters.\r\nAverage and limit-average automata are shown to prohibit approximate determinization with\r\nrespect to any distance function, and this is the case even for two weights, 0 and 1."}],"alternative_title":["LIPIcs"],"type":"conference"},{"date_published":"2012-10-01T00:00:00Z","doi":"10.1145/2362355.2362357","language":[{"iso":"eng"}],"publication":"ACM Transactions on Computational Logic (TOCL)","citation":{"chicago":"Boker, Udi, and Orna Kupferman. “Translating to Co-Büchi Made Tight, Unified, and Useful.” ACM Transactions on Computational Logic (TOCL). ACM, 2012. https://doi.org/10.1145/2362355.2362357.","short":"U. Boker, O. Kupferman, ACM Transactions on Computational Logic (TOCL) 13 (2012).","mla":"Boker, Udi, and Orna Kupferman. “Translating to Co-Büchi Made Tight, Unified, and Useful.” ACM Transactions on Computational Logic (TOCL), vol. 13, no. 4, 29, ACM, 2012, doi:10.1145/2362355.2362357.","ieee":"U. Boker and O. Kupferman, “Translating to Co-Büchi made tight, unified, and useful,” ACM Transactions on Computational Logic (TOCL), vol. 13, no. 4. ACM, 2012.","apa":"Boker, U., & Kupferman, O. (2012). Translating to Co-Büchi made tight, unified, and useful. ACM Transactions on Computational Logic (TOCL). ACM. https://doi.org/10.1145/2362355.2362357","ista":"Boker U, Kupferman O. 2012. Translating to Co-Büchi made tight, unified, and useful. ACM Transactions on Computational Logic (TOCL). 13(4), 29.","ama":"Boker U, Kupferman O. Translating to Co-Büchi made tight, unified, and useful. ACM Transactions on Computational Logic (TOCL). 2012;13(4). doi:10.1145/2362355.2362357"},"quality_controlled":"1","day":"01","month":"10","scopus_import":1,"author":[{"full_name":"Boker, Udi","id":"31E297B6-F248-11E8-B48F-1D18A9856A87","first_name":"Udi","last_name":"Boker"},{"first_name":"Orna","last_name":"Kupferman","full_name":"Kupferman, Orna"}],"date_created":"2018-12-11T11:46:47Z","date_updated":"2021-01-12T08:01:03Z","oa_version":"None","volume":13,"year":"2012","_id":"494","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","publication_status":"published","status":"public","title":"Translating to Co-Büchi made tight, unified, and useful","publisher":"ACM","intvolume":" 13","department":[{"_id":"ToHe"}],"abstract":[{"lang":"eng","text":"We solve the longstanding open problems of the blow-up involved in the translations, when possible, of a nondeterministic Büchi word automaton (NBW) to a nondeterministic co-Büchi word automaton (NCW) and to a deterministic co-Büchi word automaton (DCW). For the NBW to NCW translation, the currently known upper bound is 2o(nlog n) and the lower bound is 1.5n. We improve the upper bound to n2n and describe a matching lower bound of 2ω(n). For the NBW to DCW translation, the currently known upper bound is 2o(nlog n). We improve it to 2 o(n), which is asymptotically tight. Both of our upper-bound constructions are based on a simple subset construction, do not involve intermediate automata with richer acceptance conditions, and can be implemented symbolically. We continue and solve the open problems of translating nondeterministic Streett, Rabin, Muller, and parity word automata to NCW and to DCW. Going via an intermediate NBW is not optimal and we describe direct, simple, and asymptotically tight constructions, involving a 2o(n) blow-up. The constructions are variants of the subset construction, providing a unified approach for translating all common classes of automata to NCW and DCW. Beyond the theoretical importance of the results, we point to numerous applications of the new constructions. In particular, they imply a simple subset-construction based translation, when possible, of LTL to deterministic Büchi word automata."}],"issue":"4","publist_id":"7326","article_number":"29","type":"journal_article"},{"page":"482 - 491","citation":{"ama":"Almagor S, Boker U, Kupferman O. What’s decidable about weighted automata . In: Vol 6996. Springer; 2011:482-491. doi:10.1007/978-3-642-24372-1_37","ista":"Almagor S, Boker U, Kupferman O. 2011. What’s decidable about weighted automata . ATVA: Automated Technology for Verification and Analysis, LNCS, vol. 6996, 482–491.","ieee":"S. Almagor, U. Boker, and O. Kupferman, “What’s decidable about weighted automata ,” presented at the ATVA: Automated Technology for Verification and Analysis, Taipei, Taiwan, 2011, vol. 6996, pp. 482–491.","apa":"Almagor, S., Boker, U., & Kupferman, O. (2011). What’s decidable about weighted automata (Vol. 6996, pp. 482–491). Presented at the ATVA: Automated Technology for Verification and Analysis, Taipei, Taiwan: Springer. https://doi.org/10.1007/978-3-642-24372-1_37","mla":"Almagor, Shaull, et al. What’s Decidable about Weighted Automata . Vol. 6996, Springer, 2011, pp. 482–91, doi:10.1007/978-3-642-24372-1_37.","short":"S. Almagor, U. Boker, O. Kupferman, in:, Springer, 2011, pp. 482–491.","chicago":"Almagor, Shaull, Udi Boker, and Orna Kupferman. “What’s Decidable about Weighted Automata ,” 6996:482–91. Springer, 2011. https://doi.org/10.1007/978-3-642-24372-1_37."},"date_published":"2011-10-14T00:00:00Z","article_processing_charge":"No","has_accepted_license":"1","day":"14","intvolume":" 6996","status":"public","ddc":["000"],"title":"What’s decidable about weighted automata ","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"3326","file":[{"access_level":"open_access","file_name":"2011_LNCS_Almagor.pdf","creator":"dernst","content_type":"application/pdf","file_size":182309,"file_id":"7868","relation":"main_file","checksum":"a7ca08a2cb1b6925f4c18a3034ae5659","date_updated":"2020-07-14T12:46:07Z","date_created":"2020-05-19T16:08:32Z"}],"oa_version":"Submitted Version","alternative_title":["LNCS"],"type":"conference","abstract":[{"text":"Weighted automata map input words to numerical values. Ap- plications of weighted automata include formal verification of quantitative properties, as well as text, speech, and image processing. A weighted au- tomaton is defined with respect to a semiring. For the tropical semiring, the weight of a run is the sum of the weights of the transitions taken along the run, and the value of a word is the minimal weight of an accepting run on it. In the 90’s, Krob studied the decidability of problems on rational series defined with respect to the tropical semiring. Rational series are strongly related to weighted automata, and Krob’s results apply to them. In par- ticular, it follows from Krob’s results that the universality problem (that is, deciding whether the values of all words are below some threshold) is decidable for weighted automata defined with respect to the tropical semir- ing with domain ∪ {∞}, and that the equality problem is undecidable when the domain is ∪ {∞}. In this paper we continue the study of the borders of decidability in weighted automata, describe alternative and direct proofs of the above results, and tighten them further. Unlike the proofs of Krob, which are algebraic in their nature, our proofs stay in the terrain of state machines, and the reduction is from the halting problem of a two-counter machine. This enables us to significantly simplify Krob’s reasoning, make the un- decidability result accessible to the automata-theoretic community, and strengthen it to apply already to a very simple class of automata: all the states are accepting, there are no initial nor final weights, and all the weights on the transitions are from the set {−1, 0, 1}. The fact we work directly with the automata enables us to tighten also the decidability re- sults and to show that the universality problem for weighted automata defined with respect to the tropical semiring with domain ∪ {∞}, and in fact even with domain ≥0 ∪ {∞}, is PSPACE-complete. Our results thus draw a sharper picture about the decidability of decision problems for weighted automata, in both the front of containment vs. universality and the front of the ∪ {∞} vs. the ∪ {∞} domains.","lang":"eng"}],"quality_controlled":"1","oa":1,"language":[{"iso":"eng"}],"doi":"10.1007/978-3-642-24372-1_37","conference":{"name":"ATVA: Automated Technology for Verification and Analysis","end_date":"2011-10-14","start_date":"2011-10-11","location":"Taipei, Taiwan"},"month":"10","publisher":"Springer","department":[{"_id":"ToHe"}],"publication_status":"published","year":"2011","volume":6996,"date_updated":"2021-01-12T07:42:40Z","date_created":"2018-12-11T12:02:41Z","author":[{"first_name":"Shaull","last_name":"Almagor","full_name":"Almagor, Shaull"},{"full_name":"Boker, Udi","id":"31E297B6-F248-11E8-B48F-1D18A9856A87","last_name":"Boker","first_name":"Udi"},{"full_name":"Kupferman, Orna","first_name":"Orna","last_name":"Kupferman"}],"publist_id":"3309","file_date_updated":"2020-07-14T12:46:07Z"},{"year":"2011","_id":"3327","user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","intvolume":" 6604","editor":[{"last_name":"Hofmann","first_name":"Martin","full_name":"Hofmann, Martin"}],"publisher":"Springer","status":"public","publication_status":"published","title":"Co-Büching them all","author":[{"id":"31E297B6-F248-11E8-B48F-1D18A9856A87","first_name":"Udi","last_name":"Boker","full_name":"Boker, Udi"},{"first_name":"Orna","last_name":"Kupferman","full_name":"Kupferman, Orna"}],"oa_version":"None","volume":6604,"date_updated":"2021-01-12T07:42:41Z","date_created":"2018-12-11T12:02:41Z","type":"conference","alternative_title":["LNCS"],"publist_id":"3308","abstract":[{"lang":"eng","text":"We solve the open problems of translating, when possible, all common classes of nondeterministic word automata to deterministic and nondeterministic co-Büchi word automata. The handled classes include Büchi, parity, Rabin, Streett and Muller automata. The translations follow a unified approach and are all asymptotically tight. The problem of translating Büchi automata to equivalent co-Büchi automata was solved in [2], leaving open the problems of translating automata with richer acceptance conditions. For these classes, one cannot easily extend or use the construction in [2]. In particular, going via an intermediate Büchi automaton is not optimal and might involve a blow-up exponentially higher than the known lower bound. Other known translations are also not optimal and involve a doubly exponential blow-up. We describe direct, simple, and asymptotically tight constructions, involving a 2Θ(n) blow-up. The constructions are variants of the subset construction, and allow for symbolic implementations. Beyond the theoretical importance of the results, the new constructions have various applications, among which is an improved algorithm for translating, when possible, LTL formulas to deterministic Büchi word automata."}],"extern":"1","citation":{"ieee":"U. Boker and O. Kupferman, “Co-Büching them all,” presented at the FoSSaCS: Foundations of Software Science and Computation Structures, Saarbrücken, Germany, 2011, vol. 6604, pp. 184–198.","apa":"Boker, U., & Kupferman, O. (2011). Co-Büching them all. In M. Hofmann (Ed.) (Vol. 6604, pp. 184–198). Presented at the FoSSaCS: Foundations of Software Science and Computation Structures, Saarbrücken, Germany: Springer. https://doi.org/10.1007/978-3-642-19805-2_13","ista":"Boker U, Kupferman O. 2011. Co-Büching them all. FoSSaCS: Foundations of Software Science and Computation Structures, LNCS, vol. 6604, 184–198.","ama":"Boker U, Kupferman O. Co-Büching them all. In: Hofmann M, ed. Vol 6604. Springer; 2011:184-198. doi:10.1007/978-3-642-19805-2_13","chicago":"Boker, Udi, and Orna Kupferman. “Co-Büching Them All.” edited by Martin Hofmann, 6604:184–98. Springer, 2011. https://doi.org/10.1007/978-3-642-19805-2_13.","short":"U. Boker, O. Kupferman, in:, M. Hofmann (Ed.), Springer, 2011, pp. 184–198.","mla":"Boker, Udi, and Orna Kupferman. Co-Büching Them All. Edited by Martin Hofmann, vol. 6604, Springer, 2011, pp. 184–98, doi:10.1007/978-3-642-19805-2_13."},"page":"184 - 198","quality_controlled":"1","date_published":"2011-03-29T00:00:00Z","doi":"10.1007/978-3-642-19805-2_13","conference":{"end_date":"2011-04-03","location":"Saarbrücken, Germany","start_date":"2011-03-26","name":"FoSSaCS: Foundations of Software Science and Computation Structures"},"language":[{"iso":"eng"}],"month":"03","day":"29"},{"file_date_updated":"2020-07-14T12:46:10Z","publist_id":"3255","ec_funded":1,"date_updated":"2021-01-12T07:42:56Z","date_created":"2018-12-11T12:02:53Z","volume":12,"author":[{"full_name":"Boker, Udi","id":"31E297B6-F248-11E8-B48F-1D18A9856A87","last_name":"Boker","first_name":"Udi"},{"first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A"}],"publication_status":"published","department":[{"_id":"ToHe"}],"publisher":"Springer","year":"2011","month":"08","language":[{"iso":"eng"}],"conference":{"start_date":"2011-09-12","location":"Bergen, Norway","end_date":"2011-09-15","name":"CSL: Computer Science Logic"},"doi":"10.4230/LIPIcs.CSL.2011.82","quality_controlled":"1","project":[{"grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering"},{"name":"COMponent-Based Embedded Systems design Techniques","call_identifier":"FP7","_id":"25EFB36C-B435-11E9-9278-68D0E5697425","grant_number":"215543"},{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","call_identifier":"FP7","name":"Quantitative Reactive Modeling"},{"_id":"25F1337C-B435-11E9-9278-68D0E5697425","grant_number":"214373","name":"Design for Embedded Systems","call_identifier":"FP7"}],"tmp":{"name":"Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International (CC BY-NC-ND 4.0)","legal_code_url":"https://creativecommons.org/licenses/by-nc-nd/4.0/legalcode","short":"CC BY-NC-ND (4.0)","image":"/images/cc_by_nc_nd.png"},"oa":1,"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. "}],"alternative_title":["LIPIcs"],"type":"conference","oa_version":"Published Version","file":[{"file_id":"4803","relation":"main_file","date_created":"2018-12-12T10:10:17Z","date_updated":"2020-07-14T12:46:10Z","checksum":"250603c6be8ccad4fbd4d7b24221f0ee","file_name":"IST-2012-82-v1+1_Determinizing_discounted-sum_automata.pdf","access_level":"open_access","creator":"system","content_type":"application/pdf","file_size":504270}],"pubrep_id":"82","ddc":["004"],"status":"public","title":"Determinizing discounted-sum automata","intvolume":" 12","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"3360","day":"31","has_accepted_license":"1","scopus_import":1,"date_published":"2011-08-31T00:00:00Z","page":"82 - 96","citation":{"short":"U. Boker, T.A. Henzinger, in:, Springer, 2011, pp. 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.","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.","ama":"Boker U, Henzinger TA. Determinizing discounted-sum automata. In: Vol 12. Springer; 2011:82-96. doi: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.","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","ista":"Boker U, Henzinger TA. 2011. Determinizing discounted-sum automata. CSL: Computer Science Logic, LIPIcs, vol. 12, 82–96."}},{"date_published":"2011-06-21T00:00:00Z","citation":{"short":"U. Boker, K. Chatterjee, T.A. Henzinger, O. Kupferman, in:, IEEE, 2011.","mla":"Boker, Udi, et al. Temporal Specifications with Accumulative Values. 5970226, IEEE, 2011, doi:10.1109/LICS.2011.33.","chicago":"Boker, Udi, Krishnendu Chatterjee, Thomas A Henzinger, and Orna Kupferman. “Temporal Specifications with Accumulative Values.” IEEE, 2011. https://doi.org/10.1109/LICS.2011.33.","ama":"Boker U, Chatterjee K, Henzinger TA, Kupferman O. Temporal specifications with accumulative values. In: IEEE; 2011. doi:10.1109/LICS.2011.33","apa":"Boker, U., Chatterjee, K., Henzinger, T. A., & Kupferman, O. (2011). Temporal specifications with accumulative values. Presented at the LICS: Logic in Computer Science, Toronto, Canada: IEEE. https://doi.org/10.1109/LICS.2011.33","ieee":"U. Boker, K. Chatterjee, T. A. Henzinger, and O. Kupferman, “Temporal specifications with accumulative values,” presented at the LICS: Logic in Computer Science, Toronto, Canada, 2011.","ista":"Boker U, Chatterjee K, Henzinger TA, Kupferman O. 2011. Temporal specifications with accumulative values. LICS: Logic in Computer Science, 5970226."},"has_accepted_license":"1","day":"21","scopus_import":1,"file":[{"creator":"system","file_size":225426,"content_type":"application/pdf","access_level":"open_access","file_name":"IST-2012-83-v1+1_Temporal_specifications_with_accumulative_values.pdf","checksum":"792128f5455f0f40f1105f0398e05fa9","date_created":"2018-12-12T10:12:42Z","date_updated":"2020-07-14T12:46:09Z","file_id":"4960","relation":"main_file"}],"oa_version":"Submitted Version","pubrep_id":"83","status":"public","ddc":["000","004"],"title":"Temporal specifications with accumulative values","user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","_id":"3356","abstract":[{"lang":"eng","text":"There is recently a significant effort to add quantitative objectives to formal verification and synthesis. We introduce and investigate the extension of temporal logics with quantitative atomic assertions, aiming for a general and flexible framework for quantitative-oriented specifications. In the heart of quantitative objectives lies the accumulation of values along a computation. It is either the accumulated summation, as with the energy objectives, or the accumulated average, as with the mean-payoff objectives. We investigate the extension of temporal logics with the prefix-accumulation assertions Sum(v) ≥ c and Avg(v) ≥ c, where v is a numeric variable of the system, c is a constant rational number, and Sum(v) and Avg(v) denote the accumulated sum and average of the values of v from the beginning of the computation up to the current point of time. We also allow the path-accumulation assertions LimInfAvg(v) ≥ c and LimSupAvg(v) ≥ c, referring to the average value along an entire computation. We study the border of decidability for extensions of various temporal logics. In particular, we show that extending the fragment of CTL that has only the EX, EF, AX, and AG temporal modalities by prefix-accumulation assertions and extending LTL with path-accumulation assertions, result in temporal logics whose model-checking problem is decidable. The extended logics allow to significantly extend the currently known energy and mean-payoff objectives. Moreover, the prefix-accumulation assertions may be refined with \"controlled-accumulation\", allowing, for example, to specify constraints on the average waiting time between a request and a grant. On the negative side, we show that the fragment we point to is, in a sense, the maximal logic whose extension with prefix-accumulation assertions permits a decidable model-checking procedure. Extending a temporal logic that has the EG or EU modalities, and in particular CTL and LTL, makes the problem undecidable."}],"type":"conference","language":[{"iso":"eng"}],"doi":"10.1109/LICS.2011.33","conference":{"end_date":"2011-06-24","location":"Toronto, Canada","start_date":"2011-06-21","name":"LICS: Logic in Computer Science"},"project":[{"call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"_id":"25EFB36C-B435-11E9-9278-68D0E5697425","grant_number":"215543","name":"COMponent-Based Embedded Systems design Techniques","call_identifier":"FP7"},{"grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling","call_identifier":"FP7"},{"call_identifier":"FP7","name":"Design for Embedded Systems","grant_number":"214373","_id":"25F1337C-B435-11E9-9278-68D0E5697425"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"oa":1,"month":"06","date_updated":"2023-02-23T12:23:54Z","date_created":"2018-12-11T12:02:52Z","related_material":{"record":[{"relation":"later_version","status":"public","id":"2038"},{"id":"5385","status":"public","relation":"earlier_version"}]},"author":[{"full_name":"Boker, Udi","first_name":"Udi","last_name":"Boker","id":"31E297B6-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"},{"full_name":"Henzinger, Thomas A","last_name":"Henzinger","first_name":"Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Kupferman, Orna","first_name":"Orna","last_name":"Kupferman"}],"department":[{"_id":"ToHe"},{"_id":"KrCh"}],"publisher":"IEEE","publication_status":"published","year":"2011","ec_funded":1,"publist_id":"3259","file_date_updated":"2020-07-14T12:46:09Z","article_number":"5970226"},{"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"5385","ddc":["000","004"],"status":"public","title":"Temporal specifications with accumulative values","pubrep_id":"21","file":[{"access_level":"open_access","file_name":"IST-2011-0003_IST-2011-0003.pdf","file_size":366281,"content_type":"application/pdf","creator":"system","relation":"main_file","file_id":"5461","checksum":"8491d0d48c4911620ecd5350b413c11e","date_created":"2018-12-12T11:53:00Z","date_updated":"2020-07-14T12:46:41Z"}],"oa_version":"Published Version","type":"technical_report","alternative_title":["IST Austria Technical Report"],"abstract":[{"text":"There is recently a significant effort to add quantitative objectives to formal verification and synthesis. We introduce and investigate the extension of temporal logics with quantitative atomic assertions, aiming for a general and flexible framework for quantitative-oriented specifications. In the heart of quantitative objectives lies the accumulation of values along a computation. It is either the accumulated summation, as with the energy objectives, or the accumulated average, as with the mean-payoff objectives. We investigate the extension of temporal logics with the prefix-accumulation assertions Sum(v) ≥ c and Avg(v) ≥ c, where v is a numeric variable of the system, c is a constant rational number, and Sum(v) and Avg(v) denote the accumulated sum and average of the values of v from the beginning of the computation up to the current point of time. We also allow the path-accumulation assertions LimInfAvg(v) ≥ c and LimSupAvg(v) ≥ c, referring to the average value along an entire computation. We study the border of decidability for extensions of various temporal logics. In particular, we show that extending the fragment of CTL that has only the EX, EF, AX, and AG temporal modalities by prefix-accumulation assertions and extending LTL with path-accumulation assertions, result in temporal logics whose model-checking problem is decidable. The extended logics allow to significantly extend the currently known energy and mean-payoff objectives. Moreover, the prefix-accumulation assertions may be refined with “controlled-accumulation”, allowing, for example, to specify constraints on the average waiting time between a request and a grant. On the negative side, we show that the fragment we point to is, in a sense, the maximal logic whose extension with prefix-accumulation assertions permits a decidable model-checking procedure. Extending a temporal logic that has the EG or EU modalities, and in particular CTL and LTL, makes the problem undecidable.","lang":"eng"}],"citation":{"ieee":"U. Boker, K. Chatterjee, T. A. Henzinger, and O. Kupferman, Temporal specifications with accumulative values. IST Austria, 2011.","apa":"Boker, U., Chatterjee, K., Henzinger, T. A., & Kupferman, O. (2011). Temporal specifications with accumulative values. IST Austria. https://doi.org/10.15479/AT:IST-2011-0003","ista":"Boker U, Chatterjee K, Henzinger TA, Kupferman O. 2011. Temporal specifications with accumulative values, IST Austria, 14p.","ama":"Boker U, Chatterjee K, Henzinger TA, Kupferman O. Temporal Specifications with Accumulative Values. IST Austria; 2011. doi:10.15479/AT:IST-2011-0003","chicago":"Boker, Udi, Krishnendu Chatterjee, Thomas A Henzinger, and Orna Kupferman. Temporal Specifications with Accumulative Values. IST Austria, 2011. https://doi.org/10.15479/AT:IST-2011-0003.","short":"U. Boker, K. Chatterjee, T.A. Henzinger, O. Kupferman, Temporal Specifications with Accumulative Values, IST Austria, 2011.","mla":"Boker, Udi, et al. Temporal Specifications with Accumulative Values. IST Austria, 2011, doi:10.15479/AT:IST-2011-0003."},"page":"14","date_published":"2011-04-04T00:00:00Z","day":"04","has_accepted_license":"1","year":"2011","publication_status":"published","publisher":"IST Austria","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"author":[{"full_name":"Boker, Udi","first_name":"Udi","last_name":"Boker","id":"31E297B6-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"},{"first_name":"Orna","last_name":"Kupferman","full_name":"Kupferman, Orna"}],"related_material":{"record":[{"status":"public","relation":"later_version","id":"2038"},{"id":"3356","relation":"later_version","status":"public"}]},"date_created":"2018-12-12T11:39:02Z","date_updated":"2023-02-23T11:23:41Z","file_date_updated":"2020-07-14T12:46:41Z","ec_funded":1,"oa":1,"project":[{"call_identifier":"FWF","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"},{"grant_number":"215543","_id":"25EFB36C-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"COMponent-Based Embedded Systems design Techniques"},{"grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Reactive Modeling"},{"name":"Design for Embedded Systems","call_identifier":"FP7","_id":"25F1337C-B435-11E9-9278-68D0E5697425","grant_number":"214373"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"doi":"10.15479/AT:IST-2011-0003","language":[{"iso":"eng"}],"month":"04","publication_identifier":{"issn":["2664-1690"]}}]