[{"das_tickbox":"1","ec_funded":1,"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)"},"department":[{"_id":"KrCh"},{"_id":"ToHe"}],"article_processing_charge":"No","external_id":{"isi":["000419163000005"]},"issue":"3","date_updated":"2026-07-06T13:27:53Z","title":"Edit distance for pushdown automata","publist_id":"7356","date_published":"2017-09-13T00:00:00Z","author":[{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu"},{"full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A"},{"orcid":"0000-0003-4783-0389","last_name":"Ibsen-Jensen","first_name":"Rasmus","id":"3B699956-F248-11E8-B48F-1D18A9856A87","full_name":"Ibsen-Jensen, Rasmus"},{"full_name":"Otop, Jan","last_name":"Otop","first_name":"Jan"}],"project":[{"call_identifier":"FWF","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","grant_number":"S11402-N23","name":"Moderne Concurrency Paradigms"},{"_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","name":"Formal methods for the design and analysis of complex systems"},{"name":"Quantitative Reactive Modeling","grant_number":"267989","call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications"},{"call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425","name":"Game Theory","grant_number":"S11407"}],"abstract":[{"text":"The edit distance between two words w 1 , w 2 is the minimal number of word operations (letter insertions, deletions, and substitutions) necessary to transform w 1 to w 2 . The edit distance generalizes to languages L 1 , L 2 , where the edit distance from L 1 to L 2 is the minimal number k such that for every word from L 1 there exists a word in L 2 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 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 the following problems: (1) deciding whether, for a given threshold k , the edit distance from a pushdown automaton to a finite automaton is at most k , and (2) deciding whether the edit distance from a pushdown automaton to a finite automaton is finite. ","lang":"eng"}],"publisher":"International Federation for Computational Logic","pubrep_id":"955","month":"09","year":"2017","language":[{"iso":"eng"}],"isi":1,"oa":1,"date_created":"2018-12-11T11:46:37Z","corr_author":"1","related_material":{"record":[{"relation":"earlier_version","id":"5438","status":"public"},{"status":"public","id":"1610","relation":"earlier_version"}]},"oa_version":"Published Version","publication":"Logical Methods in Computer Science","status":"public","type":"journal_article","publication_status":"published","intvolume":"        13","day":"13","_id":"465","publication_identifier":{"issn":["1860-5974"]},"scopus_import":"1","has_accepted_license":"1","ddc":["004"],"doi":"10.23638/LMCS-13(3:23)2017","volume":13,"license":"https://creativecommons.org/licenses/by-nd/4.0/","citation":{"mla":"Chatterjee, Krishnendu, et al. “Edit Distance for Pushdown Automata.” <i>Logical Methods in Computer Science</i>, vol. 13, no. 3, International Federation for Computational Logic, 2017, doi:<a href=\"https://doi.org/10.23638/LMCS-13(3:23)2017\">10.23638/LMCS-13(3:23)2017</a>.","ista":"Chatterjee K, Henzinger TA, Ibsen-Jensen R, Otop J. 2017. Edit distance for pushdown automata. Logical Methods in Computer Science. 13(3).","apa":"Chatterjee, K., Henzinger, T. A., Ibsen-Jensen, R., &#38; Otop, J. (2017). Edit distance for pushdown automata. <i>Logical Methods in Computer Science</i>. International Federation for Computational Logic. <a href=\"https://doi.org/10.23638/LMCS-13(3:23)2017\">https://doi.org/10.23638/LMCS-13(3:23)2017</a>","short":"K. Chatterjee, T.A. Henzinger, R. Ibsen-Jensen, J. Otop, Logical Methods in Computer Science 13 (2017).","ama":"Chatterjee K, Henzinger TA, Ibsen-Jensen R, Otop J. Edit distance for pushdown automata. <i>Logical Methods in Computer Science</i>. 2017;13(3). doi:<a href=\"https://doi.org/10.23638/LMCS-13(3:23)2017\">10.23638/LMCS-13(3:23)2017</a>","ieee":"K. Chatterjee, T. A. Henzinger, R. Ibsen-Jensen, and J. Otop, “Edit distance for pushdown automata,” <i>Logical Methods in Computer Science</i>, vol. 13, no. 3. International Federation for Computational Logic, 2017.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, Rasmus Ibsen-Jensen, and Jan Otop. “Edit Distance for Pushdown Automata.” <i>Logical Methods in Computer Science</i>. International Federation for Computational Logic, 2017. <a href=\"https://doi.org/10.23638/LMCS-13(3:23)2017\">https://doi.org/10.23638/LMCS-13(3:23)2017</a>."},"file_date_updated":"2020-07-14T12:46:33Z","quality_controlled":"1","file":[{"file_size":279071,"date_updated":"2020-07-14T12:46:33Z","checksum":"08041379ba408d40664f449eb5907a8f","content_type":"application/pdf","relation":"main_file","file_id":"5090","access_level":"open_access","date_created":"2018-12-12T10:14:37Z","creator":"system","file_name":"IST-2015-321-v1+1_main.pdf"},{"content_type":"application/pdf","relation":"main_file","file_id":"5091","file_size":279071,"date_updated":"2020-07-14T12:46:33Z","checksum":"08041379ba408d40664f449eb5907a8f","date_created":"2018-12-12T10:14:38Z","creator":"system","file_name":"IST-2018-955-v1+1_2017_Chatterjee_Edit_distance.pdf","access_level":"open_access"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87"},{"ec_funded":1,"das_tickbox":"1","external_id":{"arxiv":["1606.03598"],"isi":["000419237100006"]},"article_processing_charge":"No","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1606.03598"}],"author":[{"full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee"},{"first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","last_name":"Henzinger","full_name":"Henzinger, Thomas A"},{"id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","first_name":"Jan","last_name":"Otop","full_name":"Otop, Jan"}],"date_published":"2017-12-01T00:00:00Z","publist_id":"7354","title":"Nested weighted automata","issue":"4","date_updated":"2026-07-07T14:01:10Z","project":[{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","name":"Formal methods for the design and analysis of complex systems"},{"name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"publisher":"ACM","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."}],"isi":1,"language":[{"iso":"eng"}],"month":"12","year":"2017","oa":1,"corr_author":"1","related_material":{"record":[{"relation":"earlier_version","status":"public","id":"5415"},{"relation":"earlier_version","id":"5436","status":"public"},{"relation":"earlier_version","status":"public","id":"1656"}]},"date_created":"2018-12-11T11:46:38Z","arxiv":1,"type":"journal_article","oa_version":"Preprint","publication":"ACM Transactions on Computational Logic","status":"public","publication_identifier":{"issn":["1529-3785"]},"_id":"467","intvolume":"        18","day":"01","publication_status":"published","scopus_import":"1","doi":"10.1145/3152769","article_number":"31","citation":{"chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. “Nested Weighted Automata.” <i>ACM Transactions on Computational Logic</i>. ACM, 2017. <a href=\"https://doi.org/10.1145/3152769\">https://doi.org/10.1145/3152769</a>.","ieee":"K. Chatterjee, T. A. Henzinger, and J. Otop, “Nested weighted automata,” <i>ACM Transactions on Computational Logic</i>, vol. 18, no. 4. ACM, 2017.","mla":"Chatterjee, Krishnendu, et al. “Nested Weighted Automata.” <i>ACM Transactions on Computational Logic</i>, vol. 18, no. 4, 31, ACM, 2017, doi:<a href=\"https://doi.org/10.1145/3152769\">10.1145/3152769</a>.","ama":"Chatterjee K, Henzinger TA, Otop J. Nested weighted automata. <i>ACM Transactions on Computational Logic</i>. 2017;18(4). 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. 18(4), 31.","apa":"Chatterjee, K., Henzinger, T. A., &#38; Otop, J. (2017). Nested weighted automata. <i>ACM Transactions on Computational Logic</i>. ACM. <a href=\"https://doi.org/10.1145/3152769\">https://doi.org/10.1145/3152769</a>","short":"K. Chatterjee, T.A. Henzinger, J. Otop, ACM Transactions on Computational Logic 18 (2017)."},"volume":18,"quality_controlled":"1","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87"},{"abstract":[{"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.","lang":"eng"}],"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","pubrep_id":"795","project":[{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","name":"Formal methods for the design and analysis of complex systems"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications"},{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","name":"Efficient Algorithms for Computer Aided Verification","grant_number":"ICT15-003"}],"oa":1,"month":"08","year":"2016","language":[{"iso":"eng"}],"tmp":{"image":"/images/cc_by.png","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"ec_funded":1,"date_updated":"2025-07-10T11:50:02Z","title":"Nested weighted limit-average automata of bounded width","date_published":"2016-08-01T00:00:00Z","publist_id":"6286","author":[{"first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu"},{"orcid":"0000−0002−2985−7724","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","full_name":"Henzinger, Thomas A"},{"full_name":"Otop, Jan","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","first_name":"Jan","last_name":"Otop"}],"department":[{"_id":"KrCh"},{"_id":"ToHe"}],"article_processing_charge":"No","citation":{"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, Krakow; Poland, 2016, vol. 58.","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>.","short":"K. Chatterjee, T.A. Henzinger, J. Otop, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016.","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, 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>","ista":"Chatterjee K, Henzinger TA, Otop J. 2016. Nested weighted limit-average automata of bounded width. MFCS: Mathematical Foundations of Computer Science, 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>","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>."},"license":"https://creativecommons.org/licenses/by/4.0/","volume":58,"article_number":"24","doi":"10.4230/LIPIcs.MFCS.2016.24","file":[{"file_name":"IST-2017-795-v1+1_LIPIcs-MFCS-2016-24.pdf","creator":"system","date_created":"2018-12-12T10:17:31Z","access_level":"open_access","file_id":"5286","relation":"main_file","content_type":"application/pdf","date_updated":"2018-12-12T10:17:31Z","file_size":564560}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","file_date_updated":"2018-12-12T10:17:31Z","quality_controlled":"1","oa_version":"Published Version","status":"public","alternative_title":["LIPIcs"],"type":"conference","conference":{"end_date":"2016-08-26","location":"Krakow; Poland","name":"MFCS: Mathematical Foundations of Computer Science","start_date":"2016-08-22"},"date_created":"2018-12-11T11:50:05Z","scopus_import":"1","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.","has_accepted_license":"1","ddc":["004"],"publication_status":"published","intvolume":"        58","day":"01","_id":"1090"},{"tmp":{"image":"/images/cc_by.png","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"ec_funded":1,"title":"Linear distances between Markov chains","date_updated":"2026-04-15T10:02:12Z","author":[{"full_name":"Daca, Przemyslaw","id":"49351290-F248-11E8-B48F-1D18A9856A87","first_name":"Przemyslaw","last_name":"Daca"},{"last_name":"Henzinger","orcid":"0000−0002−2985−7724","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A"},{"full_name":"Kretinsky, Jan","last_name":"Kretinsky","orcid":"0000-0002-8122-2881","first_name":"Jan","id":"44CEF464-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Tatjana","id":"3D5811FC-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-9041-0905","last_name":"Petrov","full_name":"Petrov, Tatjana"}],"date_published":"2016-08-01T00:00:00Z","publist_id":"6283","department":[{"_id":"ToHe"},{"_id":"KrCh"},{"_id":"CaGu"}],"abstract":[{"text":"We introduce a general class of distances (metrics) between Markov chains, which are based on linear behaviour. This class encompasses distances given topologically (such as the total variation distance or trace distance) as well as by temporal logics or automata. We investigate which of the distances can be approximated by observing the systems, i.e. by black-box testing or simulation, and we provide both negative and positive results. ","lang":"eng"}],"pubrep_id":"794","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","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","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"},{"name":"Formal methods for the design and analysis of complex systems","grant_number":"Z211","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425"}],"oa":1,"month":"08","year":"2016","language":[{"iso":"eng"}],"status":"public","oa_version":"Published Version","conference":{"end_date":"2016-08-26","location":"Quebec City; Canada","start_date":"2016-08-23","name":"CONCUR: Concurrency Theory"},"type":"conference","alternative_title":["LIPIcs"],"date_created":"2018-12-11T11:50:06Z","related_material":{"record":[{"relation":"dissertation_contains","status":"public","id":"1155"}]},"scopus_import":1,"ddc":["004"],"has_accepted_license":"1","acknowledgement":"This research was funded in part by the European Research Council (ERC) under grant agreement 267989\r\n(QUAREM), the Austrian Science Fund (FWF) under grants project S11402-N23 (RiSE and SHiNE)\r\nand Z211-N23 (Wittgenstein Award), by the Czech Science Foundation Grant No. P202/12/G061, and\r\nby the SNSF Advanced Postdoc. Mobility Fellowship – grant number P300P2_161067.","day":"01","intvolume":"        59","publication_status":"published","_id":"1093","volume":59,"citation":{"chicago":"Daca, Przemyslaw, Thomas A Henzinger, Jan Kretinsky, and Tatjana Petrov. “Linear Distances between Markov Chains,” Vol. 59. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2016.20\">https://doi.org/10.4230/LIPIcs.CONCUR.2016.20</a>.","ieee":"P. Daca, T. A. Henzinger, J. Kretinsky, and T. Petrov, “Linear distances between Markov chains,” presented at the CONCUR: Concurrency Theory, Quebec City; Canada, 2016, vol. 59.","ama":"Daca P, Henzinger TA, Kretinsky J, Petrov T. Linear distances between Markov chains. In: Vol 59. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2016. doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2016.20\">10.4230/LIPIcs.CONCUR.2016.20</a>","apa":"Daca, P., Henzinger, T. A., Kretinsky, J., &#38; Petrov, T. (2016). Linear distances between Markov chains (Vol. 59). Presented at the CONCUR: Concurrency Theory, Quebec City; Canada: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2016.20\">https://doi.org/10.4230/LIPIcs.CONCUR.2016.20</a>","short":"P. Daca, T.A. Henzinger, J. Kretinsky, T. Petrov, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016.","ista":"Daca P, Henzinger TA, Kretinsky J, Petrov T. 2016. Linear distances between Markov chains. CONCUR: Concurrency Theory, LIPIcs, vol. 59, 20.","mla":"Daca, Przemyslaw, et al. <i>Linear Distances between Markov Chains</i>. Vol. 59, 20, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016, doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2016.20\">10.4230/LIPIcs.CONCUR.2016.20</a>."},"article_number":"20","doi":"10.4230/LIPIcs.CONCUR.2016.20","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","file":[{"date_updated":"2018-12-12T10:11:39Z","file_size":501827,"relation":"main_file","content_type":"application/pdf","file_id":"4895","access_level":"open_access","date_created":"2018-12-12T10:11:39Z","file_name":"IST-2017-794-v1+1_LIPIcs-CONCUR-2016-20.pdf","creator":"system"}],"file_date_updated":"2018-12-12T10:11:39Z","quality_controlled":"1"},{"oa":1,"language":[{"iso":"eng"}],"month":"08","year":"2016","pubrep_id":"793","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","abstract":[{"text":" The semantics of concurrent data structures is usually given by a sequential specification and a consistency condition. Linearizability is the most popular consistency condition due to its simplicity and general applicability. Nevertheless, for applications that do not require all guarantees offered by linearizability, recent research has focused on improving performance and scalability of concurrent data structures by relaxing their semantics. In this paper, we present local linearizability, a relaxed consistency condition that is applicable to container-type concurrent data structures like pools, queues, and stacks. While linearizability requires that the effect of each operation is observed by all threads at the same time, local linearizability only requires that for each thread T, the effects of its local insertion operations and the effects of those removal operations that remove values inserted by T are observed by all threads at the same time. We investigate theoretical and practical properties of local linearizability and its relationship to many existing consistency conditions. We present a generic implementation method for locally linearizable data structures that uses existing linearizable data structures as building blocks. Our implementations show performance and scalability improvements over the original building blocks and outperform the fastest existing container-type implementations. ","lang":"eng"}],"project":[{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"},{"name":"Quantitative Reactive Modeling","grant_number":"267989","call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"grant_number":"Z211","name":"Formal methods for the design and analysis of complex systems","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"date_published":"2016-08-01T00:00:00Z","publist_id":"6280","author":[{"full_name":"Haas, Andreas","first_name":"Andreas","last_name":"Haas"},{"orcid":"0000−0002−2985−7724","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","full_name":"Henzinger, Thomas A"},{"last_name":"Holzer","first_name":"Andreas","full_name":"Holzer, Andreas"},{"last_name":"Kirsch","first_name":"Christoph","full_name":"Kirsch, Christoph"},{"first_name":"Michael","last_name":"Lippautz","full_name":"Lippautz, Michael"},{"last_name":"Payer","first_name":"Hannes","full_name":"Payer, Hannes"},{"full_name":"Sezgin, Ali","first_name":"Ali","id":"4C7638DA-F248-11E8-B48F-1D18A9856A87","last_name":"Sezgin"},{"first_name":"Ana","last_name":"Sokolova","full_name":"Sokolova, Ana"},{"first_name":"Helmut","last_name":"Veith","full_name":"Veith, Helmut"}],"date_updated":"2025-04-15T06:25:58Z","title":"Local linearizability for concurrent container-type data structures","department":[{"_id":"ToHe"}],"tmp":{"image":"/images/cc_by.png","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"ec_funded":1,"file":[{"access_level":"open_access","date_created":"2018-12-12T10:10:10Z","file_name":"IST-2017-793-v1+1_LIPIcs-CONCUR-2016-6.pdf","creator":"system","date_updated":"2018-12-12T10:10:10Z","file_size":589747,"relation":"main_file","content_type":"application/pdf","file_id":"4795"}],"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","quality_controlled":"1","file_date_updated":"2018-12-12T10:10:10Z","article_number":"6","citation":{"ieee":"A. Haas <i>et al.</i>, “Local linearizability for concurrent container-type data structures,” in <i>Leibniz International Proceedings in Informatics</i>, Quebec City; Canada, 2016, vol. 59.","chicago":"Haas, Andreas, Thomas A Henzinger, Andreas Holzer, Christoph Kirsch, Michael Lippautz, Hannes Payer, Ali Sezgin, Ana Sokolova, and Helmut Veith. “Local Linearizability for Concurrent Container-Type Data Structures.” In <i>Leibniz International Proceedings in Informatics</i>, Vol. 59. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2016.6\">https://doi.org/10.4230/LIPIcs.CONCUR.2016.6</a>.","short":"A. Haas, T.A. Henzinger, A. Holzer, C. Kirsch, M. Lippautz, H. Payer, A. Sezgin, A. Sokolova, H. Veith, in:, Leibniz International Proceedings in Informatics, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016.","apa":"Haas, A., Henzinger, T. A., Holzer, A., Kirsch, C., Lippautz, M., Payer, H., … Veith, H. (2016). Local linearizability for concurrent container-type data structures. In <i>Leibniz International Proceedings in Informatics</i> (Vol. 59). Quebec City; Canada: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2016.6\">https://doi.org/10.4230/LIPIcs.CONCUR.2016.6</a>","ista":"Haas A, Henzinger TA, Holzer A, Kirsch C, Lippautz M, Payer H, Sezgin A, Sokolova A, Veith H. 2016. Local linearizability for concurrent container-type data structures. Leibniz International Proceedings in Informatics. CONCUR: Concurrency Theory, LIPIcs, vol. 59, 6.","ama":"Haas A, Henzinger TA, Holzer A, et al. Local linearizability for concurrent container-type data structures. In: <i>Leibniz International Proceedings in Informatics</i>. Vol 59. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2016. doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2016.6\">10.4230/LIPIcs.CONCUR.2016.6</a>","mla":"Haas, Andreas, et al. “Local Linearizability for Concurrent Container-Type Data Structures.” <i>Leibniz International Proceedings in Informatics</i>, vol. 59, 6, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016, doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2016.6\">10.4230/LIPIcs.CONCUR.2016.6</a>."},"volume":59,"doi":"10.4230/LIPIcs.CONCUR.2016.6","acknowledgement":"This work has been supported by the National Research Network RiSE on Rigorous Systems Engineering\r\n(Austrian Science Fund (FWF): S11402-N23, S11403-N23, S11404-N23, S11411-N23), a Google\r\nPhD Fellowship, an Erwin Schrödinger Fellowship (Austrian Science Fund (FWF): J3696-N26), EPSRC\r\ngrants EP/H005633/1 and EP/K008528/1, the Vienna Science and Technology Fund (WWTF) trough\r\ngrant PROSEED, the European Research Council (ERC) under grant 267989 (QUAREM) and by the\r\nAustrian Science Fund (FWF) under grant Z211-N23 (Wittgenstein Award).","has_accepted_license":"1","ddc":["004"],"scopus_import":1,"_id":"1095","publication_status":"published","intvolume":"        59","day":"01","alternative_title":["LIPIcs"],"type":"conference","conference":{"start_date":"2016-08-23","name":"CONCUR: Concurrency Theory","location":"Quebec City; Canada","end_date":"2016-08-26"},"oa_version":"Published Version","publication":"Leibniz International Proceedings in Informatics","status":"public","date_created":"2018-12-11T11:50:07Z"},{"department":[{"_id":"ToHe"}],"article_processing_charge":"No","external_id":{"arxiv":["1606.05473"]},"title":"Parallel reachability analysis for hybrid systems","date_updated":"2025-06-04T11:52:29Z","publist_id":"6272","date_published":"2016-12-27T00:00:00Z","main_file_link":[{"url":"https://arxiv.org/abs/1606.05473","open_access":"1"}],"author":[{"full_name":"Gurung, Amit","last_name":"Gurung","first_name":"Amit"},{"last_name":"Deka","first_name":"Arup","full_name":"Deka, Arup"},{"last_name":"Bartocci","first_name":"Ezio","full_name":"Bartocci, Ezio"},{"full_name":"Bogomolov, Sergiy","orcid":"0000-0002-0686-0365","last_name":"Bogomolov","first_name":"Sergiy","id":"369D9A44-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Radu","last_name":"Grosu","full_name":"Grosu, Radu"},{"full_name":"Ray, Rajarshi","first_name":"Rajarshi","last_name":"Ray"}],"ec_funded":1,"year":"2016","month":"12","language":[{"iso":"eng"}],"oa":1,"project":[{"grant_number":"267989","name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"name":"Formal methods for the design and analysis of complex systems","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"}],"abstract":[{"text":"We propose two parallel state-space-exploration algorithms for hybrid automaton (HA), with the goal of enhancing performance on multi-core shared-memory systems. The first uses the parallel, breadth-first-search algorithm (PBFS) of the SPIN model checker, when traversing the discrete modes of the HA, and enhances it with a parallel exploration of the continuous states within each mode. We show that this simple-minded extension of PBFS does not provide the desired load balancing in many HA benchmarks. The second algorithm is a task-parallel BFS algorithm (TP-BFS), which uses a cheap precomputation of the cost associated with the post operations (both continuous and discrete) in order to improve load balancing. We illustrate the TP-BFS and the cost precomputation of the post operators on a support-function-based algorithm for state-space exploration. The performance comparison of the two algorithms shows that, in general, TP-BFS provides a better utilization/load-balancing of the CPU. Both algorithms are implemented in the model checker XSpeed. Our experiments show a maximum speed-up of more than 2000 χ on a navigation benchmark, with respect to SpaceEx LGG scenario. In order to make the comparison fair, we employed an equal number of post operations in both tools. To the best of our knowledge, this paper represents the first attempt to provide parallel, reachability-analysis algorithms for HA.","lang":"eng"}],"publisher":"IEEE","publication_status":"published","day":"27","_id":"1103","scopus_import":"1","acknowledgement":"This work was supported in part by DST-SERB, GoI under Project No. YSS/2014/000623 and by the European Research Council (ERC) under grant 267989 (QUAREM) and by the Austrian Science Fund (FWF) under grants S11402-N23, S11405-N23 and S11412-N23 (RiSE/SHiNE) and Z211-N23 (Wittgenstein Award).","arxiv":1,"date_created":"2018-12-11T11:50:09Z","status":"public","oa_version":"Preprint","type":"conference","conference":{"end_date":"2016-11-20","location":"Kanpur, India ","start_date":"2016-11-18","name":"MEMOCODE: Conference on Formal Methods and Models for System Design"},"quality_controlled":"1","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","doi":"10.1109/MEMCOD.2016.7797741","citation":{"ieee":"A. Gurung, A. Deka, E. Bartocci, S. Bogomolov, R. Grosu, and R. Ray, “Parallel reachability analysis for hybrid systems,” presented at the MEMOCODE: Conference on Formal Methods and Models for System Design, Kanpur, India , 2016.","chicago":"Gurung, Amit, Arup Deka, Ezio Bartocci, Sergiy Bogomolov, Radu Grosu, and Rajarshi Ray. “Parallel Reachability Analysis for Hybrid Systems.” IEEE, 2016. <a href=\"https://doi.org/10.1109/MEMCOD.2016.7797741\">https://doi.org/10.1109/MEMCOD.2016.7797741</a>.","mla":"Gurung, Amit, et al. <i>Parallel Reachability Analysis for Hybrid Systems</i>. 7797741, IEEE, 2016, doi:<a href=\"https://doi.org/10.1109/MEMCOD.2016.7797741\">10.1109/MEMCOD.2016.7797741</a>.","apa":"Gurung, A., Deka, A., Bartocci, E., Bogomolov, S., Grosu, R., &#38; Ray, R. (2016). Parallel reachability analysis for hybrid systems. Presented at the MEMOCODE: Conference on Formal Methods and Models for System Design, Kanpur, India : IEEE. <a href=\"https://doi.org/10.1109/MEMCOD.2016.7797741\">https://doi.org/10.1109/MEMCOD.2016.7797741</a>","short":"A. Gurung, A. Deka, E. Bartocci, S. Bogomolov, R. Grosu, R. Ray, in:, IEEE, 2016.","ista":"Gurung A, Deka A, Bartocci E, Bogomolov S, Grosu R, Ray R. 2016. Parallel reachability analysis for hybrid systems. MEMOCODE: Conference on Formal Methods and Models for System Design, 7797741.","ama":"Gurung A, Deka A, Bartocci E, Bogomolov S, Grosu R, Ray R. Parallel reachability analysis for hybrid systems. In: IEEE; 2016. doi:<a href=\"https://doi.org/10.1109/MEMCOD.2016.7797741\">10.1109/MEMCOD.2016.7797741</a>"},"article_number":"7797741"},{"oa":1,"language":[{"iso":"eng"}],"year":"2016","month":"07","page":"151","publisher":"Institute of Science and Technology Austria","degree_awarded":"PhD","abstract":[{"lang":"eng","text":"In this thesis we present a computer-aided programming approach to concurrency. Our approach helps the programmer by automatically fixing concurrency-related bugs, i.e. bugs that occur when the program is executed using an aggressive preemptive scheduler, but not when using a non-preemptive (cooperative) scheduler. Bugs are program behaviours that are incorrect w.r.t. a specification. We consider both user-provided explicit specifications in the form of assertion\r\nstatements in the code as well as an implicit specification. The implicit specification is inferred from the non-preemptive behaviour. Let us consider sequences of calls that the program makes to an external interface. The implicit specification requires that any such sequence produced under a preemptive scheduler should be included in the set of sequences produced under a non-preemptive scheduler. We consider several semantics-preserving fixes that go beyond atomic sections typically explored in the synchronisation synthesis literature. Our synthesis is able to place locks, barriers and wait-signal statements and last, but not least reorder independent statements. The latter may be useful if a thread is released to early, e.g., before some initialisation is completed. We guarantee that our synthesis does not introduce deadlocks and that the synchronisation inserted is optimal w.r.t. a given objective function. We dub our solution trace-based synchronisation synthesis and it is loosely based on counterexample-guided inductive synthesis (CEGIS). The synthesis works by discovering a trace that is incorrect w.r.t. the specification and identifying ordering constraints crucial to trigger the specification violation. Synchronisation may be placed immediately (greedy approach) or delayed until all incorrect traces are found (non-greedy approach). For the non-greedy approach we construct a set of global constraints over synchronisation placements. Each model of the global constraints set corresponds to a correctness-ensuring synchronisation placement. The placement that is optimal w.r.t. the given objective function is chosen as the synchronisation solution. We evaluate our approach on a number of realistic (albeit simplified) Linux device-driver\r\nbenchmarks. The benchmarks are versions of the drivers with known concurrency-related bugs. For the experiments with an explicit specification we added assertions that would detect the bugs in the experiments. Device drivers lend themselves to implicit specification, where the device and the operating system are the external interfaces. Our experiments demonstrate that our synthesis method is precise and efficient. We implemented objective functions for coarse-grained and fine-grained locking and observed that different synchronisation placements are produced for our experiments, favouring e.g. a minimal number of synchronisation operations or maximum concurrency."}],"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","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"},{"grant_number":"Z211","name":"Formal methods for the design and analysis of complex systems","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425"}],"main_file_link":[{"open_access":"1","url":"http://thorstent.github.io/theses/phd_thorsten_tarrach.pdf"}],"author":[{"full_name":"Tarrach, Thorsten","first_name":"Thorsten","id":"3D6E8F2C-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-4409-8487","last_name":"Tarrach"}],"publist_id":"6230","date_published":"2016-07-07T00:00:00Z","title":"Automatic synthesis of synchronisation primitives for concurrent programs","date_updated":"2026-04-09T10:54:01Z","article_processing_charge":"No","department":[{"_id":"ToHe"},{"_id":"GradSch"}],"ec_funded":1,"user_id":"ba8df636-2132-11f1-aed0-ed93e2281fdd","file":[{"content_type":"application/pdf","relation":"main_file","file_id":"9179","file_size":1523935,"date_updated":"2021-02-22T11:39:32Z","checksum":"319a506831650327e85376db41fc1094","date_created":"2021-02-22T11:39:32Z","success":1,"creator":"dernst","file_name":"2016_Tarrach_Thesis.pdf","access_level":"open_access"},{"access_level":"closed","file_name":"2016_Tarrach_Thesispdfa.pdf","creator":"cchlebak","date_created":"2021-11-16T14:14:38Z","checksum":"39efcd789f0ad859ff15652cb7afc412","date_updated":"2021-11-17T13:46:55Z","file_size":1306068,"file_id":"10296","relation":"main_file","content_type":"application/pdf"}],"file_date_updated":"2021-11-17T13:46:55Z","citation":{"mla":"Tarrach, Thorsten. <i>Automatic Synthesis of Synchronisation Primitives for Concurrent Programs</i>. Institute of Science and Technology Austria, 2016, doi:<a href=\"https://doi.org/10.15479/at:ista:1130\">10.15479/at:ista:1130</a>.","apa":"Tarrach, T. (2016). <i>Automatic synthesis of synchronisation primitives for concurrent programs</i>. Institute of Science and Technology Austria. <a href=\"https://doi.org/10.15479/at:ista:1130\">https://doi.org/10.15479/at:ista:1130</a>","short":"T. Tarrach, Automatic Synthesis of Synchronisation Primitives for Concurrent Programs, Institute of Science and Technology Austria, 2016.","ista":"Tarrach T. 2016. Automatic synthesis of synchronisation primitives for concurrent programs. Institute of Science and Technology Austria.","ama":"Tarrach T. Automatic synthesis of synchronisation primitives for concurrent programs. 2016. doi:<a href=\"https://doi.org/10.15479/at:ista:1130\">10.15479/at:ista:1130</a>","ieee":"T. Tarrach, “Automatic synthesis of synchronisation primitives for concurrent programs,” Institute of Science and Technology Austria, 2016.","chicago":"Tarrach, Thorsten. “Automatic Synthesis of Synchronisation Primitives for Concurrent Programs.” Institute of Science and Technology Austria, 2016. <a href=\"https://doi.org/10.15479/at:ista:1130\">https://doi.org/10.15479/at:ista:1130</a>."},"doi":"10.15479/at:ista:1130","ddc":["000"],"has_accepted_license":"1","publication_identifier":{"issn":["2663-337X"]},"_id":"1130","OA_place":"publisher","day":"07","publication_status":"published","supervisor":[{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","last_name":"Henzinger"}],"alternative_title":["ISTA Thesis"],"type":"dissertation","status":"public","oa_version":"Published Version","corr_author":"1","related_material":{"record":[{"relation":"part_of_dissertation","id":"2218","status":"public"},{"relation":"part_of_dissertation","status":"public","id":"2445"},{"status":"public","id":"1729","relation":"part_of_dissertation"}]},"date_created":"2018-12-11T11:50:19Z"},{"_id":"1134","department":[{"_id":"ToHe"}],"day":"10","publication_status":"published","author":[{"last_name":"Duggirala","first_name":"Parasara","full_name":"Duggirala, Parasara"},{"last_name":"Fan","first_name":"Chuchu","full_name":"Fan, Chuchu"},{"full_name":"Potok, Matthew","first_name":"Matthew","last_name":"Potok"},{"full_name":"Qi, Bolun","first_name":"Bolun","last_name":"Qi"},{"full_name":"Mitra, Sayan","first_name":"Sayan","last_name":"Mitra"},{"full_name":"Viswanathan, Mahesh","last_name":"Viswanathan","first_name":"Mahesh"},{"last_name":"Bak","first_name":"Stanley","full_name":"Bak, Stanley"},{"id":"369D9A44-F248-11E8-B48F-1D18A9856A87","first_name":"Sergiy","orcid":"0000-0002-0686-0365","last_name":"Bogomolov","full_name":"Bogomolov, Sergiy"},{"first_name":"Taylor","last_name":"Johnson","full_name":"Johnson, Taylor"},{"last_name":"Nguyen","first_name":"Luan","full_name":"Nguyen, Luan"},{"full_name":"Schilling, Christian","orcid":"0000-0003-3658-1065","last_name":"Schilling","id":"3A2F4DCE-F248-11E8-B48F-1D18A9856A87","first_name":"Christian"},{"full_name":"Sogokon, Andrew","last_name":"Sogokon","first_name":"Andrew"},{"full_name":"Tran, Hoang","first_name":"Hoang","last_name":"Tran"},{"full_name":"Xiang, Weiming","last_name":"Xiang","first_name":"Weiming"}],"date_published":"2016-10-10T00:00:00Z","publist_id":"6224","scopus_import":1,"title":"Tutorial: Software tools for hybrid systems verification transformation and synthesis C2E2 HyST and TuLiP","date_updated":"2021-01-12T06:48:32Z","date_created":"2018-12-11T11:50:20Z","conference":{"end_date":"2016-09-22","name":"CCA: Control Applications ","start_date":"2016-09-19","location":"Buenos Aires, Argentina "},"type":"conference","status":"public","publication":"2016 IEEE Conference on Control Applications","oa_version":"None","language":[{"iso":"eng"}],"quality_controlled":"1","year":"2016","month":"10","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","doi":"10.1109/CCA.2016.7587948","article_number":"7587948","publisher":"IEEE","abstract":[{"text":"Hybrid systems have both continuous and discrete dynamics and are useful for modeling a variety of control systems, from air traffic control protocols to robotic maneuvers and beyond. Recently, numerous powerful and scalable tools for analyzing hybrid systems have emerged. Several of these tools implement automated formal methods for mathematically proving a system meets a specification. This tutorial session will present three recent hybrid systems tools: C2E2, HyST, and TuLiP. C2E2 is a simulated-based verification tool for hybrid systems, and uses validated numerical solvers and bloating of simulation traces to verify systems meet specifications. HyST is a hybrid systems model transformation and translation tool, and uses a canonical intermediate representation to support most of the recent verification tools, as well as automated sound abstractions that simplify verification of a given hybrid system. TuLiP is a controller synthesis tool for hybrid systems, where given a temporal logic specification to be satisfied for a system (plant) model, TuLiP will find a controller that meets a given specification. © 2016 IEEE.","lang":"eng"}],"citation":{"mla":"Duggirala, Parasara, et al. “Tutorial: Software Tools for Hybrid Systems Verification Transformation and Synthesis C2E2 HyST and TuLiP.” <i>2016 IEEE Conference on Control Applications</i>, 7587948, IEEE, 2016, doi:<a href=\"https://doi.org/10.1109/CCA.2016.7587948\">10.1109/CCA.2016.7587948</a>.","ama":"Duggirala P, Fan C, Potok M, et al. Tutorial: Software tools for hybrid systems verification transformation and synthesis C2E2 HyST and TuLiP. In: <i>2016 IEEE Conference on Control Applications</i>. IEEE; 2016. doi:<a href=\"https://doi.org/10.1109/CCA.2016.7587948\">10.1109/CCA.2016.7587948</a>","apa":"Duggirala, P., Fan, C., Potok, M., Qi, B., Mitra, S., Viswanathan, M., … Xiang, W. (2016). Tutorial: Software tools for hybrid systems verification transformation and synthesis C2E2 HyST and TuLiP. In <i>2016 IEEE Conference on Control Applications</i>. Buenos Aires, Argentina : IEEE. <a href=\"https://doi.org/10.1109/CCA.2016.7587948\">https://doi.org/10.1109/CCA.2016.7587948</a>","ista":"Duggirala P, Fan C, Potok M, Qi B, Mitra S, Viswanathan M, Bak S, Bogomolov S, Johnson T, Nguyen L, Schilling C, Sogokon A, Tran H, Xiang W. 2016. Tutorial: Software tools for hybrid systems verification transformation and synthesis C2E2 HyST and TuLiP. 2016 IEEE Conference on Control Applications. CCA: Control Applications , 7587948.","short":"P. Duggirala, C. Fan, M. Potok, B. Qi, S. Mitra, M. Viswanathan, S. Bak, S. Bogomolov, T. Johnson, L. Nguyen, C. Schilling, A. Sogokon, H. Tran, W. Xiang, in:, 2016 IEEE Conference on Control Applications, IEEE, 2016.","chicago":"Duggirala, Parasara, Chuchu Fan, Matthew Potok, Bolun Qi, Sayan Mitra, Mahesh Viswanathan, Stanley Bak, et al. “Tutorial: Software Tools for Hybrid Systems Verification Transformation and Synthesis C2E2 HyST and TuLiP.” In <i>2016 IEEE Conference on Control Applications</i>. IEEE, 2016. <a href=\"https://doi.org/10.1109/CCA.2016.7587948\">https://doi.org/10.1109/CCA.2016.7587948</a>.","ieee":"P. Duggirala <i>et al.</i>, “Tutorial: Software tools for hybrid systems verification transformation and synthesis C2E2 HyST and TuLiP,” in <i>2016 IEEE Conference on Control Applications</i>, Buenos Aires, Argentina , 2016."}},{"ec_funded":1,"date_published":"2016-10-01T00:00:00Z","publist_id":"6223","author":[{"last_name":"Avni","orcid":"0000-0001-5588-8287","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","first_name":"Guy","full_name":"Avni, Guy"},{"last_name":"Guha","first_name":"Shibashis","full_name":"Guha, Shibashis"},{"full_name":"Rodríguez Navas, Guillermo","last_name":"Rodríguez Navas","first_name":"Guillermo"}],"date_updated":"2025-09-22T14:14:05Z","title":"Synthesizing time triggered schedules for switched networks with faulty links","article_processing_charge":"No","external_id":{"isi":["000414220100026"]},"department":[{"_id":"ToHe"}],"pubrep_id":"644","publisher":"ACM","abstract":[{"lang":"eng","text":"Time-triggered (TT) switched networks are a deterministic communication infrastructure used by real-time distributed embedded systems. These networks rely on the notion of globally discretized time (i.e. time slots) and a static TT schedule that prescribes which message is sent through which link at every time slot, such that all messages reach their destination before a global timeout. These schedules are generated offline, assuming a static network with fault-free links, and entrusting all error-handling functions to the end user. Assuming the network is static is an over-optimistic view, and indeed links tend to fail in practice. We study synthesis of TT schedules on a network in which links fail over time and we assume the switches run a very simple error-recovery protocol once they detect a crashed link. We address the problem of finding a pk; qresistant schedule; namely, one that, assuming the switches run a fixed error-recovery protocol, guarantees that the number of messages that arrive at their destination by the timeout is at least no matter what sequence of at most k links fail. Thus, we maintain the simplicity of the switches while giving a guarantee on the number of messages that meet the timeout. We show how a pk; q-resistant schedule can be obtained using a CEGAR-like approach: find a schedule, decide whether it is pk; q-resistant, and if it is not, use the witnessing fault sequence to generate a constraint that is added to the program. The newly added constraint disallows the schedule to be regenerated in a future iteration while also eliminating several other schedules that are not pk; q-resistant. We illustrate the applicability of our approach using an SMT-based implementation. © 2016 ACM."}],"project":[{"name":"Quantitative Reactive Modeling","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"name":"Formal methods for the design and analysis of complex systems","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"oa":1,"language":[{"iso":"eng"}],"isi":1,"year":"2016","month":"10","type":"conference","conference":{"end_date":"2016-10-07","name":"EMSOFT: Embedded Software ","start_date":"2016-10-01","location":"Pittsburgh, PA, USA"},"status":"public","publication":"Proceedings of the 13th International Conference on Embedded Software ","oa_version":"Submitted Version","date_created":"2018-12-11T11:50:20Z","has_accepted_license":"1","ddc":["000"],"scopus_import":"1","_id":"1135","publication_status":"published","day":"01","article_number":"26","citation":{"ista":"Avni G, Guha S, Rodríguez Navas G. 2016. Synthesizing time triggered schedules for switched networks with faulty links. Proceedings of the 13th International Conference on Embedded Software . EMSOFT: Embedded Software , 26.","apa":"Avni, G., Guha, S., &#38; Rodríguez Navas, G. (2016). Synthesizing time triggered schedules for switched networks with faulty links. In <i>Proceedings of the 13th International Conference on Embedded Software </i>. Pittsburgh, PA, USA: ACM. <a href=\"https://doi.org/10.1145/2968478.2968499\">https://doi.org/10.1145/2968478.2968499</a>","short":"G. Avni, S. Guha, G. Rodríguez Navas, in:, Proceedings of the 13th International Conference on Embedded Software , ACM, 2016.","ama":"Avni G, Guha S, Rodríguez Navas G. Synthesizing time triggered schedules for switched networks with faulty links. In: <i>Proceedings of the 13th International Conference on Embedded Software </i>. ACM; 2016. doi:<a href=\"https://doi.org/10.1145/2968478.2968499\">10.1145/2968478.2968499</a>","mla":"Avni, Guy, et al. “Synthesizing Time Triggered Schedules for Switched Networks with Faulty Links.” <i>Proceedings of the 13th International Conference on Embedded Software </i>, 26, ACM, 2016, doi:<a href=\"https://doi.org/10.1145/2968478.2968499\">10.1145/2968478.2968499</a>.","ieee":"G. Avni, S. Guha, and G. Rodríguez Navas, “Synthesizing time triggered schedules for switched networks with faulty links,” in <i>Proceedings of the 13th International Conference on Embedded Software </i>, Pittsburgh, PA, USA, 2016.","chicago":"Avni, Guy, Shibashis Guha, and Guillermo Rodríguez Navas. “Synthesizing Time Triggered Schedules for Switched Networks with Faulty Links.” In <i>Proceedings of the 13th International Conference on Embedded Software </i>. ACM, 2016. <a href=\"https://doi.org/10.1145/2968478.2968499\">https://doi.org/10.1145/2968478.2968499</a>."},"doi":"10.1145/2968478.2968499","file":[{"file_size":279240,"date_updated":"2018-12-12T10:09:31Z","content_type":"application/pdf","relation":"main_file","file_id":"4755","access_level":"open_access","date_created":"2018-12-12T10:09:31Z","creator":"system","file_name":"IST-2016-644-v1+1_emsoft-no-format.pdf"}],"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","quality_controlled":"1","file_date_updated":"2018-12-12T10:09:31Z"},{"citation":{"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.","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.","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."},"doi":"10.1145/2933575.2933588","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","quality_controlled":"1","conference":{"end_date":"2016-07-08","start_date":"2016-07-05","name":"LICS: Logic in Computer Science","location":"New York, NY, USA"},"type":"conference","oa_version":"Preprint","status":"public","publication":"Proceedings of the 31st Annual ACM/IEEE Symposium","arxiv":1,"date_created":"2018-12-11T11:50:21Z","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","scopus_import":"1","_id":"1138","day":"05","publication_status":"published","publisher":"IEEE","abstract":[{"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.","lang":"eng"}],"project":[{"name":"Quantitative Reactive Modeling","grant_number":"267989","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"},{"name":"Formal methods for the design and analysis of complex systems","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications"},{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","name":"Efficient Algorithms for Computer Aided Verification","grant_number":"ICT15-003"}],"oa":1,"isi":1,"language":[{"iso":"eng"}],"month":"07","page":"76 - 85","year":"2016","ec_funded":1,"author":[{"first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"},{"last_name":"Henzinger","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","full_name":"Henzinger, Thomas A"},{"full_name":"Otop, Jan","last_name":"Otop","first_name":"Jan","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87"}],"main_file_link":[{"url":"https://arxiv.org/abs/1604.06764","open_access":"1"}],"date_published":"2016-07-05T00:00:00Z","publist_id":"6220","title":"Quantitative automata under probabilistic semantics","date_updated":"2025-09-22T14:12:47Z","external_id":{"arxiv":["1604.06764"],"isi":["000387609200008"]},"article_processing_charge":"No","department":[{"_id":"KrCh"},{"_id":"ToHe"}]},{"quality_controlled":"1","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","doi":"10.1016/j.biosystems.2016.07.005","citation":{"ieee":"C. Schilling, S. Bogomolov, T. A. Henzinger, A. Podelski, and J. Ruess, “Adaptive moment closure for parameter inference of biochemical reaction networks,” <i>Biosystems</i>, vol. 149. Elsevier, pp. 15–25, 2016.","chicago":"Schilling, Christian, Sergiy Bogomolov, Thomas A Henzinger, Andreas Podelski, and Jakob Ruess. “Adaptive Moment Closure for Parameter Inference of Biochemical Reaction Networks.” <i>Biosystems</i>. Elsevier, 2016. <a href=\"https://doi.org/10.1016/j.biosystems.2016.07.005\">https://doi.org/10.1016/j.biosystems.2016.07.005</a>.","apa":"Schilling, C., Bogomolov, S., Henzinger, T. A., Podelski, A., &#38; Ruess, J. (2016). Adaptive moment closure for parameter inference of biochemical reaction networks. <i>Biosystems</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.biosystems.2016.07.005\">https://doi.org/10.1016/j.biosystems.2016.07.005</a>","ista":"Schilling C, Bogomolov S, Henzinger TA, Podelski A, Ruess J. 2016. Adaptive moment closure for parameter inference of biochemical reaction networks. Biosystems. 149, 15–25.","short":"C. Schilling, S. Bogomolov, T.A. Henzinger, A. Podelski, J. Ruess, Biosystems 149 (2016) 15–25.","ama":"Schilling C, Bogomolov S, Henzinger TA, Podelski A, Ruess J. Adaptive moment closure for parameter inference of biochemical reaction networks. <i>Biosystems</i>. 2016;149:15-25. doi:<a href=\"https://doi.org/10.1016/j.biosystems.2016.07.005\">10.1016/j.biosystems.2016.07.005</a>","mla":"Schilling, Christian, et al. “Adaptive Moment Closure for Parameter Inference of Biochemical Reaction Networks.” <i>Biosystems</i>, vol. 149, Elsevier, 2016, pp. 15–25, doi:<a href=\"https://doi.org/10.1016/j.biosystems.2016.07.005\">10.1016/j.biosystems.2016.07.005</a>."},"volume":149,"_id":"1148","intvolume":"       149","day":"01","publication_status":"published","acknowledgement":"This work is based on the CMSB 2015 paper “Adaptive moment closure for parameter inference of biochemical reaction networks” (Bogomolov et al., 2015). The work was partly supported by the German Research Foundation (DFG) as part of the Transregional Collaborative Research Center “Automatic Verification and Analysis of Complex Systems” (SFB/TR 14 AVACS1), by the European Research Council (ERC) under grant 267989 (QUAREM) and by the Austrian Science Fund (FWF) under grants S11402-N23 (RiSE) and Z211-N23 (Wittgenstein Award). J.R. acknowledges support from the People Programme (Marie Curie Actions) of the European Union's Seventh Framework Programme (FP7/2007-2013) under REA grant agreement no. 291734.","scopus_import":"1","related_material":{"record":[{"relation":"earlier_version","status":"public","id":"1658"}]},"date_created":"2018-12-11T11:50:24Z","type":"journal_article","status":"public","publication":"Biosystems","oa_version":"None","isi":1,"language":[{"iso":"eng"}],"month":"11","year":"2016","page":"15 - 25","project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"267989","name":"Quantitative Reactive Modeling"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","name":"Formal methods for the design and analysis of complex systems"},{"_id":"25681D80-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"291734","name":"International IST Postdoc Fellowship Programme"}],"publisher":"Elsevier","abstract":[{"text":"Continuous-time Markov chain (CTMC) models have become a central tool for understanding the dynamics of complex reaction networks and the importance of stochasticity in the underlying biochemical processes. When such models are employed to answer questions in applications, in order to ensure that the model provides a sufficiently accurate representation of the real system, it is of vital importance that the model parameters are inferred from real measured data. This, however, is often a formidable task and all of the existing methods fail in one case or the other, usually because the underlying CTMC model is high-dimensional and computationally difficult to analyze. The parameter inference methods that tend to scale best in the dimension of the CTMC are based on so-called moment closure approximations. However, there exists a large number of different moment closure approximations and it is typically hard to say a priori which of the approximations is the most suitable for the inference procedure. Here, we propose a moment-based parameter inference method that automatically chooses the most appropriate moment closure method. Accordingly, contrary to existing methods, the user is not required to be experienced in moment closure techniques. In addition to that, our method adaptively changes the approximation during the parameter inference to ensure that always the best approximation is used, even in cases where different approximations are best in different regions of the parameter space. © 2016 Elsevier Ireland Ltd","lang":"eng"}],"external_id":{"isi":["000390743600003"]},"article_processing_charge":"No","department":[{"_id":"ToHe"},{"_id":"GaTk"}],"author":[{"first_name":"Christian","last_name":"Schilling","full_name":"Schilling, Christian"},{"full_name":"Bogomolov, Sergiy","id":"369D9A44-F248-11E8-B48F-1D18A9856A87","first_name":"Sergiy","last_name":"Bogomolov","orcid":"0000-0002-0686-0365"},{"last_name":"Henzinger","orcid":"0000−0002−2985−7724","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A"},{"last_name":"Podelski","first_name":"Andreas","full_name":"Podelski, Andreas"},{"full_name":"Ruess, Jakob","id":"4A245D00-F248-11E8-B48F-1D18A9856A87","first_name":"Jakob","last_name":"Ruess","orcid":"0000-0003-1615-3282"}],"date_published":"2016-11-01T00:00:00Z","publist_id":"6210","date_updated":"2025-09-23T07:44:57Z","title":"Adaptive moment closure for parameter inference of biochemical reaction networks","ec_funded":1},{"ec_funded":1,"main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.1511.08456"}],"author":[{"full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee"},{"last_name":"Chmelik","first_name":"Martin","id":"3624234E-F248-11E8-B48F-1D18A9856A87","full_name":"Chmelik, Martin"},{"full_name":"Davies, Jessica","last_name":"Davies","first_name":"Jessica","id":"378E0060-F248-11E8-B48F-1D18A9856A87"}],"date_published":"2016-12-02T00:00:00Z","publist_id":"6191","date_updated":"2025-06-25T11:52:14Z","title":"A symbolic SAT based algorithm for almost sure reachability with small strategies in POMDPs","external_id":{"arxiv":["1511.08456"]},"article_processing_charge":"No","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"publisher":"AAAI Press","abstract":[{"lang":"eng","text":"POMDPs are standard models for probabilistic planning problems, where an agent interacts with an uncertain environment. We study the problem of almost-sure reachability, where given a set of target states, the question is to decide whether there is a policy to ensure that the target set is reached with probability 1 (almost-surely). While in general the problem is EXPTIMEcomplete, in many practical cases policies with a small amount of memory suffice. Moreover, the existing solution to the problem is explicit, which first requires to construct explicitly an exponential reduction to a belief-support MDP. In this work, we first study the existence of observation-stationary strategies, which is NP-complete, and then small-memory strategies. We present a symbolic algorithm by an efficient encoding to SAT and using a SAT solver for the problem. We report experimental results demonstrating the scalability of our symbolic (SAT-based) approach. © 2016, Association for the Advancement of Artificial Intelligence (www.aaai.org). All rights reserved."}],"project":[{"_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"}],"oa":1,"language":[{"iso":"eng"}],"page":"3225 - 3232","year":"2016","month":"12","conference":{"start_date":"2016-02-12","name":"AAAI: Conference on Artificial Intelligence","location":"Phoenix, AZ, United States","end_date":"2016-02-17"},"type":"conference","oa_version":"Preprint","publication":"Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence","status":"public","corr_author":"1","related_material":{"link":[{"relation":"table_of_contents","url":"https://dl.acm.org/citation.cfm?id=3016355"}],"record":[{"relation":"earlier_version","id":"5443","status":"public"}]},"date_created":"2018-12-11T11:50:30Z","arxiv":1,"OA_type":"green","acknowledgement":"The research was partly supported by Austrian Science Fund (FWF) Grant No P23499-N23, FWF NFN Grant No S11407-N23 (RiSE), ERC Start grant (279307: Graph Games), and Microsoft faculty fellows award.","_id":"1166","intvolume":"      2016","OA_place":"repository","day":"02","publication_status":"published","volume":2016,"citation":{"apa":"Chatterjee, K., Chmelik, M., &#38; Davies, J. (2016). A symbolic SAT based algorithm for almost sure reachability with small strategies in POMDPs. In <i>Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence</i> (Vol. 2016, pp. 3225–3232). Phoenix, AZ, United States: AAAI Press. <a href=\"https://doi.org/10.1609/aaai.v30i1.10422\">https://doi.org/10.1609/aaai.v30i1.10422</a>","ista":"Chatterjee K, Chmelik M, Davies J. 2016. A symbolic SAT based algorithm for almost sure reachability with small strategies in POMDPs. Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence. AAAI: Conference on Artificial Intelligence vol. 2016, 3225–3232.","short":"K. Chatterjee, M. Chmelik, J. Davies, in:, Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence, AAAI Press, 2016, pp. 3225–3232.","ama":"Chatterjee K, Chmelik M, Davies J. A symbolic SAT based algorithm for almost sure reachability with small strategies in POMDPs. In: <i>Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence</i>. Vol 2016. AAAI Press; 2016:3225-3232. doi:<a href=\"https://doi.org/10.1609/aaai.v30i1.10422\">10.1609/aaai.v30i1.10422</a>","mla":"Chatterjee, Krishnendu, et al. “A Symbolic SAT Based Algorithm for Almost Sure Reachability with Small Strategies in POMDPs.” <i>Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence</i>, vol. 2016, AAAI Press, 2016, pp. 3225–32, doi:<a href=\"https://doi.org/10.1609/aaai.v30i1.10422\">10.1609/aaai.v30i1.10422</a>.","ieee":"K. Chatterjee, M. Chmelik, and J. Davies, “A symbolic SAT based algorithm for almost sure reachability with small strategies in POMDPs,” in <i>Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence</i>, Phoenix, AZ, United States, 2016, vol. 2016, pp. 3225–3232.","chicago":"Chatterjee, Krishnendu, Martin Chmelik, and Jessica Davies. “A Symbolic SAT Based Algorithm for Almost Sure Reachability with Small Strategies in POMDPs.” In <i>Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence</i>, 2016:3225–32. AAAI Press, 2016. <a href=\"https://doi.org/10.1609/aaai.v30i1.10422\">https://doi.org/10.1609/aaai.v30i1.10422</a>."},"doi":"10.1609/aaai.v30i1.10422","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","quality_controlled":"1"},{"date_created":"2018-12-11T11:50:42Z","related_material":{"record":[{"id":"434","status":"public","relation":"later_version"}]},"status":"public","oa_version":"Submitted Version","conference":{"end_date":"2016-11-11","location":"Limassol, Cyprus","name":"FM: Formal Methods","start_date":"2016-11-09"},"alternative_title":["LNCS"],"type":"conference","intvolume":"      9995","day":"08","publication_status":"published","_id":"1205","scopus_import":"1","ddc":["004"],"has_accepted_license":"1","acknowledgement":"This research is sponsored in part by NSFC Program (No. 91218302, No. 61527812), National Science and Technology Major Project (No. 2016ZX01038101), Tsinghua University Initiative Scientific Research Program (20131089331), MIIT IT funds (Research and application of TCN key technologies) of China, and the National Key Technology R&D Program (No. 2015BAG14B01-02), Austrian Science Fund (FWF) under grants S11402-N23 (RiSE/SHiNE) and Z211-N23.\r\n","doi":"10.1007/978-3-319-48989-6_47","volume":9995,"citation":{"ieee":"Y. Jiang <i>et al.</i>, “Safety assured formal model driven design of the multifunction vehicle bus controller,” presented at the FM: Formal Methods, Limassol, Cyprus, 2016, vol. 9995, pp. 757–763.","chicago":"Jiang, Yu, Han Liu, Houbing Song, Hui Kong, Ming Gu, Jiaguang Sun, and Lui Sha. “Safety Assured Formal Model Driven Design of the Multifunction Vehicle Bus Controller,” 9995:757–63. Springer, 2016. <a href=\"https://doi.org/10.1007/978-3-319-48989-6_47\">https://doi.org/10.1007/978-3-319-48989-6_47</a>.","mla":"Jiang, Yu, et al. <i>Safety Assured Formal Model Driven Design of the Multifunction Vehicle Bus Controller</i>. Vol. 9995, Springer, 2016, pp. 757–63, doi:<a href=\"https://doi.org/10.1007/978-3-319-48989-6_47\">10.1007/978-3-319-48989-6_47</a>.","ista":"Jiang Y, Liu H, Song H, Kong H, Gu M, Sun J, Sha L. 2016. Safety assured formal model driven design of the multifunction vehicle bus controller. FM: Formal Methods, LNCS, vol. 9995, 757–763.","apa":"Jiang, Y., Liu, H., Song, H., Kong, H., Gu, M., Sun, J., &#38; Sha, L. (2016). Safety assured formal model driven design of the multifunction vehicle bus controller (Vol. 9995, pp. 757–763). Presented at the FM: Formal Methods, Limassol, Cyprus: Springer. <a href=\"https://doi.org/10.1007/978-3-319-48989-6_47\">https://doi.org/10.1007/978-3-319-48989-6_47</a>","short":"Y. Jiang, H. Liu, H. Song, H. Kong, M. Gu, J. Sun, L. Sha, in:, Springer, 2016, pp. 757–763.","ama":"Jiang Y, Liu H, Song H, et al. Safety assured formal model driven design of the multifunction vehicle bus controller. In: Vol 9995. Springer; 2016:757-763. doi:<a href=\"https://doi.org/10.1007/978-3-319-48989-6_47\">10.1007/978-3-319-48989-6_47</a>"},"file_date_updated":"2020-07-14T12:44:39Z","quality_controlled":"1","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","file":[{"creator":"system","file_name":"IST-2017-783-v1+1_FM-Safety-Assured-Development-of-MVBC.pdf","date_created":"2018-12-12T10:08:13Z","access_level":"open_access","file_id":"4673","content_type":"application/pdf","relation":"main_file","checksum":"fea0b3fae9a2a42e8bfec59840e30d8c","file_size":281501,"date_updated":"2020-07-14T12:44:39Z"}],"department":[{"_id":"ToHe"}],"external_id":{"isi":["000389793300047"]},"article_processing_charge":"No","title":"Safety assured formal model driven design of the multifunction vehicle bus controller","date_updated":"2025-09-22T09:39:55Z","author":[{"last_name":"Jiang","first_name":"Yu","full_name":"Jiang, Yu"},{"full_name":"Liu, Han","first_name":"Han","last_name":"Liu"},{"first_name":"Houbing","last_name":"Song","full_name":"Song, Houbing"},{"full_name":"Kong, Hui","first_name":"Hui","id":"3BDE25AA-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-3066-6941","last_name":"Kong"},{"last_name":"Gu","first_name":"Ming","full_name":"Gu, Ming"},{"full_name":"Sun, Jiaguang","last_name":"Sun","first_name":"Jiaguang"},{"full_name":"Sha, Lui","first_name":"Lui","last_name":"Sha"}],"publist_id":"6144","date_published":"2016-11-08T00:00:00Z","project":[{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"Z211","name":"Formal methods for the design and analysis of complex systems"}],"abstract":[{"text":"In this paper, we present a formal model-driven engineering approach to establishing a safety-assured implementation of Multifunction vehicle bus controller (MVBC) based on the generic reference models and requirements described in the International Electrotechnical Commission (IEC) standard IEC-61375. First, the generic models described in IEC-61375 are translated into a network of timed automata, and some safety requirements tested in IEC-61375 are formalized as timed computation tree logic (TCTL) formulas. With the help of Uppaal, we check and debug whether the timed automata satisfy the formulas or not. Within this step, several logic inconsistencies in the original standard are detected and corrected. Then, we apply the tool Times to generate C code from the verified model, which was later synthesized into a real MVBC chip. Finally, the runtime verification tool RMOR is applied to verify some safety requirements at the implementation level. We set up a real platform with worldwide mostly used MVBC D113, and verify the correctness and the scalability of the synthesized MVBC chip more comprehensively. The errors in the standard has been confirmed and the resulted MVBC has been deployed in real train communication network.","lang":"eng"}],"publisher":"Springer","pubrep_id":"783","month":"11","year":"2016","page":"757 - 763","language":[{"iso":"eng"}],"isi":1,"oa":1},{"date_published":"2016-09-25T00:00:00Z","publist_id":"6107","author":[{"full_name":"Kong, Hui","orcid":"0000-0002-3066-6941","last_name":"Kong","first_name":"Hui","id":"3BDE25AA-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Bartocci","first_name":"Ezio","full_name":"Bartocci, Ezio"},{"full_name":"Bogomolov, Sergiy","id":"369D9A44-F248-11E8-B48F-1D18A9856A87","first_name":"Sergiy","orcid":"0000-0002-0686-0365","last_name":"Bogomolov"},{"full_name":"Grosu, Radu","first_name":"Radu","last_name":"Grosu"},{"full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Jiang, Yu","first_name":"Yu","last_name":"Jiang"},{"last_name":"Schilling","orcid":"0000-0003-3658-1065","first_name":"Christian","id":"3A2F4DCE-F248-11E8-B48F-1D18A9856A87","full_name":"Schilling, Christian"}],"title":"Discrete abstraction of multiaffine systems","date_updated":"2025-09-22T09:24:50Z","article_processing_charge":"No","external_id":{"isi":["000389928100009"]},"department":[{"_id":"ToHe"}],"publisher":"Springer","pubrep_id":"781","abstract":[{"text":"Many biological systems can be modeled as multiaffine hybrid systems. Due to the nonlinearity of multiaffine systems, it is difficult to verify their properties of interest directly. A common strategy to tackle this problem is to construct and analyze a discrete overapproximation of the original system. However, the conservativeness of a discrete abstraction significantly determines the level of confidence we can have in the properties of the original system. In this paper, in order to reduce the conservativeness of a discrete abstraction, we propose a new method based on a sufficient and necessary decision condition for computing discrete transitions between states in the abstract system. We assume the state space partition of a multiaffine system to be based on a set of multivariate polynomials. Hence, a rectangular partition defined in terms of polynomials of the form (xi − c) is just a simple case of multivariate polynomial partition, and the new decision condition applies naturally. We analyze and demonstrate the improvement of our method over the existing methods using some examples.","lang":"eng"}],"project":[{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"Formal methods for the design and analysis of complex systems","grant_number":"Z211"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"}],"oa":1,"isi":1,"language":[{"iso":"eng"}],"page":"128 - 144","month":"09","year":"2016","alternative_title":["LNCS"],"type":"conference","conference":{"location":"Grenoble, France","start_date":"2016-10-20","name":"HSB: Hybrid Systems Biology","end_date":"2016-10-21"},"oa_version":"Submitted Version","status":"public","date_created":"2018-12-11T11:50:49Z","acknowledgement":"This research was supported in part by the Austrian Science Fund (FWF) under grants S11402-N23, S11405-N23 and S11412-N23 (RiSE/SHiNE) and Z211-N23 (Wittgenstein Award).","has_accepted_license":"1","ddc":["005"],"scopus_import":"1","_id":"1227","publication_status":"published","day":"25","intvolume":"      9957","volume":9957,"citation":{"ieee":"H. Kong <i>et al.</i>, “Discrete abstraction of multiaffine systems,” presented at the HSB: Hybrid Systems Biology, Grenoble, France, 2016, vol. 9957, pp. 128–144.","chicago":"Kong, Hui, Ezio Bartocci, Sergiy Bogomolov, Radu Grosu, Thomas A Henzinger, Yu Jiang, and Christian Schilling. “Discrete Abstraction of Multiaffine Systems,” 9957:128–44. Springer, 2016. <a href=\"https://doi.org/10.1007/978-3-319-47151-8_9\">https://doi.org/10.1007/978-3-319-47151-8_9</a>.","short":"H. Kong, E. Bartocci, S. Bogomolov, R. Grosu, T.A. Henzinger, Y. Jiang, C. Schilling, in:, Springer, 2016, pp. 128–144.","apa":"Kong, H., Bartocci, E., Bogomolov, S., Grosu, R., Henzinger, T. A., Jiang, Y., &#38; Schilling, C. (2016). Discrete abstraction of multiaffine systems (Vol. 9957, pp. 128–144). Presented at the HSB: Hybrid Systems Biology, Grenoble, France: Springer. <a href=\"https://doi.org/10.1007/978-3-319-47151-8_9\">https://doi.org/10.1007/978-3-319-47151-8_9</a>","ista":"Kong H, Bartocci E, Bogomolov S, Grosu R, Henzinger TA, Jiang Y, Schilling C. 2016. Discrete abstraction of multiaffine systems. HSB: Hybrid Systems Biology, LNCS, vol. 9957, 128–144.","ama":"Kong H, Bartocci E, Bogomolov S, et al. Discrete abstraction of multiaffine systems. In: Vol 9957. Springer; 2016:128-144. doi:<a href=\"https://doi.org/10.1007/978-3-319-47151-8_9\">10.1007/978-3-319-47151-8_9</a>","mla":"Kong, Hui, et al. <i>Discrete Abstraction of Multiaffine Systems</i>. Vol. 9957, Springer, 2016, pp. 128–44, doi:<a href=\"https://doi.org/10.1007/978-3-319-47151-8_9\">10.1007/978-3-319-47151-8_9</a>."},"doi":"10.1007/978-3-319-47151-8_9","file":[{"date_created":"2018-12-12T10:10:49Z","file_name":"IST-2017-781-v1+1_main.pdf","creator":"system","access_level":"open_access","relation":"main_file","content_type":"application/pdf","file_id":"4840","date_updated":"2020-07-14T12:44:39Z","file_size":683955,"checksum":"994e164b558c47bacf8dc066dd27c8fc"}],"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","quality_controlled":"1","file_date_updated":"2020-07-14T12:44:39Z"},{"page":"328 - 347","year":"2016","month":"01","isi":1,"language":[{"iso":"eng"}],"oa":1,"project":[{"name":"Quantitative Reactive Modeling","grant_number":"267989","call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"grant_number":"Z211","name":"Formal methods for the design and analysis of complex systems","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425"},{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"}],"abstract":[{"lang":"eng","text":"Concolic testing is a promising method for generating test suites for large programs. However, it suffers from the path-explosion problem and often fails to find tests that cover difficult-to-reach parts of programs. In contrast, model checkers based on counterexample-guided abstraction refinement explore programs exhaustively, while failing to scale on large programs with precision. In this paper, we present a novel method that iteratively combines concolic testing and model checking to find a test suite for a given coverage criterion. If concolic testing fails to cover some test goals, then the model checker refines its program abstraction to prove more paths infeasible, which reduces the search space for concolic testing. We have implemented our method on top of the concolictesting tool Crest and the model checker CpaChecker. We evaluated our tool on a collection of programs and a category of SvComp benchmarks. In our experiments, we observed an improvement in branch coverage compared to Crest from 48% to 63% in the best case, and from 66% to 71% on average."}],"publisher":"Springer","department":[{"_id":"ToHe"}],"external_id":{"arxiv":["1511.02615"],"isi":["000375148800016"]},"article_processing_charge":"No","date_updated":"2026-04-15T10:02:12Z","title":"Abstraction-driven concolic testing","main_file_link":[{"url":"https://arxiv.org/abs/1511.02615","open_access":"1"}],"author":[{"last_name":"Daca","first_name":"Przemyslaw","id":"49351290-F248-11E8-B48F-1D18A9856A87","full_name":"Daca, Przemyslaw"},{"last_name":"Gupta","id":"335E5684-F248-11E8-B48F-1D18A9856A87","first_name":"Ashutosh","full_name":"Gupta, Ashutosh"},{"orcid":"0000−0002−2985−7724","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","full_name":"Henzinger, Thomas A"}],"date_published":"2016-01-01T00:00:00Z","publist_id":"6104","ec_funded":1,"quality_controlled":"1","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","doi":"10.1007/978-3-662-49122-5_16","citation":{"mla":"Daca, Przemyslaw, et al. <i>Abstraction-Driven Concolic Testing</i>. Vol. 9583, Springer, 2016, pp. 328–47, doi:<a href=\"https://doi.org/10.1007/978-3-662-49122-5_16\">10.1007/978-3-662-49122-5_16</a>.","ama":"Daca P, Gupta A, Henzinger TA. Abstraction-driven concolic testing. In: Vol 9583. Springer; 2016:328-347. doi:<a href=\"https://doi.org/10.1007/978-3-662-49122-5_16\">10.1007/978-3-662-49122-5_16</a>","apa":"Daca, P., Gupta, A., &#38; Henzinger, T. A. (2016). Abstraction-driven concolic testing (Vol. 9583, pp. 328–347). 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_16\">https://doi.org/10.1007/978-3-662-49122-5_16</a>","short":"P. Daca, A. Gupta, T.A. Henzinger, in:, Springer, 2016, pp. 328–347.","ista":"Daca P, Gupta A, Henzinger TA. 2016. Abstraction-driven concolic testing. VMCAI: Verification, Model Checking and Abstract Interpretation, LNCS, vol. 9583, 328–347.","chicago":"Daca, Przemyslaw, Ashutosh Gupta, and Thomas A Henzinger. “Abstraction-Driven Concolic Testing,” 9583:328–47. Springer, 2016. <a href=\"https://doi.org/10.1007/978-3-662-49122-5_16\">https://doi.org/10.1007/978-3-662-49122-5_16</a>.","ieee":"P. Daca, A. Gupta, and T. A. Henzinger, “Abstraction-driven concolic testing,” presented at the VMCAI: Verification, Model Checking and Abstract Interpretation, St. Petersburg, FL, USA, 2016, vol. 9583, pp. 328–347."},"volume":9583,"day":"01","intvolume":"      9583","publication_status":"published","_id":"1230","scopus_import":"1","acknowledgement":"We thank Andrey Kupriyanov for feedback on the manuscript,\r\nand Michael Tautschnig for help with preparing the experiments. This research was supported in part by the European Research Council (ERC) under grant 267989 (QUAREM) and by the Austrian Science Fund (FWF) under grants S11402-N23 (RiSE) and Z211-N23 (Wittgenstein Award).","arxiv":1,"date_created":"2018-12-11T11:50:50Z","related_material":{"record":[{"id":"1155","status":"public","relation":"dissertation_contains"}]},"status":"public","oa_version":"Preprint","conference":{"end_date":"2016-01-19","location":"St. Petersburg, FL, USA","start_date":"2016-01-17","name":"VMCAI: Verification, Model Checking and Abstract Interpretation"},"type":"conference","alternative_title":["LNCS"]},{"related_material":{"record":[{"relation":"later_version","id":"471","status":"public"},{"status":"public","id":"1155","relation":"dissertation_contains"}]},"arxiv":1,"date_created":"2018-12-11T11:50:51Z","conference":{"start_date":"2016-04-02","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","location":"Eindhoven, The Netherlands","end_date":"2016-04-08"},"alternative_title":["LNCS"],"type":"conference","oa_version":"Preprint","status":"public","_id":"1234","day":"01","intvolume":"      9636","publication_status":"published","acknowledgement":"This research was funded in part by the European Research Council (ERC) under\r\ngrant  agreement  267989  (QUAREM),  the  Austrian  Science  Fund  (FWF)  under\r\ngrants project S11402-N23 (RiSE) and Z211-N23 (Wittgenstein Award), the Peo-\r\nple Programme (Marie Curie Actions) of the European Union’s Seventh Framework\r\nProgramme (FP7/2007-2013) REA Grant No 291734, the SNSF Advanced Postdoc.\r\nMobility Fellowship – grant number P300P2\r\n161067, and the Czech Science Foun-\r\ndation under grant agreement P202/12/G061.","scopus_import":"1","doi":"10.1007/978-3-662-49674-9_7","volume":9636,"citation":{"mla":"Daca, Przemyslaw, et al. <i>Faster Statistical Model Checking for Unbounded Temporal Properties</i>. Vol. 9636, Springer, 2016, pp. 112–29, doi:<a href=\"https://doi.org/10.1007/978-3-662-49674-9_7\">10.1007/978-3-662-49674-9_7</a>.","apa":"Daca, P., Henzinger, T. A., Kretinsky, J., &#38; Petrov, T. (2016). Faster statistical model checking for unbounded temporal properties (Vol. 9636, pp. 112–129). Presented at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems, Eindhoven, The Netherlands: Springer. <a href=\"https://doi.org/10.1007/978-3-662-49674-9_7\">https://doi.org/10.1007/978-3-662-49674-9_7</a>","ista":"Daca P, Henzinger TA, Kretinsky J, Petrov T. 2016. Faster statistical model checking for unbounded temporal properties. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 9636, 112–129.","short":"P. Daca, T.A. Henzinger, J. Kretinsky, T. Petrov, in:, Springer, 2016, pp. 112–129.","ama":"Daca P, Henzinger TA, Kretinsky J, Petrov T. Faster statistical model checking for unbounded temporal properties. In: Vol 9636. Springer; 2016:112-129. doi:<a href=\"https://doi.org/10.1007/978-3-662-49674-9_7\">10.1007/978-3-662-49674-9_7</a>","ieee":"P. Daca, T. A. Henzinger, J. Kretinsky, and T. Petrov, “Faster statistical model checking for unbounded temporal properties,” presented at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems, Eindhoven, The Netherlands, 2016, vol. 9636, pp. 112–129.","chicago":"Daca, Przemyslaw, Thomas A Henzinger, Jan Kretinsky, and Tatjana Petrov. “Faster Statistical Model Checking for Unbounded Temporal Properties,” 9636:112–29. Springer, 2016. <a href=\"https://doi.org/10.1007/978-3-662-49674-9_7\">https://doi.org/10.1007/978-3-662-49674-9_7</a>."},"quality_controlled":"1","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","ec_funded":1,"external_id":{"arxiv":["1504.05739"],"isi":["000406428000007"]},"article_processing_charge":"No","department":[{"_id":"ToHe"},{"_id":"CaGu"}],"author":[{"full_name":"Daca, Przemyslaw","last_name":"Daca","first_name":"Przemyslaw","id":"49351290-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Henzinger","orcid":"0000−0002−2985−7724","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A"},{"full_name":"Kretinsky, Jan","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","first_name":"Jan","last_name":"Kretinsky","orcid":"0000-0002-8122-2881"},{"orcid":"0000-0002-9041-0905","last_name":"Petrov","first_name":"Tatjana","id":"3D5811FC-F248-11E8-B48F-1D18A9856A87","full_name":"Petrov, Tatjana"}],"main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1504.05739"}],"publist_id":"6099","date_published":"2016-01-01T00:00:00Z","title":"Faster statistical model checking for unbounded temporal properties","date_updated":"2026-04-15T10:02:12Z","project":[{"grant_number":"267989","name":"Quantitative Reactive Modeling","call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"},{"grant_number":"Z211","name":"Formal methods for the design and analysis of complex systems","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425"},{"name":"International IST Postdoc Fellowship Programme","grant_number":"291734","_id":"25681D80-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"}],"publisher":"Springer","abstract":[{"lang":"eng","text":"We present a new algorithm for the statistical model checking of Markov chains with respect to unbounded temporal properties, including full linear temporal logic. The main idea is that we monitor each simulation run on the fly, in order to detect quickly if a bottom strongly connected component is entered with high probability, in which case the simulation run can be terminated early. As a result, our simulation runs are often much shorter than required by termination bounds that are computed a priori for a desired level of confidence on a large state space. In comparison to previous algorithms for statistical model checking our method is not only faster in many cases but also requires less information about the system, namely, only the minimum transition probability that occurs in the Markov chain. In addition, our method can be generalised to unbounded quantitative properties such as mean-payoff bounds."}],"language":[{"iso":"eng"}],"isi":1,"month":"01","year":"2016","page":"112 - 129","oa":1},{"ddc":["005"],"has_accepted_license":"1","acknowledgement":"This work is supported in part by NSF CNS 13-30077, NSF CNS 13-29886, NSF CNS 15-45002, NSFC 61303014, NSFC 61202010, and NSFC 91218302.","scopus_import":1,"_id":"1256","day":"27","publication_status":"published","conference":{"end_date":"2016-04-14","start_date":"2016-04-11","name":"RTAS: Real-time and Embedded Technology and Applications Symposium","location":"Vienna, Austria"},"type":"conference","oa_version":"Submitted Version","status":"public","date_created":"2018-12-11T11:50:58Z","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","file":[{"content_type":"application/pdf","relation":"main_file","file_id":"4949","file_size":1293599,"date_updated":"2020-07-14T12:44:41Z","checksum":"42f0462911cc9957f2356b12fb33b4b6","date_created":"2018-12-12T10:12:31Z","creator":"system","file_name":"IST-2017-780-v1+1_RTAS-42-Camera-Ready.pdf","access_level":"open_access"}],"quality_controlled":"1","file_date_updated":"2020-07-14T12:44:41Z","article_number":"7461337","citation":{"mla":"Jiang, Yu, et al. <i>From Stateflow Simulation to Verified Implementation: A Verification Approach and a Real-Time Train Controller Design</i>. 7461337, IEEE, 2016, doi:<a href=\"https://doi.org/10.1109/RTAS.2016.7461337\">10.1109/RTAS.2016.7461337</a>.","ista":"Jiang Y, Yang Y, Liu H, Kong H, Gu M, Sun J, Sha L. 2016. From stateflow simulation to verified implementation: A verification approach and a real-time train controller design. RTAS: Real-time and Embedded Technology and Applications Symposium, 7461337.","apa":"Jiang, Y., Yang, Y., Liu, H., Kong, H., Gu, M., Sun, J., &#38; Sha, L. (2016). From stateflow simulation to verified implementation: A verification approach and a real-time train controller design. Presented at the RTAS: Real-time and Embedded Technology and Applications Symposium, Vienna, Austria: IEEE. <a href=\"https://doi.org/10.1109/RTAS.2016.7461337\">https://doi.org/10.1109/RTAS.2016.7461337</a>","short":"Y. Jiang, Y. Yang, H. Liu, H. Kong, M. Gu, J. Sun, L. Sha, in:, IEEE, 2016.","ama":"Jiang Y, Yang Y, Liu H, et al. From stateflow simulation to verified implementation: A verification approach and a real-time train controller design. In: IEEE; 2016. doi:<a href=\"https://doi.org/10.1109/RTAS.2016.7461337\">10.1109/RTAS.2016.7461337</a>","ieee":"Y. Jiang <i>et al.</i>, “From stateflow simulation to verified implementation: A verification approach and a real-time train controller design,” presented at the RTAS: Real-time and Embedded Technology and Applications Symposium, Vienna, Austria, 2016.","chicago":"Jiang, Yu, Yixiao Yang, Han Liu, Hui Kong, Ming Gu, Jiaguang Sun, and Lui Sha. “From Stateflow Simulation to Verified Implementation: A Verification Approach and a Real-Time Train Controller Design.” IEEE, 2016. <a href=\"https://doi.org/10.1109/RTAS.2016.7461337\">https://doi.org/10.1109/RTAS.2016.7461337</a>."},"doi":"10.1109/RTAS.2016.7461337","author":[{"first_name":"Yu","last_name":"Jiang","full_name":"Jiang, Yu"},{"full_name":"Yang, Yixiao","last_name":"Yang","first_name":"Yixiao"},{"first_name":"Han","last_name":"Liu","full_name":"Liu, Han"},{"id":"3BDE25AA-F248-11E8-B48F-1D18A9856A87","first_name":"Hui","orcid":"0000-0002-3066-6941","last_name":"Kong","full_name":"Kong, Hui"},{"full_name":"Gu, Ming","first_name":"Ming","last_name":"Gu"},{"first_name":"Jiaguang","last_name":"Sun","full_name":"Sun, Jiaguang"},{"full_name":"Sha, Lui","last_name":"Sha","first_name":"Lui"}],"date_published":"2016-04-27T00:00:00Z","publist_id":"6069","title":"From stateflow simulation to verified implementation: A verification approach and a real-time train controller design","date_updated":"2021-01-12T06:49:26Z","department":[{"_id":"ToHe"}],"oa":1,"language":[{"iso":"eng"}],"year":"2016","month":"04","pubrep_id":"780","publisher":"IEEE","abstract":[{"lang":"eng","text":"Simulink is widely used for model driven development (MDD) of industrial software systems. Typically, the Simulink based development is initiated from Stateflow modeling, followed by simulation, validation and code generation mapped to physical execution platforms. However, recent industrial trends have raised the demands of rigorous verification on safety-critical applications, which is unfortunately challenging for Simulink. In this paper, we present an approach to bridge the Stateflow based model driven development and a well- defined rigorous verification. First, we develop a self- contained toolkit to translate Stateflow model into timed automata, where major advanced modeling features in Stateflow are supported. Taking advantage of the strong verification capability of Uppaal, we can not only find bugs in Stateflow models which are missed by Simulink Design Verifier, but also check more important temporal properties. Next, we customize a runtime verifier for the generated nonintrusive VHDL and C code of Stateflow model for monitoring. The major strength of the customization is the flexibility to collect and analyze runtime properties with a pure software monitor, which opens more opportunities for engineers to achieve high reliability of the target system compared with the traditional act that only relies on Simulink Polyspace. We incorporate these two parts into original Stateflow based MDD seamlessly. In this way, safety-critical properties are both verified at the model level, and at the consistent system implementation level with physical execution environment in consideration. We apply our approach on a train controller design, and the verified implementation is tested and deployed on a real hardware platform."}]},{"page":"23 - 38","year":"2016","month":"08","isi":1,"language":[{"iso":"eng"}],"oa":1,"project":[{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"grant_number":"Z211","name":"Formal methods for the design and analysis of complex systems","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications"},{"grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification","_id":"25892FC0-B435-11E9-9278-68D0E5697425"}],"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."}],"publisher":"Springer","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"external_id":{"isi":["000388924600002"],"arxiv":["1604.06764"]},"article_processing_charge":"No","title":"Quantitative monitor automata","date_updated":"2025-09-22T08:19:49Z","main_file_link":[{"url":"https://arxiv.org/abs/1604.06764","open_access":"1"}],"author":[{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","orcid":"0000-0002-4561-241X"},{"last_name":"Henzinger","orcid":"0000−0002−2985−7724","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A"},{"full_name":"Otop, Jan","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","first_name":"Jan","last_name":"Otop"}],"publist_id":"5932","date_published":"2016-08-31T00:00:00Z","ec_funded":1,"quality_controlled":"1","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","doi":"10.1007/978-3-662-53413-7_2","citation":{"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.","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>","ista":"Chatterjee K, Henzinger TA, Otop J. 2016. Quantitative monitor automata. SAS: Static Analysis Symposium, LNCS, vol. 9837, 23–38.","short":"K. Chatterjee, T.A. Henzinger, J. Otop, in:, Springer, 2016, pp. 23–38.","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>."},"volume":9837,"day":"31","intvolume":"      9837","publication_status":"published","_id":"1335","scopus_import":"1","date_created":"2018-12-11T11:51:26Z","arxiv":1,"corr_author":"1","status":"public","oa_version":"Preprint","conference":{"end_date":"2016-09-10","location":"Edinburgh, United Kingdom","name":"SAS: Static Analysis Symposium","start_date":"2016-09-08"},"type":"conference","alternative_title":["LNCS"]},{"file":[{"file_id":"5073","content_type":"application/pdf","relation":"main_file","checksum":"0825eefd4e22774f6f62cb7d7389b05a","file_size":243458,"date_updated":"2020-07-14T12:44:45Z","creator":"system","file_name":"IST-2016-645-v1+1_sagt-cr.pdf","date_created":"2018-12-12T10:14:22Z","access_level":"open_access"}],"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","file_date_updated":"2020-07-14T12:44:45Z","quality_controlled":"1","citation":{"mla":"Avni, Guy, et al. <i>Dynamic Resource Allocation Games</i>. Vol. 9928, Springer, 2016, pp. 153–66, doi:<a href=\"https://doi.org/10.1007/978-3-662-53354-3_13\">10.1007/978-3-662-53354-3_13</a>.","ama":"Avni G, Henzinger TA, Kupferman O. Dynamic resource allocation games. In: Vol 9928. Springer; 2016:153-166. doi:<a href=\"https://doi.org/10.1007/978-3-662-53354-3_13\">10.1007/978-3-662-53354-3_13</a>","short":"G. Avni, T.A. Henzinger, O. Kupferman, in:, Springer, 2016, pp. 153–166.","ista":"Avni G, Henzinger TA, Kupferman O. 2016. Dynamic resource allocation games. SAGT: Symposium on Algorithmic Game Theory, LNCS, vol. 9928, 153–166.","apa":"Avni, G., Henzinger, T. A., &#38; Kupferman, O. (2016). Dynamic resource allocation games (Vol. 9928, pp. 153–166). Presented at the SAGT: Symposium on Algorithmic Game Theory, Liverpool, United Kingdom: Springer. <a href=\"https://doi.org/10.1007/978-3-662-53354-3_13\">https://doi.org/10.1007/978-3-662-53354-3_13</a>","chicago":"Avni, Guy, Thomas A Henzinger, and Orna Kupferman. “Dynamic Resource Allocation Games,” 9928:153–66. Springer, 2016. <a href=\"https://doi.org/10.1007/978-3-662-53354-3_13\">https://doi.org/10.1007/978-3-662-53354-3_13</a>.","ieee":"G. Avni, T. A. Henzinger, and O. Kupferman, “Dynamic resource allocation games,” presented at the SAGT: Symposium on Algorithmic Game Theory, Liverpool, United Kingdom, 2016, vol. 9928, pp. 153–166."},"volume":9928,"doi":"10.1007/978-3-662-53354-3_13","scopus_import":"1","has_accepted_license":"1","acknowledgement":"This research was supported in part by the European Research Council (ERC) under grants 267989 (QUAREM) and 278410 (QUALITY), and by the Austrian Science Fund (FWF) under grants S11402-N23 (RiSE) and Z211-N23 (Wittgenstein Award).","ddc":["000"],"publication_status":"published","day":"01","intvolume":"      9928","_id":"1341","oa_version":"Preprint","status":"public","type":"conference","alternative_title":["LNCS"],"conference":{"end_date":"2016-09-21","start_date":"2016-09-19","name":"SAGT: Symposium on Algorithmic Game Theory","location":"Liverpool, United Kingdom"},"date_created":"2018-12-11T11:51:28Z","corr_author":"1","related_material":{"record":[{"relation":"later_version","id":"6761","status":"public"}]},"oa":1,"page":"153 - 166","month":"09","year":"2016","language":[{"iso":"eng"}],"isi":1,"abstract":[{"lang":"eng","text":"In resource allocation games, selfish players share resources that are needed in order to fulfill their objectives. The cost of using a resource depends on the load on it. In the traditional setting, the players make their choices concurrently and in one-shot. That is, a strategy for a player is a subset of the resources. We introduce and study dynamic resource allocation games. In this setting, the game proceeds in phases. In each phase each player chooses one resource. A scheduler dictates the order in which the players proceed in a phase, possibly scheduling several players to proceed concurrently. The game ends when each player has collected a set of resources that fulfills his objective. The cost for each player then depends on this set as well as on the load on the resources in it – we consider both congestion and cost-sharing games. We argue that the dynamic setting is the suitable setting for many applications in practice. We study the stability of dynamic resource allocation games, where the appropriate notion of stability is that of subgame perfect equilibrium, study the inefficiency incurred due to selfish behavior, and also study problems that are particular to the dynamic setting, like constraints on the order in which resources can be chosen or the problem of finding a scheduler that achieves stability."}],"publisher":"Springer","pubrep_id":"645","project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"267989","name":"Quantitative Reactive Modeling"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Formal methods for the design and analysis of complex systems","grant_number":"Z211"}],"title":"Dynamic resource allocation games","date_updated":"2026-04-16T09:35:14Z","date_published":"2016-09-01T00:00:00Z","publist_id":"5926","author":[{"orcid":"0000-0001-5588-8287","last_name":"Avni","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","first_name":"Guy","full_name":"Avni, Guy"},{"full_name":"Henzinger, Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Orna","last_name":"Kupferman","full_name":"Kupferman, Orna"}],"department":[{"_id":"ToHe"}],"article_processing_charge":"No","external_id":{"isi":["000389020400013"]},"ec_funded":1},{"scopus_import":"1","_id":"1390","intvolume":"      9780","day":"13","publication_status":"published","conference":{"end_date":"2016-07-23","location":"Toronto, Canada","start_date":"2016-07-17","name":"CAV: Computer Aided Verification"},"alternative_title":["LNCS"],"type":"conference","status":"public","oa_version":"None","corr_author":"1","date_created":"2018-12-11T11:51:45Z","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","quality_controlled":"1","citation":{"mla":"D’Antoni, Loris, et al. <i>QLOSE: Program Repair with Quantitative Objectives</i>. Vol. 9780, Springer, 2016, pp. 383–401, doi:<a href=\"https://doi.org/10.1007/978-3-319-41540-6_21\">10.1007/978-3-319-41540-6_21</a>.","apa":"D’Antoni, L., Samanta, R., &#38; Singh, R. (2016). QLOSE: Program repair with quantitative objectives (Vol. 9780, pp. 383–401). Presented at the CAV: Computer Aided Verification, Toronto, Canada: Springer. <a href=\"https://doi.org/10.1007/978-3-319-41540-6_21\">https://doi.org/10.1007/978-3-319-41540-6_21</a>","ista":"D’Antoni L, Samanta R, Singh R. 2016. QLOSE: Program repair with quantitative objectives. CAV: Computer Aided Verification, LNCS, vol. 9780, 383–401.","short":"L. D’Antoni, R. Samanta, R. Singh, in:, Springer, 2016, pp. 383–401.","ama":"D’Antoni L, Samanta R, Singh R. QLOSE: Program repair with quantitative objectives. In: Vol 9780. Springer; 2016:383-401. doi:<a href=\"https://doi.org/10.1007/978-3-319-41540-6_21\">10.1007/978-3-319-41540-6_21</a>","ieee":"L. D’Antoni, R. Samanta, and R. Singh, “QLOSE: Program repair with quantitative objectives,” presented at the CAV: Computer Aided Verification, Toronto, Canada, 2016, vol. 9780, pp. 383–401.","chicago":"D’Antoni, Loris, Roopsha Samanta, and Rishabh Singh. “QLOSE: Program Repair with Quantitative Objectives,” 9780:383–401. Springer, 2016. <a href=\"https://doi.org/10.1007/978-3-319-41540-6_21\">https://doi.org/10.1007/978-3-319-41540-6_21</a>."},"volume":9780,"doi":"10.1007/978-3-319-41540-6_21","author":[{"full_name":"D'Antoni, Loris","first_name":"Loris","last_name":"D'Antoni"},{"full_name":"Samanta, Roopsha","last_name":"Samanta","first_name":"Roopsha","id":"3D2AAC08-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Rishabh","last_name":"Singh","full_name":"Singh, Rishabh"}],"date_published":"2016-07-13T00:00:00Z","publist_id":"5819","date_updated":"2025-09-22T07:30:07Z","title":"QLOSE: Program repair with quantitative objectives","external_id":{"isi":["000387731400021"]},"article_processing_charge":"No","department":[{"_id":"ToHe"}],"ec_funded":1,"language":[{"iso":"eng"}],"isi":1,"year":"2016","month":"07","page":"383 - 401","publisher":"Springer","abstract":[{"lang":"eng","text":"The goal of automatic program repair is to identify a set of syntactic changes that can turn a program that is incorrect with respect\r\nto a given specification into a correct one. Existing program repair techniques typically aim to find any program that meets the given specification. Such “best-effort” strategies can end up generating a program that is quite different from the original one. Novel techniques have been proposed to compute syntactically minimal program fixes, but the smallest syntactic fix to a program can still significantly alter the original program’s behaviour. We propose a new approach to program repair based on program distances, which can quantify changes not only to the program syntax but also to the program semantics. We call this the quantitative program repair problem where the “optimal” repair is derived using multiple distances. We implement a solution to the quantitative repair\r\nproblem in a prototype tool called Qlose\r\n(Quantitatively close), using the program synthesizer Sketch. We evaluate the effectiveness of different distances in obtaining desirable repairs by evaluating\r\nQlose on programs taken from educational tools such as CodeHunt and edX."}],"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","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"},{"name":"Formal methods for the design and analysis of complex systems","grant_number":"Z211","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425"}]}]