[{"year":"2018","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publication_status":"published","article_processing_charge":"No","day":"30","author":[{"last_name":"Bakhirkin","full_name":"Bakhirkin, Alexey","first_name":"Alexey"},{"full_name":"Ferrere, Thomas","first_name":"Thomas","id":"40960E6E-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-5199-3143","last_name":"Ferrere"},{"last_name":"Henzinger","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","full_name":"Henzinger, Thomas A"},{"last_name":"Nickovicl","first_name":"Deian","full_name":"Nickovicl, Deian"}],"date_published":"2018-09-30T00:00:00Z","project":[{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF"},{"name":"Formal methods for the design and analysis of complex systems","call_identifier":"FWF","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425"}],"doi":"10.1109/emsoft.2018.8537203","quality_controlled":"1","file":[{"file_size":338006,"date_created":"2020-05-14T16:01:29Z","relation":"main_file","checksum":"234a33ad9055b3458fcdda6af251b33a","content_type":"application/pdf","access_level":"open_access","file_id":"7839","file_name":"2018_EMSOFT_Bakhirkin.pdf","date_updated":"2020-07-14T12:47:13Z","creator":"dernst"}],"department":[{"_id":"ToHe"}],"title":"Keynote: The first-order logic of signals","oa_version":"Published Version","date_updated":"2025-07-10T11:53:06Z","oa":1,"publication_identifier":{"isbn":["9781538655603"]},"page":"1-10","publication":"2018 International Conference on Embedded Software","publisher":"IEEE","date_created":"2019-02-13T09:19:28Z","citation":{"short":"A. Bakhirkin, T. Ferrere, T.A. Henzinger, D. Nickovicl, in:, 2018 International Conference on Embedded Software, IEEE, 2018, pp. 1–10.","mla":"Bakhirkin, Alexey, et al. “Keynote: The First-Order Logic of Signals.” <i>2018 International Conference on Embedded Software</i>, IEEE, 2018, pp. 1–10, doi:<a href=\"https://doi.org/10.1109/emsoft.2018.8537203\">10.1109/emsoft.2018.8537203</a>.","ieee":"A. Bakhirkin, T. Ferrere, T. A. Henzinger, and D. Nickovicl, “Keynote: The first-order logic of signals,” in <i>2018 International Conference on Embedded Software</i>, Turin, Italy, 2018, pp. 1–10.","ama":"Bakhirkin A, Ferrere T, Henzinger TA, Nickovicl D. Keynote: The first-order logic of signals. In: <i>2018 International Conference on Embedded Software</i>. IEEE; 2018:1-10. doi:<a href=\"https://doi.org/10.1109/emsoft.2018.8537203\">10.1109/emsoft.2018.8537203</a>","ista":"Bakhirkin A, Ferrere T, Henzinger TA, Nickovicl D. 2018. Keynote: The first-order logic of signals. 2018 International Conference on Embedded Software. EMSOFT: Embedded Software, 1–10.","apa":"Bakhirkin, A., Ferrere, T., Henzinger, T. A., &#38; Nickovicl, D. (2018). Keynote: The first-order logic of signals. In <i>2018 International Conference on Embedded Software</i> (pp. 1–10). Turin, Italy: IEEE. <a href=\"https://doi.org/10.1109/emsoft.2018.8537203\">https://doi.org/10.1109/emsoft.2018.8537203</a>","chicago":"Bakhirkin, Alexey, Thomas Ferrere, Thomas A Henzinger, and Deian Nickovicl. “Keynote: The First-Order Logic of Signals.” In <i>2018 International Conference on Embedded Software</i>, 1–10. IEEE, 2018. <a href=\"https://doi.org/10.1109/emsoft.2018.8537203\">https://doi.org/10.1109/emsoft.2018.8537203</a>."},"ddc":["000"],"external_id":{"isi":["000492828500005"]},"language":[{"iso":"eng"}],"isi":1,"month":"09","has_accepted_license":"1","_id":"5959","abstract":[{"lang":"eng","text":"Formalizing properties of systems with continuous dynamics is a challenging task. In this paper, we propose a formal framework for specifying and monitoring rich temporal properties of real-valued signals. We introduce signal first-order logic (SFO) as a specification language that combines first-order logic with linear-real arithmetic and unary function symbols interpreted as piecewise-linear signals. We first show that while the satisfiability problem for SFO is undecidable, its membership and monitoring problems are decidable. We develop an offline monitoring procedure for SFO that has polynomial complexity in the size of the input trace and the specification, for a fixed number of quantifiers and function symbols. We show that the algorithm has computation time linear in the size of the input trace for the important fragment of bounded-response specifications interpreted over input traces with finite variability. We can use our results to extend signal temporal logic with first-order quantifiers over time and value parameters, while preserving its efficient monitoring. We finally demonstrate the practical appeal of our logic through a case study in the micro-electronics domain."}],"type":"conference","scopus_import":"1","file_date_updated":"2020-07-14T12:47:13Z","conference":{"name":"EMSOFT: Embedded Software","end_date":"2018-10-05","location":"Turin, Italy","start_date":"2018-09-30"},"status":"public"},{"publisher":"Springer","publication":"Handbook of Model Checking","date_published":"2018-05-19T00:00:00Z","date_created":"2018-12-11T11:44:25Z","citation":{"short":"E. Clarke, T.A. Henzinger, H. Veith, in:, T.A. Henzinger (Ed.), Handbook of Model Checking, Springer, 2018, pp. 1–26.","mla":"Clarke, Edmund, et al. “Introduction to Model Checking.” <i>Handbook of Model Checking</i>, edited by Thomas A Henzinger, Springer, 2018, pp. 1–26, doi:<a href=\"https://doi.org/10.1007/978-3-319-10575-8_1\">10.1007/978-3-319-10575-8_1</a>.","ama":"Clarke E, Henzinger TA, Veith H. Introduction to model checking. In: Henzinger TA, ed. <i>Handbook of Model Checking</i>. Handbook of Model Checking. Springer; 2018:1-26. doi:<a href=\"https://doi.org/10.1007/978-3-319-10575-8_1\">10.1007/978-3-319-10575-8_1</a>","ieee":"E. Clarke, T. A. Henzinger, and H. Veith, “Introduction to model checking,” in <i>Handbook of Model Checking</i>, T. A. Henzinger, Ed. Springer, 2018, pp. 1–26.","ista":"Clarke E, Henzinger TA, Veith H. 2018.Introduction to model checking. In: Handbook of Model Checking. , 1–26.","apa":"Clarke, E., Henzinger, T. A., &#38; Veith, H. (2018). Introduction to model checking. In T. A. Henzinger (Ed.), <i>Handbook of Model Checking</i> (pp. 1–26). Springer. <a href=\"https://doi.org/10.1007/978-3-319-10575-8_1\">https://doi.org/10.1007/978-3-319-10575-8_1</a>","chicago":"Clarke, Edmund, Thomas A Henzinger, and Helmut Veith. “Introduction to Model Checking.” In <i>Handbook of Model Checking</i>, edited by Thomas A Henzinger, 1–26. Handbook of Model Checking. Springer, 2018. <a href=\"https://doi.org/10.1007/978-3-319-10575-8_1\">https://doi.org/10.1007/978-3-319-10575-8_1</a>."},"day":"19","author":[{"last_name":"Clarke","full_name":"Clarke, Edmund","first_name":"Edmund"},{"first_name":"Thomas A","full_name":"Henzinger, Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"},{"first_name":"Helmut","full_name":"Veith, Helmut","last_name":"Veith"}],"page":"1 - 26","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","oa_version":"None","year":"2018","date_updated":"2021-01-12T08:05:35Z","publication_status":"published","scopus_import":1,"status":"public","title":"Introduction to model checking","department":[{"_id":"ToHe"}],"editor":[{"first_name":"Thomas A","full_name":"Henzinger, Thomas A","last_name":"Henzinger"}],"month":"05","series_title":"Handbook of Model Checking","language":[{"iso":"eng"}],"doi":"10.1007/978-3-319-10575-8_1","type":"book_chapter","quality_controlled":"1","_id":"60","abstract":[{"text":"Model checking is a computer-assisted method for the analysis of dynamical systems that can be modeled by state-transition systems. Drawing from research traditions in mathematical logic, programming languages, hardware design, and theoretical computer science, model checking is now widely used for the verification of hardware and software in industry. This chapter is an introduction and short survey of model checking. The chapter aims to motivate and link the individual chapters of the handbook, and to provide context for readers who are not familiar with model checking.","lang":"eng"}],"publist_id":"7994"},{"citation":{"apa":"Avni, G., Guha, S., &#38; Kupferman, O. (2018). Timed network games with clocks (Vol. 117). Presented at the MFCS: Mathematical Foundations of Computer Science, Liverpool, United Kingdom: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPICS.MFCS.2018.23\">https://doi.org/10.4230/LIPICS.MFCS.2018.23</a>","chicago":"Avni, Guy, Shibashis Guha, and Orna Kupferman. “Timed Network Games with Clocks,” Vol. 117. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. <a href=\"https://doi.org/10.4230/LIPICS.MFCS.2018.23\">https://doi.org/10.4230/LIPICS.MFCS.2018.23</a>.","ista":"Avni G, Guha S, Kupferman O. 2018. Timed network games with clocks. MFCS: Mathematical Foundations of Computer Science, LIPIcs, vol. 117, 23.","ieee":"G. Avni, S. Guha, and O. Kupferman, “Timed network games with clocks,” presented at the MFCS: Mathematical Foundations of Computer Science, Liverpool, United Kingdom, 2018, vol. 117.","ama":"Avni G, Guha S, Kupferman O. Timed network games with clocks. In: Vol 117. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2018. doi:<a href=\"https://doi.org/10.4230/LIPICS.MFCS.2018.23\">10.4230/LIPICS.MFCS.2018.23</a>","mla":"Avni, Guy, et al. <i>Timed Network Games with Clocks</i>. Vol. 117, 23, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018, doi:<a href=\"https://doi.org/10.4230/LIPICS.MFCS.2018.23\">10.4230/LIPICS.MFCS.2018.23</a>.","short":"G. Avni, S. Guha, O. Kupferman, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018."},"ddc":["000"],"intvolume":"       117","date_created":"2019-02-14T14:12:09Z","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","volume":117,"publication_identifier":{"issn":["1868-8969"]},"oa":1,"date_updated":"2025-07-10T12:01:59Z","related_material":{"record":[{"relation":"earlier_version","status":"public","id":"963"}]},"oa_version":"Published Version","alternative_title":["LIPIcs"],"status":"public","scopus_import":"1","file_date_updated":"2020-07-14T12:47:15Z","conference":{"name":"MFCS: Mathematical Foundations of Computer Science","start_date":"2018-08-27","location":"Liverpool, United Kingdom","end_date":"2018-08-31"},"abstract":[{"text":"Network games are widely used as a model for selfish resource-allocation problems. In the classicalmodel, each player selects a path connecting her source and target vertices. The cost of traversingan edge depends on theload; namely, number of players that traverse it. Thus, it abstracts the factthat different users may use a resource at different times and for different durations, which playsan important role in determining the costs of the users in reality. For example, when transmittingpackets in a communication network, routing traffic in a road network, or processing a task in aproduction system, actual sharing and congestion of resources crucially depends on time.In [13], we introducedtimed network games, which add a time component to network games.Each vertexvin the network is associated with a cost function, mapping the load onvto theprice that a player pays for staying invfor one time unit with this load.  Each edge in thenetwork is guarded by the time intervals in which it can be traversed, which forces the players tospend time in the vertices. In this work we significantly extend the way time can be referred toin timed network games. In the model we study, the network is equipped withclocks, and, as intimed automata, edges are guarded by constraints on the values of the clocks, and their traversalmay involve a reset of some clocks. We argue that the stronger model captures many realisticnetworks.  The addition of clocks breaks the techniques we developed in [13] and we developnew techniques in order to show that positive results on classic network games carry over to thestronger timed setting.","lang":"eng"}],"has_accepted_license":"1","_id":"6005","type":"conference","language":[{"iso":"eng"}],"article_number":"23","month":"08","author":[{"full_name":"Avni, Guy","first_name":"Guy","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-5588-8287","last_name":"Avni"},{"last_name":"Guha","first_name":"Shibashis","full_name":"Guha, Shibashis"},{"full_name":"Kupferman, Orna","first_name":"Orna","last_name":"Kupferman"}],"day":"01","tmp":{"image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"date_published":"2018-08-01T00:00:00Z","article_processing_charge":"No","publication_status":"published","year":"2018","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","department":[{"_id":"ToHe"}],"title":"Timed network games with clocks","file":[{"relation":"main_file","date_created":"2019-02-14T14:22:04Z","content_type":"application/pdf","checksum":"41ab2ae9b63f5eb49fa995250c0ba128","file_size":542889,"date_updated":"2020-07-14T12:47:15Z","creator":"dernst","file_name":"2018_LIPIcs_Avni.pdf","access_level":"open_access","file_id":"6007"}],"quality_controlled":"1","project":[{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","call_identifier":"FWF","name":"Rigorous Systems Engineering"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","call_identifier":"FWF","name":"Formal methods for the design and analysis of complex systems"},{"_id":"264B3912-B435-11E9-9278-68D0E5697425","grant_number":"M02369","call_identifier":"FWF","name":"Formal Methods meets Algorithmic Game Theory"}],"doi":"10.4230/LIPICS.MFCS.2018.23"},{"publication_status":"published","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","year":"2018","tmp":{"image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"date_published":"2018-09-01T00:00:00Z","day":"01","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","full_name":"Guha, Shibashis","first_name":"Shibashis"},{"last_name":"Kupferman","first_name":"Orna","full_name":"Kupferman, Orna"}],"article_processing_charge":"No","project":[{"name":"Formal Methods meets Algorithmic Game Theory","call_identifier":"FWF","_id":"264B3912-B435-11E9-9278-68D0E5697425","grant_number":"M02369"},{"grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","call_identifier":"FWF"},{"call_identifier":"FWF","name":"Formal methods for the design and analysis of complex systems","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425"}],"doi":"10.3390/g9030039","quality_controlled":"1","title":"An abstraction-refinement methodology for reasoning about network games","department":[{"_id":"ToHe"}],"file":[{"creator":"kschuh","date_updated":"2020-07-14T12:47:16Z","file_name":"2018_MDPI_Avni.pdf","access_level":"open_access","file_id":"6008","content_type":"application/pdf","checksum":"749d65ca4ce74256a029d9644a1b1cb0","relation":"main_file","date_created":"2019-02-14T14:20:31Z","file_size":505155}],"related_material":{"record":[{"relation":"earlier_version","status":"public","id":"1003"}]},"oa":1,"date_updated":"2025-07-10T11:49:38Z","oa_version":"Published Version","publisher":"MDPI","publication":"Games","intvolume":"         9","citation":{"apa":"Avni, G., Guha, S., &#38; Kupferman, O. (2018). An abstraction-refinement methodology for reasoning about network games. <i>Games</i>. MDPI. <a href=\"https://doi.org/10.3390/g9030039\">https://doi.org/10.3390/g9030039</a>","chicago":"Avni, Guy, Shibashis Guha, and Orna Kupferman. “An Abstraction-Refinement Methodology for Reasoning about Network Games.” <i>Games</i>. MDPI, 2018. <a href=\"https://doi.org/10.3390/g9030039\">https://doi.org/10.3390/g9030039</a>.","ista":"Avni G, Guha S, Kupferman O. 2018. An abstraction-refinement methodology for reasoning about network games. Games. 9(3), 39.","ieee":"G. Avni, S. Guha, and O. Kupferman, “An abstraction-refinement methodology for reasoning about network games,” <i>Games</i>, vol. 9, no. 3. MDPI, 2018.","ama":"Avni G, Guha S, Kupferman O. An abstraction-refinement methodology for reasoning about network games. <i>Games</i>. 2018;9(3). doi:<a href=\"https://doi.org/10.3390/g9030039\">10.3390/g9030039</a>","mla":"Avni, Guy, et al. “An Abstraction-Refinement Methodology for Reasoning about Network Games.” <i>Games</i>, vol. 9, no. 3, 39, MDPI, 2018, doi:<a href=\"https://doi.org/10.3390/g9030039\">10.3390/g9030039</a>.","short":"G. Avni, S. Guha, O. Kupferman, Games 9 (2018)."},"date_created":"2019-02-14T14:17:54Z","ddc":["004"],"volume":9,"publication_identifier":{"issn":["2073-4336"]},"type":"journal_article","has_accepted_license":"1","_id":"6006","abstract":[{"lang":"eng","text":"Network games (NGs) are played on directed graphs and are extensively used in network design and analysis. Search problems for NGs include finding special strategy profiles such as a Nash equilibrium and a globally-optimal solution. The networks modeled by NGs may be huge. In formal verification, abstraction has proven to be an extremely effective technique for reasoning about systems with big and even infinite state spaces. We describe an abstraction-refinement methodology for reasoning about NGs. Our methodology is based on an abstraction function that maps the state space of an NG to a much smaller state space. We search for a global optimum and a Nash equilibrium by reasoning on an under- and an over-approximation defined on top of this smaller state space. When the approximations are too coarse to find such profiles, we refine the abstraction function. We extend the abstraction-refinement methodology to labeled networks, where the objectives of the players are regular languages. Our experimental results demonstrate the effectiveness of the methodology. "}],"month":"09","article_number":"39","language":[{"iso":"eng"}],"status":"public","issue":"3","scopus_import":"1","file_date_updated":"2020-07-14T12:47:16Z"},{"date_updated":"2026-06-18T18:58:53Z","oa":1,"oa_version":"Published Version","citation":{"mla":"Avni, Guy, and Orna Kupferman. “Synthesis from Component Libraries with Costs.” <i>Theoretical Computer Science</i>, vol. 712, Elsevier, 2018, pp. 50–72, doi:<a href=\"https://doi.org/10.1016/j.tcs.2017.11.001\">10.1016/j.tcs.2017.11.001</a>.","short":"G. Avni, O. Kupferman, Theoretical Computer Science 712 (2018) 50–72.","ista":"Avni G, Kupferman O. 2018. Synthesis from component libraries with costs. Theoretical Computer Science. 712, 50–72.","chicago":"Avni, Guy, and Orna Kupferman. “Synthesis from Component Libraries with Costs.” <i>Theoretical Computer Science</i>. Elsevier, 2018. <a href=\"https://doi.org/10.1016/j.tcs.2017.11.001\">https://doi.org/10.1016/j.tcs.2017.11.001</a>.","apa":"Avni, G., &#38; Kupferman, O. (2018). Synthesis from component libraries with costs. <i>Theoretical Computer Science</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.tcs.2017.11.001\">https://doi.org/10.1016/j.tcs.2017.11.001</a>","ieee":"G. Avni and O. Kupferman, “Synthesis from component libraries with costs,” <i>Theoretical Computer Science</i>, vol. 712. Elsevier, pp. 50–72, 2018.","ama":"Avni G, Kupferman O. Synthesis from component libraries with costs. <i>Theoretical Computer Science</i>. 2018;712:50-72. doi:<a href=\"https://doi.org/10.1016/j.tcs.2017.11.001\">10.1016/j.tcs.2017.11.001</a>"},"date_created":"2018-12-11T11:47:28Z","ddc":["000"],"intvolume":"       712","publication":"Theoretical Computer Science","publisher":"Elsevier","page":"50 - 72","ec_funded":1,"volume":712,"article_type":"original","main_file_link":[{"open_access":"1","url":"http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.636.4529"}],"type":"journal_article","abstract":[{"text":"Synthesis is the automated construction of a system from its specification. In real life, hardware and software systems are rarely constructed from scratch. Rather, a system is typically constructed from a library of components. Lustig and Vardi formalized this intuition and studied LTL synthesis from component libraries. In real life, designers seek optimal systems. In this paper we add optimality considerations to the setting. We distinguish between quality considerations (for example, size - the smaller a system is, the better it is), and pricing (for example, the payment to the company who manufactured the component). We study the problem of designing systems with minimal quality-cost and price. A key point is that while the quality cost is individual - the choices of a designer are independent of choices made by other designers that use the same library, pricing gives rise to a resource-allocation game - designers that use the same component share its price, with the share being proportional to the number of uses (a component can be used several times in a design). We study both closed and open settings, and in both we solve the problem of finding an optimal design. In a setting with multiple designers, we also study the game-theoretic problems of the induced resource-allocation game.","lang":"eng"}],"publist_id":"7197","_id":"608","month":"02","external_id":{"isi":["000424959200003"]},"language":[{"iso":"eng"}],"isi":1,"status":"public","scopus_import":"1","publication_status":"published","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","year":"2018","date_published":"2018-02-15T00:00:00Z","author":[{"first_name":"Guy","full_name":"Avni, Guy","last_name":"Avni","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-5588-8287"},{"full_name":"Kupferman, Orna","first_name":"Orna","last_name":"Kupferman"}],"day":"15","corr_author":"1","article_processing_charge":"No","quality_controlled":"1","project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","call_identifier":"FP7","name":"Quantitative Reactive Modeling"},{"call_identifier":"FWF","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"},{"grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"Formal methods for the design and analysis of complex systems","call_identifier":"FWF"}],"doi":"10.1016/j.tcs.2017.11.001","title":"Synthesis from component libraries with costs","department":[{"_id":"ToHe"}]},{"user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","year":"2018","oa_version":"None","date_updated":"2021-12-21T10:49:36Z","place":"Cham","publication_status":"published","publication_identifier":{"eisbn":["978-3-319-10575-8"],"isbn":["978-3-319-10574-1"]},"article_processing_charge":"No","date_created":"2018-12-11T12:02:32Z","citation":{"ista":"Clarke EM, Henzinger TA, Veith H, Bloem R. 2018. Handbook of Model Checking 1st ed., Cham: Springer Nature, XLVIII, 1212p.","apa":"Clarke, E. M., Henzinger, T. A., Veith, H., &#38; Bloem, R. (2018). <i>Handbook of Model Checking</i> (1st ed.). Cham: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-319-10575-8\">https://doi.org/10.1007/978-3-319-10575-8</a>","chicago":"Clarke, Edmund M., Thomas A Henzinger, Helmut Veith, and Roderick Bloem. <i>Handbook of Model Checking</i>. 1st ed. Cham: Springer Nature, 2018. <a href=\"https://doi.org/10.1007/978-3-319-10575-8\">https://doi.org/10.1007/978-3-319-10575-8</a>.","ama":"Clarke EM, Henzinger TA, Veith H, Bloem R. <i>Handbook of Model Checking</i>. 1st ed. Cham: Springer Nature; 2018. doi:<a href=\"https://doi.org/10.1007/978-3-319-10575-8\">10.1007/978-3-319-10575-8</a>","ieee":"E. M. Clarke, T. A. Henzinger, H. Veith, and R. Bloem, <i>Handbook of Model Checking</i>, 1st ed. Cham: Springer Nature, 2018.","mla":"Clarke, Edmund M., et al. <i>Handbook of Model Checking</i>. 1st ed., Springer Nature, 2018, doi:<a href=\"https://doi.org/10.1007/978-3-319-10575-8\">10.1007/978-3-319-10575-8</a>.","short":"E.M. Clarke, T.A. Henzinger, H. Veith, R. Bloem, Handbook of Model Checking, 1st ed., Springer Nature, Cham, 2018."},"date_published":"2018-06-08T00:00:00Z","publisher":"Springer Nature","author":[{"last_name":"Clarke","first_name":"Edmund M.","full_name":"Clarke, Edmund M."},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","last_name":"Henzinger","full_name":"Henzinger, Thomas A","first_name":"Thomas A"},{"last_name":"Veith","first_name":"Helmut","full_name":"Veith, Helmut"},{"first_name":"Roderick","full_name":"Bloem, Roderick","last_name":"Bloem"}],"page":"XLVIII, 1212","day":"08","month":"06","language":[{"iso":"eng"}],"edition":"1","quality_controlled":"1","doi":"10.1007/978-3-319-10575-8","type":"book","publist_id":"3340","abstract":[{"text":"This book first explores the origins of this idea, grounded in theoretical work on temporal logic and automata. The editors and authors are among the world's leading researchers in this domain, and they contributed 32 chapters representing a thorough view of the development and application of the technique. Topics covered include binary decision diagrams, symbolic model checking, satisfiability modulo theories, partial-order reduction, abstraction, interpolation, concurrency, security protocols, games, probabilistic model checking, and process algebra, and chapters on the transfer of theory to industrial practice, property specification languages for hardware, and verification of real-time systems and hybrid systems.\r\n\r\nThe book will be valuable for researchers and graduate students engaged with the development of formal methods and verification tools.","lang":"eng"}],"_id":"3300","scopus_import":"1","title":"Handbook of Model Checking","status":"public","department":[{"_id":"ToHe"}]},{"volume":19,"page":"3320 - 3333","date_created":"2018-12-11T11:46:27Z","intvolume":"        19","citation":{"apa":"Jiang, Y., Liu, H., Song, H., Kong, H., Wang, R., Guan, Y., &#38; Sha, L. (2018). Safety-assured model-driven design of the multifunction vehicle bus controller. <i>IEEE Transactions on Intelligent Transportation Systems</i>. IEEE. <a href=\"https://doi.org/10.1109/TITS.2017.2778077\">https://doi.org/10.1109/TITS.2017.2778077</a>","chicago":"Jiang, Yu, Han Liu, Huobing Song, Hui Kong, Rui Wang, Yong Guan, and Lui Sha. “Safety-Assured Model-Driven Design of the Multifunction Vehicle Bus Controller.” <i>IEEE Transactions on Intelligent Transportation Systems</i>. IEEE, 2018. <a href=\"https://doi.org/10.1109/TITS.2017.2778077\">https://doi.org/10.1109/TITS.2017.2778077</a>.","ista":"Jiang Y, Liu H, Song H, Kong H, Wang R, Guan Y, Sha L. 2018. Safety-assured model-driven design of the multifunction vehicle bus controller. IEEE Transactions on Intelligent Transportation Systems. 19(10), 3320–3333.","ieee":"Y. Jiang <i>et al.</i>, “Safety-assured model-driven design of the multifunction vehicle bus controller,” <i>IEEE Transactions on Intelligent Transportation Systems</i>, vol. 19, no. 10. IEEE, pp. 3320–3333, 2018.","ama":"Jiang Y, Liu H, Song H, et al. Safety-assured model-driven design of the multifunction vehicle bus controller. <i>IEEE Transactions on Intelligent Transportation Systems</i>. 2018;19(10):3320-3333. doi:<a href=\"https://doi.org/10.1109/TITS.2017.2778077\">10.1109/TITS.2017.2778077</a>","mla":"Jiang, Yu, et al. “Safety-Assured Model-Driven Design of the Multifunction Vehicle Bus Controller.” <i>IEEE Transactions on Intelligent Transportation Systems</i>, vol. 19, no. 10, IEEE, 2018, pp. 3320–33, doi:<a href=\"https://doi.org/10.1109/TITS.2017.2778077\">10.1109/TITS.2017.2778077</a>.","short":"Y. Jiang, H. Liu, H. Song, H. Kong, R. Wang, Y. Guan, L. Sha, IEEE Transactions on Intelligent Transportation Systems 19 (2018) 3320–3333."},"publisher":"IEEE","publication":"IEEE Transactions on Intelligent Transportation Systems","oa_version":"None","date_updated":"2025-09-22T09:39:54Z","related_material":{"record":[{"id":"1205","relation":"earlier_version","status":"public"}]},"scopus_import":"1","issue":"10","status":"public","external_id":{"isi":["000446651100020"]},"isi":1,"language":[{"iso":"eng"}],"month":"01","abstract":[{"lang":"eng","text":"In this paper, we present a formal model-driven design approach to establish a safety-assured implementation of multifunction vehicle bus controller (MVBC), which controls the data transmission among the devices of the vehicle. First, the generic models and safety requirements described in International Electrotechnical Commission Standard 61375 are formalized as time automata and timed computation tree logic formulas, respectively. With model checking tool Uppaal, we verify whether or not the constructed timed automata satisfy the formulas and several logic inconsistencies in the original standard are detected and corrected. Then, we apply the code generation tool Times to generate C code from the verified model, which is later synthesized into a real MVBC chip, with some handwriting glue code. Furthermore, the runtime verification tool RMOR is applied on the integrated code, to verify some safety requirements that cannot be formalized on the timed automata. For evaluation, we compare the proposed approach with existing MVBC design methods, such as BeagleBone, Galsblock, and Simulink. Experiments show that more ambiguousness or bugs in the standard are detected during Uppaal verification, and the generated code of Times outperforms the C code generated by others in terms of the synthesized binary code size. The errors in the standard have been confirmed and the resulting MVBC has been deployed in the real train communication network."}],"publist_id":"7389","_id":"434","type":"journal_article","article_processing_charge":"No","author":[{"last_name":"Jiang","first_name":"Yu","full_name":"Jiang, Yu"},{"first_name":"Han","full_name":"Liu, Han","last_name":"Liu"},{"full_name":"Song, Huobing","first_name":"Huobing","last_name":"Song"},{"full_name":"Kong, Hui","first_name":"Hui","orcid":"0000-0002-3066-6941","id":"3BDE25AA-F248-11E8-B48F-1D18A9856A87","last_name":"Kong"},{"full_name":"Wang, Rui","first_name":"Rui","last_name":"Wang"},{"last_name":"Guan","first_name":"Yong","full_name":"Guan, Yong"},{"last_name":"Sha","first_name":"Lui","full_name":"Sha, Lui"}],"day":"01","date_published":"2018-01-01T00:00:00Z","year":"2018","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","publication_status":"published","department":[{"_id":"ToHe"}],"title":"Safety-assured model-driven design of the multifunction vehicle bus controller","quality_controlled":"1","doi":"10.1109/TITS.2017.2778077"},{"year":"2018","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publication_status":"published","article_processing_charge":"No","day":"11","author":[{"last_name":"Bakhirkin","first_name":"Alexey","full_name":"Bakhirkin, Alexey"},{"id":"40960E6E-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-5199-3143","last_name":"Ferrere","full_name":"Ferrere, Thomas","first_name":"Thomas"},{"last_name":"Maler","full_name":"Maler, Oded","first_name":"Oded"}],"date_published":"2018-04-11T00:00:00Z","doi":"10.1145/3178126.3178132","project":[{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","call_identifier":"FWF","name":"Rigorous Systems Engineering"}],"quality_controlled":"1","file":[{"content_type":"application/pdf","checksum":"81eabc96430e84336ea88310ac0a1ad0","relation":"main_file","date_created":"2020-05-14T12:18:29Z","file_size":5900421,"creator":"dernst","date_updated":"2020-07-14T12:45:17Z","file_name":"2018_HSCC_Bakhirkin.pdf","file_id":"7833","access_level":"open_access"}],"department":[{"_id":"ToHe"}],"title":"Efficient parametric identification for STL","oa_version":"Submitted Version","alternative_title":["HSCC Proceedings"],"date_updated":"2025-07-10T11:51:21Z","oa":1,"publication_identifier":{"isbn":["978-1-4503-5642-8 "]},"page":"177 - 186","publication":"Proceedings of the 21st International Conference on Hybrid Systems","publisher":"ACM","ddc":["000"],"date_created":"2018-12-11T11:45:04Z","citation":{"short":"A. Bakhirkin, T. Ferrere, O. Maler, in:, Proceedings of the 21st International Conference on Hybrid Systems, ACM, 2018, pp. 177–186.","mla":"Bakhirkin, Alexey, et al. “Efficient Parametric Identification for STL.” <i>Proceedings of the 21st International Conference on Hybrid Systems</i>, ACM, 2018, pp. 177–86, doi:<a href=\"https://doi.org/10.1145/3178126.3178132\">10.1145/3178126.3178132</a>.","ama":"Bakhirkin A, Ferrere T, Maler O. Efficient parametric identification for STL. In: <i>Proceedings of the 21st International Conference on Hybrid Systems</i>. ACM; 2018:177-186. doi:<a href=\"https://doi.org/10.1145/3178126.3178132\">10.1145/3178126.3178132</a>","ieee":"A. Bakhirkin, T. Ferrere, and O. Maler, “Efficient parametric identification for STL,” in <i>Proceedings of the 21st International Conference on Hybrid Systems</i>, Porto, Portugal, 2018, pp. 177–186.","ista":"Bakhirkin A, Ferrere T, Maler O. 2018. Efficient parametric identification for STL. Proceedings of the 21st International Conference on Hybrid Systems. HSCC: Hybrid Systems - Computation and Control, HSCC Proceedings, , 177–186.","apa":"Bakhirkin, A., Ferrere, T., &#38; Maler, O. (2018). Efficient parametric identification for STL. In <i>Proceedings of the 21st International Conference on Hybrid Systems</i> (pp. 177–186). Porto, Portugal: ACM. <a href=\"https://doi.org/10.1145/3178126.3178132\">https://doi.org/10.1145/3178126.3178132</a>","chicago":"Bakhirkin, Alexey, Thomas Ferrere, and Oded Maler. “Efficient Parametric Identification for STL.” In <i>Proceedings of the 21st International Conference on Hybrid Systems</i>, 177–86. ACM, 2018. <a href=\"https://doi.org/10.1145/3178126.3178132\">https://doi.org/10.1145/3178126.3178132</a>."},"external_id":{"isi":["000474781600020"]},"isi":1,"language":[{"iso":"eng"}],"month":"04","has_accepted_license":"1","_id":"182","abstract":[{"text":"We describe a new algorithm for the parametric identification problem for signal temporal logic (STL), stated as follows. Given a densetime real-valued signal w and a parameterized temporal logic formula φ, compute the subset of the parameter space that renders the formula satisfied by the signal. Unlike previous solutions, which were based on search in the parameter space or quantifier elimination, our procedure works recursively on φ and computes the evolution over time of the set of valid parameter assignments. This procedure is similar to that of monitoring or computing the robustness of φ relative to w. Our implementation and experiments demonstrate that this approach can work well in practice.","lang":"eng"}],"publist_id":"7739","type":"conference","file_date_updated":"2020-07-14T12:45:17Z","scopus_import":"1","conference":{"name":"HSCC: Hybrid Systems - Computation and Control","end_date":"2018-04-13","location":"Porto, Portugal","start_date":"2018-04-11"},"status":"public"},{"publisher":"Association for Computing Machinery","citation":{"ista":"Bartocci E, Ferrere T, Manjunath N, Nickovic D. 2018. Localizing faults in simulink/stateflow models with STL. HSCC: Hybrid Systems - Computation and Control, HSCC Proceedings, , 197–206.","apa":"Bartocci, E., Ferrere, T., Manjunath, N., &#38; Nickovic, D. (2018). Localizing faults in simulink/stateflow models with STL (pp. 197–206). Presented at the HSCC: Hybrid Systems - Computation and Control, Porto, Portugal: Association for Computing Machinery. <a href=\"https://doi.org/10.1145/3178126.3178131\">https://doi.org/10.1145/3178126.3178131</a>","chicago":"Bartocci, Ezio, Thomas Ferrere, Niveditha Manjunath, and Dejan Nickovic. “Localizing Faults in Simulink/Stateflow Models with STL,” 197–206. Association for Computing Machinery, 2018. <a href=\"https://doi.org/10.1145/3178126.3178131\">https://doi.org/10.1145/3178126.3178131</a>.","ieee":"E. Bartocci, T. Ferrere, N. Manjunath, and D. Nickovic, “Localizing faults in simulink/stateflow models with STL,” presented at the HSCC: Hybrid Systems - Computation and Control, Porto, Portugal, 2018, pp. 197–206.","ama":"Bartocci E, Ferrere T, Manjunath N, Nickovic D. Localizing faults in simulink/stateflow models with STL. In: Association for Computing Machinery; 2018:197-206. doi:<a href=\"https://doi.org/10.1145/3178126.3178131\">10.1145/3178126.3178131</a>","mla":"Bartocci, Ezio, et al. <i>Localizing Faults in Simulink/Stateflow Models with STL</i>. Association for Computing Machinery, 2018, pp. 197–206, doi:<a href=\"https://doi.org/10.1145/3178126.3178131\">10.1145/3178126.3178131</a>.","short":"E. Bartocci, T. Ferrere, N. Manjunath, D. Nickovic, in:, Association for Computing Machinery, 2018, pp. 197–206."},"date_created":"2018-12-11T11:45:04Z","page":"197 - 206","date_updated":"2025-07-10T11:51:22Z","alternative_title":["HSCC Proceedings"],"oa_version":"None","acknowledgement":"This work was partially supported by the Austrian Science Fund (FWF) under grants S11402-N23 and S11405-N23 (RiSE/SHiNE), the CPS/IoT project (HRSM), the EU ICT COST Action IC1402 on Run-time Verification beyond Monitoring (ARVI), the AMASS project (ECSEL 692474), and the ENABLE-S3 project (ECSEL 692455). The CPS/IoT project receives support from the Austrian government through the Federal Ministry of Science, Research and Economy (BMWFW) in the funding program Hochschulraum-Strukturmittel (HRSM) 2016. The ECSEL Joint Undertaking receives support from the European Union’s Horizon 2020 research and innovation programme and Austria, Denmark, Germany, Finland, Czech Republic, Italy, Spain, Portugal, Poland, Ireland, Belgium, France, Netherlands, United Kingdom, Slovakia, Norway.","status":"public","conference":{"name":"HSCC: Hybrid Systems - Computation and Control","location":"Porto, Portugal","end_date":"2018-04-13","start_date":"2018-04-11"},"scopus_import":"1","type":"conference","_id":"183","abstract":[{"lang":"eng","text":"Fault-localization is considered to be a very tedious and time-consuming activity in the design of complex Cyber-Physical Systems (CPS). This laborious task essentially requires expert knowledge of the system in order to discover the cause of the fault. In this context, we propose a new procedure that AIDS designers in debugging Simulink/Stateflow hybrid system models, guided by Signal Temporal Logic (STL) specifications. The proposed method relies on three main ingredients: (1) a monitoring and a trace diagnostics procedure that checks whether a tested behavior satisfies or violates an STL specification, localizes time segments and interfaces variables contributing to the property violations; (2) a slicing procedure that maps these observable behavior segments to the internal states and transitions of the Simulink model; and (3) a spectrum-based fault-localization method that combines the previous analysis from multiple tests to identify the internal states and/or transitions that are the most likely to explain the fault. We demonstrate the applicability of our approach on two Simulink models from the automotive and the avionics domain."}],"publist_id":"7738","month":"04","isi":1,"external_id":{"isi":["000474781600022"]},"language":[{"iso":"eng"}],"date_published":"2018-04-11T00:00:00Z","day":"11","author":[{"last_name":"Bartocci","first_name":"Ezio","full_name":"Bartocci, Ezio"},{"full_name":"Ferrere, Thomas","first_name":"Thomas","id":"40960E6E-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-5199-3143","last_name":"Ferrere"},{"full_name":"Manjunath, Niveditha","first_name":"Niveditha","last_name":"Manjunath"},{"last_name":"Nickovic","first_name":"Dejan","full_name":"Nickovic, Dejan"}],"article_processing_charge":"No","publication_status":"published","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","year":"2018","title":"Localizing faults in simulink/stateflow models with STL","department":[{"_id":"ToHe"}],"doi":"10.1145/3178126.3178131","project":[{"grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering"}],"quality_controlled":"1"},{"publist_id":"7976","abstract":[{"lang":"eng","text":"We provide a procedure for detecting the sub-segments of an incrementally observed Boolean signal ω that match a given temporal pattern ϕ. As a pattern specification language, we use timed regular expressions, a formalism well-suited for expressing properties of concurrent asynchronous behaviors embedded in metric time. We construct a timed automaton accepting the timed language denoted by ϕ and modify it slightly for the purpose of matching. We then apply zone-based reachability computation to this automaton while it reads ω, and retrieve all the matching segments from the results. Since the procedure is automaton based, it can be applied to patterns specified by other formalisms such as timed temporal logics reducible to timed automata or directly encoded as timed automata. The procedure has been implemented and its performance on synthetic examples is demonstrated."}],"_id":"78","has_accepted_license":"1","type":"conference","isi":1,"language":[{"iso":"eng"}],"external_id":{"isi":["000884993200013"]},"month":"08","status":"public","scopus_import":"1","file_date_updated":"2020-07-14T12:48:03Z","conference":{"name":"FORMATS: Formal Modeling and Analysis of Timed Systems","start_date":"2018-09-04","location":"Bejing, China","end_date":"2018-09-06"},"date_updated":"2025-04-15T06:26:03Z","oa":1,"oa_version":"Submitted Version","alternative_title":["LNCS"],"page":"215 - 232","citation":{"short":"A. Bakhirkin, T. Ferrere, D. Nickovic, O. Maler, E. Asarin, in:, Springer, 2018, pp. 215–232.","mla":"Bakhirkin, Alexey, et al. <i>Online Timed Pattern Matching Using Automata</i>. Vol. 11022, Springer, 2018, pp. 215–32, doi:<a href=\"https://doi.org/10.1007/978-3-030-00151-3_13\">10.1007/978-3-030-00151-3_13</a>.","ama":"Bakhirkin A, Ferrere T, Nickovic D, Maler O, Asarin E. Online timed pattern matching using automata. In: Vol 11022. Springer; 2018:215-232. doi:<a href=\"https://doi.org/10.1007/978-3-030-00151-3_13\">10.1007/978-3-030-00151-3_13</a>","ieee":"A. Bakhirkin, T. Ferrere, D. Nickovic, O. Maler, and E. Asarin, “Online timed pattern matching using automata,” presented at the FORMATS: Formal Modeling and Analysis of Timed Systems, Bejing, China, 2018, vol. 11022, pp. 215–232.","ista":"Bakhirkin A, Ferrere T, Nickovic D, Maler O, Asarin E. 2018. Online timed pattern matching using automata. FORMATS: Formal Modeling and Analysis of Timed Systems, LNCS, vol. 11022, 215–232.","chicago":"Bakhirkin, Alexey, Thomas Ferrere, Dejan Nickovic, Oded Maler, and Eugene Asarin. “Online Timed Pattern Matching Using Automata,” 11022:215–32. Springer, 2018. <a href=\"https://doi.org/10.1007/978-3-030-00151-3_13\">https://doi.org/10.1007/978-3-030-00151-3_13</a>.","apa":"Bakhirkin, A., Ferrere, T., Nickovic, D., Maler, O., &#38; Asarin, E. (2018). Online timed pattern matching using automata (Vol. 11022, pp. 215–232). Presented at the FORMATS: Formal Modeling and Analysis of Timed Systems, Bejing, China: Springer. <a href=\"https://doi.org/10.1007/978-3-030-00151-3_13\">https://doi.org/10.1007/978-3-030-00151-3_13</a>"},"ddc":["000"],"date_created":"2018-12-11T11:44:31Z","intvolume":"     11022","publisher":"Springer","publication_identifier":{"isbn":["978-3-030-00150-6"]},"volume":11022,"quality_controlled":"1","project":[{"call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","call_identifier":"FWF","name":"Formal methods for the design and analysis of complex systems"}],"doi":"10.1007/978-3-030-00151-3_13","department":[{"_id":"ToHe"}],"title":"Online timed pattern matching using automata","file":[{"relation":"main_file","date_created":"2020-05-14T11:34:34Z","content_type":"application/pdf","checksum":"436b7574934324cfa7d1d3986fddc65b","file_size":374851,"date_updated":"2020-07-14T12:48:03Z","creator":"dernst","file_name":"2018_LNCS_Bakhirkin.pdf","access_level":"open_access","file_id":"7831"}],"publication_status":"published","year":"2018","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","author":[{"first_name":"Alexey","full_name":"Bakhirkin, Alexey","last_name":"Bakhirkin"},{"orcid":"0000-0001-5199-3143","id":"40960E6E-F248-11E8-B48F-1D18A9856A87","last_name":"Ferrere","full_name":"Ferrere, Thomas","first_name":"Thomas"},{"full_name":"Nickovic, Dejan","first_name":"Dejan","last_name":"Nickovic"},{"first_name":"Oded","full_name":"Maler, Oded","last_name":"Maler"},{"first_name":"Eugene","full_name":"Asarin, Eugene","last_name":"Asarin"}],"day":"26","date_published":"2018-08-26T00:00:00Z","article_processing_charge":"No"},{"page":"53-70","publisher":"Springer","date_created":"2018-12-11T11:44:31Z","intvolume":"     11024","citation":{"short":"S. Arming, E. Bartocci, K. Chatterjee, J.P. Katoen, A. Sokolova, in:, Springer, 2018, pp. 53–70.","mla":"Arming, Sebastian, et al. <i>Parameter-Independent Strategies for PMDPs via POMDPs</i>. Vol. 11024, Springer, 2018, pp. 53–70, doi:<a href=\"https://doi.org/10.1007/978-3-319-99154-2_4\">10.1007/978-3-319-99154-2_4</a>.","ieee":"S. Arming, E. Bartocci, K. Chatterjee, J. P. Katoen, and A. Sokolova, “Parameter-independent strategies for pMDPs via POMDPs,” presented at the QEST: Quantitative Evaluation of Systems, Beijing, China, 2018, vol. 11024, pp. 53–70.","ama":"Arming S, Bartocci E, Chatterjee K, Katoen JP, Sokolova A. Parameter-independent strategies for pMDPs via POMDPs. In: Vol 11024. Springer; 2018:53-70. doi:<a href=\"https://doi.org/10.1007/978-3-319-99154-2_4\">10.1007/978-3-319-99154-2_4</a>","apa":"Arming, S., Bartocci, E., Chatterjee, K., Katoen, J. P., &#38; Sokolova, A. (2018). Parameter-independent strategies for pMDPs via POMDPs (Vol. 11024, pp. 53–70). Presented at the QEST: Quantitative Evaluation of Systems, Beijing, China: Springer. <a href=\"https://doi.org/10.1007/978-3-319-99154-2_4\">https://doi.org/10.1007/978-3-319-99154-2_4</a>","chicago":"Arming, Sebastian, Ezio Bartocci, Krishnendu Chatterjee, Joost P Katoen, and Ana Sokolova. “Parameter-Independent Strategies for PMDPs via POMDPs,” 11024:53–70. Springer, 2018. <a href=\"https://doi.org/10.1007/978-3-319-99154-2_4\">https://doi.org/10.1007/978-3-319-99154-2_4</a>.","ista":"Arming S, Bartocci E, Chatterjee K, Katoen JP, Sokolova A. 2018. Parameter-independent strategies for pMDPs via POMDPs. QEST: Quantitative Evaluation of Systems, LNCS, vol. 11024, 53–70."},"main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1806.05126"}],"volume":11024,"oa":1,"date_updated":"2023-09-13T09:38:28Z","oa_version":"Preprint","alternative_title":["LNCS"],"status":"public","scopus_import":"1","conference":{"name":"QEST: Quantitative Evaluation of Systems","end_date":"2018-09-07","location":"Beijing, China","start_date":"2018-09-04"},"_id":"79","abstract":[{"text":"Markov Decision Processes (MDPs) are a popular class of models suitable for solving control decision problems in probabilistic reactive systems. We consider parametric MDPs (pMDPs) that include parameters in some of the transition probabilities to account for stochastic uncertainties of the environment such as noise or input disturbances. We study pMDPs with reachability objectives where the parameter values are unknown and impossible to measure directly during execution, but there is a probability distribution known over the parameter values. We study for the first time computing parameter-independent strategies that are expectation optimal, i.e., optimize the expected reachability probability under the probability distribution over the parameters. We present an encoding of our problem to partially observable MDPs (POMDPs), i.e., a reduction of our problem to computing optimal strategies in POMDPs. We evaluate our method experimentally on several benchmarks: a motivating (repeated) learner model; a series of benchmarks of varying configurations of a robot moving on a grid; and a consensus protocol.","lang":"eng"}],"publist_id":"7975","type":"conference","isi":1,"external_id":{"arxiv":["1806.05126"],"isi":["000548912200004"]},"language":[{"iso":"eng"}],"month":"08","day":"15","author":[{"last_name":"Arming","full_name":"Arming, Sebastian","first_name":"Sebastian"},{"full_name":"Bartocci, Ezio","first_name":"Ezio","last_name":"Bartocci"},{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu"},{"full_name":"Katoen, Joost P","first_name":"Joost P","id":"4524F760-F248-11E8-B48F-1D18A9856A87","last_name":"Katoen"},{"last_name":"Sokolova","first_name":"Ana","full_name":"Sokolova, Ana"}],"date_published":"2018-08-15T00:00:00Z","article_processing_charge":"No","arxiv":1,"publication_status":"published","year":"2018","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"title":"Parameter-independent strategies for pMDPs via POMDPs","doi":"10.1007/978-3-319-99154-2_4","quality_controlled":"1"},{"department":[{"_id":"ToHe"}],"title":"Monitoring temporal logic with clock variables","file":[{"creator":"dernst","date_updated":"2020-10-09T06:24:21Z","file_id":"8638","access_level":"open_access","file_name":"2018_LNCS_Elgyuett.pdf","checksum":"e5d81c9b50a6bd9d8a2c16953aad7e23","content_type":"application/pdf","date_created":"2020-10-09T06:24:21Z","relation":"main_file","file_size":537219,"success":1}],"doi":"10.1007/978-3-030-00151-3_4","project":[{"grant_number":"S11402-N23","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","name":"Moderne Concurrency Paradigms","call_identifier":"FWF"},{"call_identifier":"FWF","name":"Formal methods for the design and analysis of complex systems","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211"}],"quality_controlled":"1","day":"26","author":[{"last_name":"Elgyütt","id":"4A2E9DBA-F248-11E8-B48F-1D18A9856A87","first_name":"Adrian","full_name":"Elgyütt, Adrian"},{"full_name":"Ferrere, Thomas","first_name":"Thomas","orcid":"0000-0001-5199-3143","id":"40960E6E-F248-11E8-B48F-1D18A9856A87","last_name":"Ferrere"},{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger"}],"date_published":"2018-08-26T00:00:00Z","article_processing_charge":"No","publication_status":"published","year":"2018","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","status":"public","file_date_updated":"2020-10-09T06:24:21Z","scopus_import":"1","conference":{"start_date":"2018-09-04","location":"Beijing, China","end_date":"2018-09-06","name":"FORMATS: Formal Modeling and Analysis of Timed Systems"},"_id":"81","has_accepted_license":"1","publist_id":"7973","abstract":[{"text":"We solve the offline monitoring problem for timed propositional temporal logic (TPTL), interpreted over dense-time Boolean signals. The variant of TPTL we consider extends linear temporal logic (LTL) with clock variables and reset quantifiers, providing a mechanism to specify real-time constraints. We first describe a general monitoring algorithm based on an exhaustive computation of the set of satisfying clock assignments as a finite union of zones. We then propose a specialized monitoring algorithm for the one-variable case using a partition of the time domain based on the notion of region equivalence, whose complexity is linear in the length of the signal, thereby generalizing a known result regarding the monitoring of metric temporal logic (MTL). The region and zone representations of time constraints are known from timed automata verification and can also be used in the discrete-time case. Our prototype implementation appears to outperform previous discrete-time implementations of TPTL monitoring,","lang":"eng"}],"type":"conference","external_id":{"isi":["000884993200004"]},"language":[{"iso":"eng"}],"isi":1,"month":"08","page":"53 - 70","publisher":"Springer","intvolume":"     11022","citation":{"mla":"Elgyütt, Adrian, et al. <i>Monitoring Temporal Logic with Clock Variables</i>. Vol. 11022, Springer, 2018, pp. 53–70, doi:<a href=\"https://doi.org/10.1007/978-3-030-00151-3_4\">10.1007/978-3-030-00151-3_4</a>.","short":"A. Elgyütt, T. Ferrere, T.A. Henzinger, in:, Springer, 2018, pp. 53–70.","ista":"Elgyütt A, Ferrere T, Henzinger TA. 2018. Monitoring temporal logic with clock variables. FORMATS: Formal Modeling and Analysis of Timed Systems, LNCS, vol. 11022, 53–70.","apa":"Elgyütt, A., Ferrere, T., &#38; Henzinger, T. A. (2018). Monitoring temporal logic with clock variables (Vol. 11022, pp. 53–70). Presented at the FORMATS: Formal Modeling and Analysis of Timed Systems, Beijing, China: Springer. <a href=\"https://doi.org/10.1007/978-3-030-00151-3_4\">https://doi.org/10.1007/978-3-030-00151-3_4</a>","chicago":"Elgyütt, Adrian, Thomas Ferrere, and Thomas A Henzinger. “Monitoring Temporal Logic with Clock Variables,” 11022:53–70. Springer, 2018. <a href=\"https://doi.org/10.1007/978-3-030-00151-3_4\">https://doi.org/10.1007/978-3-030-00151-3_4</a>.","ama":"Elgyütt A, Ferrere T, Henzinger TA. Monitoring temporal logic with clock variables. In: Vol 11022. Springer; 2018:53-70. doi:<a href=\"https://doi.org/10.1007/978-3-030-00151-3_4\">10.1007/978-3-030-00151-3_4</a>","ieee":"A. Elgyütt, T. Ferrere, and T. A. Henzinger, “Monitoring temporal logic with clock variables,” presented at the FORMATS: Formal Modeling and Analysis of Timed Systems, Beijing, China, 2018, vol. 11022, pp. 53–70."},"ddc":["000"],"date_created":"2018-12-11T11:44:31Z","volume":11022,"oa":1,"date_updated":"2025-04-15T06:26:03Z","oa_version":"Submitted Version","alternative_title":["LNCS"]},{"oa":1,"date_updated":"2025-04-15T06:26:15Z","oa_version":"Submitted Version","alternative_title":["LNCS"],"page":"143 - 161","ec_funded":1,"publication":"Principles of Modeling","publisher":"Springer","citation":{"chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. “Computing Average Response Time.” In <i>Principles of Modeling</i>, edited by Marten Lohstroh, Patricia Derler, and Marjan Sirjani, 10760:143–61. Springer, 2018. <a href=\"https://doi.org/10.1007/978-3-319-95246-8_9\">https://doi.org/10.1007/978-3-319-95246-8_9</a>.","apa":"Chatterjee, K., Henzinger, T. A., &#38; Otop, J. (2018). Computing average response time. In M. Lohstroh, P. Derler, &#38; M. Sirjani (Eds.), <i>Principles of Modeling</i> (Vol. 10760, pp. 143–161). Springer. <a href=\"https://doi.org/10.1007/978-3-319-95246-8_9\">https://doi.org/10.1007/978-3-319-95246-8_9</a>","ista":"Chatterjee K, Henzinger TA, Otop J. 2018.Computing average response time. In: Principles of Modeling. LNCS, vol. 10760, 143–161.","ama":"Chatterjee K, Henzinger TA, Otop J. Computing average response time. In: Lohstroh M, Derler P, Sirjani M, eds. <i>Principles of Modeling</i>. Vol 10760. Springer; 2018:143-161. doi:<a href=\"https://doi.org/10.1007/978-3-319-95246-8_9\">10.1007/978-3-319-95246-8_9</a>","ieee":"K. Chatterjee, T. A. Henzinger, and J. Otop, “Computing average response time,” in <i>Principles of Modeling</i>, vol. 10760, M. Lohstroh, P. Derler, and M. Sirjani, Eds. Springer, 2018, pp. 143–161.","mla":"Chatterjee, Krishnendu, et al. “Computing Average Response Time.” <i>Principles of Modeling</i>, edited by Marten Lohstroh et al., vol. 10760, Springer, 2018, pp. 143–61, doi:<a href=\"https://doi.org/10.1007/978-3-319-95246-8_9\">10.1007/978-3-319-95246-8_9</a>.","short":"K. Chatterjee, T.A. Henzinger, J. Otop, in:, M. Lohstroh, P. Derler, M. Sirjani (Eds.), Principles of Modeling, Springer, 2018, pp. 143–161."},"intvolume":"     10760","ddc":["000"],"date_created":"2018-12-11T11:44:33Z","volume":10760,"_id":"86","has_accepted_license":"1","publist_id":"7968","abstract":[{"lang":"eng","text":"Responsiveness—the requirement that every request to a system be eventually handled—is one of the fundamental liveness properties of a reactive system. Average response time is a quantitative measure for the responsiveness requirement used commonly in performance evaluation. We show how average response time can be computed on state-transition graphs, on Markov chains, and on game graphs. In all three cases, we give polynomial-time algorithms."}],"type":"book_chapter","language":[{"iso":"eng"}],"month":"07","acknowledgement":"This research was supported in part by the Austrian Science Fund (FWF) under grants S11402-N23, S11407-N23 (RiSE/SHiNE) and Z211-N23 (Wittgenstein Award), ERC Start grant (279307: Graph Games), Vienna Science and Technology Fund (WWTF) through project ICT15-003 and by the National Science Centre (NCN), Poland under grant 2014/15/D/ST6/04543.","status":"public","scopus_import":1,"file_date_updated":"2020-07-14T12:48:14Z","publication_status":"published","year":"2018","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","day":"20","author":[{"first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Thomas A","full_name":"Henzinger, Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","last_name":"Otop","full_name":"Otop, Jan","first_name":"Jan"}],"date_published":"2018-07-20T00:00:00Z","doi":"10.1007/978-3-319-95246-8_9","project":[{"grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering"},{"_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407","call_identifier":"FWF","name":"Game Theory"},{"grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"Formal methods for the design and analysis of complex systems","call_identifier":"FWF"},{"name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"grant_number":"ICT15-003","_id":"25892FC0-B435-11E9-9278-68D0E5697425","name":"Efficient Algorithms for Computer Aided Verification"}],"quality_controlled":"1","editor":[{"last_name":"Lohstroh","first_name":"Marten","full_name":"Lohstroh, Marten"},{"last_name":"Derler","first_name":"Patricia","full_name":"Derler, Patricia"},{"first_name":"Marjan","full_name":"Sirjani, Marjan","last_name":"Sirjani"}],"department":[{"_id":"KrCh"},{"_id":"ToHe"}],"title":"Computing average response time","file":[{"file_size":516307,"date_created":"2019-11-19T08:22:18Z","relation":"main_file","checksum":"9995c6ce6957333baf616fc4f20be597","content_type":"application/pdf","access_level":"open_access","file_id":"7053","file_name":"2018_PrinciplesModeling_Chatterjee.pdf","date_updated":"2020-07-14T12:48:14Z","creator":"dernst"}]},{"quality_controlled":"1","project":[{"grant_number":"S11402-N23","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Moderne Concurrency Paradigms"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","name":"Formal methods for the design and analysis of complex systems","call_identifier":"FWF"}],"doi":"10.1007/978-3-662-54580-5_10","department":[{"_id":"ToHe"}],"title":"Computing scores of forwarding schemes in switched networks with probabilistic faults","file":[{"file_size":321800,"content_type":"application/pdf","relation":"main_file","date_created":"2018-12-12T10:08:37Z","file_name":"IST-2017-758-v1+1_tacas-cr.pdf","file_id":"4698","access_level":"open_access","creator":"system","date_updated":"2018-12-12T10:08:37Z"}],"publication_status":"published","year":"2017","user_id":"ba8df636-2132-11f1-aed0-ed93e2281fdd","author":[{"first_name":"Guy","full_name":"Avni, Guy","last_name":"Avni","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-5588-8287"},{"first_name":"Shubham","full_name":"Goel, Shubham","last_name":"Goel"},{"last_name":"Henzinger","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","full_name":"Henzinger, Thomas A"},{"first_name":"Guillermo","full_name":"Rodríguez Navas, Guillermo","last_name":"Rodríguez Navas"}],"pubrep_id":"758","day":"31","date_published":"2017-03-31T00:00:00Z","corr_author":"1","article_processing_charge":"No","publist_id":"6246","abstract":[{"lang":"eng","text":"Time-triggered switched networks are a deterministic communication infrastructure used by real-time distributed embedded systems. Due to the criticality of the applications running over them, developers need to ensure that end-to-end communication is dependable and predictable. Traditional approaches assume static networks that are not flexible to changes caused by reconfigurations or, more importantly, faults, which are dealt with in the application using redundancy. We adopt the concept of handling faults in the switches from non-real-time networks while maintaining the required predictability. \r\n\r\nWe study a class of forwarding schemes that can handle various types of failures. We consider probabilistic failures. We study a class of forwarding schemes that can handle various types of failures. We consider probabilistic failures. For a given network with a forwarding scheme and a constant ℓ, we compute the {\\em score} of the scheme, namely the probability (induced by faults) that at least ℓ messages arrive on time. We reduce the scoring problem to a reachability problem on a Markov chain with a &quot;product-like&quot; structure. Its special structure allows us to reason about it symbolically, and reduce the scoring problem to #SAT. Our solution is generic and can be adapted to different networks and other contexts. Also, we show the computational complexity of the scoring problem is #P-complete, and we study methods to estimate the score. We evaluate the effectiveness of our techniques with an implementation. "}],"has_accepted_license":"1","_id":"1116","type":"conference","language":[{"iso":"eng"}],"isi":1,"external_id":{"isi":["000440733400010"]},"month":"03","status":"public","scopus_import":"1","file_date_updated":"2018-12-12T10:08:37Z","conference":{"location":"Uppsala, Sweden","end_date":"2017-04-29","start_date":"2017-04-22","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems"},"date_updated":"2026-04-16T09:56:24Z","oa":1,"oa_version":"Submitted Version","alternative_title":["LNCS"],"page":"169 - 187","date_created":"2018-12-11T11:50:14Z","intvolume":"     10206","ddc":["000"],"citation":{"ieee":"G. Avni, S. Goel, T. A. Henzinger, and G. Rodríguez Navas, “Computing scores of forwarding schemes in switched networks with probabilistic faults,” presented at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems, Uppsala, Sweden, 2017, vol. 10206, pp. 169–187.","ama":"Avni G, Goel S, Henzinger TA, Rodríguez Navas G. Computing scores of forwarding schemes in switched networks with probabilistic faults. In: Vol 10206. Springer; 2017:169-187. doi:<a href=\"https://doi.org/10.1007/978-3-662-54580-5_10\">10.1007/978-3-662-54580-5_10</a>","ista":"Avni G, Goel S, Henzinger TA, Rodríguez Navas G. 2017. Computing scores of forwarding schemes in switched networks with probabilistic faults. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 10206, 169–187.","chicago":"Avni, Guy, Shubham Goel, Thomas A Henzinger, and Guillermo Rodríguez Navas. “Computing Scores of Forwarding Schemes in Switched Networks with Probabilistic Faults,” 10206:169–87. Springer, 2017. <a href=\"https://doi.org/10.1007/978-3-662-54580-5_10\">https://doi.org/10.1007/978-3-662-54580-5_10</a>.","apa":"Avni, G., Goel, S., Henzinger, T. A., &#38; Rodríguez Navas, G. (2017). Computing scores of forwarding schemes in switched networks with probabilistic faults (Vol. 10206, pp. 169–187). Presented at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems, Uppsala, Sweden: Springer. <a href=\"https://doi.org/10.1007/978-3-662-54580-5_10\">https://doi.org/10.1007/978-3-662-54580-5_10</a>","short":"G. Avni, S. Goel, T.A. Henzinger, G. Rodríguez Navas, in:, Springer, 2017, pp. 169–187.","mla":"Avni, Guy, et al. <i>Computing Scores of Forwarding Schemes in Switched Networks with Probabilistic Faults</i>. Vol. 10206, Springer, 2017, pp. 169–87, doi:<a href=\"https://doi.org/10.1007/978-3-662-54580-5_10\">10.1007/978-3-662-54580-5_10</a>."},"publisher":"Springer","volume":10206,"publication_identifier":{"issn":["0302-9743"]}},{"publication_identifier":{"issn":["2663-337X"]},"citation":{"short":"P. Daca, Statistical and Logical Methods for Property Checking, Institute of Science and Technology Austria, 2017.","mla":"Daca, Przemyslaw. <i>Statistical and Logical Methods for Property Checking</i>. Institute of Science and Technology Austria, 2017, doi:<a href=\"https://doi.org/10.15479/AT:ISTA:TH_730\">10.15479/AT:ISTA:TH_730</a>.","ama":"Daca P. Statistical and logical methods for property checking. 2017. doi:<a href=\"https://doi.org/10.15479/AT:ISTA:TH_730\">10.15479/AT:ISTA:TH_730</a>","ieee":"P. Daca, “Statistical and logical methods for property checking,” Institute of Science and Technology Austria, 2017.","chicago":"Daca, Przemyslaw. “Statistical and Logical Methods for Property Checking.” Institute of Science and Technology Austria, 2017. <a href=\"https://doi.org/10.15479/AT:ISTA:TH_730\">https://doi.org/10.15479/AT:ISTA:TH_730</a>.","apa":"Daca, P. (2017). <i>Statistical and logical methods for property checking</i>. Institute of Science and Technology Austria. <a href=\"https://doi.org/10.15479/AT:ISTA:TH_730\">https://doi.org/10.15479/AT:ISTA:TH_730</a>","ista":"Daca P. 2017. Statistical and logical methods for property checking. Institute of Science and Technology Austria."},"ddc":["004","005"],"date_created":"2018-12-11T11:50:27Z","publisher":"Institute of Science and Technology Austria","page":"163","ec_funded":1,"alternative_title":["ISTA Thesis"],"oa_version":"Published Version","oa":1,"date_updated":"2026-04-15T10:02:13Z","related_material":{"record":[{"id":"2063","relation":"part_of_dissertation","status":"public"},{"id":"1093","status":"public","relation":"part_of_dissertation"},{"status":"public","relation":"part_of_dissertation","id":"1391"},{"id":"1234","relation":"part_of_dissertation","status":"public"},{"id":"1230","relation":"part_of_dissertation","status":"public"},{"status":"public","relation":"part_of_dissertation","id":"1501"},{"relation":"part_of_dissertation","status":"public","id":"1502"},{"id":"2167","relation":"part_of_dissertation","status":"public"}]},"file_date_updated":"2020-07-14T12:44:34Z","status":"public","acknowledgement":" First of all, I want to thank my advisor, prof. Thomas A. Henzinger, for his guidance during my PhD program. I am grateful for the freedom I was given to pursue my research interests, and his continuous support. Working with prof. Henzinger was a truly inspiring experience and taught me what it means to be a scientist. I want to express my gratitude to my collaborators: Nikola Beneš, Krishnendu Chatterjee, Martin Chmelík, Ashutosh Gupta, Willibald Krenn, Jan Kˇretínský, Dejan Nickovic, Andrey Kupriyanov, and Tatjana Petrov. I have learned a great deal from my collaborators, and without their help this thesis would not be possible. In addition, I want to thank the members of my thesis committee: Dirk Beyer, Dejan Nickovic, and Georg Weissenbacher for their advice and reviewing this dissertation. I would especially like to acknowledge the late Helmut Veith, who was a member of my committee. I will remember Helmut for his kindness, enthusiasm, and wit, as well as for being an inspiring scientist. Finally, I would like to thank my colleagues for making my stay at IST such a pleasant experience: Guy Avni, Sergiy Bogomolov, Ventsislav Chonev, Rasmus Ibsen-Jensen, Mirco Giacobbe, Bernhard Kragl, Hui Kong, Petr Novotný, Jan Otop, Andreas Pavlogiannis, Tantjana Petrov, Arjun Radhakrishna, Jakob Ruess, Thorsten Tarrach, as well as other members of groups Henzinger and Chatterjee. ","month":"01","language":[{"iso":"eng"}],"type":"dissertation","abstract":[{"lang":"eng","text":"This dissertation concerns the automatic verification of probabilistic systems and programs with arrays by statistical and logical methods. Although statistical and logical methods are different in nature, we show that they can be successfully combined for system analysis. In the first part of the dissertation we present a new statistical algorithm for the verification of probabilistic systems with respect to unbounded properties, including linear temporal logic. Our algorithm often performs faster than the previous approaches, and at the same time requires less information about the system. In addition, our method can be generalized to unbounded quantitative properties such as mean-payoff bounds. In the second part, we introduce two techniques for comparing probabilistic systems. Probabilistic systems are typically compared using the notion of equivalence, which requires the systems to have the equal probability of all behaviors. However, this notion is often too strict, since probabilities are typically only empirically estimated, and any imprecision may break the relation between processes. On the one hand, we propose to replace the Boolean notion of equivalence by a quantitative distance of similarity. For this purpose, we introduce a statistical framework for estimating distances between Markov chains based on their simulation runs, and we investigate which distances can be approximated in our framework. On the other hand, we propose to compare systems with respect to a new qualitative logic, which expresses that behaviors occur with probability one or a positive probability. This qualitative analysis is robust with respect to modeling errors and applicable to many domains. In the last part, we present a new quantifier-free logic for integer arrays, which allows us to express counting. Counting properties are prevalent in array-manipulating programs, however they cannot be expressed in the quantified fragments of the theory of arrays. We present a decision procedure for our logic, and provide several complexity results."}],"publist_id":"6203","_id":"1155","has_accepted_license":"1","OA_place":"publisher","corr_author":"1","article_processing_charge":"No","date_published":"2017-01-02T00:00:00Z","pubrep_id":"730","author":[{"last_name":"Daca","id":"49351290-F248-11E8-B48F-1D18A9856A87","first_name":"Przemyslaw","full_name":"Daca, Przemyslaw"}],"day":"02","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","year":"2017","publication_status":"published","file":[{"date_updated":"2020-07-14T12:44:34Z","creator":"system","file_name":"IST-2017-730-v1+1_Statistical_and_Logical_Methods_for_Property_Checking.pdf","access_level":"open_access","file_id":"4880","relation":"main_file","date_created":"2018-12-12T10:11:26Z","content_type":"application/pdf","checksum":"1406a681cb737508234fde34766be2c2","file_size":1028586}],"title":"Statistical and logical methods for property checking","supervisor":[{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger"}],"department":[{"_id":"ToHe"}],"project":[{"grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Reactive Modeling"},{"name":"Formal methods for the design and analysis of complex systems","call_identifier":"FWF","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425"},{"grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering"}],"degree_awarded":"PhD","doi":"10.15479/AT:ISTA:TH_730"},{"date_published":"2017-02-01T00:00:00Z","day":"01","author":[{"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","first_name":"Jan","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","last_name":"Otop"}],"article_processing_charge":"No","publication_status":"published","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","year":"2017","title":"Model measuring for discrete and hybrid systems","department":[{"_id":"ToHe"}],"doi":"10.1016/j.nahs.2016.09.001","project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","call_identifier":"FP7","name":"Quantitative Reactive Modeling"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","call_identifier":"FWF","name":"Rigorous Systems Engineering"},{"call_identifier":"FWF","name":"Formal methods for the design and analysis of complex systems","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211"}],"quality_controlled":"1","publisher":"Elsevier","publication":"Nonlinear Analysis: Hybrid Systems","date_created":"2018-12-11T11:50:39Z","intvolume":"        23","citation":{"ieee":"T. A. Henzinger and J. Otop, “Model measuring for discrete and hybrid systems,” <i>Nonlinear Analysis: Hybrid Systems</i>, vol. 23. Elsevier, pp. 166–190, 2017.","ama":"Henzinger TA, Otop J. Model measuring for discrete and hybrid systems. <i>Nonlinear Analysis: Hybrid Systems</i>. 2017;23:166-190. doi:<a href=\"https://doi.org/10.1016/j.nahs.2016.09.001\">10.1016/j.nahs.2016.09.001</a>","ista":"Henzinger TA, Otop J. 2017. Model measuring for discrete and hybrid systems. Nonlinear Analysis: Hybrid Systems. 23, 166–190.","chicago":"Henzinger, Thomas A, and Jan Otop. “Model Measuring for Discrete and Hybrid Systems.” <i>Nonlinear Analysis: Hybrid Systems</i>. Elsevier, 2017. <a href=\"https://doi.org/10.1016/j.nahs.2016.09.001\">https://doi.org/10.1016/j.nahs.2016.09.001</a>.","apa":"Henzinger, T. A., &#38; Otop, J. (2017). Model measuring for discrete and hybrid systems. <i>Nonlinear Analysis: Hybrid Systems</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.nahs.2016.09.001\">https://doi.org/10.1016/j.nahs.2016.09.001</a>","short":"T.A. Henzinger, J. Otop, Nonlinear Analysis: Hybrid Systems 23 (2017) 166–190.","mla":"Henzinger, Thomas A., and Jan Otop. “Model Measuring for Discrete and Hybrid Systems.” <i>Nonlinear Analysis: Hybrid Systems</i>, vol. 23, Elsevier, 2017, pp. 166–90, doi:<a href=\"https://doi.org/10.1016/j.nahs.2016.09.001\">10.1016/j.nahs.2016.09.001</a>."},"page":"166 - 190","ec_funded":1,"volume":23,"date_updated":"2025-04-15T06:25:59Z","oa_version":"None","acknowledgement":"This research was supported in part by the European Research Council (ERC) under grant 267989 (QUAREM), by the Austrian Science Fund1 (FWF) under grants S11402-N23 (RiSE) and Z211-N23 (Wittgenstein Award), and by the National Science Centre (NCN), Poland under grant 2014/15/D/ST6/04543.\r\nA Technical Report of this article is available via: https://repository.ist.ac.at/171/","status":"public","scopus_import":"1","type":"journal_article","_id":"1196","publist_id":"6154","abstract":[{"text":"We define the . model-measuring problem: given a model . M and specification . ϕ, what is the maximal distance . ρ such that all models . M' within distance . ρ from . M satisfy (or violate) . ϕ. The model-measuring problem presupposes a distance function on models. We concentrate on . automatic distance functions, which are defined by weighted automata. The model-measuring problem subsumes several generalizations of the classical model-checking problem, in particular, quantitative model-checking problems that measure the degree of satisfaction of a specification; robustness problems that measure how much a model can be perturbed without violating the specification; and parameter synthesis for hybrid systems. We show that for automatic distance functions, and (a) . ω-regular linear-time, (b) . ω-regular branching-time, and (c) hybrid specifications, the model-measuring problem can be solved.We use automata-theoretic model-checking methods for model measuring, replacing the emptiness question for word, tree, and hybrid automata by the . optimal-value question for the weighted versions of these automata. For automata over words and trees, we consider weighted automata that accumulate weights by maximizing, summing, discounting, and limit averaging. For hybrid automata, we consider monotonic (parametric) hybrid automata, a hybrid counterpart of (discrete) weighted automata.We give several examples of using the model-measuring problem to compute various notions of robustness and quantitative satisfaction for temporal specifications. Further, we propose the modeling framework for model measuring to ease the specification and reduce the likelihood of errors in modeling.Finally, we present a variant of the model-measuring problem, called the . model-repair problem. The model-repair problem applies to models that do not satisfy the specification; it can be used to derive restrictions, under which the model satisfies the specification, i.e., to repair the model.","lang":"eng"}],"month":"02","external_id":{"isi":["000390637000011"]},"language":[{"iso":"eng"}],"isi":1},{"department":[{"_id":"ToHe"}],"title":"From non-preemptive to preemptive scheduling using synchronization synthesis","file":[{"file_name":"IST-2016-656-v1+1_s10703-016-0256-5.pdf","access_level":"open_access","file_id":"4985","creator":"system","date_updated":"2020-07-14T12:44:44Z","file_size":1416170,"content_type":"application/pdf","checksum":"1163dfd997e8212c789525d4178b1653","relation":"main_file","date_created":"2018-12-12T10:13:05Z"}],"quality_controlled":"1","project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","name":"Quantitative Reactive Modeling","call_identifier":"FP7"},{"name":"Rigorous Systems Engineering","call_identifier":"FWF","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"name":"Formal methods for the design and analysis of complex systems","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211"},{"_id":"B67AFEDC-15C9-11EA-A837-991A96BB2854","name":"IST Austria Open Access Fund"}],"doi":"10.1007/s10703-016-0256-5","pubrep_id":"656","author":[{"id":"4DCBEFFE-F248-11E8-B48F-1D18A9856A87","last_name":"Cerny","full_name":"Cerny, Pavol","first_name":"Pavol"},{"last_name":"Clarke","full_name":"Clarke, Edmund","first_name":"Edmund"},{"first_name":"Thomas A","full_name":"Henzinger, Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"},{"last_name":"Radhakrishna","id":"3B51CAC4-F248-11E8-B48F-1D18A9856A87","first_name":"Arjun","full_name":"Radhakrishna, Arjun"},{"first_name":"Leonid","full_name":"Ryzhyk, Leonid","last_name":"Ryzhyk"},{"last_name":"Samanta","id":"3D2AAC08-F248-11E8-B48F-1D18A9856A87","first_name":"Roopsha","full_name":"Samanta, Roopsha"},{"orcid":"0000-0003-4409-8487","id":"3D6E8F2C-F248-11E8-B48F-1D18A9856A87","last_name":"Tarrach","full_name":"Tarrach, Thorsten","first_name":"Thorsten"}],"day":"01","date_published":"2017-06-01T00:00:00Z","tmp":{"image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"corr_author":"1","article_processing_charge":"No","publication_status":"published","year":"2017","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","status":"public","pmid":1,"file_date_updated":"2020-07-14T12:44:44Z","scopus_import":"1","issue":"2-3","publist_id":"5929","abstract":[{"lang":"eng","text":"We present a computer-aided programming approach to concurrency. The approach allows programmers to program assuming a friendly, non-preemptive scheduler, and our synthesis procedure inserts synchronization to ensure that the final program works even with a preemptive scheduler. The correctness specification is implicit, inferred from the non-preemptive behavior. Let us consider sequences of calls that the program makes to an external interface. The 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 guarantee that our synthesis does not introduce deadlocks and that the synchronization inserted is optimal w.r.t. a given objective function. The solution is based on a finitary abstraction, an algorithm for bounded language inclusion modulo an independence relation, and generation of a set of global constraints over synchronization placements. Each model of the global constraints set corresponds to a correctness-ensuring synchronization placement. The placement that is optimal w.r.t. the given objective function is chosen as the synchronization solution. We apply the approach to device-driver programming, where the driver threads call the software interface of the device and the API provided by the operating system. Our experiments demonstrate that our synthesis method is precise and efficient. The implicit specification helped us find one concurrency bug previously missed when model-checking using an explicit, user-provided specification. We implemented objective functions for coarse-grained and fine-grained locking and observed that different synchronization placements are produced for our experiments, favoring a minimal number of synchronization operations or maximum concurrency, respectively."}],"has_accepted_license":"1","_id":"1338","type":"journal_article","external_id":{"pmid":["28490835"],"isi":["000399888900001"]},"isi":1,"language":[{"iso":"eng"}],"month":"06","page":"97 - 139","ec_funded":1,"citation":{"short":"P. Cerny, E. Clarke, T.A. Henzinger, A. Radhakrishna, L. Ryzhyk, R. Samanta, T. Tarrach, Formal Methods in System Design 50 (2017) 97–139.","mla":"Cerny, Pavol, et al. “From Non-Preemptive to Preemptive Scheduling Using Synchronization Synthesis.” <i>Formal Methods in System Design</i>, vol. 50, no. 2–3, Springer, 2017, pp. 97–139, doi:<a href=\"https://doi.org/10.1007/s10703-016-0256-5\">10.1007/s10703-016-0256-5</a>.","ieee":"P. Cerny <i>et al.</i>, “From non-preemptive to preemptive scheduling using synchronization synthesis,” <i>Formal Methods in System Design</i>, vol. 50, no. 2–3. Springer, pp. 97–139, 2017.","ama":"Cerny P, Clarke E, Henzinger TA, et al. From non-preemptive to preemptive scheduling using synchronization synthesis. <i>Formal Methods in System Design</i>. 2017;50(2-3):97-139. doi:<a href=\"https://doi.org/10.1007/s10703-016-0256-5\">10.1007/s10703-016-0256-5</a>","ista":"Cerny P, Clarke E, Henzinger TA, Radhakrishna A, Ryzhyk L, Samanta R, Tarrach T. 2017. From non-preemptive to preemptive scheduling using synchronization synthesis. Formal Methods in System Design. 50(2–3), 97–139.","apa":"Cerny, P., Clarke, E., Henzinger, T. A., Radhakrishna, A., Ryzhyk, L., Samanta, R., &#38; Tarrach, T. (2017). From non-preemptive to preemptive scheduling using synchronization synthesis. <i>Formal Methods in System Design</i>. Springer. <a href=\"https://doi.org/10.1007/s10703-016-0256-5\">https://doi.org/10.1007/s10703-016-0256-5</a>","chicago":"Cerny, Pavol, Edmund Clarke, Thomas A Henzinger, Arjun Radhakrishna, Leonid Ryzhyk, Roopsha Samanta, and Thorsten Tarrach. “From Non-Preemptive to Preemptive Scheduling Using Synchronization Synthesis.” <i>Formal Methods in System Design</i>. Springer, 2017. <a href=\"https://doi.org/10.1007/s10703-016-0256-5\">https://doi.org/10.1007/s10703-016-0256-5</a>."},"ddc":["000"],"date_created":"2018-12-11T11:51:27Z","intvolume":"        50","publisher":"Springer","publication":"Formal Methods in System Design","volume":50,"oa":1,"date_updated":"2025-09-23T08:54:01Z","related_material":{"record":[{"relation":"earlier_version","status":"public","id":"1729"}]},"oa_version":"Published Version"},{"quality_controlled":"1","doi":"10.1007/s00236-016-0278-x","project":[{"grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling","call_identifier":"FP7"},{"name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","name":"Formal methods for the design and analysis of complex systems","call_identifier":"FWF"},{"name":"Speed of Adaptation in Population Genetics and Evolutionary Computation","call_identifier":"FP7","_id":"25B1EC9E-B435-11E9-9278-68D0E5697425","grant_number":"618091"},{"grant_number":"291734","_id":"25681D80-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"International IST Postdoc Fellowship Programme"},{"name":"Limits to selection in biology and in evolutionary computation","call_identifier":"FP7","_id":"25B07788-B435-11E9-9278-68D0E5697425","grant_number":"250152"}],"title":"Model checking the evolution of gene regulatory networks","department":[{"_id":"ToHe"},{"_id":"CaGu"},{"_id":"NiBa"}],"file":[{"file_size":755241,"content_type":"application/pdf","checksum":"4e661d9135d7f8c342e8e258dee76f3e","relation":"main_file","date_created":"2019-01-17T15:57:29Z","file_name":"2017_ActaInformatica_Giacobbe.pdf","access_level":"open_access","file_id":"5841","creator":"dernst","date_updated":"2020-07-14T12:44:46Z"}],"publication_status":"published","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","year":"2017","date_published":"2017-12-01T00:00:00Z","tmp":{"image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"pubrep_id":"649","author":[{"orcid":"0000-0001-8180-0904","id":"3444EA5E-F248-11E8-B48F-1D18A9856A87","last_name":"Giacobbe","full_name":"Giacobbe, Mirco","first_name":"Mirco"},{"id":"47F8433E-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-6220-2052","last_name":"Guet","full_name":"Guet, Calin C","first_name":"Calin C"},{"last_name":"Gupta","id":"335E5684-F248-11E8-B48F-1D18A9856A87","first_name":"Ashutosh","full_name":"Gupta, Ashutosh"},{"last_name":"Henzinger","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","full_name":"Henzinger, Thomas A"},{"first_name":"Tiago","full_name":"Paixao, Tiago","last_name":"Paixao","orcid":"0000-0003-2361-3953","id":"2C5658E6-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000-0002-9041-0905","id":"3D5811FC-F248-11E8-B48F-1D18A9856A87","last_name":"Petrov","full_name":"Petrov, Tatjana","first_name":"Tatjana"}],"day":"01","corr_author":"1","article_processing_charge":"No","type":"journal_article","abstract":[{"text":"The behaviour of gene regulatory networks (GRNs) is typically analysed using simulation-based statistical testing-like methods. In this paper, we demonstrate that we can replace this approach by a formal verification-like method that gives higher assurance and scalability. We focus on Wagner’s weighted GRN model with varying weights, which is used in evolutionary biology. In the model, weight parameters represent the gene interaction strength that may change due to genetic mutations. For a property of interest, we synthesise the constraints over the parameter space that represent the set of GRNs satisfying the property. We experimentally show that our parameter synthesis procedure computes the mutational robustness of GRNs—an important problem of interest in evolutionary biology—more efficiently than the classical simulation method. We specify the property in linear temporal logic. We employ symbolic bounded model checking and SMT solving to compute the space of GRNs that satisfy the property, which amounts to synthesizing a set of linear constraints on the weights.","lang":"eng"}],"publist_id":"5898","_id":"1351","has_accepted_license":"1","month":"12","isi":1,"external_id":{"isi":["000414343200003"]},"language":[{"iso":"eng"}],"status":"public","issue":"8","file_date_updated":"2020-07-14T12:44:46Z","scopus_import":"1","date_updated":"2025-07-10T11:50:42Z","oa":1,"related_material":{"record":[{"status":"public","relation":"earlier_version","id":"1835"}]},"oa_version":"Published Version","ddc":["006","576"],"citation":{"short":"M. Giacobbe, C.C. Guet, A. Gupta, T.A. Henzinger, T. Paixao, T. Petrov, Acta Informatica 54 (2017) 765–787.","mla":"Giacobbe, Mirco, et al. “Model Checking the Evolution of Gene Regulatory Networks.” <i>Acta Informatica</i>, vol. 54, no. 8, Springer, 2017, pp. 765–87, doi:<a href=\"https://doi.org/10.1007/s00236-016-0278-x\">10.1007/s00236-016-0278-x</a>.","ama":"Giacobbe M, Guet CC, Gupta A, Henzinger TA, Paixao T, Petrov T. Model checking the evolution of gene regulatory networks. <i>Acta Informatica</i>. 2017;54(8):765-787. doi:<a href=\"https://doi.org/10.1007/s00236-016-0278-x\">10.1007/s00236-016-0278-x</a>","ieee":"M. Giacobbe, C. C. Guet, A. Gupta, T. A. Henzinger, T. Paixao, and T. Petrov, “Model checking the evolution of gene regulatory networks,” <i>Acta Informatica</i>, vol. 54, no. 8. Springer, pp. 765–787, 2017.","ista":"Giacobbe M, Guet CC, Gupta A, Henzinger TA, Paixao T, Petrov T. 2017. Model checking the evolution of gene regulatory networks. Acta Informatica. 54(8), 765–787.","chicago":"Giacobbe, Mirco, Calin C Guet, Ashutosh Gupta, Thomas A Henzinger, Tiago Paixao, and Tatjana Petrov. “Model Checking the Evolution of Gene Regulatory Networks.” <i>Acta Informatica</i>. Springer, 2017. <a href=\"https://doi.org/10.1007/s00236-016-0278-x\">https://doi.org/10.1007/s00236-016-0278-x</a>.","apa":"Giacobbe, M., Guet, C. C., Gupta, A., Henzinger, T. A., Paixao, T., &#38; Petrov, T. (2017). Model checking the evolution of gene regulatory networks. <i>Acta Informatica</i>. Springer. <a href=\"https://doi.org/10.1007/s00236-016-0278-x\">https://doi.org/10.1007/s00236-016-0278-x</a>"},"intvolume":"        54","date_created":"2018-12-11T11:51:32Z","publisher":"Springer","publication":"Acta Informatica","ec_funded":1,"page":"765 - 787","publication_identifier":{"issn":["0001-5903"]},"volume":54},{"page":"230 - 253","ec_funded":1,"publication":"Nonlinear Analysis: Hybrid Systems","publisher":"Elsevier","date_created":"2018-12-11T11:51:50Z","citation":{"apa":"Svoreňová, M., Kretinsky, J., Chmelik, M., Chatterjee, K., Cěrná, I., &#38; Belta, C. (2017). Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games. <i>Nonlinear Analysis: Hybrid Systems</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.nahs.2016.04.006\">https://doi.org/10.1016/j.nahs.2016.04.006</a>","chicago":"Svoreňová, Mária, Jan Kretinsky, Martin Chmelik, Krishnendu Chatterjee, Ivana Cěrná, and Cǎlin Belta. “Temporal Logic Control for Stochastic Linear Systems Using Abstraction Refinement of Probabilistic Games.” <i>Nonlinear Analysis: Hybrid Systems</i>. Elsevier, 2017. <a href=\"https://doi.org/10.1016/j.nahs.2016.04.006\">https://doi.org/10.1016/j.nahs.2016.04.006</a>.","ista":"Svoreňová M, Kretinsky J, Chmelik M, Chatterjee K, Cěrná I, Belta C. 2017. Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games. Nonlinear Analysis: Hybrid Systems. 23(2), 230–253.","ieee":"M. Svoreňová, J. Kretinsky, M. Chmelik, K. Chatterjee, I. Cěrná, and C. Belta, “Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games,” <i>Nonlinear Analysis: Hybrid Systems</i>, vol. 23, no. 2. Elsevier, pp. 230–253, 2017.","ama":"Svoreňová M, Kretinsky J, Chmelik M, Chatterjee K, Cěrná I, Belta C. Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games. <i>Nonlinear Analysis: Hybrid Systems</i>. 2017;23(2):230-253. doi:<a href=\"https://doi.org/10.1016/j.nahs.2016.04.006\">10.1016/j.nahs.2016.04.006</a>","mla":"Svoreňová, Mária, et al. “Temporal Logic Control for Stochastic Linear Systems Using Abstraction Refinement of Probabilistic Games.” <i>Nonlinear Analysis: Hybrid Systems</i>, vol. 23, no. 2, Elsevier, 2017, pp. 230–53, doi:<a href=\"https://doi.org/10.1016/j.nahs.2016.04.006\">10.1016/j.nahs.2016.04.006</a>.","short":"M. Svoreňová, J. Kretinsky, M. Chmelik, K. Chatterjee, I. Cěrná, C. Belta, Nonlinear Analysis: Hybrid Systems 23 (2017) 230–253."},"intvolume":"        23","main_file_link":[{"url":"http://arxiv.org/abs/1410.5387","open_access":"1"}],"volume":23,"related_material":{"record":[{"status":"public","relation":"earlier_version","id":"1689"}]},"date_updated":"2025-06-11T06:33:00Z","oa":1,"oa_version":"Preprint","status":"public","scopus_import":"1","issue":"2","_id":"1407","publist_id":"5800","abstract":[{"lang":"eng","text":"We consider the problem of computing the set of initial states of a dynamical system such that there exists a control strategy to ensure that the trajectories satisfy a temporal logic specification with probability 1 (almost-surely). We focus on discrete-time, stochastic linear dynamics and specifications given as formulas of the Generalized Reactivity(1) fragment of Linear Temporal Logic over linear predicates in the states of the system. We propose a solution based on iterative abstraction-refinement, and turn-based 2-player probabilistic games. While the theoretical guarantee of our algorithm after any finite number of iterations is only a partial solution, we show that if our algorithm terminates, then the result is the set of all satisfying initial states. Moreover, for any (partial) solution our algorithm synthesizes witness control strategies to ensure almost-sure satisfaction of the temporal logic specification. While the proposed algorithm guarantees progress and soundness in every iteration, it is computationally demanding. We offer an alternative, more efficient solution for the reachability properties that decomposes the problem into a series of smaller problems of the same type. All algorithms are demonstrated on an illustrative case study."}],"type":"journal_article","external_id":{"isi":["000390637000014"],"arxiv":["1410.5387"]},"language":[{"iso":"eng"}],"isi":1,"month":"02","day":"01","author":[{"first_name":"Mária","full_name":"Svoreňová, Mária","last_name":"Svoreňová"},{"last_name":"Kretinsky","orcid":"0000-0002-8122-2881","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","first_name":"Jan","full_name":"Kretinsky, Jan"},{"full_name":"Chmelik, Martin","first_name":"Martin","id":"3624234E-F248-11E8-B48F-1D18A9856A87","last_name":"Chmelik"},{"first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"last_name":"Cěrná","first_name":"Ivana","full_name":"Cěrná, Ivana"},{"first_name":"Cǎlin","full_name":"Belta, Cǎlin","last_name":"Belta"}],"date_published":"2017-02-01T00:00:00Z","article_processing_charge":"No","arxiv":1,"publication_status":"published","year":"2017","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"title":"Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games","doi":"10.1016/j.nahs.2016.04.006","project":[{"grant_number":"291734","_id":"25681D80-B435-11E9-9278-68D0E5697425","name":"International IST Postdoc Fellowship Programme","call_identifier":"FP7"},{"call_identifier":"FP7","name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989"},{"grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF"},{"name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF","grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","name":"Game Theory","_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407"}],"quality_controlled":"1"},{"status":"public","scopus_import":"1","issue":"2","_id":"471","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. "}],"publist_id":"7349","type":"journal_article","article_number":"12","external_id":{"arxiv":["1504.05739"],"isi":["000405208400005"]},"language":[{"iso":"eng"}],"isi":1,"month":"05","ec_funded":1,"publication":"ACM Transactions on Computational Logic","publisher":"ACM","date_created":"2018-12-11T11:46:39Z","intvolume":"        18","citation":{"ieee":"P. Daca, T. A. Henzinger, J. Kretinsky, and T. Petrov, “Faster statistical model checking for unbounded temporal properties,” <i>ACM Transactions on Computational Logic</i>, vol. 18, no. 2. ACM, 2017.","ama":"Daca P, Henzinger TA, Kretinsky J, Petrov T. Faster statistical model checking for unbounded temporal properties. <i>ACM Transactions on Computational Logic</i>. 2017;18(2). doi:<a href=\"https://doi.org/10.1145/3060139\">10.1145/3060139</a>","apa":"Daca, P., Henzinger, T. A., Kretinsky, J., &#38; Petrov, T. (2017). Faster statistical model checking for unbounded temporal properties. <i>ACM Transactions on Computational Logic</i>. ACM. <a href=\"https://doi.org/10.1145/3060139\">https://doi.org/10.1145/3060139</a>","chicago":"Daca, Przemyslaw, Thomas A Henzinger, Jan Kretinsky, and Tatjana Petrov. “Faster Statistical Model Checking for Unbounded Temporal Properties.” <i>ACM Transactions on Computational Logic</i>. ACM, 2017. <a href=\"https://doi.org/10.1145/3060139\">https://doi.org/10.1145/3060139</a>.","ista":"Daca P, Henzinger TA, Kretinsky J, Petrov T. 2017. Faster statistical model checking for unbounded temporal properties. ACM Transactions on Computational Logic. 18(2), 12.","short":"P. Daca, T.A. Henzinger, J. Kretinsky, T. Petrov, ACM Transactions on Computational Logic 18 (2017).","mla":"Daca, Przemyslaw, et al. “Faster Statistical Model Checking for Unbounded Temporal Properties.” <i>ACM Transactions on Computational Logic</i>, vol. 18, no. 2, 12, ACM, 2017, doi:<a href=\"https://doi.org/10.1145/3060139\">10.1145/3060139</a>."},"main_file_link":[{"url":"https://arxiv.org/abs/1504.05739","open_access":"1"}],"publication_identifier":{"issn":["1529-3785"]},"volume":18,"related_material":{"record":[{"status":"public","relation":"earlier_version","id":"1234"}]},"date_updated":"2025-09-22T09:21:16Z","oa":1,"oa_version":"Submitted Version","department":[{"_id":"ToHe"}],"title":"Faster statistical model checking for unbounded temporal properties","doi":"10.1145/3060139","project":[{"grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Reactive Modeling"},{"_id":"25F5A88A-B435-11E9-9278-68D0E5697425","grant_number":"S11402-N23","call_identifier":"FWF","name":"Moderne Concurrency Paradigms"},{"grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"Formal methods for the design and analysis of complex systems","call_identifier":"FWF"},{"grant_number":"291734","_id":"25681D80-B435-11E9-9278-68D0E5697425","name":"International IST Postdoc Fellowship Programme","call_identifier":"FP7"}],"quality_controlled":"1","day":"01","author":[{"id":"49351290-F248-11E8-B48F-1D18A9856A87","last_name":"Daca","full_name":"Daca, Przemyslaw","first_name":"Przemyslaw"},{"last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A","full_name":"Henzinger, Thomas A"},{"first_name":"Jan","full_name":"Kretinsky, Jan","last_name":"Kretinsky","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8122-2881"},{"first_name":"Tatjana","full_name":"Petrov, Tatjana","last_name":"Petrov","id":"3D5811FC-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-9041-0905"}],"date_published":"2017-05-01T00:00:00Z","article_processing_charge":"No","arxiv":1,"corr_author":"1","publication_status":"published","year":"2017","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345"}]