[{"oa":1,"publication_status":"published","has_accepted_license":"1","date_published":"2020-08-06T00:00:00Z","ddc":["000"],"alternative_title":["LIPIcs"],"status":"public","external_id":{"arxiv":["2007.08917"]},"intvolume":"       171","citation":{"short":"K. Chatterjee, T.A. Henzinger, J. Otop, in:, 31st International Conference on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. “Multi-Dimensional Long-Run Average Problems for Vector Addition Systems with States.” In <i>31st International Conference on Concurrency Theory</i>, Vol. 171. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2020.23\">https://doi.org/10.4230/LIPIcs.CONCUR.2020.23</a>.","ieee":"K. Chatterjee, T. A. Henzinger, and J. Otop, “Multi-dimensional long-run average problems for vector addition systems with states,” in <i>31st International Conference on Concurrency Theory</i>, Virtual, 2020, vol. 171.","apa":"Chatterjee, K., Henzinger, T. A., &#38; Otop, J. (2020). Multi-dimensional long-run average problems for vector addition systems with states. In <i>31st International Conference on Concurrency Theory</i> (Vol. 171). Virtual: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2020.23\">https://doi.org/10.4230/LIPIcs.CONCUR.2020.23</a>","mla":"Chatterjee, Krishnendu, et al. “Multi-Dimensional Long-Run Average Problems for Vector Addition Systems with States.” <i>31st International Conference on Concurrency Theory</i>, vol. 171, 23, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020, doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2020.23\">10.4230/LIPIcs.CONCUR.2020.23</a>.","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.","ama":"Chatterjee K, Henzinger TA, Otop J. Multi-dimensional long-run average problems for vector addition systems with states. In: <i>31st International Conference on Concurrency Theory</i>. Vol 171. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2020. doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2020.23\">10.4230/LIPIcs.CONCUR.2020.23</a>"},"type":"conference","month":"08","oa_version":"Published Version","date_updated":"2021-01-12T08:20:15Z","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."}],"volume":171,"date_created":"2020-10-04T22:01:36Z","file_date_updated":"2020-10-05T14:04:25Z","year":"2020","_id":"8600","publication_identifier":{"isbn":["9783959771603"],"issn":["18688969"]},"doi":"10.4230/LIPIcs.CONCUR.2020.23","quality_controlled":"1","project":[{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"_id":"25F2ACDE-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S11402-N23"},{"grant_number":"Z211","name":"The Wittgenstein Prize","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425"}],"conference":{"start_date":"2020-09-01","location":"Virtual","name":"CONCUR: Conference on Concurrency Theory","end_date":"2020-09-04"},"language":[{"iso":"eng"}],"author":[{"last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-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"},{"last_name":"Otop","first_name":"Jan","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","full_name":"Otop, Jan"}],"day":"06","file":[{"file_name":"2020_LIPIcsCONCUR_Chatterjee.pdf","success":1,"file_size":601231,"relation":"main_file","content_type":"application/pdf","creator":"dernst","file_id":"8610","date_updated":"2020-10-05T14:04:25Z","checksum":"5039752f644c4b72b9361d21a5e31baf","date_created":"2020-10-05T14:04:25Z","access_level":"open_access"}],"article_number":"23","title":"Multi-dimensional long-run average problems for vector addition systems with states","arxiv":1,"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"publication":"31st International Conference on Concurrency Theory","tmp":{"short":"CC BY (3.0)","name":"Creative Commons Attribution 3.0 Unported (CC BY 3.0)","legal_code_url":"https://creativecommons.org/licenses/by/3.0/legalcode","image":"/images/cc_by.png"},"article_processing_charge":"No","scopus_import":"1"},{"_id":"86","year":"2018","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.","date_created":"2018-12-11T11:44:33Z","file_date_updated":"2020-07-14T12:48:14Z","volume":10760,"type":"book_chapter","month":"07","oa_version":"Submitted Version","date_updated":"2021-01-12T08:20:14Z","abstract":[{"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.","lang":"eng"}],"page":"143 - 161","citation":{"ieee":"K. Chatterjee, T. A. Henzinger, and J. Otop, “Computing average response time,” in <i>Principles of Modeling</i>, vol. 10760, M. Lohstroh, P. Derler, and M. Sirjani, Eds. Springer, 2018, pp. 143–161.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. “Computing Average Response Time.” In <i>Principles of Modeling</i>, edited by Marten Lohstroh, Patricia Derler, and Marjan Sirjani, 10760:143–61. Springer, 2018. <a href=\"https://doi.org/10.1007/978-3-319-95246-8_9\">https://doi.org/10.1007/978-3-319-95246-8_9</a>.","short":"K. Chatterjee, T.A. Henzinger, J. Otop, in:, M. Lohstroh, P. Derler, M. Sirjani (Eds.), Principles of Modeling, Springer, 2018, pp. 143–161.","ama":"Chatterjee K, Henzinger TA, Otop J. Computing average response time. In: Lohstroh M, Derler P, Sirjani M, eds. <i>Principles of Modeling</i>. Vol 10760. Springer; 2018:143-161. doi:<a href=\"https://doi.org/10.1007/978-3-319-95246-8_9\">10.1007/978-3-319-95246-8_9</a>","mla":"Chatterjee, Krishnendu, et al. “Computing Average Response Time.” <i>Principles of Modeling</i>, edited by Marten Lohstroh et al., vol. 10760, Springer, 2018, pp. 143–61, doi:<a href=\"https://doi.org/10.1007/978-3-319-95246-8_9\">10.1007/978-3-319-95246-8_9</a>.","ista":"Chatterjee K, Henzinger TA, Otop J. 2018.Computing average response time. In: Principles of Modeling. LNCS, vol. 10760, 143–161.","apa":"Chatterjee, K., Henzinger, T. A., &#38; Otop, J. (2018). Computing average response time. In M. Lohstroh, P. Derler, &#38; M. Sirjani (Eds.), <i>Principles of Modeling</i> (Vol. 10760, pp. 143–161). Springer. <a href=\"https://doi.org/10.1007/978-3-319-95246-8_9\">https://doi.org/10.1007/978-3-319-95246-8_9</a>"},"intvolume":"     10760","status":"public","editor":[{"last_name":"Lohstroh","first_name":"Marten","full_name":"Lohstroh, Marten"},{"full_name":"Derler, Patricia","last_name":"Derler","first_name":"Patricia"},{"full_name":"Sirjani, Marjan","last_name":"Sirjani","first_name":"Marjan"}],"alternative_title":["LNCS"],"date_published":"2018-07-20T00:00:00Z","ddc":["000"],"has_accepted_license":"1","oa":1,"publication_status":"published","ec_funded":1,"scopus_import":1,"publication":"Principles of Modeling","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"publisher":"Springer","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publist_id":"7968","title":"Computing average response time","day":"20","file":[{"creator":"dernst","file_size":516307,"relation":"main_file","content_type":"application/pdf","file_name":"2018_PrinciplesModeling_Chatterjee.pdf","access_level":"open_access","date_created":"2019-11-19T08:22:18Z","checksum":"9995c6ce6957333baf616fc4f20be597","file_id":"7053","date_updated":"2020-07-14T12:48:14Z"}],"author":[{"first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu"},{"full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A"},{"first_name":"Jan","last_name":"Otop","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","full_name":"Otop, Jan"}],"language":[{"iso":"eng"}],"project":[{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"grant_number":"S11407","name":"Game Theory","_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"grant_number":"Z211","name":"The Wittgenstein Prize","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425"},{"name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"279307"},{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","name":"Efficient Algorithms for Computer Aided Verification","grant_number":"ICT15-003"}],"quality_controlled":"1","doi":"10.1007/978-3-319-95246-8_9"},{"publisher":"Elsevier","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"publication":"Information and Computation","scopus_import":"1","article_processing_charge":"No","ec_funded":1,"author":[{"first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"},{"first_name":"Thomas A","last_name":"Henzinger","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"},{"id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","full_name":"Otop, Jan","last_name":"Otop","first_name":"Jan"},{"full_name":"Velner, Yaron","first_name":"Yaron","last_name":"Velner"}],"day":"01","title":"Quantitative fair simulation games","publist_id":"6322","project":[{"name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"279307"},{"name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"267989"},{"name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"P 23499-N23"},{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"isi":1,"issue":"2","language":[{"iso":"eng"}],"doi":"10.1016/j.ic.2016.10.006","quality_controlled":"1","year":"2017","_id":"1066","page":"143 - 166","month":"06","oa_version":"None","type":"journal_article","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."}],"date_updated":"2023-09-20T12:07:48Z","volume":254,"date_created":"2018-12-11T11:49:58Z","status":"public","external_id":{"isi":["000402025600002"]},"intvolume":"       254","related_material":{"record":[{"status":"public","id":"5428","relation":"earlier_version"}]},"citation":{"ama":"Chatterjee K, Henzinger TA, Otop J, Velner Y. Quantitative fair simulation games. <i>Information and Computation</i>. 2017;254(2):143-166. doi:<a href=\"https://doi.org/10.1016/j.ic.2016.10.006\">10.1016/j.ic.2016.10.006</a>","mla":"Chatterjee, Krishnendu, et al. “Quantitative Fair Simulation Games.” <i>Information and Computation</i>, vol. 254, no. 2, Elsevier, 2017, pp. 143–66, doi:<a href=\"https://doi.org/10.1016/j.ic.2016.10.006\">10.1016/j.ic.2016.10.006</a>.","ista":"Chatterjee K, Henzinger TA, Otop J, Velner Y. 2017. Quantitative fair simulation games. Information and Computation. 254(2), 143–166.","apa":"Chatterjee, K., Henzinger, T. A., Otop, J., &#38; Velner, Y. (2017). Quantitative fair simulation games. <i>Information and Computation</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.ic.2016.10.006\">https://doi.org/10.1016/j.ic.2016.10.006</a>","ieee":"K. Chatterjee, T. A. Henzinger, J. Otop, and Y. Velner, “Quantitative fair simulation games,” <i>Information and Computation</i>, vol. 254, no. 2. Elsevier, pp. 143–166, 2017.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, Jan Otop, and Yaron Velner. “Quantitative Fair Simulation Games.” <i>Information and Computation</i>. Elsevier, 2017. <a href=\"https://doi.org/10.1016/j.ic.2016.10.006\">https://doi.org/10.1016/j.ic.2016.10.006</a>.","short":"K. Chatterjee, T.A. Henzinger, J. Otop, Y. Velner, Information and Computation 254 (2017) 143–166."},"publication_status":"published","date_published":"2017-06-01T00:00:00Z"},{"publication":"ACM Transactions on Computational Logic (TOCL)","ec_funded":1,"scopus_import":1,"publisher":"ACM","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"title":"Nested weighted automata","arxiv":1,"article_number":"31","publist_id":"7354","author":[{"full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","last_name":"Chatterjee"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger","first_name":"Thomas A"},{"first_name":"Jan","last_name":"Otop","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","full_name":"Otop, Jan"}],"day":"01","language":[{"iso":"eng"}],"issue":"4","project":[{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"name":"The Wittgenstein Prize","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"Z211"},{"grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"doi":"10.1145/3152769","quality_controlled":"1","publication_identifier":{"issn":["15293785"]},"_id":"467","year":"2017","volume":18,"date_created":"2018-12-11T11:46:38Z","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."}],"date_updated":"2023-02-23T12:26:19Z","type":"journal_article","oa_version":"Preprint","month":"12","intvolume":"        18","related_material":{"record":[{"relation":"earlier_version","id":"1656","status":"public"},{"id":"5415","status":"public","relation":"earlier_version"},{"id":"5436","status":"public","relation":"earlier_version"}]},"citation":{"short":"K. Chatterjee, T.A. Henzinger, J. Otop, ACM Transactions on Computational Logic (TOCL) 18 (2017).","ieee":"K. Chatterjee, T. A. Henzinger, and J. Otop, “Nested weighted automata,” <i>ACM Transactions on Computational Logic (TOCL)</i>, vol. 18, no. 4. ACM, 2017.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. “Nested Weighted Automata.” <i>ACM Transactions on Computational Logic (TOCL)</i>. ACM, 2017. <a href=\"https://doi.org/10.1145/3152769\">https://doi.org/10.1145/3152769</a>.","mla":"Chatterjee, Krishnendu, et al. “Nested Weighted Automata.” <i>ACM Transactions on Computational Logic (TOCL)</i>, vol. 18, no. 4, 31, ACM, 2017, doi:<a href=\"https://doi.org/10.1145/3152769\">10.1145/3152769</a>.","ista":"Chatterjee K, Henzinger TA, Otop J. 2017. Nested weighted automata. ACM Transactions on Computational Logic (TOCL). 18(4), 31.","apa":"Chatterjee, K., Henzinger, T. A., &#38; Otop, J. (2017). Nested weighted automata. <i>ACM Transactions on Computational Logic (TOCL)</i>. ACM. <a href=\"https://doi.org/10.1145/3152769\">https://doi.org/10.1145/3152769</a>","ama":"Chatterjee K, Henzinger TA, Otop J. Nested weighted automata. <i>ACM Transactions on Computational Logic (TOCL)</i>. 2017;18(4). doi:<a href=\"https://doi.org/10.1145/3152769\">10.1145/3152769</a>"},"external_id":{"arxiv":["1606.03598"]},"status":"public","date_published":"2017-12-01T00:00:00Z","main_file_link":[{"url":"https://arxiv.org/abs/1606.03598","open_access":"1"}],"publication_status":"published","oa":1},{"publist_id":"6154","title":"Model measuring for discrete and hybrid systems","day":"01","author":[{"first_name":"Thomas A","last_name":"Henzinger","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Otop, Jan","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","last_name":"Otop","first_name":"Jan"}],"scopus_import":"1","article_processing_charge":"No","ec_funded":1,"publication":"Nonlinear Analysis: Hybrid Systems","department":[{"_id":"ToHe"}],"publisher":"Elsevier","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","quality_controlled":"1","doi":"10.1016/j.nahs.2016.09.001","language":[{"iso":"eng"}],"isi":1,"project":[{"name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"267989"},{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"The Wittgenstein Prize","grant_number":"Z211"}],"date_created":"2018-12-11T11:50:39Z","volume":23,"month":"02","type":"journal_article","oa_version":"None","date_updated":"2023-09-20T11:18:50Z","abstract":[{"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.","lang":"eng"}],"page":"166 - 190","_id":"1196","year":"2017","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/","date_published":"2017-02-01T00:00:00Z","publication_status":"published","citation":{"apa":"Henzinger, T. A., &#38; Otop, J. (2017). Model measuring for discrete and hybrid systems. <i>Nonlinear Analysis: Hybrid Systems</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.nahs.2016.09.001\">https://doi.org/10.1016/j.nahs.2016.09.001</a>","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.” <i>Nonlinear Analysis: Hybrid Systems</i>, vol. 23, Elsevier, 2017, pp. 166–90, doi:<a href=\"https://doi.org/10.1016/j.nahs.2016.09.001\">10.1016/j.nahs.2016.09.001</a>.","ama":"Henzinger TA, Otop J. Model measuring for discrete and hybrid systems. <i>Nonlinear Analysis: Hybrid Systems</i>. 2017;23:166-190. doi:<a href=\"https://doi.org/10.1016/j.nahs.2016.09.001\">10.1016/j.nahs.2016.09.001</a>","short":"T.A. Henzinger, J. Otop, Nonlinear Analysis: Hybrid Systems 23 (2017) 166–190.","chicago":"Henzinger, Thomas A, and Jan Otop. “Model Measuring for Discrete and Hybrid Systems.” <i>Nonlinear Analysis: Hybrid Systems</i>. Elsevier, 2017. <a href=\"https://doi.org/10.1016/j.nahs.2016.09.001\">https://doi.org/10.1016/j.nahs.2016.09.001</a>.","ieee":"T. A. Henzinger and J. Otop, “Model measuring for discrete and hybrid systems,” <i>Nonlinear Analysis: Hybrid Systems</i>, vol. 23. Elsevier, pp. 166–190, 2017."},"intvolume":"        23","external_id":{"isi":["000390637000011"]},"status":"public"},{"alternative_title":["LIPIcs"],"status":"public","intvolume":"        58","citation":{"short":"K. Chatterjee, T.A. Henzinger, J. Otop, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016.","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. <a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2016.24\">https://doi.org/10.4230/LIPIcs.MFCS.2016.24</a>.","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.","apa":"Chatterjee, K., Henzinger, T. A., &#38; 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. <a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2016.24\">https://doi.org/10.4230/LIPIcs.MFCS.2016.24</a>","mla":"Chatterjee, Krishnendu, et al. <i>Nested Weighted Limit-Average Automata of Bounded Width</i>. Vol. 58, 24, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016, doi:<a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2016.24\">10.4230/LIPIcs.MFCS.2016.24</a>.","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.","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:<a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2016.24\">10.4230/LIPIcs.MFCS.2016.24</a>"},"oa":1,"publication_status":"published","has_accepted_license":"1","ddc":["004"],"date_published":"2016-08-01T00:00:00Z","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.","year":"2016","_id":"1090","oa_version":"Published Version","month":"08","type":"conference","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."}],"date_updated":"2021-01-12T06:48:12Z","volume":58,"date_created":"2018-12-11T11:50:05Z","file_date_updated":"2018-12-12T10:17:31Z","project":[{"grant_number":"S 11407_N23","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering"},{"grant_number":"Z211","name":"The Wittgenstein Prize","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications"},{"grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification","_id":"25892FC0-B435-11E9-9278-68D0E5697425"}],"conference":{"start_date":"2016-08-22","location":"Krakow; Poland","name":"MFCS: Mathematical Foundations of Computer Science (SG)","end_date":"2016-08-26"},"language":[{"iso":"eng"}],"pubrep_id":"795","doi":"10.4230/LIPIcs.MFCS.2016.24","quality_controlled":"1","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"ec_funded":1,"scopus_import":1,"author":[{"last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger"},{"last_name":"Otop","first_name":"Jan","full_name":"Otop, Jan","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87"}],"file":[{"file_name":"IST-2017-795-v1+1_LIPIcs-MFCS-2016-24.pdf","creator":"system","file_size":564560,"content_type":"application/pdf","relation":"main_file","file_id":"5286","date_updated":"2018-12-12T10:17:31Z","access_level":"open_access","date_created":"2018-12-12T10:17:31Z"}],"day":"01","article_number":"24","title":"Nested weighted limit-average automata of bounded width","publist_id":"6286"},{"_id":"1138","year":"2016","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","date_created":"2018-12-11T11:50:21Z","date_updated":"2021-01-12T06:48:34Z","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."}],"oa_version":"Preprint","month":"07","type":"conference","page":"76 - 85","citation":{"apa":"Chatterjee, K., Henzinger, T. A., &#38; Otop, J. (2016). Quantitative automata under probabilistic semantics. In <i>Proceedings of the 31st Annual ACM/IEEE Symposium</i> (pp. 76–85). New York, NY, USA: IEEE. <a href=\"https://doi.org/10.1145/2933575.2933588\">https://doi.org/10.1145/2933575.2933588</a>","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.” <i>Proceedings of the 31st Annual ACM/IEEE Symposium</i>, IEEE, 2016, pp. 76–85, doi:<a href=\"https://doi.org/10.1145/2933575.2933588\">10.1145/2933575.2933588</a>.","ama":"Chatterjee K, Henzinger TA, Otop J. Quantitative automata under probabilistic semantics. In: <i>Proceedings of the 31st Annual ACM/IEEE Symposium</i>. IEEE; 2016:76-85. doi:<a href=\"https://doi.org/10.1145/2933575.2933588\">10.1145/2933575.2933588</a>","short":"K. Chatterjee, T.A. Henzinger, J. Otop, in:, Proceedings of the 31st Annual ACM/IEEE Symposium, IEEE, 2016, pp. 76–85.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. “Quantitative Automata under Probabilistic Semantics.” In <i>Proceedings of the 31st Annual ACM/IEEE Symposium</i>, 76–85. IEEE, 2016. <a href=\"https://doi.org/10.1145/2933575.2933588\">https://doi.org/10.1145/2933575.2933588</a>.","ieee":"K. Chatterjee, T. A. Henzinger, and J. Otop, “Quantitative automata under probabilistic semantics,” in <i>Proceedings of the 31st Annual ACM/IEEE Symposium</i>, New York, NY, USA, 2016, pp. 76–85."},"external_id":{"arxiv":["1604.06764"]},"status":"public","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1604.06764"}],"date_published":"2016-07-05T00:00:00Z","oa":1,"publication_status":"published","ec_funded":1,"scopus_import":1,"publication":"Proceedings of the 31st Annual ACM/IEEE Symposium","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"publisher":"IEEE","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publist_id":"6220","title":"Quantitative automata under probabilistic semantics","arxiv":1,"day":"05","author":[{"first_name":"Krishnendu","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger"},{"last_name":"Otop","first_name":"Jan","full_name":"Otop, Jan","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87"}],"language":[{"iso":"eng"}],"conference":{"end_date":"2016-07-08","location":"New York, NY, USA","name":"LICS: Logic in Computer Science","start_date":"2016-07-05"},"project":[{"grant_number":"267989","name":"Quantitative Reactive Modeling","call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"The Wittgenstein Prize"},{"grant_number":"P 23499-N23","call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"grant_number":"ICT15-003","_id":"25892FC0-B435-11E9-9278-68D0E5697425","name":"Efficient Algorithms for Computer Aided Verification"}],"quality_controlled":"1","doi":"10.1145/2933575.2933588"},{"publist_id":"5647","title":"Lipschitz robustness of timed I/O systems","day":"01","author":[{"first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A"},{"last_name":"Otop","first_name":"Jan","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","full_name":"Otop, Jan"},{"full_name":"Samanta, Roopsha","id":"3D2AAC08-F248-11E8-B48F-1D18A9856A87","last_name":"Samanta","first_name":"Roopsha"}],"ec_funded":1,"scopus_import":1,"department":[{"_id":"ToHe"}],"publisher":"Springer","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","quality_controlled":"1","doi":"10.1007/978-3-662-49122-5_12","language":[{"iso":"eng"}],"conference":{"end_date":"2016-01-19","start_date":"2016-01-17","location":"St. Petersburg, FL, USA","name":"VMCAI: Verification, Model Checking and Abstract Interpretation"},"project":[{"grant_number":"267989","call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling"},{"grant_number":"Z211","name":"The Wittgenstein Prize","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"}],"date_created":"2018-12-11T11:52:32Z","volume":9583,"month":"01","type":"conference","oa_version":"Preprint","abstract":[{"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.","lang":"eng"}],"date_updated":"2021-01-12T06:51:23Z","page":"250 - 267","_id":"1526","year":"2016","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.","main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1506.01233"}],"date_published":"2016-01-01T00:00:00Z","oa":1,"publication_status":"published","citation":{"chicago":"Henzinger, Thomas A, Jan Otop, and Roopsha Samanta. “Lipschitz Robustness of Timed I/O Systems,” 9583:250–67. Springer, 2016. <a href=\"https://doi.org/10.1007/978-3-662-49122-5_12\">https://doi.org/10.1007/978-3-662-49122-5_12</a>.","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.","short":"T.A. Henzinger, J. Otop, R. Samanta, in:, Springer, 2016, pp. 250–267.","ama":"Henzinger TA, Otop J, Samanta R. Lipschitz robustness of timed I/O systems. In: Vol 9583. Springer; 2016:250-267. doi:<a href=\"https://doi.org/10.1007/978-3-662-49122-5_12\">10.1007/978-3-662-49122-5_12</a>","apa":"Henzinger, T. A., Otop, J., &#38; 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. <a href=\"https://doi.org/10.1007/978-3-662-49122-5_12\">https://doi.org/10.1007/978-3-662-49122-5_12</a>","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. <i>Lipschitz Robustness of Timed I/O Systems</i>. Vol. 9583, Springer, 2016, pp. 250–67, doi:<a href=\"https://doi.org/10.1007/978-3-662-49122-5_12\">10.1007/978-3-662-49122-5_12</a>."},"intvolume":"      9583","status":"public","alternative_title":["LNCS"]},{"alternative_title":["LNCS"],"status":"public","intvolume":"      9837","citation":{"ama":"Chatterjee K, Henzinger TA, Otop J. Quantitative monitor automata. In: Vol 9837. Springer; 2016:23-38. doi:<a href=\"https://doi.org/10.1007/978-3-662-53413-7_2\">10.1007/978-3-662-53413-7_2</a>","apa":"Chatterjee, K., Henzinger, T. A., &#38; Otop, J. (2016). Quantitative monitor automata (Vol. 9837, pp. 23–38). Presented at the SAS: Static Analysis Symposium, Edinburgh, United Kingdom: Springer. <a href=\"https://doi.org/10.1007/978-3-662-53413-7_2\">https://doi.org/10.1007/978-3-662-53413-7_2</a>","mla":"Chatterjee, Krishnendu, et al. <i>Quantitative Monitor Automata</i>. Vol. 9837, Springer, 2016, pp. 23–38, doi:<a href=\"https://doi.org/10.1007/978-3-662-53413-7_2\">10.1007/978-3-662-53413-7_2</a>.","ista":"Chatterjee K, Henzinger TA, Otop J. 2016. Quantitative monitor automata. SAS: Static Analysis Symposium, LNCS, vol. 9837, 23–38.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. “Quantitative Monitor Automata,” 9837:23–38. Springer, 2016. <a href=\"https://doi.org/10.1007/978-3-662-53413-7_2\">https://doi.org/10.1007/978-3-662-53413-7_2</a>.","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.","short":"K. Chatterjee, T.A. Henzinger, J. Otop, in:, Springer, 2016, pp. 23–38."},"publication_status":"published","oa":1,"date_published":"2016-08-31T00:00:00Z","main_file_link":[{"url":"https://arxiv.org/abs/1604.06764","open_access":"1"}],"year":"2016","_id":"1335","page":"23 - 38","date_updated":"2021-01-12T06:49:58Z","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."}],"type":"conference","month":"08","oa_version":"Preprint","volume":9837,"date_created":"2018-12-11T11:51:26Z","project":[{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"grant_number":"Z211","name":"The Wittgenstein Prize","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"},{"name":"Efficient Algorithms for Computer Aided Verification","_id":"25892FC0-B435-11E9-9278-68D0E5697425","grant_number":"ICT15-003"}],"conference":{"start_date":"2016-09-08","location":"Edinburgh, United Kingdom","name":"SAS: Static Analysis Symposium","end_date":"2016-09-10"},"language":[{"iso":"eng"}],"doi":"10.1007/978-3-662-53413-7_2","quality_controlled":"1","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","publisher":"Springer","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"ec_funded":1,"scopus_import":1,"author":[{"last_name":"Chatterjee","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu"},{"full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","last_name":"Henzinger"},{"first_name":"Jan","last_name":"Otop","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","full_name":"Otop, Jan"}],"day":"31","title":"Quantitative monitor automata","publist_id":"5932"},{"publist_id":"5494","arxiv":1,"title":"Nested weighted automata","article_number":"7174926","day":"31","author":[{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee"},{"first_name":"Thomas A","last_name":"Henzinger","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Jan","last_name":"Otop","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","full_name":"Otop, Jan"}],"scopus_import":1,"ec_funded":1,"publication":"Proceedings - Symposium on Logic in Computer Science","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publisher":"IEEE","quality_controlled":"1","doi":"10.1109/LICS.2015.72","language":[{"iso":"eng"}],"conference":{"end_date":"2015-07-10","start_date":"2015-07-06","location":"Kyoto, Japan","name":"LICS: Logic in Computer Science"},"project":[{"name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"267989"},{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"grant_number":"Z211","name":"The Wittgenstein Prize","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"date_created":"2018-12-11T11:53:17Z","volume":"2015-July","date_updated":"2023-02-23T12:26:19Z","abstract":[{"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.","lang":"eng"}],"type":"conference","month":"07","oa_version":"None","_id":"1656","year":"2015","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","date_published":"2015-07-31T00:00:00Z","publication_status":"published","citation":{"short":"K. Chatterjee, T.A. Henzinger, J. Otop, in:, Proceedings - Symposium on Logic in Computer Science, IEEE, 2015.","ieee":"K. Chatterjee, T. A. Henzinger, and J. Otop, “Nested weighted automata,” in <i>Proceedings - Symposium on Logic in Computer Science</i>, Kyoto, Japan, 2015, vol. 2015–July.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. “Nested Weighted Automata.” In <i>Proceedings - Symposium on Logic in Computer Science</i>, Vol. 2015–July. IEEE, 2015. <a href=\"https://doi.org/10.1109/LICS.2015.72\">https://doi.org/10.1109/LICS.2015.72</a>.","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.” <i>Proceedings - Symposium on Logic in Computer Science</i>, vol. 2015–July, 7174926, IEEE, 2015, doi:<a href=\"https://doi.org/10.1109/LICS.2015.72\">10.1109/LICS.2015.72</a>.","apa":"Chatterjee, K., Henzinger, T. A., &#38; Otop, J. (2015). Nested weighted automata. In <i>Proceedings - Symposium on Logic in Computer Science</i> (Vol. 2015–July). Kyoto, Japan: IEEE. <a href=\"https://doi.org/10.1109/LICS.2015.72\">https://doi.org/10.1109/LICS.2015.72</a>","ama":"Chatterjee K, Henzinger TA, Otop J. Nested weighted automata. In: <i>Proceedings - Symposium on Logic in Computer Science</i>. Vol 2015-July. IEEE; 2015. doi:<a href=\"https://doi.org/10.1109/LICS.2015.72\">10.1109/LICS.2015.72</a>"},"related_material":{"record":[{"status":"public","id":"467","relation":"later_version"},{"status":"public","id":"5415","relation":"earlier_version"},{"status":"public","id":"5436","relation":"earlier_version"}]},"status":"public","external_id":{"arxiv":["1606.03598"]}},{"date_updated":"2023-02-23T12:26:27Z","abstract":[{"text":"The target discounted-sum problem is the following: Given a rational discount factor 0 &lt; λ &lt; 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.","lang":"eng"}],"oa_version":"Submitted Version","type":"conference","month":"07","page":"750 - 761","file_date_updated":"2020-07-14T12:45:10Z","date_created":"2018-12-11T11:53:19Z","year":"2015","acknowledgement":"A technical report of the article is available at: https://research-explorer.app.ist.ac.at/record/5439","_id":"1659","has_accepted_license":"1","oa":1,"publication_status":"published","ddc":["000"],"date_published":"2015-07-01T00:00:00Z","status":"public","citation":{"short":"U. Boker, T.A. Henzinger, J. Otop, in:, LICS, IEEE, 2015, pp. 750–761.","chicago":"Boker, Udi, Thomas A Henzinger, and Jan Otop. “The Target Discounted-Sum Problem.” In <i>LICS</i>, 750–61. Logic in Computer Science. IEEE, 2015. <a href=\"https://doi.org/10.1109/LICS.2015.74\">https://doi.org/10.1109/LICS.2015.74</a>.","ieee":"U. Boker, T. A. Henzinger, and J. Otop, “The target discounted-sum problem,” in <i>LICS</i>, Kyoto, Japan, 2015, pp. 750–761.","apa":"Boker, U., Henzinger, T. A., &#38; Otop, J. (2015). The target discounted-sum problem. In <i>LICS</i> (pp. 750–761). Kyoto, Japan: IEEE. <a href=\"https://doi.org/10.1109/LICS.2015.74\">https://doi.org/10.1109/LICS.2015.74</a>","mla":"Boker, Udi, et al. “The Target Discounted-Sum Problem.” <i>LICS</i>, IEEE, 2015, pp. 750–61, doi:<a href=\"https://doi.org/10.1109/LICS.2015.74\">10.1109/LICS.2015.74</a>.","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: <i>LICS</i>. Logic in Computer Science. IEEE; 2015:750-761. doi:<a href=\"https://doi.org/10.1109/LICS.2015.74\">10.1109/LICS.2015.74</a>"},"related_material":{"record":[{"id":"5439","status":"public","relation":"earlier_version"}]},"day":"01","file":[{"access_level":"open_access","date_created":"2020-05-15T08:53:29Z","checksum":"6abebca9c1a620e9e103a8f9222befac","file_id":"7852","date_updated":"2020-07-14T12:45:10Z","creator":"dernst","file_size":340215,"relation":"main_file","content_type":"application/pdf","file_name":"2015_LICS_Boker.pdf"}],"author":[{"full_name":"Boker, Udi","id":"31E297B6-F248-11E8-B48F-1D18A9856A87","first_name":"Udi","last_name":"Boker"},{"first_name":"Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A"},{"id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","full_name":"Otop, Jan","last_name":"Otop","first_name":"Jan"}],"publist_id":"5491","title":"The target discounted-sum problem","department":[{"_id":"ToHe"}],"publisher":"IEEE","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","ec_funded":1,"scopus_import":1,"article_processing_charge":"No","publication":"LICS","publication_identifier":{"issn":["1043-6871 "],"eisbn":["978-1-4799-8875-4 "]},"quality_controlled":"1","doi":"10.1109/LICS.2015.74","project":[{"name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"267989"},{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"The Wittgenstein Prize","grant_number":"Z211"}],"language":[{"iso":"eng"}],"series_title":"Logic in Computer Science","conference":{"start_date":"2015-007-06","location":"Kyoto, Japan","name":"LICS: Logic in Computer Science","end_date":"2015-07-10"}},{"title":"On the decidability of elementary modal logics","volume":17,"article_number":"2","publist_id":"5468","date_created":"2018-12-11T11:53:26Z","author":[{"full_name":"Michaliszyn, Jakub","last_name":"Michaliszyn","first_name":"Jakub"},{"id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","full_name":"Otop, Jan","last_name":"Otop","first_name":"Jan"},{"full_name":"Kieroňski, Emanuel","last_name":"Kieroňski","first_name":"Emanuel"}],"day":"01","abstract":[{"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.","lang":"eng"}],"date_updated":"2021-01-12T06:52:29Z","month":"09","type":"journal_article","oa_version":"None","publication":"ACM Transactions on Computational Logic","_id":"1680","ec_funded":1,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publisher":"ACM","year":"2015","department":[{"_id":"ToHe"}],"date_published":"2015-09-01T00:00:00Z","doi":"10.1145/2817825","quality_controlled":"1","publication_status":"published","intvolume":"        17","language":[{"iso":"eng"}],"citation":{"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.” <i>ACM Transactions on Computational Logic</i>, vol. 17, no. 1, 2, ACM, 2015, doi:<a href=\"https://doi.org/10.1145/2817825\">10.1145/2817825</a>.","apa":"Michaliszyn, J., Otop, J., &#38; Kieroňski, E. (2015). On the decidability of elementary modal logics. <i>ACM Transactions on Computational Logic</i>. ACM. <a href=\"https://doi.org/10.1145/2817825\">https://doi.org/10.1145/2817825</a>","ama":"Michaliszyn J, Otop J, Kieroňski E. On the decidability of elementary modal logics. <i>ACM Transactions on Computational Logic</i>. 2015;17(1). doi:<a href=\"https://doi.org/10.1145/2817825\">10.1145/2817825</a>","short":"J. Michaliszyn, J. Otop, E. Kieroňski, ACM Transactions on Computational Logic 17 (2015).","ieee":"J. Michaliszyn, J. Otop, and E. Kieroňski, “On the decidability of elementary modal logics,” <i>ACM Transactions on Computational Logic</i>, vol. 17, no. 1. ACM, 2015.","chicago":"Michaliszyn, Jakub, Jan Otop, and Emanuel Kieroňski. “On the Decidability of Elementary Modal Logics.” <i>ACM Transactions on Computational Logic</i>. ACM, 2015. <a href=\"https://doi.org/10.1145/2817825\">https://doi.org/10.1145/2817825</a>."},"issue":"1","project":[{"call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling","grant_number":"267989"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"grant_number":"Z211","name":"The Wittgenstein Prize","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"status":"public"},{"language":[{"iso":"eng"}],"citation":{"mla":"Chatterjee, Krishnendu, et al. <i>Nested Weighted Automata</i>. IST Austria, 2015, doi:<a href=\"https://doi.org/10.15479/AT:IST-2015-170-v2-2\">10.15479/AT:IST-2015-170-v2-2</a>.","ista":"Chatterjee K, Henzinger TA, Otop J. 2015. Nested weighted automata, IST Austria, 29p.","apa":"Chatterjee, K., Henzinger, T. A., &#38; Otop, J. (2015). <i>Nested weighted automata</i>. IST Austria. <a href=\"https://doi.org/10.15479/AT:IST-2015-170-v2-2\">https://doi.org/10.15479/AT:IST-2015-170-v2-2</a>","ama":"Chatterjee K, Henzinger TA, Otop J. <i>Nested Weighted Automata</i>. IST Austria; 2015. doi:<a href=\"https://doi.org/10.15479/AT:IST-2015-170-v2-2\">10.15479/AT:IST-2015-170-v2-2</a>","short":"K. Chatterjee, T.A. Henzinger, J. Otop, Nested Weighted Automata, IST Austria, 2015.","ieee":"K. Chatterjee, T. A. Henzinger, and J. Otop, <i>Nested weighted automata</i>. IST Austria, 2015.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. <i>Nested Weighted Automata</i>. IST Austria, 2015. <a href=\"https://doi.org/10.15479/AT:IST-2015-170-v2-2\">https://doi.org/10.15479/AT:IST-2015-170-v2-2</a>."},"related_material":{"record":[{"relation":"later_version","id":"1656","status":"public"},{"relation":"later_version","id":"467","status":"public"},{"status":"public","id":"5415","relation":"earlier_version"}]},"status":"public","alternative_title":["IST Austria Technical Report"],"ddc":["000"],"date_published":"2015-04-24T00:00:00Z","doi":"10.15479/AT:IST-2015-170-v2-2","has_accepted_license":"1","pubrep_id":"331","publication_identifier":{"issn":["2664-1690"]},"publication_status":"published","oa":1,"_id":"5436","year":"2015","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publisher":"IST Austria","date_created":"2018-12-12T11:39:19Z","file_date_updated":"2020-07-14T12:46:54Z","title":"Nested weighted automata","month":"04","oa_version":"Published Version","type":"technical_report","day":"24","date_updated":"2023-02-23T12:25:21Z","file":[{"file_name":"IST-2015-170-v2+2_report.pdf","creator":"system","file_size":569991,"relation":"main_file","content_type":"application/pdf","checksum":"3c402f47d3669c28d04d1af405a08e3f","file_id":"5541","date_updated":"2020-07-14T12:46:54Z","access_level":"open_access","date_created":"2018-12-12T11:54:19Z"}],"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."}],"author":[{"last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"},{"full_name":"Otop, Jan","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","last_name":"Otop","first_name":"Jan"}],"page":"29"},{"ddc":["004"],"doi":"10.15479/AT:IST-2015-334-v1-1","date_published":"2015-05-05T00:00:00Z","has_accepted_license":"1","pubrep_id":"334","publication_identifier":{"issn":["2664-1690"]},"oa":1,"publication_status":"published","language":[{"iso":"eng"}],"citation":{"ista":"Chatterjee K, Henzinger TA, Ibsen-Jensen R, Otop J. 2015. Edit distance for pushdown automata, IST Austria, 15p.","mla":"Chatterjee, Krishnendu, et al. <i>Edit Distance for Pushdown Automata</i>. IST Austria, 2015, doi:<a href=\"https://doi.org/10.15479/AT:IST-2015-334-v1-1\">10.15479/AT:IST-2015-334-v1-1</a>.","apa":"Chatterjee, K., Henzinger, T. A., Ibsen-Jensen, R., &#38; Otop, J. (2015). <i>Edit distance for pushdown automata</i>. IST Austria. <a href=\"https://doi.org/10.15479/AT:IST-2015-334-v1-1\">https://doi.org/10.15479/AT:IST-2015-334-v1-1</a>","ama":"Chatterjee K, Henzinger TA, Ibsen-Jensen R, Otop J. <i>Edit Distance for Pushdown Automata</i>. IST Austria; 2015. doi:<a href=\"https://doi.org/10.15479/AT:IST-2015-334-v1-1\">10.15479/AT:IST-2015-334-v1-1</a>","short":"K. Chatterjee, T.A. Henzinger, R. Ibsen-Jensen, J. Otop, Edit Distance for Pushdown Automata, IST Austria, 2015.","ieee":"K. Chatterjee, T. A. Henzinger, R. Ibsen-Jensen, and J. Otop, <i>Edit distance for pushdown automata</i>. IST Austria, 2015.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, Rasmus Ibsen-Jensen, and Jan Otop. <i>Edit Distance for Pushdown Automata</i>. IST Austria, 2015. <a href=\"https://doi.org/10.15479/AT:IST-2015-334-v1-1\">https://doi.org/10.15479/AT:IST-2015-334-v1-1</a>."},"related_material":{"record":[{"id":"1610","status":"public","relation":"later_version"},{"status":"public","id":"465","relation":"later_version"}]},"status":"public","alternative_title":["IST Austria Technical Report"],"file_date_updated":"2020-07-14T12:46:55Z","date_created":"2018-12-12T11:39:20Z","title":"Edit distance for pushdown automata","type":"technical_report","oa_version":"Published Version","month":"05","day":"05","date_updated":"2023-02-23T12:20:08Z","file":[{"creator":"system","relation":"main_file","content_type":"application/pdf","file_size":422573,"file_name":"IST-2015-334-v1+1_report.pdf","access_level":"open_access","date_created":"2018-12-12T11:53:56Z","checksum":"8a5f2d77560e552af87eb1982437a43b","date_updated":"2020-07-14T12:46:55Z","file_id":"5518"}],"abstract":[{"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. ","lang":"eng"}],"author":[{"last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"},{"id":"3B699956-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-4783-0389","full_name":"Ibsen-Jensen, Rasmus","first_name":"Rasmus","last_name":"Ibsen-Jensen"},{"last_name":"Otop","first_name":"Jan","full_name":"Otop, Jan","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87"}],"page":"15","_id":"5438","department":[{"_id":"KrCh"}],"year":"2015","publisher":"IST Austria","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87"},{"alternative_title":["IST Austria Technical Report"],"status":"public","related_material":{"record":[{"id":"1659","status":"public","relation":"later_version"}]},"language":[{"iso":"eng"}],"citation":{"apa":"Boker, U., Henzinger, T. A., &#38; Otop, J. (2015). <i>The target discounted-sum problem</i>. IST Austria. <a href=\"https://doi.org/10.15479/AT:IST-2015-335-v1-1\">https://doi.org/10.15479/AT:IST-2015-335-v1-1</a>","mla":"Boker, Udi, et al. <i>The Target Discounted-Sum Problem</i>. IST Austria, 2015, doi:<a href=\"https://doi.org/10.15479/AT:IST-2015-335-v1-1\">10.15479/AT:IST-2015-335-v1-1</a>.","ista":"Boker U, Henzinger TA, Otop J. 2015. The target discounted-sum problem, IST Austria, 20p.","ama":"Boker U, Henzinger TA, Otop J. <i>The Target Discounted-Sum Problem</i>. IST Austria; 2015. doi:<a href=\"https://doi.org/10.15479/AT:IST-2015-335-v1-1\">10.15479/AT:IST-2015-335-v1-1</a>","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. <i>The Target Discounted-Sum Problem</i>. IST Austria, 2015. <a href=\"https://doi.org/10.15479/AT:IST-2015-335-v1-1\">https://doi.org/10.15479/AT:IST-2015-335-v1-1</a>.","ieee":"U. Boker, T. A. Henzinger, and J. Otop, <i>The target discounted-sum problem</i>. IST Austria, 2015."},"publication_identifier":{"issn":["2664-1690"]},"publication_status":"published","oa":1,"pubrep_id":"335","has_accepted_license":"1","ddc":["004","512","513"],"doi":"10.15479/AT:IST-2015-335-v1-1","date_published":"2015-05-18T00:00:00Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publisher":"IST Austria","year":"2015","department":[{"_id":"ToHe"}],"_id":"5439","author":[{"id":"31E297B6-F248-11E8-B48F-1D18A9856A87","full_name":"Boker, Udi","last_name":"Boker","first_name":"Udi"},{"full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","last_name":"Henzinger"},{"full_name":"Otop, Jan","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","last_name":"Otop","first_name":"Jan"}],"page":"20","type":"technical_report","oa_version":"Published Version","month":"05","date_updated":"2023-02-23T10:08:48Z","abstract":[{"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. ","lang":"eng"}],"day":"18","file":[{"checksum":"40405907aa012acece1bc26cf0be554d","file_id":"5517","date_updated":"2020-07-14T12:46:55Z","access_level":"open_access","date_created":"2018-12-12T11:53:55Z","file_name":"IST-2015-335-v1+1_report.pdf","creator":"system","file_size":589619,"relation":"main_file","content_type":"application/pdf"}],"title":"The target discounted-sum problem","date_created":"2018-12-12T11:39:20Z","file_date_updated":"2020-07-14T12:46:55Z"},{"project":[{"grant_number":"267989","name":"Quantitative Reactive Modeling","call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"The Wittgenstein Prize"},{"grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"grant_number":"S11407","call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425","name":"Game Theory"},{"grant_number":"279307","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"}],"language":[{"iso":"eng"}],"issue":"Part II","conference":{"start_date":"2015-07-06","location":"Kyoto, Japan","name":"ICALP: Automata, Languages and Programming","end_date":"2015-07-10"},"pubrep_id":"321","publication_identifier":{"isbn":["978-3-662-47665-9"]},"quality_controlled":"1","doi":"10.1007/978-3-662-47666-6_10","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","publisher":"Springer Nature","article_processing_charge":"No","scopus_import":"1","ec_funded":1,"publication":"42nd International Colloquium","day":"01","author":[{"full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger","first_name":"Thomas A"},{"first_name":"Rasmus","last_name":"Ibsen-Jensen","full_name":"Ibsen-Jensen, Rasmus","orcid":"0000-0003-4783-0389","id":"3B699956-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Otop, Jan","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","first_name":"Jan","last_name":"Otop"}],"publist_id":"5556","arxiv":1,"title":"Edit distance for pushdown automata","external_id":{"arxiv":["1504.08259"]},"status":"public","alternative_title":["LNCS"],"citation":{"chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, Rasmus Ibsen-Jensen, and Jan Otop. “Edit Distance for Pushdown Automata.” In <i>42nd International Colloquium</i>, 9135:121–33. Springer Nature, 2015. <a href=\"https://doi.org/10.1007/978-3-662-47666-6_10\">https://doi.org/10.1007/978-3-662-47666-6_10</a>.","ieee":"K. Chatterjee, T. A. Henzinger, R. Ibsen-Jensen, and J. Otop, “Edit distance for pushdown automata,” in <i>42nd International Colloquium</i>, Kyoto, Japan, 2015, vol. 9135, no. Part II, pp. 121–133.","short":"K. Chatterjee, T.A. Henzinger, R. Ibsen-Jensen, J. Otop, in:, 42nd International Colloquium, Springer Nature, 2015, pp. 121–133.","ama":"Chatterjee K, Henzinger TA, Ibsen-Jensen R, Otop J. Edit distance for pushdown automata. In: <i>42nd International Colloquium</i>. Vol 9135. Springer Nature; 2015:121-133. doi:<a href=\"https://doi.org/10.1007/978-3-662-47666-6_10\">10.1007/978-3-662-47666-6_10</a>","apa":"Chatterjee, K., Henzinger, T. A., Ibsen-Jensen, R., &#38; Otop, J. (2015). Edit distance for pushdown automata. In <i>42nd International Colloquium</i> (Vol. 9135, pp. 121–133). Kyoto, Japan: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-662-47666-6_10\">https://doi.org/10.1007/978-3-662-47666-6_10</a>","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.” <i>42nd International Colloquium</i>, vol. 9135, no. Part II, Springer Nature, 2015, pp. 121–33, doi:<a href=\"https://doi.org/10.1007/978-3-662-47666-6_10\">10.1007/978-3-662-47666-6_10</a>."},"intvolume":"      9135","related_material":{"record":[{"relation":"later_version","status":"public","id":"465"},{"id":"5438","status":"public","relation":"earlier_version"}]},"publication_status":"published","oa":1,"main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1504.08259"}],"date_published":"2015-07-01T00:00:00Z","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."}],"date_updated":"2023-02-23T12:26:24Z","oa_version":"None","month":"07","type":"conference","page":"121 - 133","date_created":"2018-12-11T11:53:01Z","volume":9135},{"author":[{"orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","last_name":"Henzinger","first_name":"Thomas A"},{"first_name":"Jan","last_name":"Otop","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","full_name":"Otop, Jan"},{"id":"3D2AAC08-F248-11E8-B48F-1D18A9856A87","full_name":"Samanta, Roopsha","last_name":"Samanta","first_name":"Roopsha"}],"file":[{"creator":"system","file_size":562151,"content_type":"application/pdf","relation":"main_file","file_name":"IST-2017-804-v1+1_37.pdf","access_level":"open_access","date_created":"2018-12-12T10:09:11Z","checksum":"7b1aff1710a8bffb7080ec07f62d9a17","file_id":"4734","date_updated":"2020-07-14T12:45:19Z"}],"day":"01","title":"Lipschitz robustness of finite-state transducers","publist_id":"5227","user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","department":[{"_id":"ToHe"}],"publication":"Leibniz International Proceedings in Informatics, LIPIcs","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"pubrep_id":"804","doi":"10.4230/LIPIcs.FSTTCS.2014.431","quality_controlled":"1","conference":{"location":"Delhi, India","name":"FSTTCS: Foundations of Software Technology and Theoretical Computer Science","start_date":"2014-12-15","end_date":"2014-12-17"},"language":[{"iso":"eng"}],"page":"431 - 443","date_updated":"2021-01-12T06:53:45Z","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."}],"oa_version":"Published Version","month":"12","type":"conference","volume":29,"date_created":"2018-12-11T11:54:27Z","file_date_updated":"2020-07-14T12:45:19Z","year":"2014","_id":"1870","publication_status":"published","oa":1,"has_accepted_license":"1","ddc":["004"],"date_published":"2014-12-01T00:00:00Z","alternative_title":["LIPIcs"],"status":"public","intvolume":"        29","citation":{"ieee":"T. A. Henzinger, J. Otop, and R. Samanta, “Lipschitz robustness of finite-state transducers,” in <i>Leibniz International Proceedings in Informatics, LIPIcs</i>, Delhi, India, 2014, vol. 29, pp. 431–443.","chicago":"Henzinger, Thomas A, Jan Otop, and Roopsha Samanta. “Lipschitz Robustness of Finite-State Transducers.” In <i>Leibniz International Proceedings in Informatics, LIPIcs</i>, 29:431–43. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2014. <a href=\"https://doi.org/10.4230/LIPIcs.FSTTCS.2014.431\">https://doi.org/10.4230/LIPIcs.FSTTCS.2014.431</a>.","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.","ama":"Henzinger TA, Otop J, Samanta R. Lipschitz robustness of finite-state transducers. In: <i>Leibniz International Proceedings in Informatics, LIPIcs</i>. Vol 29. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2014:431-443. doi:<a href=\"https://doi.org/10.4230/LIPIcs.FSTTCS.2014.431\">10.4230/LIPIcs.FSTTCS.2014.431</a>","mla":"Henzinger, Thomas A., et al. “Lipschitz Robustness of Finite-State Transducers.” <i>Leibniz International Proceedings in Informatics, LIPIcs</i>, vol. 29, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2014, pp. 431–43, doi:<a href=\"https://doi.org/10.4230/LIPIcs.FSTTCS.2014.431\">10.4230/LIPIcs.FSTTCS.2014.431</a>.","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.","apa":"Henzinger, T. A., Otop, J., &#38; Samanta, R. (2014). Lipschitz robustness of finite-state transducers. In <i>Leibniz International Proceedings in Informatics, LIPIcs</i> (Vol. 29, pp. 431–443). Delhi, India: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.FSTTCS.2014.431\">https://doi.org/10.4230/LIPIcs.FSTTCS.2014.431</a>"}},{"date_published":"2014-04-01T00:00:00Z","publication_status":"published","related_material":{"record":[{"id":"5416","status":"public","relation":"earlier_version"}]},"citation":{"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.” <i>Proceedings of the 17th International Conference on Hybrid Systems: Computation and Control</i>, Springer, 2014, pp. 213–22, doi:<a href=\"https://doi.org/10.1145/2562059.2562130\">10.1145/2562059.2562130</a>.","apa":"Henzinger, T. A., &#38; Otop, J. (2014). Model measuring for hybrid systems. In <i>Proceedings of the 17th international conference on Hybrid systems: computation and control</i> (pp. 213–222). Berlin, Germany: Springer. <a href=\"https://doi.org/10.1145/2562059.2562130\">https://doi.org/10.1145/2562059.2562130</a>","ama":"Henzinger TA, Otop J. Model measuring for hybrid systems. In: <i>Proceedings of the 17th International Conference on Hybrid Systems: Computation and Control</i>. Springer; 2014:213-222. doi:<a href=\"https://doi.org/10.1145/2562059.2562130\">10.1145/2562059.2562130</a>","short":"T.A. Henzinger, J. Otop, in:, Proceedings of the 17th International Conference on Hybrid Systems: Computation and Control, Springer, 2014, pp. 213–222.","ieee":"T. A. Henzinger and J. Otop, “Model measuring for hybrid systems,” in <i>Proceedings of the 17th international conference on Hybrid systems: computation and control</i>, Berlin, Germany, 2014, pp. 213–222.","chicago":"Henzinger, Thomas A, and Jan Otop. “Model Measuring for Hybrid Systems.” In <i>Proceedings of the 17th International Conference on Hybrid Systems: Computation and Control</i>, 213–22. Springer, 2014. <a href=\"https://doi.org/10.1145/2562059.2562130\">https://doi.org/10.1145/2562059.2562130</a>."},"status":"public","date_created":"2018-12-11T11:56:23Z","page":"213 - 222","month":"04","oa_version":"None","type":"conference","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."}],"date_updated":"2023-02-23T12:25:23Z","_id":"2217","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","year":"2014","doi":"10.1145/2562059.2562130","quality_controlled":"1","conference":{"start_date":"2014-04-15","location":"Berlin, Germany","name":"HSCC: Hybrid Systems - Computation and Control","end_date":"2014-04-17"},"language":[{"iso":"eng"}],"project":[{"name":"Quantitative Reactive Modeling","call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989"},{"grant_number":"S 11407_N23","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering"}],"title":"Model measuring for hybrid systems","publist_id":"4751","author":[{"full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A"},{"id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","full_name":"Otop, Jan","first_name":"Jan","last_name":"Otop"}],"day":"01","publication":"Proceedings of the 17th international conference on Hybrid systems: computation and control","scopus_import":1,"ec_funded":1,"article_processing_charge":"No","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publisher":"Springer","department":[{"_id":"ToHe"}]},{"month":"02","oa_version":"Published Version","type":"technical_report","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.  "}],"file":[{"file_name":"IST-2014-170-v1+1_main.pdf","content_type":"application/pdf","relation":"main_file","file_size":573457,"creator":"system","date_updated":"2020-07-14T12:46:48Z","file_id":"5497","checksum":"31f90dcf2cf899c3f8c6427cfcc2b3c7","date_created":"2018-12-12T11:53:36Z","access_level":"open_access"}],"day":"19","date_updated":"2023-02-23T12:26:19Z","author":[{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","first_name":"Krishnendu"},{"full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A"},{"last_name":"Otop","first_name":"Jan","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","full_name":"Otop, Jan"}],"page":"27","date_created":"2018-12-12T11:39:12Z","file_date_updated":"2020-07-14T12:46:48Z","title":"Nested weighted automata","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"year":"2014","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publisher":"IST Austria","_id":"5415","pubrep_id":"170","has_accepted_license":"1","publication_identifier":{"issn":["2664-1690"]},"oa":1,"publication_status":"published","ddc":["004"],"doi":"10.15479/AT:IST-2014-170-v1-1","date_published":"2014-02-19T00:00:00Z","status":"public","alternative_title":["IST Austria Technical Report"],"language":[{"iso":"eng"}],"citation":{"short":"K. Chatterjee, T.A. Henzinger, J. Otop, Nested Weighted Automata, IST Austria, 2014.","ieee":"K. Chatterjee, T. A. Henzinger, and J. Otop, <i>Nested weighted automata</i>. IST Austria, 2014.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. <i>Nested Weighted Automata</i>. IST Austria, 2014. <a href=\"https://doi.org/10.15479/AT:IST-2014-170-v1-1\">https://doi.org/10.15479/AT:IST-2014-170-v1-1</a>.","ista":"Chatterjee K, Henzinger TA, Otop J. 2014. Nested weighted automata, IST Austria, 27p.","mla":"Chatterjee, Krishnendu, et al. <i>Nested Weighted Automata</i>. IST Austria, 2014, doi:<a href=\"https://doi.org/10.15479/AT:IST-2014-170-v1-1\">10.15479/AT:IST-2014-170-v1-1</a>.","apa":"Chatterjee, K., Henzinger, T. A., &#38; Otop, J. (2014). <i>Nested weighted automata</i>. IST Austria. <a href=\"https://doi.org/10.15479/AT:IST-2014-170-v1-1\">https://doi.org/10.15479/AT:IST-2014-170-v1-1</a>","ama":"Chatterjee K, Henzinger TA, Otop J. <i>Nested Weighted Automata</i>. IST Austria; 2014. doi:<a href=\"https://doi.org/10.15479/AT:IST-2014-170-v1-1\">10.15479/AT:IST-2014-170-v1-1</a>"},"related_material":{"record":[{"relation":"later_version","status":"public","id":"1656"},{"relation":"later_version","status":"public","id":"467"},{"relation":"later_version","id":"5436","status":"public"}]}},{"has_accepted_license":"1","pubrep_id":"171","oa":1,"publication_status":"published","publication_identifier":{"issn":["2664-1690"]},"doi":"10.15479/AT:IST-2014-171-v1-1","ddc":["005"],"date_published":"2014-02-19T00:00:00Z","status":"public","alternative_title":["IST Austria Technical Report"],"language":[{"iso":"eng"}],"citation":{"ama":"Henzinger TA, Otop J. <i>Model Measuring for Hybrid Systems</i>. IST Austria; 2014. doi:<a href=\"https://doi.org/10.15479/AT:IST-2014-171-v1-1\">10.15479/AT:IST-2014-171-v1-1</a>","apa":"Henzinger, T. A., &#38; Otop, J. (2014). <i>Model measuring for hybrid systems</i>. IST Austria. <a href=\"https://doi.org/10.15479/AT:IST-2014-171-v1-1\">https://doi.org/10.15479/AT:IST-2014-171-v1-1</a>","mla":"Henzinger, Thomas A., and Jan Otop. <i>Model Measuring for Hybrid Systems</i>. IST Austria, 2014, doi:<a href=\"https://doi.org/10.15479/AT:IST-2014-171-v1-1\">10.15479/AT:IST-2014-171-v1-1</a>.","ista":"Henzinger TA, Otop J. 2014. Model measuring for hybrid systems, IST Austria, 22p.","chicago":"Henzinger, Thomas A, and Jan Otop. <i>Model Measuring for Hybrid Systems</i>. IST Austria, 2014. <a href=\"https://doi.org/10.15479/AT:IST-2014-171-v1-1\">https://doi.org/10.15479/AT:IST-2014-171-v1-1</a>.","ieee":"T. A. Henzinger and J. Otop, <i>Model measuring for hybrid systems</i>. IST Austria, 2014.","short":"T.A. Henzinger, J. Otop, Model Measuring for Hybrid Systems, IST Austria, 2014."},"related_material":{"record":[{"relation":"later_version","status":"public","id":"2217"}]},"file":[{"date_updated":"2020-07-14T12:46:49Z","file_id":"5492","checksum":"445456d22371e4e49aad2b9a0c13bf80","date_created":"2018-12-12T11:53:32Z","access_level":"open_access","file_name":"IST-2014-171-v1+1_report.pdf","content_type":"application/pdf","relation":"main_file","file_size":712077,"creator":"system"}],"abstract":[{"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.","lang":"eng"}],"day":"19","date_updated":"2023-02-23T10:33:21Z","oa_version":"Published Version","type":"technical_report","month":"02","page":"22","author":[{"full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A","last_name":"Henzinger"},{"first_name":"Jan","last_name":"Otop","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","full_name":"Otop, Jan"}],"date_created":"2018-12-12T11:39:12Z","file_date_updated":"2020-07-14T12:46:49Z","title":"Model measuring for hybrid systems","department":[{"_id":"ToHe"}],"year":"2014","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publisher":"IST Austria","_id":"5416"}]