[{"department":[{"_id":"CaGu"},{"_id":"ToHe"}],"issue":"4","citation":{"short":"B. Geiger, T. Petrov, G. Kubin, H. Koeppl, IEEE Transactions on Automatic Control 60 (2015) 1010–1022.","chicago":"Geiger, Bernhard, Tatjana Petrov, Gernot Kubin, and Heinz Koeppl. “Optimal Kullback-Leibler Aggregation via Information Bottleneck.” IEEE Transactions on Automatic Control. IEEE, 2015. https://doi.org/10.1109/TAC.2014.2364971.","mla":"Geiger, Bernhard, et al. “Optimal Kullback-Leibler Aggregation via Information Bottleneck.” IEEE Transactions on Automatic Control, vol. 60, no. 4, IEEE, 2015, pp. 1010–22, doi:10.1109/TAC.2014.2364971.","ista":"Geiger B, Petrov T, Kubin G, Koeppl H. 2015. Optimal Kullback-Leibler aggregation via information bottleneck. IEEE Transactions on Automatic Control. 60(4), 1010–1022.","ama":"Geiger B, Petrov T, Kubin G, Koeppl H. Optimal Kullback-Leibler aggregation via information bottleneck. IEEE Transactions on Automatic Control. 2015;60(4):1010-1022. doi:10.1109/TAC.2014.2364971","apa":"Geiger, B., Petrov, T., Kubin, G., & Koeppl, H. (2015). Optimal Kullback-Leibler aggregation via information bottleneck. IEEE Transactions on Automatic Control. IEEE. https://doi.org/10.1109/TAC.2014.2364971","ieee":"B. Geiger, T. Petrov, G. Kubin, and H. Koeppl, “Optimal Kullback-Leibler aggregation via information bottleneck,” IEEE Transactions on Automatic Control, vol. 60, no. 4. IEEE, pp. 1010–1022, 2015."},"page":"1010 - 1022","publication":"IEEE Transactions on Automatic Control","isi":1,"scopus_import":"1","status":"public","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","language":[{"iso":"eng"}],"quality_controlled":"1","article_processing_charge":"No","title":"Optimal Kullback-Leibler aggregation via information bottleneck","date_updated":"2025-09-23T09:45:33Z","acknowledgement":"This work was supported by the Austrian Research Association under Project 06/12684, by the Swiss National Science Foundation (SNSF) under Grant PP00P2 128503/1, by the SystemsX.ch (the Swiss Inititative for Systems Biology), and by a SNSF Early Postdoc.Mobility Fellowship grant P2EZP2_148797.\r\n","publication_identifier":{"issn":["0018-9286"]},"month":"04","oa_version":"Preprint","external_id":{"isi":["000351731600009"],"arxiv":["1304.6603"]},"day":"01","publist_id":"5262","abstract":[{"text":"In this paper, we present a method for reducing a regular, discrete-time Markov chain (DTMC) to another DTMC with a given, typically much smaller number of states. The cost of reduction is defined as the Kullback-Leibler divergence rate between a projection of the original process through a partition function and a DTMC on the correspondingly partitioned state space. Finding the reduced model with minimal cost is computationally expensive, as it requires an exhaustive search among all state space partitions, and an exact evaluation of the reduction cost for each candidate partition. Our approach deals with the latter problem by minimizing an upper bound on the reduction cost instead of minimizing the exact cost. The proposed upper bound is easy to compute and it is tight if the original chain is lumpable with respect to the partition. Then, we express the problem in the form of information bottleneck optimization, and propose using the agglomerative information bottleneck algorithm for searching a suboptimal partition greedily, rather than exhaustively. The theory is illustrated with examples and one application scenario in the context of modeling bio-molecular interactions.","lang":"eng"}],"publication_status":"published","arxiv":1,"date_published":"2015-04-01T00:00:00Z","volume":60,"year":"2015","oa":1,"_id":"1840","main_file_link":[{"url":"http://arxiv.org/abs/1304.6603","open_access":"1"}],"publisher":"IEEE","intvolume":" 60","type":"journal_article","date_created":"2018-12-11T11:54:18Z","author":[{"last_name":"Geiger","first_name":"Bernhard","full_name":"Geiger, Bernhard"},{"first_name":"Tatjana","last_name":"Petrov","id":"3D5811FC-F248-11E8-B48F-1D18A9856A87","full_name":"Petrov, Tatjana","orcid":"0000-0002-9041-0905"},{"full_name":"Kubin, Gernot","last_name":"Kubin","first_name":"Gernot"},{"full_name":"Koeppl, Heinz","first_name":"Heinz","last_name":"Koeppl"}],"doi":"10.1109/TAC.2014.2364971"},{"ec_funded":1,"external_id":{"isi":["000353193000019"]},"oa_version":"Published Version","day":"01","month":"04","has_accepted_license":"1","oa":1,"year":"2015","volume":11,"date_published":"2015-04-01T00:00:00Z","file_date_updated":"2020-07-14T12:45:17Z","publist_id":"5271","related_material":{"record":[{"relation":"earlier_version","id":"2328","status":"public"}]},"article_type":"original","publication_status":"published","abstract":[{"text":"Linearizability of concurrent data structures is usually proved by monolithic simulation arguments relying on the identification of the so-called linearization points. Regrettably, such proofs, whether manual or automatic, are often complicated and scale poorly to advanced non-blocking concurrency patterns, such as helping and optimistic updates. In response, we propose a more modular way of checking linearizability of concurrent queue algorithms that does not involve identifying linearization points. We reduce the task of proving linearizability with respect to the queue specification to establishing four basic properties, each of which can be proved independently by simpler arguments. As a demonstration of our approach, we verify the Herlihy and Wing queue, an algorithm that is challenging to verify by a simulation proof. ","lang":"eng"}],"file":[{"relation":"main_file","checksum":"7370e164d0a731f442424a92669efc34","file_id":"4881","content_type":"application/pdf","access_level":"open_access","file_size":380203,"date_updated":"2020-07-14T12:45:17Z","date_created":"2018-12-12T10:11:27Z","file_name":"IST-2015-390-v1+1_1502.07639.pdf","creator":"system"}],"_id":"1832","publisher":"International Federation for Computational Logic","author":[{"first_name":"Soham","last_name":"Chakraborty","full_name":"Chakraborty, Soham"},{"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":"Sezgin","first_name":"Ali","full_name":"Sezgin, Ali"},{"full_name":"Vafeiadis, Viktor","first_name":"Viktor","last_name":"Vafeiadis"}],"date_created":"2018-12-11T11:54:15Z","doi":"10.2168/LMCS-11(1:20)2015","project":[{"grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","call_identifier":"FWF"},{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Reactive Modeling","grant_number":"267989"}],"type":"journal_article","intvolume":" 11","issue":"1","corr_author":"1","ddc":["000"],"department":[{"_id":"ToHe"}],"das_tickbox":"1","status":"public","pubrep_id":"390","publication":"Logical Methods in Computer Science","citation":{"ama":"Chakraborty S, Henzinger TA, Sezgin A, Vafeiadis V. Aspect-oriented linearizability proofs. Logical Methods in Computer Science. 2015;11(1). doi:10.2168/LMCS-11(1:20)2015","apa":"Chakraborty, S., Henzinger, T. A., Sezgin, A., & Vafeiadis, V. (2015). Aspect-oriented linearizability proofs. Logical Methods in Computer Science. International Federation for Computational Logic. https://doi.org/10.2168/LMCS-11(1:20)2015","ieee":"S. Chakraborty, T. A. Henzinger, A. Sezgin, and V. Vafeiadis, “Aspect-oriented linearizability proofs,” Logical Methods in Computer Science, vol. 11, no. 1. International Federation for Computational Logic, 2015.","short":"S. Chakraborty, T.A. Henzinger, A. Sezgin, V. Vafeiadis, Logical Methods in Computer Science 11 (2015).","chicago":"Chakraborty, Soham, Thomas A Henzinger, Ali Sezgin, and Viktor Vafeiadis. “Aspect-Oriented Linearizability Proofs.” Logical Methods in Computer Science. International Federation for Computational Logic, 2015. https://doi.org/10.2168/LMCS-11(1:20)2015.","mla":"Chakraborty, Soham, et al. “Aspect-Oriented Linearizability Proofs.” Logical Methods in Computer Science, vol. 11, no. 1, 20, International Federation for Computational Logic, 2015, doi:10.2168/LMCS-11(1:20)2015.","ista":"Chakraborty S, Henzinger TA, Sezgin A, Vafeiadis V. 2015. Aspect-oriented linearizability proofs. Logical Methods in Computer Science. 11(1), 20."},"tmp":{"image":"/image/cc_by_nd.png","short":"CC BY-ND (4.0)","legal_code_url":"https://creativecommons.org/licenses/by-nd/4.0/legalcode","name":"Creative Commons Attribution-NoDerivatives 4.0 International (CC BY-ND 4.0)"},"scopus_import":"1","isi":1,"language":[{"iso":"eng"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","quality_controlled":"1","title":"Aspect-oriented linearizability proofs","date_updated":"2026-07-06T13:24:05Z","article_processing_charge":"No","article_number":"20"},{"_id":"1610","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1504.08259"}],"publisher":"Springer Nature","intvolume":" 9135","type":"conference","author":[{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","first_name":"Krishnendu"},{"last_name":"Henzinger","first_name":"Thomas A","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Rasmus","last_name":"Ibsen-Jensen","id":"3B699956-F248-11E8-B48F-1D18A9856A87","full_name":"Ibsen-Jensen, Rasmus","orcid":"0000-0003-4783-0389"},{"id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","full_name":"Otop, Jan","last_name":"Otop","first_name":"Jan"}],"date_created":"2018-12-11T11:53:01Z","doi":"10.1007/978-3-662-47666-6_10","project":[{"call_identifier":"FP7","name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989"},{"grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"Formal methods for the design and analysis of complex systems","call_identifier":"FWF"},{"call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23"},{"_id":"25863FF4-B435-11E9-9278-68D0E5697425","name":"Game Theory","call_identifier":"FWF","grant_number":"S11407"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","grant_number":"279307"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"},{"name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"}],"month":"07","external_id":{"isi":["000364317900010"],"arxiv":["1504.08259"]},"ec_funded":1,"oa_version":"Preprint","OA_place":"repository","day":"01","related_material":{"record":[{"id":"5438","status":"public","relation":"earlier_version"},{"relation":"later_version","id":"465","status":"public"}]},"publist_id":"5556","publication_status":"published","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."}],"arxiv":1,"alternative_title":["LNCS"],"year":"2015","oa":1,"volume":9135,"date_published":"2015-07-01T00:00:00Z","OA_type":"green","conference":{"name":"ICALP: Automata, Languages and Programming","location":"Kyoto, Japan","end_date":"2015-07-10","start_date":"2015-07-06"},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","language":[{"iso":"eng"}],"quality_controlled":"1","article_processing_charge":"No","title":"Edit distance for pushdown automata","publication_identifier":{"isbn":["978-3-662-47665-9"]},"date_updated":"2026-07-06T13:27:53Z","acknowledgement":"This research was funded in part by the European Research Council (ERC) under\r\ngrant agreement 267989 (QUAREM), by the Austrian Science Fund (FWF) projects\r\nS11402-N23 (RiSE) and Z211-N23 (Wittgenstein Award), FWF Grant No P23499-\r\nN23, FWF NFN Grant No S11407-N23 (RiSE), ERC Start grant (279307: Graph\r\nGames), and MSR faculty fellows award.","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"issue":"Part II","publication":"42nd International Colloquium on Automata, Languages, and Programming","citation":{"chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, Rasmus Ibsen-Jensen, and Jan Otop. “Edit Distance for Pushdown Automata.” In 42nd International Colloquium on Automata, Languages, and Programming, 9135:121–33. Springer Nature, 2015. https://doi.org/10.1007/978-3-662-47666-6_10.","ista":"Chatterjee K, Henzinger TA, Ibsen-Jensen R, Otop J. 2015. Edit distance for pushdown automata. 42nd International Colloquium on Automata, Languages, and Programming. ICALP: Automata, Languages and Programming, LNCS, vol. 9135, 121–133.","mla":"Chatterjee, Krishnendu, et al. “Edit Distance for Pushdown Automata.” 42nd International Colloquium on Automata, Languages, and Programming, vol. 9135, no. Part II, Springer Nature, 2015, pp. 121–33, doi:10.1007/978-3-662-47666-6_10.","short":"K. Chatterjee, T.A. Henzinger, R. Ibsen-Jensen, J. Otop, in:, 42nd International Colloquium on Automata, Languages, and Programming, Springer Nature, 2015, pp. 121–133.","apa":"Chatterjee, K., Henzinger, T. A., Ibsen-Jensen, R., & Otop, J. (2015). Edit distance for pushdown automata. In 42nd International Colloquium on Automata, Languages, and Programming (Vol. 9135, pp. 121–133). Kyoto, Japan: Springer Nature. https://doi.org/10.1007/978-3-662-47666-6_10","ama":"Chatterjee K, Henzinger TA, Ibsen-Jensen R, Otop J. Edit distance for pushdown automata. In: 42nd International Colloquium on Automata, Languages, and Programming. Vol 9135. Springer Nature; 2015:121-133. doi:10.1007/978-3-662-47666-6_10","ieee":"K. Chatterjee, T. A. Henzinger, R. Ibsen-Jensen, and J. Otop, “Edit distance for pushdown automata,” in 42nd International Colloquium on Automata, Languages, and Programming, Kyoto, Japan, 2015, vol. 9135, no. Part II, pp. 121–133."},"page":"121 - 133","scopus_import":"1","isi":1,"pubrep_id":"321","status":"public"},{"department":[{"_id":"KrCh"},{"_id":"ToHe"}],"status":"public","scopus_import":"1","isi":1,"citation":{"short":"K. Chatterjee, Z. Komárková, J. Kretinsky, (2015) 244–256.","chicago":"Chatterjee, Krishnendu, Zuzana Komárková, and Jan Kretinsky. “Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes.” LICS. IEEE, 2015. https://doi.org/10.1109/LICS.2015.32.","ista":"Chatterjee K, Komárková Z, Kretinsky J. 2015. Unifying two views on multiple mean-payoff objectives in Markov decision processes. , 244–256.","mla":"Chatterjee, Krishnendu, et al. Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes. IEEE, 2015, pp. 244–56, doi:10.1109/LICS.2015.32.","apa":"Chatterjee, K., Komárková, Z., & Kretinsky, J. (2015). Unifying two views on multiple mean-payoff objectives in Markov decision processes. Presented at the LICS: Logic in Computer Science, Kyoto, Japan: IEEE. https://doi.org/10.1109/LICS.2015.32","ama":"Chatterjee K, Komárková Z, Kretinsky J. Unifying two views on multiple mean-payoff objectives in Markov decision processes. 2015:244-256. doi:10.1109/LICS.2015.32","ieee":"K. Chatterjee, Z. Komárková, and J. Kretinsky, “Unifying two views on multiple mean-payoff objectives in Markov decision processes.” IEEE, pp. 244–256, 2015."},"page":"244 - 256","quality_controlled":"1","conference":{"start_date":"2015-07-06","name":"LICS: Logic in Computer Science","end_date":"2015-07-10","location":"Kyoto, Japan"},"language":[{"iso":"eng"}],"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","OA_type":"green","acknowledgement":"A Technical Report of this paper is available at DOI: 10.15479/AT:IST-2015-318-v1-1\r\n","date_updated":"2026-07-06T13:26:26Z","title":"Unifying two views on multiple mean-payoff objectives in Markov decision processes","article_processing_charge":"No","OA_place":"repository","day":"01","ec_funded":1,"external_id":{"isi":["000380427100024"]},"oa_version":"Preprint","month":"07","series_title":"LICS","oa":1,"year":"2015","date_published":"2015-07-01T00:00:00Z","alternative_title":["LICS"],"publication_status":"published","abstract":[{"lang":"eng","text":"We consider Markov decision processes (MDPs) with multiple limit-average (or mean-payoff) objectives. There exist two different views: (i) ~the expectation semantics, where the goal is to optimize the expected mean-payoff objective, and (ii) ~the satisfaction semantics, where the goal is to maximize the probability of runs such that the mean-payoff value stays above a given vector. We consider optimization with respect to both objectives at once, thus unifying the existing semantics. Precisely, the goal is to optimize the expectation while ensuring the satisfaction constraint. Our problem captures the notion of optimization with respect to strategies that are risk-averse (i.e., Ensure certain probabilistic guarantee). Our main results are as follows: First, we present algorithms for the decision problems, which are always polynomial in the size of the MDP. We also show that an approximation of the Pareto curve can be computed in time polynomial in the size of the MDP, and the approximation factor, but exponential in the number of dimensions. Second, we present a complete characterization of the strategy complexity (in terms of memory bounds and randomization) required to solve our problem. "}],"publist_id":"5493","related_material":{"record":[{"status":"public","id":"5429","relation":"earlier_version"},{"relation":"earlier_version","id":"5435","status":"public"},{"id":"466","status":"public","relation":"later_version"}]},"publisher":"IEEE","main_file_link":[{"url":"https://doi.org/10.15479/AT:IST-2015-318-v1-1","open_access":"1"}],"_id":"1657","project":[{"grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","call_identifier":"FWF"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Formal methods for the design and analysis of complex systems","grant_number":"Z211"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","grant_number":"279307"},{"grant_number":"267989","name":"Quantitative Reactive Modeling","call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"_id":"25681D80-B435-11E9-9278-68D0E5697425","name":"International IST Postdoc Fellowship Programme","call_identifier":"FP7","grant_number":"291734"}],"doi":"10.1109/LICS.2015.32","date_created":"2018-12-11T11:53:18Z","author":[{"last_name":"Chatterjee","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Komárková, Zuzana","first_name":"Zuzana","last_name":"Komárková"},{"first_name":"Jan","last_name":"Kretinsky","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","full_name":"Kretinsky, Jan","orcid":"0000-0002-8122-2881"}],"type":"conference"},{"publication":"Proceedings - Symposium on Logic in Computer Science","citation":{"chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. “Nested Weighted Automata.” In Proceedings - Symposium on Logic in Computer Science, Vol. 2015–July. IEEE, 2015. https://doi.org/10.1109/LICS.2015.72.","ista":"Chatterjee K, Henzinger TA, Otop J. 2015. Nested weighted automata. Proceedings - Symposium on Logic in Computer Science. LICS: Logic in Computer Science vol. 2015–July, 7174926.","mla":"Chatterjee, Krishnendu, et al. “Nested Weighted Automata.” Proceedings - Symposium on Logic in Computer Science, vol. 2015–July, 7174926, IEEE, 2015, doi:10.1109/LICS.2015.72.","short":"K. Chatterjee, T.A. Henzinger, J. Otop, in:, Proceedings - Symposium on Logic in Computer Science, IEEE, 2015.","apa":"Chatterjee, K., Henzinger, T. A., & Otop, J. (2015). Nested weighted automata. In Proceedings - Symposium on Logic in Computer Science (Vol. 2015–July). Kyoto, Japan: IEEE. https://doi.org/10.1109/LICS.2015.72","ama":"Chatterjee K, Henzinger TA, Otop J. Nested weighted automata. In: Proceedings - Symposium on Logic in Computer Science. Vol 2015-July. IEEE; 2015. doi:10.1109/LICS.2015.72","ieee":"K. Chatterjee, T. A. Henzinger, and J. Otop, “Nested weighted automata,” in Proceedings - Symposium on Logic in Computer Science, Kyoto, Japan, 2015, vol. 2015–July."},"scopus_import":"1","isi":1,"status":"public","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"corr_author":"1","article_processing_charge":"No","article_number":"7174926","title":"Nested weighted automata","date_updated":"2026-07-07T14:01:10Z","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","OA_type":"green","conference":{"location":"Kyoto, Japan","end_date":"2015-07-10","name":"LICS: Logic in Computer Science","start_date":"2015-07-06"},"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","language":[{"iso":"eng"}],"quality_controlled":"1","publist_id":"5494","related_material":{"record":[{"relation":"earlier_version","id":"5415","status":"public"},{"id":"5436","status":"public","relation":"earlier_version"},{"relation":"later_version","id":"467","status":"public"}]},"publication_status":"published","abstract":[{"lang":"eng","text":"Recently there has been a significant effort to handle quantitative properties in formal verification and synthesis. While weighted automata over finite and infinite words provide a natural and flexible framework to express quantitative properties, perhaps surprisingly, some basic system properties such as average response time cannot be expressed using weighted automata, nor in any other know decidable formalism. In this work, we introduce nested weighted automata as a natural extension of weighted automata which makes it possible to express important quantitative properties such as average response time. In nested weighted automata, a master automaton spins off and collects results from weighted slave automata, each of which computes a quantity along a finite portion of an infinite word. Nested weighted automata can be viewed as the quantitative analogue of monitor automata, which are used in run-time verification. We establish an almost complete decidability picture for the basic decision problems about nested weighted automata, and illustrate their applicability in several domains. In particular, nested weighted automata can be used to decide average response time properties."}],"arxiv":1,"year":"2015","oa":1,"date_published":"2015-07-31T00:00:00Z","volume":"2015-July","month":"07","ec_funded":1,"external_id":{"arxiv":["1606.03598"],"isi":["000380427100064"]},"oa_version":"Preprint","OA_place":"repository","day":"31","type":"conference","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","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A","last_name":"Henzinger"},{"last_name":"Otop","first_name":"Jan","full_name":"Otop, Jan","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87"}],"date_created":"2018-12-11T11:53:17Z","project":[{"name":"Quantitative Reactive Modeling","call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"name":"Formal methods for the design and analysis of complex systems","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211"},{"grant_number":"P 23499-N23","call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification","_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"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"doi":"10.1109/LICS.2015.72","_id":"1656","publisher":"IEEE","main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.1606.03598"}]},{"date_updated":"2026-07-07T14:01:10Z","publication_identifier":{"issn":["2664-1690"]},"doi":"10.15479/AT:IST-2015-170-v2-2","title":"Nested weighted automata","date_created":"2018-12-12T11:39:19Z","author":[{"first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X"},{"first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724"},{"last_name":"Otop","first_name":"Jan","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","full_name":"Otop, Jan"}],"type":"technical_report","file":[{"date_updated":"2020-07-14T12:46:54Z","file_name":"IST-2015-170-v2+2_report.pdf","date_created":"2018-12-12T11:54:19Z","creator":"system","checksum":"3c402f47d3669c28d04d1af405a08e3f","relation":"main_file","file_id":"5541","content_type":"application/pdf","file_size":569991,"access_level":"open_access"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","language":[{"iso":"eng"}],"publisher":"IST Austria","_id":"5436","status":"public","pubrep_id":"331","date_published":"2015-04-24T00:00:00Z","year":"2015","oa":1,"alternative_title":["IST Austria Technical Report"],"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.\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.","lang":"eng"}],"publication_status":"published","related_material":{"record":[{"relation":"earlier_version","status":"public","id":"5415"},{"relation":"later_version","id":"1656","status":"public"},{"relation":"later_version","id":"467","status":"public"}]},"page":"29","citation":{"mla":"Chatterjee, Krishnendu, et al. Nested Weighted Automata. IST Austria, 2015, doi:10.15479/AT:IST-2015-170-v2-2.","ista":"Chatterjee K, Henzinger TA, Otop J. 2015. Nested weighted automata, IST Austria, 29p.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. Nested Weighted Automata. IST Austria, 2015. https://doi.org/10.15479/AT:IST-2015-170-v2-2.","short":"K. Chatterjee, T.A. Henzinger, J. Otop, Nested Weighted Automata, IST Austria, 2015.","ieee":"K. Chatterjee, T. A. Henzinger, and J. Otop, Nested weighted automata. IST Austria, 2015.","apa":"Chatterjee, K., Henzinger, T. A., & Otop, J. (2015). Nested weighted automata. IST Austria. https://doi.org/10.15479/AT:IST-2015-170-v2-2","ama":"Chatterjee K, Henzinger TA, Otop J. Nested Weighted Automata. IST Austria; 2015. doi:10.15479/AT:IST-2015-170-v2-2"},"file_date_updated":"2020-07-14T12:46:54Z","ddc":["000"],"day":"24","oa_version":"Published Version","has_accepted_license":"1","month":"04","department":[{"_id":"KrCh"},{"_id":"ToHe"}]},{"department":[{"_id":"ToHe"}],"status":"public","scopus_import":"1","publication":"Proceedings of the 17th international conference on Hybrid systems: computation and control","citation":{"ama":"Henzinger TA, Otop J. Model measuring for hybrid systems. In: Proceedings of the 17th International Conference on Hybrid Systems: Computation and Control. Springer; 2014:213-222. doi:10.1145/2562059.2562130","apa":"Henzinger, T. A., & Otop, J. (2014). Model measuring for hybrid systems. In Proceedings of the 17th international conference on Hybrid systems: computation and control (pp. 213–222). Berlin, Germany: Springer. https://doi.org/10.1145/2562059.2562130","ieee":"T. A. Henzinger and J. Otop, “Model measuring for hybrid systems,” in Proceedings of the 17th international conference on Hybrid systems: computation and control, Berlin, Germany, 2014, pp. 213–222.","chicago":"Henzinger, Thomas A, and Jan Otop. “Model Measuring for Hybrid Systems.” In Proceedings of the 17th International Conference on Hybrid Systems: Computation and Control, 213–22. Springer, 2014. https://doi.org/10.1145/2562059.2562130.","mla":"Henzinger, Thomas A., and Jan Otop. “Model Measuring for Hybrid Systems.” Proceedings of the 17th International Conference on Hybrid Systems: Computation and Control, Springer, 2014, pp. 213–22, doi:10.1145/2562059.2562130.","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.","short":"T.A. Henzinger, J. Otop, in:, Proceedings of the 17th International Conference on Hybrid Systems: Computation and Control, Springer, 2014, pp. 213–222."},"page":"213 - 222","quality_controlled":"1","conference":{"start_date":"2014-04-15","name":"HSCC: Hybrid Systems - Computation and Control","location":"Berlin, Germany","end_date":"2014-04-17"},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","language":[{"iso":"eng"}],"OA_type":"green","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","date_updated":"2025-06-26T08:32:32Z","title":"Model measuring for hybrid systems","article_processing_charge":"No","OA_place":"repository","day":"01","ec_funded":1,"oa_version":"Preprint","month":"04","year":"2014","oa":1,"date_published":"2014-04-01T00:00:00Z","publication_status":"published","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."}],"related_material":{"record":[{"relation":"earlier_version","id":"5416","status":"public"}]},"publist_id":"4751","publisher":"Springer","main_file_link":[{"url":"https://doi.org/10.15479/AT:IST-2014-171-v1-1","open_access":"1"}],"_id":"2217","doi":"10.1145/2562059.2562130","project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Reactive Modeling","grant_number":"267989"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"}],"date_created":"2018-12-11T11:56:23Z","author":[{"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"}],"type":"conference"},{"month":"07","has_accepted_license":"1","ec_funded":1,"oa_version":"Submitted Version","day":"22","file_date_updated":"2020-07-14T12:45:33Z","related_material":{"record":[{"status":"public","id":"1130","relation":"dissertation_contains"}]},"publist_id":"4749","publication_status":"published","abstract":[{"text":"While fixing concurrency bugs, program repair algorithms may introduce new concurrency bugs. We present an algorithm that avoids such regressions. The solution space is given by a set of program transformations we consider in the repair process. These include reordering of instructions within a thread and inserting atomic sections. The new algorithm learns a constraint on the space of candidate solutions, from both positive examples (error-free traces) and counterexamples (error traces). From each counterexample, the algorithm learns a constraint necessary to remove the errors. From each positive examples, it learns a constraint that is necessary in order to prevent the repair from turning the trace into an error trace. We implemented the algorithm and evaluated it on simplified Linux device drivers with known bugs.","lang":"eng"}],"alternative_title":["LNCS"],"year":"2014","oa":1,"date_published":"2014-07-22T00:00:00Z","volume":8559,"_id":"2218","main_file_link":[{"url":"https://link.springer.com/chapter/10.1007%2F978-3-319-08867-9_38","open_access":"1"}],"publisher":"Springer","file":[{"file_id":"4995","checksum":"a631d3105509f239724644e77a1212e2","relation":"main_file","file_size":416732,"access_level":"open_access","content_type":"application/pdf","file_name":"IST-2014-297-v1+1_cav14-final.pdf","date_created":"2018-12-12T10:13:14Z","creator":"system","date_updated":"2020-07-14T12:45:33Z"},{"access_level":"open_access","file_size":616293,"content_type":"application/pdf","file_id":"4996","checksum":"f8b0f748cc9fa697ca992cc56c87bc4e","relation":"main_file","date_created":"2018-12-12T10:13:15Z","file_name":"IST-2014-297-v2+1_cav14-final2.pdf","creator":"system","date_updated":"2020-07-14T12:45:33Z"}],"intvolume":" 8559","type":"conference","date_created":"2018-12-11T11:56:23Z","author":[{"last_name":"Cerny","first_name":"Pavol","full_name":"Cerny, Pavol"},{"first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724"},{"full_name":"Radhakrishna, Arjun","id":"3B51CAC4-F248-11E8-B48F-1D18A9856A87","first_name":"Arjun","last_name":"Radhakrishna"},{"full_name":"Ryzhyk, Leonid","first_name":"Leonid","last_name":"Ryzhyk"},{"first_name":"Thorsten","last_name":"Tarrach","id":"3D6E8F2C-F248-11E8-B48F-1D18A9856A87","full_name":"Tarrach, Thorsten","orcid":"0000-0003-4409-8487"}],"project":[{"call_identifier":"FP7","name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989"},{"grant_number":"S11402-N23","call_identifier":"FWF","name":"Moderne Concurrency Paradigms","_id":"25F5A88A-B435-11E9-9278-68D0E5697425"}],"doi":"10.1007/978-3-319-08867-9_38","department":[{"_id":"ToHe"}],"ddc":["000"],"citation":{"short":"P. Cerny, T.A. Henzinger, A. Radhakrishna, L. Ryzhyk, T. Tarrach, in:, Springer, 2014, pp. 568–584.","chicago":"Cerny, Pavol, Thomas A Henzinger, Arjun Radhakrishna, Leonid Ryzhyk, and Thorsten Tarrach. “Regression-Free Synthesis for Concurrency,” 8559:568–84. Springer, 2014. https://doi.org/10.1007/978-3-319-08867-9_38.","mla":"Cerny, Pavol, et al. Regression-Free Synthesis for Concurrency. Vol. 8559, Springer, 2014, pp. 568–84, doi:10.1007/978-3-319-08867-9_38.","ista":"Cerny P, Henzinger TA, Radhakrishna A, Ryzhyk L, Tarrach T. 2014. Regression-free synthesis for concurrency. CAV: Computer Aided Verification, LNCS, vol. 8559, 568–584.","ama":"Cerny P, Henzinger TA, Radhakrishna A, Ryzhyk L, Tarrach T. Regression-free synthesis for concurrency. In: Vol 8559. Springer; 2014:568-584. doi:10.1007/978-3-319-08867-9_38","apa":"Cerny, P., Henzinger, T. A., Radhakrishna, A., Ryzhyk, L., & Tarrach, T. (2014). Regression-free synthesis for concurrency (Vol. 8559, pp. 568–584). Presented at the CAV: Computer Aided Verification, Vienna, Austria: Springer. https://doi.org/10.1007/978-3-319-08867-9_38","ieee":"P. Cerny, T. A. Henzinger, A. Radhakrishna, L. Ryzhyk, and T. Tarrach, “Regression-free synthesis for concurrency,” presented at the CAV: Computer Aided Verification, Vienna, Austria, 2014, vol. 8559, pp. 568–584."},"page":"568 - 584","scopus_import":"1","status":"public","pubrep_id":"297","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","language":[{"iso":"eng"}],"conference":{"start_date":"2014-07-18","name":"CAV: Computer Aided Verification","end_date":"2014-07-22","location":"Vienna, Austria"},"quality_controlled":"1","title":"Regression-free synthesis for concurrency","publication_identifier":{"isbn":["978-331908866-2"]},"date_updated":"2026-04-09T10:54:00Z"},{"citation":{"ieee":"U. Boker, T. A. Henzinger, and A. Radhakrishna, “Battery transition systems,” presented at the POPL: Principles of Programming Languages, San Diego, USA, 2014, vol. 49, no. 1, pp. 595–606.","apa":"Boker, U., Henzinger, T. A., & Radhakrishna, A. (2014). Battery transition systems (Vol. 49, pp. 595–606). Presented at the POPL: Principles of Programming Languages, San Diego, USA: ACM. https://doi.org/10.1145/2535838.2535875","ama":"Boker U, Henzinger TA, Radhakrishna A. Battery transition systems. In: Vol 49. ACM; 2014:595-606. doi:10.1145/2535838.2535875","short":"U. Boker, T.A. Henzinger, A. Radhakrishna, in:, ACM, 2014, pp. 595–606.","mla":"Boker, Udi, et al. Battery Transition Systems. Vol. 49, no. 1, ACM, 2014, pp. 595–606, doi:10.1145/2535838.2535875.","ista":"Boker U, Henzinger TA, Radhakrishna A. 2014. Battery transition systems. POPL: Principles of Programming Languages vol. 49, 595–606.","chicago":"Boker, Udi, Thomas A Henzinger, and Arjun Radhakrishna. “Battery Transition Systems,” 49:595–606. ACM, 2014. https://doi.org/10.1145/2535838.2535875."},"page":"595 - 606","scopus_import":1,"status":"public","department":[{"_id":"ToHe"}],"issue":"1","title":"Battery transition systems","publication_identifier":{"isbn":["978-145032544-8"]},"date_updated":"2021-01-12T06:56:13Z","language":[{"iso":"eng"}],"conference":{"start_date":"2014-01-22","name":"POPL: Principles of Programming Languages","location":"San Diego, USA","end_date":"2014-01-24"},"user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","quality_controlled":"1","publist_id":"4722","publication_status":"published","abstract":[{"text":"The analysis of the energy consumption of software is an important goal for quantitative formal methods. Current methods, using weighted transition systems or energy games, model the energy source as an ideal resource whose status is characterized by one number, namely the amount of remaining energy. Real batteries, however, exhibit behaviors that can deviate substantially from an ideal energy resource. Based on a discretization of a standard continuous battery model, we introduce battery transition systems. In this model, a battery is viewed as consisting of two parts-the available-charge tank and the bound-charge tank. Any charge or discharge is applied to the available-charge tank. Over time, the energy from each tank diffuses to the other tank. Battery transition systems are infinite state systems that, being not well-structured, fall into no decidable class that is known to us. Nonetheless, we are able to prove that the !-regular modelchecking problem is decidable for battery transition systems. We also present a case study on the verification of control programs for energy-constrained semi-autonomous robots.","lang":"eng"}],"year":"2014","date_published":"2014-01-13T00:00:00Z","volume":49,"month":"01","ec_funded":1,"oa_version":"None","day":"13","intvolume":" 49","type":"conference","author":[{"first_name":"Udi","last_name":"Boker","id":"31E297B6-F248-11E8-B48F-1D18A9856A87","full_name":"Boker, Udi"},{"orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A"},{"id":"3B51CAC4-F248-11E8-B48F-1D18A9856A87","full_name":"Radhakrishna, Arjun","first_name":"Arjun","last_name":"Radhakrishna"}],"date_created":"2018-12-11T11:56:30Z","project":[{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"name":"Quantitative Reactive Modeling","call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989"}],"doi":"10.1145/2535838.2535875","_id":"2239","publisher":"ACM"},{"main_file_link":[{"url":"https://arxiv.org/abs/1904.07083","open_access":"1"}],"publisher":"IEEE","_id":"2167","type":"conference","project":[{"name":"Quantitative Reactive Modeling","call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989"},{"name":"Moderne Concurrency Paradigms","call_identifier":"FWF","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","grant_number":"S11402-N23"}],"doi":"10.1109/ICST.2014.50","author":[{"last_name":"Daca","first_name":"Przemyslaw","full_name":"Daca, Przemyslaw","id":"49351290-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Henzinger","first_name":"Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A"},{"last_name":"Krenn","first_name":"Willibald","full_name":"Krenn, Willibald"},{"first_name":"Dejan","last_name":"Nickovic","full_name":"Nickovic, Dejan"}],"date_created":"2018-12-11T11:56:06Z","month":"03","day":"01","ec_funded":1,"external_id":{"isi":["000355985000040"],"arxiv":["1904.07083"]},"oa_version":"Preprint","publication_status":"published","abstract":[{"text":"Model-based testing is a promising technology for black-box software and hardware testing, in which test cases are generated automatically from high-level specifications. Nowadays, systems typically consist of multiple interacting components and, due to their complexity, testing presents a considerable portion of the effort and cost in the design process. Exploiting the compositional structure of system specifications can considerably reduce the effort in model-based testing. Moreover, inferring properties about the system from testing its individual components allows the designer to reduce the amount of integration testing. In this paper, we study compositional properties of the ioco-testing theory. We propose a new approach to composition and hiding operations, inspired by contract-based design and interface theories. These operations preserve behaviors that are compatible under composition and hiding, and prune away incompatible ones. The resulting specification characterizes the input sequences for which the unit testing of components is sufficient to infer the correctness of component integration without the need for further tests. We provide a methodology that uses these results to minimize integration testing effort, but also to detect potential weaknesses in specifications. While we focus on asynchronous models and the ioco conformance relation, the resulting methodology can be applied to a broader class of systems.","lang":"eng"}],"publist_id":"4817","related_material":{"record":[{"id":"5411","status":"public","relation":"earlier_version"},{"relation":"dissertation_contains","status":"public","id":"1155"}]},"oa":1,"year":"2014","date_published":"2014-03-01T00:00:00Z","arxiv":1,"quality_controlled":"1","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","conference":{"start_date":"2014-03-31","end_date":"2014-04-04","location":"Cleveland, USA","name":"ICST: International Conference on Software Testing, Verification and Validation"},"language":[{"iso":"eng"}],"article_number":"6823899","article_processing_charge":"No","publication_identifier":{"issn":["2159-4848"],"isbn":["978-1-4799-2255-0"]},"date_updated":"2026-04-15T10:02:12Z","title":"Compositional specifications for IOCO testing","department":[{"_id":"ToHe"}],"scopus_import":"1","isi":1,"publication":"IEEE 7th International Conference on Software Testing, Verification and Validation","citation":{"ieee":"P. Daca, T. A. Henzinger, W. Krenn, and D. Nickovic, “Compositional specifications for IOCO testing,” in IEEE 7th International Conference on Software Testing, Verification and Validation, Cleveland, USA, 2014.","apa":"Daca, P., Henzinger, T. A., Krenn, W., & Nickovic, D. (2014). Compositional specifications for IOCO testing. In IEEE 7th International Conference on Software Testing, Verification and Validation. Cleveland, USA: IEEE. https://doi.org/10.1109/ICST.2014.50","ama":"Daca P, Henzinger TA, Krenn W, Nickovic D. Compositional specifications for IOCO testing. In: IEEE 7th International Conference on Software Testing, Verification and Validation. IEEE; 2014. doi:10.1109/ICST.2014.50","short":"P. Daca, T.A. Henzinger, W. Krenn, D. Nickovic, in:, IEEE 7th International Conference on Software Testing, Verification and Validation, IEEE, 2014.","ista":"Daca P, Henzinger TA, Krenn W, Nickovic D. 2014. Compositional specifications for IOCO testing. IEEE 7th International Conference on Software Testing, Verification and Validation. ICST: International Conference on Software Testing, Verification and Validation, 6823899.","mla":"Daca, Przemyslaw, et al. “Compositional Specifications for IOCO Testing.” IEEE 7th International Conference on Software Testing, Verification and Validation, 6823899, IEEE, 2014, doi:10.1109/ICST.2014.50.","chicago":"Daca, Przemyslaw, Thomas A Henzinger, Willibald Krenn, and Dejan Nickovic. “Compositional Specifications for IOCO Testing.” In IEEE 7th International Conference on Software Testing, Verification and Validation. IEEE, 2014. https://doi.org/10.1109/ICST.2014.50."},"status":"public"},{"quality_controlled":"1","language":[{"iso":"eng"}],"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","date_updated":"2025-09-29T11:32:51Z","title":"Synthesizing robust systems","article_processing_charge":"No","issue":"3-4","ddc":["621"],"department":[{"_id":"KrCh"},{"_id":"ToHe"}],"status":"public","pubrep_id":"71","scopus_import":"1","isi":1,"publication":"Acta Informatica","citation":{"short":"R. Bloem, K. Chatterjee, K. Greimel, T.A. Henzinger, G. Hofferek, B. Jobstmann, B. Könighofer, R. Könighofer, Acta Informatica 51 (2014) 193–220.","chicago":"Bloem, Roderick, Krishnendu Chatterjee, Karin Greimel, Thomas A Henzinger, Georg Hofferek, Barbara Jobstmann, Bettina Könighofer, and Robert Könighofer. “Synthesizing Robust Systems.” Acta Informatica. Springer, 2014. https://doi.org/10.1007/s00236-013-0191-5.","mla":"Bloem, Roderick, et al. “Synthesizing Robust Systems.” Acta Informatica, vol. 51, no. 3–4, Springer, 2014, pp. 193–220, doi:10.1007/s00236-013-0191-5.","ista":"Bloem R, Chatterjee K, Greimel K, Henzinger TA, Hofferek G, Jobstmann B, Könighofer B, Könighofer R. 2014. Synthesizing robust systems. Acta Informatica. 51(3–4), 193–220.","ama":"Bloem R, Chatterjee K, Greimel K, et al. Synthesizing robust systems. Acta Informatica. 2014;51(3-4):193-220. doi:10.1007/s00236-013-0191-5","apa":"Bloem, R., Chatterjee, K., Greimel, K., Henzinger, T. A., Hofferek, G., Jobstmann, B., … Könighofer, R. (2014). Synthesizing robust systems. Acta Informatica. Springer. https://doi.org/10.1007/s00236-013-0191-5","ieee":"R. Bloem et al., “Synthesizing robust systems,” Acta Informatica, vol. 51, no. 3–4. Springer, pp. 193–220, 2014."},"page":"193 - 220","file":[{"creator":"system","date_created":"2018-12-12T10:16:44Z","file_name":"IST-2012-71-v1+1_Synthesizing_robust_systems.pdf","date_updated":"2020-07-14T12:45:31Z","file_id":"5234","checksum":"d7f560f3d923f0f00aa10a0652f83273","relation":"main_file","file_size":169523,"access_level":"open_access","content_type":"application/pdf"}],"publisher":"Springer","_id":"2187","doi":"10.1007/s00236-013-0191-5","project":[{"call_identifier":"FWF","name":"Moderne Concurrency Paradigms","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","grant_number":"S11402-N23"},{"_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF","grant_number":"P 23499-N23"},{"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"},{"grant_number":"267989","call_identifier":"FP7","name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425"}],"author":[{"first_name":"Roderick","last_name":"Bloem","full_name":"Bloem, Roderick"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","last_name":"Chatterjee"},{"first_name":"Karin","last_name":"Greimel","full_name":"Greimel, Karin"},{"first_name":"Thomas A","last_name":"Henzinger","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"},{"full_name":"Hofferek, Georg","first_name":"Georg","last_name":"Hofferek"},{"first_name":"Barbara","last_name":"Jobstmann","full_name":"Jobstmann, Barbara"},{"last_name":"Könighofer","first_name":"Bettina","full_name":"Könighofer, Bettina"},{"full_name":"Könighofer, Robert","last_name":"Könighofer","first_name":"Robert"}],"date_created":"2018-12-11T11:56:13Z","type":"journal_article","intvolume":" 51","day":"01","ec_funded":1,"external_id":{"isi":["000335981500004"]},"oa_version":"Submitted Version","month":"06","has_accepted_license":"1","oa":1,"year":"2014","volume":51,"date_published":"2014-06-01T00:00:00Z","article_type":"original","publication_status":"published","abstract":[{"lang":"eng","text":"Systems should not only be correct but also robust in the sense that they behave reasonably in unexpected situations. This article addresses synthesis of robust reactive systems from temporal specifications. Existing methods allow arbitrary behavior if assumptions in the specification are violated. To overcome this, we define two robustness notions, combine them, and show how to enforce them in synthesis. The first notion applies to safety properties: If safety assumptions are violated temporarily, we require that the system recovers to normal operation with as few errors as possible. The second notion requires that, if liveness assumptions are violated, as many guarantees as possible should be fulfilled nevertheless. We present a synthesis procedure achieving this for the important class of GR(1) specifications, and establish complexity bounds. We also present an implementation of a special case of robustness, and show experimental results."}],"file_date_updated":"2020-07-14T12:45:31Z","publist_id":"4787"},{"publisher":"Springer","main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1402.3388"}],"_id":"2190","project":[{"call_identifier":"FP7","name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989"},{"name":"Moderne Concurrency Paradigms","call_identifier":"FWF","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","grant_number":"S11402-N23"}],"doi":"10.1007/978-3-319-08867-9_13","author":[{"full_name":"Esparza, Javier","first_name":"Javier","last_name":"Esparza"},{"first_name":"Jan","last_name":"Kretinsky","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","full_name":"Kretinsky, Jan","orcid":"0000-0002-8122-2881"}],"date_created":"2018-12-11T11:56:14Z","type":"conference","intvolume":" 8559","day":"01","ec_funded":1,"external_id":{"arxiv":["1402.3388"]},"oa_version":"Submitted Version","month":"01","oa":1,"year":"2014","volume":8559,"date_published":"2014-01-01T00:00:00Z","arxiv":1,"alternative_title":["LNCS"],"publication_status":"published","abstract":[{"lang":"eng","text":"We present a new algorithm to construct a (generalized) deterministic Rabin automaton for an LTL formula φ. The automaton is the product of a master automaton and an array of slave automata, one for each G-subformula of φ. The slave automaton for G ψ is in charge of recognizing whether FG ψ holds. As opposed to standard determinization procedures, the states of all our automata have a clear logical structure, which allows for various optimizations. Our construction subsumes former algorithms for fragments of LTL. Experimental results show improvement in the sizes of the resulting automata compared to existing methods."}],"publist_id":"4784","quality_controlled":"1","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","language":[{"iso":"eng"}],"conference":{"name":"CAV: Computer Aided Verification"},"acknowledgement":"The author is on leave from Faculty of Informatics, Masaryk University, Czech Republic, and partially supported by the Czech Science Foundation, grant No. P202/12/G061.","date_updated":"2025-06-11T08:01:04Z","title":"From LTL to deterministic automata: A safraless compositional approach","article_processing_charge":"No","corr_author":"1","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"status":"public","scopus_import":"1","page":"192 - 208","citation":{"ieee":"J. Esparza and J. Kretinsky, “From LTL to deterministic automata: A safraless compositional approach,” presented at the CAV: Computer Aided Verification, 2014, vol. 8559, pp. 192–208.","ama":"Esparza J, Kretinsky J. From LTL to deterministic automata: A safraless compositional approach. In: Vol 8559. Springer; 2014:192-208. doi:10.1007/978-3-319-08867-9_13","apa":"Esparza, J., & Kretinsky, J. (2014). From LTL to deterministic automata: A safraless compositional approach (Vol. 8559, pp. 192–208). Presented at the CAV: Computer Aided Verification, Springer. https://doi.org/10.1007/978-3-319-08867-9_13","mla":"Esparza, Javier, and Jan Kretinsky. From LTL to Deterministic Automata: A Safraless Compositional Approach. Vol. 8559, Springer, 2014, pp. 192–208, doi:10.1007/978-3-319-08867-9_13.","ista":"Esparza J, Kretinsky J. 2014. From LTL to deterministic automata: A safraless compositional approach. CAV: Computer Aided Verification, LNCS, vol. 8559, 192–208.","chicago":"Esparza, Javier, and Jan Kretinsky. “From LTL to Deterministic Automata: A Safraless Compositional Approach,” 8559:192–208. Springer, 2014. https://doi.org/10.1007/978-3-319-08867-9_13.","short":"J. Esparza, J. Kretinsky, in:, Springer, 2014, pp. 192–208."}},{"intvolume":" 8318","type":"conference","project":[{"grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","call_identifier":"FWF"},{"grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling","call_identifier":"FP7"}],"doi":"10.1007/978-3-642-54013-4_10","author":[{"last_name":"Dragoi","first_name":"Cezara","full_name":"Dragoi, Cezara","id":"2B2B5ED0-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724"},{"full_name":"Veith, Helmut","first_name":"Helmut","last_name":"Veith"},{"full_name":"Widder, Josef","first_name":"Josef","last_name":"Widder"},{"orcid":"0000-0002-3197-8736","id":"4397AC76-F248-11E8-B48F-1D18A9856A87","full_name":"Zufferey, Damien","last_name":"Zufferey","first_name":"Damien"}],"date_created":"2018-12-11T11:51:45Z","publisher":"Springer","_id":"1392","file":[{"creator":"system","file_name":"IST-2014-179-v1+1_vmcai14.pdf","date_created":"2018-12-12T10:11:06Z","date_updated":"2020-07-14T12:44:48Z","file_id":"4859","relation":"main_file","checksum":"bffa33d39be77df0da39defe97eabf84","access_level":"open_access","file_size":444138,"content_type":"application/pdf"}],"abstract":[{"text":"Fault-tolerant distributed algorithms play an important role in ensuring the reliability of many software applications. In this paper we consider distributed algorithms whose computations are organized in rounds. To verify the correctness of such algorithms, we reason about (i) properties (such as invariants) of the state, (ii) the transitions controlled by the algorithm, and (iii) the communication graph. We introduce a logic that addresses these points, and contains set comprehensions with cardinality constraints, function symbols to describe the local states of each process, and a limited form of quantifier alternation to express the verification conditions. We show its use in automating the verification of consensus algorithms. In particular, we give a semi-decision procedure for the unsatisfiability problem of the logic and identify a decidable fragment. We successfully applied our framework to verify the correctness of a variety of consensus algorithms tolerant to both benign faults (message loss, process crashes) and value faults (message corruption).","lang":"eng"}],"publication_status":"published","publist_id":"5817","file_date_updated":"2020-07-14T12:44:48Z","date_published":"2014-01-01T00:00:00Z","volume":8318,"year":"2014","oa":1,"alternative_title":["LNCS"],"has_accepted_license":"1","month":"01","day":"01","oa_version":"Submitted Version","ec_funded":1,"acknowledgement":"Supported by the Vienna Science and Technology Fund (WWTF) through grant PROSEED.","date_updated":"2021-01-12T06:50:22Z","title":"A logic-based framework for verifying consensus algorithms","quality_controlled":"1","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","language":[{"iso":"eng"}],"conference":{"start_date":"2014-01-19","name":"VMCAI: Verification, Model Checking and Abstract Interpretation","end_date":"2014-01-21","location":"San Diego, USA"},"scopus_import":1,"page":"161 - 181","citation":{"chicago":"Dragoi, Cezara, Thomas A Henzinger, Helmut Veith, Josef Widder, and Damien Zufferey. “A Logic-Based Framework for Verifying Consensus Algorithms,” 8318:161–81. Springer, 2014. https://doi.org/10.1007/978-3-642-54013-4_10.","mla":"Dragoi, Cezara, et al. A Logic-Based Framework for Verifying Consensus Algorithms. Vol. 8318, Springer, 2014, pp. 161–81, doi:10.1007/978-3-642-54013-4_10.","ista":"Dragoi C, Henzinger TA, Veith H, Widder J, Zufferey D. 2014. A logic-based framework for verifying consensus algorithms. VMCAI: Verification, Model Checking and Abstract Interpretation, LNCS, vol. 8318, 161–181.","short":"C. Dragoi, T.A. Henzinger, H. Veith, J. Widder, D. Zufferey, in:, Springer, 2014, pp. 161–181.","apa":"Dragoi, C., Henzinger, T. A., Veith, H., Widder, J., & Zufferey, D. (2014). A logic-based framework for verifying consensus algorithms (Vol. 8318, pp. 161–181). Presented at the VMCAI: Verification, Model Checking and Abstract Interpretation, San Diego, USA: Springer. https://doi.org/10.1007/978-3-642-54013-4_10","ama":"Dragoi C, Henzinger TA, Veith H, Widder J, Zufferey D. A logic-based framework for verifying consensus algorithms. In: Vol 8318. Springer; 2014:161-181. doi:10.1007/978-3-642-54013-4_10","ieee":"C. Dragoi, T. A. Henzinger, H. Veith, J. Widder, and D. Zufferey, “A logic-based framework for verifying consensus algorithms,” presented at the VMCAI: Verification, Model Checking and Abstract Interpretation, San Diego, USA, 2014, vol. 8318, pp. 161–181."},"pubrep_id":"179","status":"public","department":[{"_id":"ToHe"}],"ddc":["000","005"]},{"department":[{"_id":"ToHe"}],"ddc":["000"],"scopus_import":"1","citation":{"ista":"Gordon A, Henzinger TA, Nori A, Rajamani S. 2014. Probabilistic programming. Proceedings of the on Future of Software Engineering. FOSE: Future of Software Engineering, 167–181.","mla":"Gordon, Andrew, et al. “Probabilistic Programming.” Proceedings of the on Future of Software Engineering, ACM, 2014, pp. 167–81, doi:10.1145/2593882.2593900.","chicago":"Gordon, Andrew, Thomas A Henzinger, Aditya Nori, and Sriram Rajamani. “Probabilistic Programming.” In Proceedings of the on Future of Software Engineering, 167–81. ACM, 2014. https://doi.org/10.1145/2593882.2593900.","short":"A. Gordon, T.A. Henzinger, A. Nori, S. Rajamani, in:, Proceedings of the on Future of Software Engineering, ACM, 2014, pp. 167–181.","ieee":"A. Gordon, T. A. Henzinger, A. Nori, and S. Rajamani, “Probabilistic programming,” in Proceedings of the on Future of Software Engineering, Hyderabad, India, 2014, pp. 167–181.","apa":"Gordon, A., Henzinger, T. A., Nori, A., & Rajamani, S. (2014). Probabilistic programming. In Proceedings of the on Future of Software Engineering (pp. 167–181). Hyderabad, India: ACM. https://doi.org/10.1145/2593882.2593900","ama":"Gordon A, Henzinger TA, Nori A, Rajamani S. Probabilistic programming. In: Proceedings of the on Future of Software Engineering. ACM; 2014:167-181. doi:10.1145/2593882.2593900"},"page":"167 - 181","publication":"Proceedings of the on Future of Software Engineering","status":"public","quality_controlled":"1","conference":{"start_date":"2014-05-31","name":"FOSE: Future of Software Engineering","location":"Hyderabad, India","end_date":"2014-06-07"},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","language":[{"iso":"eng"}],"article_processing_charge":"No","date_updated":"2026-06-18T17:31:28Z","title":"Probabilistic programming","month":"05","day":"31","oa_version":"Published Version","ec_funded":1,"abstract":[{"lang":"eng","text":"Probabilistic programs are usual functional or imperative programs with two added constructs: (1) the ability to draw values at random from distributions, and (2) the ability to condition values of variables in a program via observations. Models from diverse application areas such as computer vision, coding theory, cryptographic protocols, biology and reliability analysis can be written as probabilistic programs. Probabilistic inference is the problem of computing an explicit representation of the probability distribution implicitly specified by a probabilistic program. Depending on the application, the desired output from inference may vary-we may want to estimate the expected value of some function f with respect to the distribution, or the mode of the distribution, or simply a set of samples drawn from the distribution. In this paper, we describe connections this research area called \\Probabilistic Programming" has with programming languages and software engineering, and this includes language design, and the static and dynamic analysis of programs. We survey current state of the art and speculate on promising directions for future research."}],"publication_status":"published","publist_id":"5816","date_published":"2014-05-31T00:00:00Z","year":"2014","oa":1,"publisher":"ACM","main_file_link":[{"open_access":"1","url":"https://doi.org/10.1145/2593882.2593900"}],"_id":"1393","type":"conference","project":[{"call_identifier":"FP7","name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989"},{"call_identifier":"FWF","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"}],"doi":"10.1145/2593882.2593900","date_created":"2018-12-11T11:51:45Z","author":[{"first_name":"Andrew","last_name":"Gordon","full_name":"Gordon, Andrew"},{"last_name":"Henzinger","first_name":"Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A"},{"full_name":"Nori, Aditya","last_name":"Nori","first_name":"Aditya"},{"first_name":"Sriram","last_name":"Rajamani","full_name":"Rajamani, Sriram"}]},{"alternative_title":["EPTCS"],"arxiv":1,"volume":169,"date_published":"2014-12-02T00:00:00Z","year":"2014","oa":1,"publist_id":"5435","abstract":[{"text":"In this paper we present INTERHORN, a solver for recursion-free Horn clauses. The main application domain of INTERHORN lies in solving interpolation problems arising in software verification. We show how a range of interpolation problems, including path, transition, nested, state/transition and well-founded interpolation can be handled directly by INTERHORN. By detailing these interpolation problems and their Horn clause representations, we hope to encourage the emergence of a common back-end interpolation interface useful for diverse verification tools.","lang":"eng"}],"publication_status":"published","oa_version":"Submitted Version","external_id":{"arxiv":["1303.7378"]},"day":"02","month":"12","author":[{"full_name":"Gupta, Ashutosh","id":"335E5684-F248-11E8-B48F-1D18A9856A87","last_name":"Gupta","first_name":"Ashutosh"},{"last_name":"Popeea","first_name":"Corneliu","full_name":"Popeea, Corneliu"},{"last_name":"Rybalchenko","first_name":"Andrey","full_name":"Rybalchenko, Andrey"}],"date_created":"2018-12-11T11:53:33Z","doi":"10.4204/EPTCS.169.5","type":"conference","intvolume":" 169","_id":"1702","main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1303.7378"}],"publisher":"Open Publishing Association","status":"public","citation":{"chicago":"Gupta, Ashutosh, Corneliu Popeea, and Andrey Rybalchenko. “Generalised Interpolation by Solving Recursion Free-Horn Clauses.” In Electronic Proceedings in Theoretical Computer Science, EPTCS, 169:31–38. Open Publishing Association, 2014. https://doi.org/10.4204/EPTCS.169.5.","ista":"Gupta A, Popeea C, Rybalchenko A. 2014. Generalised interpolation by solving recursion free-horn clauses. Electronic Proceedings in Theoretical Computer Science, EPTCS. HCVS: Horn Clauses for Verification and Synthesis, EPTCS, vol. 169, 31–38.","mla":"Gupta, Ashutosh, et al. “Generalised Interpolation by Solving Recursion Free-Horn Clauses.” Electronic Proceedings in Theoretical Computer Science, EPTCS, vol. 169, Open Publishing Association, 2014, pp. 31–38, doi:10.4204/EPTCS.169.5.","short":"A. Gupta, C. Popeea, A. Rybalchenko, in:, Electronic Proceedings in Theoretical Computer Science, EPTCS, Open Publishing Association, 2014, pp. 31–38.","apa":"Gupta, A., Popeea, C., & Rybalchenko, A. (2014). Generalised interpolation by solving recursion free-horn clauses. In Electronic Proceedings in Theoretical Computer Science, EPTCS (Vol. 169, pp. 31–38). Vienna, Austria: Open Publishing Association. https://doi.org/10.4204/EPTCS.169.5","ama":"Gupta A, Popeea C, Rybalchenko A. Generalised interpolation by solving recursion free-horn clauses. In: Electronic Proceedings in Theoretical Computer Science, EPTCS. Vol 169. Open Publishing Association; 2014:31-38. doi:10.4204/EPTCS.169.5","ieee":"A. Gupta, C. Popeea, and A. Rybalchenko, “Generalised interpolation by solving recursion free-horn clauses,” in Electronic Proceedings in Theoretical Computer Science, EPTCS, Vienna, Austria, 2014, vol. 169, pp. 31–38."},"page":"31 - 38","publication":"Electronic Proceedings in Theoretical Computer Science, EPTCS","scopus_import":"1","corr_author":"1","department":[{"_id":"ToHe"}],"title":"Generalised interpolation by solving recursion free-horn clauses","date_updated":"2025-06-11T08:03:28Z","article_processing_charge":"No","language":[{"iso":"eng"}],"conference":{"location":"Vienna, Austria","end_date":"2014-07-17","name":"HCVS: Horn Clauses for Verification and Synthesis","start_date":"2014-07-17"},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","quality_controlled":"1"},{"publisher":"Springer","_id":"1869","type":"conference","intvolume":" 8855","project":[{"call_identifier":"FP7","name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989"},{"_id":"25863FF4-B435-11E9-9278-68D0E5697425","name":"Game Theory","call_identifier":"FWF","grant_number":"S11407"}],"doi":"10.1007/978-3-319-13338-6_6","editor":[{"full_name":"Yahav, Eran","first_name":"Eran","last_name":"Yahav"}],"date_created":"2018-12-11T11:54:27Z","author":[{"full_name":"Hofferek, Georg","last_name":"Hofferek","first_name":"Georg"},{"id":"335E5684-F248-11E8-B48F-1D18A9856A87","full_name":"Gupta, Ashutosh","first_name":"Ashutosh","last_name":"Gupta"}],"month":"01","day":"01","oa_version":"None","ec_funded":1,"abstract":[{"lang":"eng","text":"Boolean controllers for systems with complex datapaths are often very difficult to implement correctly, in particular when concurrency is involved. Yet, in many instances it is easy to formally specify correctness. For example, the specification for the controller of a pipelined processor only has to state that the pipelined processor gives the same results as a non-pipelined reference design. This makes such controllers a good target for automated synthesis. However, an efficient abstraction for the complex datapath elements is needed, as a bit-precise description is often infeasible. We present Suraq, the first controller synthesis tool which uses uninterpreted functions for the abstraction. Quantified firstorder formulas (with specific quantifier structure) serve as the specification language from which Suraq synthesizes Boolean controllers. Suraq transforms the specification into an unsatisfiable SMT formula, and uses Craig interpolation to compute its results. Using Suraq, we were able to synthesize a controller (consisting of two Boolean signals) for a five-stage pipelined DLX processor in roughly one hour and 15 minutes."}],"publication_status":"published","publist_id":"5228","volume":8855,"date_published":"2014-01-01T00:00:00Z","year":"2014","alternative_title":["LNCS"],"quality_controlled":"1","user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","language":[{"iso":"eng"}],"conference":{"end_date":"2014-11-20","location":"Haifa, Israel","name":"HVC: Haifa Verification Conference","start_date":"2014-11-18"},"date_updated":"2024-10-21T06:02:48Z","acknowledgement":"The work presented in this paper was supported in part by the European Research Council (ERC) under grant agreement QUAINT (I774-N23)","title":"Suraq - a controller synthesis tool using uninterpreted functions","department":[{"_id":"ToHe"}],"scopus_import":"1","citation":{"mla":"Hofferek, Georg, and Ashutosh Gupta. “Suraq - a Controller Synthesis Tool Using Uninterpreted Functions.” HVC 2014, edited by Eran Yahav, vol. 8855, Springer, 2014, pp. 68–74, doi:10.1007/978-3-319-13338-6_6.","ista":"Hofferek G, Gupta A. 2014. Suraq - a controller synthesis tool using uninterpreted functions. HVC 2014. HVC: Haifa Verification Conference, LNCS, vol. 8855, 68–74.","chicago":"Hofferek, Georg, and Ashutosh Gupta. “Suraq - a Controller Synthesis Tool Using Uninterpreted Functions.” In HVC 2014, edited by Eran Yahav, 8855:68–74. Springer, 2014. https://doi.org/10.1007/978-3-319-13338-6_6.","short":"G. Hofferek, A. Gupta, in:, E. Yahav (Ed.), HVC 2014, Springer, 2014, pp. 68–74.","ieee":"G. Hofferek and A. Gupta, “Suraq - a controller synthesis tool using uninterpreted functions,” in HVC 2014, Haifa, Israel, 2014, vol. 8855, pp. 68–74.","ama":"Hofferek G, Gupta A. Suraq - a controller synthesis tool using uninterpreted functions. In: Yahav E, ed. HVC 2014. Vol 8855. Springer; 2014:68-74. doi:10.1007/978-3-319-13338-6_6","apa":"Hofferek, G., & Gupta, A. (2014). Suraq - a controller synthesis tool using uninterpreted functions. In E. Yahav (Ed.), HVC 2014 (Vol. 8855, pp. 68–74). Haifa, Israel: Springer. https://doi.org/10.1007/978-3-319-13338-6_6"},"page":"68 - 74","publication":"HVC 2014","status":"public"},{"department":[{"_id":"ToHe"}],"ddc":["004"],"corr_author":"1","publication":"Leibniz International Proceedings in Informatics, LIPIcs","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"page":"431 - 443","citation":{"ama":"Henzinger TA, Otop J, Samanta R. Lipschitz robustness of finite-state transducers. In: Leibniz International Proceedings in Informatics, LIPIcs. Vol 29. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2014:431-443. doi:10.4230/LIPIcs.FSTTCS.2014.431","apa":"Henzinger, T. A., Otop, J., & Samanta, R. (2014). Lipschitz robustness of finite-state transducers. In Leibniz International Proceedings in Informatics, LIPIcs (Vol. 29, pp. 431–443). Delhi, India: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.FSTTCS.2014.431","ieee":"T. A. Henzinger, J. Otop, and R. Samanta, “Lipschitz robustness of finite-state transducers,” in Leibniz International Proceedings in Informatics, LIPIcs, Delhi, India, 2014, vol. 29, pp. 431–443.","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.","chicago":"Henzinger, Thomas A, Jan Otop, and Roopsha Samanta. “Lipschitz Robustness of Finite-State Transducers.” In Leibniz International Proceedings in Informatics, LIPIcs, 29:431–43. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2014. https://doi.org/10.4230/LIPIcs.FSTTCS.2014.431.","mla":"Henzinger, Thomas A., et al. “Lipschitz Robustness of Finite-State Transducers.” Leibniz International Proceedings in Informatics, LIPIcs, vol. 29, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2014, pp. 431–43, doi:10.4230/LIPIcs.FSTTCS.2014.431.","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."},"scopus_import":"1","pubrep_id":"804","status":"public","conference":{"start_date":"2014-12-15","name":"FSTTCS: Foundations of Software Technology and Theoretical Computer Science","location":"Delhi, India","end_date":"2014-12-17"},"user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","language":[{"iso":"eng"}],"quality_controlled":"1","title":"Lipschitz robustness of finite-state transducers","date_updated":"2024-10-21T06:02:49Z","month":"12","has_accepted_license":"1","oa_version":"Published Version","day":"01","file_date_updated":"2020-07-14T12:45:19Z","publist_id":"5227","publication_status":"published","abstract":[{"lang":"eng","text":"We investigate the problem of checking if a finite-state transducer is robust to uncertainty in its input. Our notion of robustness is based on the analytic notion of Lipschitz continuity - a transducer is K-(Lipschitz) robust if the perturbation in its output is at most K times the perturbation in its input. We quantify input and output perturbation using similarity functions. We show that K-robustness is undecidable even for deterministic transducers. We identify a class of functional transducers, which admits a polynomial time automata-theoretic decision procedure for K-robustness. This class includes Mealy machines and functional letter-to-letter transducers. We also study K-robustness of nondeterministic transducers. Since a nondeterministic transducer generates a set of output words for each input word, we quantify output perturbation using setsimilarity functions. We show that K-robustness of nondeterministic transducers is undecidable, even for letter-to-letter transducers. We identify a class of set-similarity functions which admit decidable K-robustness of letter-to-letter transducers."}],"alternative_title":["LIPIcs"],"year":"2014","oa":1,"volume":29,"date_published":"2014-12-01T00:00:00Z","_id":"1870","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","file":[{"date_updated":"2020-07-14T12:45:19Z","creator":"system","date_created":"2018-12-12T10:09:11Z","file_name":"IST-2017-804-v1+1_37.pdf","content_type":"application/pdf","file_size":562151,"access_level":"open_access","checksum":"7b1aff1710a8bffb7080ec07f62d9a17","relation":"main_file","file_id":"4734"}],"intvolume":" 29","type":"conference","author":[{"last_name":"Henzinger","first_name":"Thomas A","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","full_name":"Otop, Jan","last_name":"Otop","first_name":"Jan"},{"full_name":"Samanta, Roopsha","id":"3D2AAC08-F248-11E8-B48F-1D18A9856A87","first_name":"Roopsha","last_name":"Samanta"}],"date_created":"2018-12-11T11:54:27Z","doi":"10.4230/LIPIcs.FSTTCS.2014.431"},{"alternative_title":["LNCS"],"year":"2014","oa":1,"date_published":"2014-09-01T00:00:00Z","volume":8723,"file_date_updated":"2020-07-14T12:45:19Z","publist_id":"5221","publication_status":"published","abstract":[{"lang":"eng","text":"We present a formal framework for repairing infinite-state, imperative, sequential programs, with (possibly recursive) procedures and multiple assertions; the framework can generate repaired programs by modifying the original erroneous program in multiple program locations, and can ensure the readability of the repaired program using user-defined expression templates; the framework also generates a set of inductive assertions that serve as a proof of correctness of the repaired program. As a step toward integrating programmer intent and intuition in automated program repair, we present a cost-aware formulation - given a cost function associated with permissible statement modifications, the goal is to ensure that the total program modification cost does not exceed a given repair budget. As part of our predicate abstractionbased solution framework, we present a sound and complete algorithm for repair of Boolean programs. We have developed a prototype tool based on SMT solving and used it successfully to repair diverse errors in benchmark C programs."}],"oa_version":"Submitted Version","day":"01","month":"09","has_accepted_license":"1","editor":[{"first_name":"Markus","last_name":"Müller-Olm","full_name":"Müller-Olm, Markus"},{"last_name":"Seidl","first_name":"Helmut","full_name":"Seidl, Helmut"}],"author":[{"last_name":"Samanta","first_name":"Roopsha","id":"3D2AAC08-F248-11E8-B48F-1D18A9856A87","full_name":"Samanta, Roopsha"},{"first_name":"Oswaldo","last_name":"Olivo","full_name":"Olivo, Oswaldo"},{"full_name":"Allen, Emerson","last_name":"Allen","first_name":"Emerson"}],"date_created":"2018-12-11T11:54:29Z","doi":"10.1007/978-3-319-10936-7_17","type":"conference","intvolume":" 8723","file":[{"date_updated":"2020-07-14T12:45:19Z","creator":"system","date_created":"2018-12-12T10:07:51Z","file_name":"IST-2014-313-v1+1_SOE.SAS14.pdf","content_type":"application/pdf","access_level":"open_access","file_size":409485,"checksum":"78ec4ea1bdecc676cd3e8cad35c6182c","relation":"main_file","file_id":"4650"}],"_id":"1875","publisher":"Springer","status":"public","pubrep_id":"313","page":"268 - 284","citation":{"ieee":"R. Samanta, O. Olivo, and E. Allen, “Cost-aware automatic program repair,” presented at the SAS: Static Analysis Symposium, Munich, Germany, 2014, vol. 8723, pp. 268–284.","apa":"Samanta, R., Olivo, O., & Allen, E. (2014). Cost-aware automatic program repair. In M. Müller-Olm & H. Seidl (Eds.) (Vol. 8723, pp. 268–284). Presented at the SAS: Static Analysis Symposium, Munich, Germany: Springer. https://doi.org/10.1007/978-3-319-10936-7_17","ama":"Samanta R, Olivo O, Allen E. Cost-aware automatic program repair. In: Müller-Olm M, Seidl H, eds. Vol 8723. Springer; 2014:268-284. doi:10.1007/978-3-319-10936-7_17","short":"R. Samanta, O. Olivo, E. Allen, in:, M. Müller-Olm, H. Seidl (Eds.), Springer, 2014, pp. 268–284.","ista":"Samanta R, Olivo O, Allen E. 2014. Cost-aware automatic program repair. SAS: Static Analysis Symposium, LNCS, vol. 8723, 268–284.","mla":"Samanta, Roopsha, et al. Cost-Aware Automatic Program Repair. Edited by Markus Müller-Olm and Helmut Seidl, vol. 8723, Springer, 2014, pp. 268–84, doi:10.1007/978-3-319-10936-7_17.","chicago":"Samanta, Roopsha, Oswaldo Olivo, and Emerson Allen. “Cost-Aware Automatic Program Repair.” edited by Markus Müller-Olm and Helmut Seidl, 8723:268–84. Springer, 2014. https://doi.org/10.1007/978-3-319-10936-7_17."},"scopus_import":1,"ddc":["000","005"],"department":[{"_id":"ToHe"}],"title":"Cost-aware automatic program repair","date_updated":"2021-01-12T06:53:46Z","user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","language":[{"iso":"eng"}],"conference":{"start_date":"2014-09-11","end_date":"2014-09-14","location":"Munich, Germany","name":"SAS: Static Analysis Symposium"},"quality_controlled":"1"},{"_id":"5411","publisher":"IST Austria","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","language":[{"iso":"eng"}],"file":[{"date_created":"2018-12-12T11:54:21Z","file_name":"IST-2014-148-v2+1_main_tr.pdf","creator":"system","date_updated":"2020-07-14T12:46:46Z","file_size":534732,"access_level":"open_access","content_type":"application/pdf","file_id":"5543","relation":"main_file","checksum":"0e03aba625cc334141a3148432aa5760"}],"type":"technical_report","title":"Compositional specifications for IOCO testing","date_created":"2018-12-12T11:39:11Z","author":[{"last_name":"Daca","first_name":"Przemyslaw","id":"49351290-F248-11E8-B48F-1D18A9856A87","full_name":"Daca, Przemyslaw"},{"first_name":"Thomas A","last_name":"Henzinger","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"},{"first_name":"Willibald","last_name":"Krenn","full_name":"Krenn, Willibald"},{"id":"41BCEE5C-F248-11E8-B48F-1D18A9856A87","full_name":"Nickovic, Dejan","last_name":"Nickovic","first_name":"Dejan"}],"publication_identifier":{"issn":["2664-1690"]},"doi":"10.15479/AT:IST-2014-148-v2-1","date_updated":"2025-09-29T11:40:47Z","department":[{"_id":"ToHe"}],"month":"01","has_accepted_license":"1","oa_version":"Published Version","day":"28","ddc":["000"],"file_date_updated":"2020-07-14T12:46:46Z","page":"20","related_material":{"record":[{"relation":"later_version","id":"2167","status":"public"}]},"citation":{"chicago":"Daca, Przemyslaw, Thomas A Henzinger, Willibald Krenn, and Dejan Nickovic. Compositional Specifications for IOCO Testing. IST Austria, 2014. https://doi.org/10.15479/AT:IST-2014-148-v2-1.","mla":"Daca, Przemyslaw, et al. Compositional Specifications for IOCO Testing. IST Austria, 2014, doi:10.15479/AT:IST-2014-148-v2-1.","ista":"Daca P, Henzinger TA, Krenn W, Nickovic D. 2014. Compositional specifications for IOCO testing, IST Austria, 20p.","short":"P. Daca, T.A. Henzinger, W. Krenn, D. Nickovic, Compositional Specifications for IOCO Testing, IST Austria, 2014.","ama":"Daca P, Henzinger TA, Krenn W, Nickovic D. Compositional Specifications for IOCO Testing. IST Austria; 2014. doi:10.15479/AT:IST-2014-148-v2-1","apa":"Daca, P., Henzinger, T. A., Krenn, W., & Nickovic, D. (2014). Compositional specifications for IOCO testing. IST Austria. https://doi.org/10.15479/AT:IST-2014-148-v2-1","ieee":"P. Daca, T. A. Henzinger, W. Krenn, and D. Nickovic, Compositional specifications for IOCO testing. IST Austria, 2014."},"publication_status":"published","abstract":[{"text":"Model-based testing is a promising technology for black-box software and hardware testing, in which test cases are generated automatically from high-level specifications. Nowadays, systems typically consist of multiple interacting components and, due to their complexity, testing presents a considerable portion of the effort and cost in the design process. Exploiting the compositional structure of system specifications can considerably reduce the effort in model-based testing. Moreover, inferring properties about the system from testing its individual components allows the designer to reduce the amount of integration testing.\r\nIn this paper, we study compositional properties of the IOCO-testing theory. We propose a new approach to composition and hiding operations, inspired by contract-based design and interface theories. These operations preserve behaviors that are compatible under composition and hiding, and prune away incompatible ones. The resulting specification characterizes the input sequences for which the unit testing of components is sufficient to infer the correctness of component integration without the need for further tests. We provide a methodology that uses these results to minimize integration testing effort, but also to detect potential weaknesses in specifications. While we focus on asynchronous models and the IOCO conformance relation, the resulting methodology can be applied to a broader class of systems.","lang":"eng"}],"alternative_title":["IST Austria Technical Report"],"year":"2014","oa":1,"date_published":"2014-01-28T00:00:00Z","pubrep_id":"152","status":"public"},{"publication_status":"published","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"}],"file_date_updated":"2020-07-14T12:46:49Z","page":"22","related_material":{"record":[{"relation":"later_version","id":"2217","status":"public"}]},"citation":{"ieee":"T. A. Henzinger and J. Otop, Model measuring for hybrid systems. IST Austria, 2014.","apa":"Henzinger, T. A., & Otop, J. (2014). Model measuring for hybrid systems. IST Austria. https://doi.org/10.15479/AT:IST-2014-171-v1-1","ama":"Henzinger TA, Otop J. Model Measuring for Hybrid Systems. IST Austria; 2014. doi:10.15479/AT:IST-2014-171-v1-1","ista":"Henzinger TA, Otop J. 2014. Model measuring for hybrid systems, IST Austria, 22p.","mla":"Henzinger, Thomas A., and Jan Otop. Model Measuring for Hybrid Systems. IST Austria, 2014, doi:10.15479/AT:IST-2014-171-v1-1.","chicago":"Henzinger, Thomas A, and Jan Otop. Model Measuring for Hybrid Systems. IST Austria, 2014. https://doi.org/10.15479/AT:IST-2014-171-v1-1.","short":"T.A. Henzinger, J. Otop, Model Measuring for Hybrid Systems, IST Austria, 2014."},"oa":1,"year":"2014","date_published":"2014-02-19T00:00:00Z","status":"public","pubrep_id":"171","alternative_title":["IST Austria Technical Report"],"month":"02","has_accepted_license":"1","department":[{"_id":"ToHe"}],"ddc":["005"],"day":"19","oa_version":"Published Version","type":"technical_report","doi":"10.15479/AT:IST-2014-171-v1-1","publication_identifier":{"issn":["2664-1690"]},"date_updated":"2025-06-26T08:32:32Z","title":"Model measuring for hybrid systems","author":[{"last_name":"Henzinger","first_name":"Thomas A","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Otop, Jan","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","first_name":"Jan","last_name":"Otop"}],"date_created":"2018-12-12T11:39:12Z","publisher":"IST Austria","_id":"5416","language":[{"iso":"eng"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","file":[{"creator":"system","file_name":"IST-2014-171-v1+1_report.pdf","date_created":"2018-12-12T11:53:32Z","date_updated":"2020-07-14T12:46:49Z","file_id":"5492","relation":"main_file","checksum":"445456d22371e4e49aad2b9a0c13bf80","access_level":"open_access","file_size":712077,"content_type":"application/pdf"}]}]