[{"department":[{"_id":"ToHe"}],"project":[{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"Formal methods for the design and analysis of complex systems","grant_number":"Z211"}],"has_accepted_license":"1","status":"public","scopus_import":"1","doi":"10.1007/978-3-030-00151-3_13","month":"08","quality_controlled":"1","file":[{"checksum":"436b7574934324cfa7d1d3986fddc65b","creator":"dernst","content_type":"application/pdf","file_name":"2018_LNCS_Bakhirkin.pdf","date_updated":"2020-07-14T12:48:03Z","date_created":"2020-05-14T11:34:34Z","file_id":"7831","access_level":"open_access","relation":"main_file","file_size":374851}],"ddc":["000"],"date_published":"2018-08-26T00:00:00Z","type":"conference","intvolume":"     11022","oa_version":"Submitted Version","language":[{"iso":"eng"}],"external_id":{"isi":["000884993200013"]},"volume":11022,"author":[{"first_name":"Alexey","last_name":"Bakhirkin","full_name":"Bakhirkin, Alexey"},{"orcid":"0000-0001-5199-3143","first_name":"Thomas","id":"40960E6E-F248-11E8-B48F-1D18A9856A87","last_name":"Ferrere","full_name":"Ferrere, Thomas"},{"first_name":"Dejan","last_name":"Nickovic","full_name":"Nickovic, Dejan"},{"last_name":"Maler","full_name":"Maler, Oded","first_name":"Oded"},{"last_name":"Asarin","full_name":"Asarin, Eugene","first_name":"Eugene"}],"title":"Online timed pattern matching using automata","page":"215 - 232","abstract":[{"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.","lang":"eng"}],"alternative_title":["LNCS"],"conference":{"name":"FORMATS: Formal Modeling and Analysis of Timed Systems","location":"Bejing, China","end_date":"2018-09-06","start_date":"2018-09-04"},"_id":"78","year":"2018","publication_identifier":{"isbn":["978-3-030-00150-6"]},"article_processing_charge":"No","day":"26","publication_status":"published","date_updated":"2025-04-15T06:26:03Z","date_created":"2018-12-11T11:44:31Z","publisher":"Springer","isi":1,"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","publist_id":"7976","fulldoi":"https://doi.org/10.1007/978-3-030-00151-3_13","oa":1,"file_date_updated":"2020-07-14T12:48:03Z","citation":{"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>.","short":"A. Bakhirkin, T. Ferrere, D. Nickovic, O. Maler, E. Asarin, in:, Springer, 2018, pp. 215–232.","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.","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>","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>"}},{"date_created":"2018-12-11T11:44:31Z","isi":1,"publisher":"Springer","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","publist_id":"7975","fulldoi":"https://doi.org/10.1007/978-3-319-99154-2_4","oa":1,"citation":{"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.","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>.","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>","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>","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.","short":"S. Arming, E. Bartocci, K. Chatterjee, J.P. Katoen, A. Sokolova, in:, Springer, 2018, pp. 53–70.","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>."},"author":[{"first_name":"Sebastian","last_name":"Arming","full_name":"Arming, Sebastian"},{"first_name":"Ezio","last_name":"Bartocci","full_name":"Bartocci, Ezio"},{"first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu"},{"id":"4524F760-F248-11E8-B48F-1D18A9856A87","first_name":"Joost P","full_name":"Katoen, Joost P","last_name":"Katoen"},{"last_name":"Sokolova","full_name":"Sokolova, Ana","first_name":"Ana"}],"title":"Parameter-independent strategies for pMDPs via POMDPs","page":"53-70","abstract":[{"lang":"eng","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."}],"alternative_title":["LNCS"],"conference":{"name":"QEST: Quantitative Evaluation of Systems","location":"Beijing, China","start_date":"2018-09-04","end_date":"2018-09-07"},"_id":"79","year":"2018","article_processing_charge":"No","day":"15","publication_status":"published","date_updated":"2023-09-13T09:38:28Z","arxiv":1,"month":"08","main_file_link":[{"url":"https://arxiv.org/abs/1806.05126","open_access":"1"}],"quality_controlled":"1","date_published":"2018-08-15T00:00:00Z","type":"conference","intvolume":"     11024","oa_version":"Preprint","language":[{"iso":"eng"}],"volume":11024,"external_id":{"isi":["000548912200004"],"arxiv":["1806.05126"]},"department":[{"_id":"KrCh"},{"_id":"ToHe"}],"status":"public","scopus_import":"1","doi":"10.1007/978-3-319-99154-2_4"},{"month":"08","ddc":["000"],"file":[{"access_level":"open_access","success":1,"file_id":"8638","date_created":"2020-10-09T06:24:21Z","file_size":537219,"relation":"main_file","content_type":"application/pdf","creator":"dernst","checksum":"e5d81c9b50a6bd9d8a2c16953aad7e23","date_updated":"2020-10-09T06:24:21Z","file_name":"2018_LNCS_Elgyuett.pdf"}],"quality_controlled":"1","oa_version":"Submitted Version","intvolume":"     11022","type":"conference","date_published":"2018-08-26T00:00:00Z","volume":11022,"external_id":{"isi":["000884993200004"]},"language":[{"iso":"eng"}],"status":"public","has_accepted_license":"1","project":[{"call_identifier":"FWF","grant_number":"S11402-N23","name":"Moderne Concurrency Paradigms","_id":"25F5A88A-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"Formal methods for the design and analysis of complex systems"}],"department":[{"_id":"ToHe"}],"scopus_import":"1","doi":"10.1007/978-3-030-00151-3_4","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","publisher":"Springer","isi":1,"date_created":"2018-12-11T11:44:31Z","publist_id":"7973","fulldoi":"https://doi.org/10.1007/978-3-030-00151-3_4","citation":{"short":"A. Elgyütt, T. Ferrere, T.A. Henzinger, in:, Springer, 2018, pp. 53–70.","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>.","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>","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>.","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>","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.","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."},"file_date_updated":"2020-10-09T06:24:21Z","oa":1,"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"}],"page":"53 - 70","title":"Monitoring temporal logic with clock variables","author":[{"last_name":"Elgyütt","full_name":"Elgyütt, Adrian","id":"4A2E9DBA-F248-11E8-B48F-1D18A9856A87","first_name":"Adrian"},{"orcid":"0000-0001-5199-3143","id":"40960E6E-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas","full_name":"Ferrere, Thomas","last_name":"Ferrere"},{"full_name":"Henzinger, Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","orcid":"0000−0002−2985−7724"}],"conference":{"start_date":"2018-09-04","end_date":"2018-09-06","location":"Beijing, China","name":"FORMATS: Formal Modeling and Analysis of Timed Systems"},"_id":"81","year":"2018","alternative_title":["LNCS"],"publication_status":"published","day":"26","article_processing_charge":"No","date_updated":"2025-04-15T06:26:03Z"},{"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."}],"page":"143 - 161","author":[{"first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee"},{"last_name":"Henzinger","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A"},{"full_name":"Otop, Jan","last_name":"Otop","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","first_name":"Jan"}],"publication":"Principles of Modeling","title":"Computing average response time","_id":"86","year":"2018","alternative_title":["LNCS"],"ec_funded":1,"publication_status":"published","day":"20","date_updated":"2025-04-15T06:26:15Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publisher":"Springer","date_created":"2018-12-11T11:44:33Z","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.","fulldoi":"https://doi.org/10.1007/978-3-319-95246-8_9","publist_id":"7968","citation":{"ieee":"K. Chatterjee, T. A. Henzinger, and J. Otop, “Computing average response time,” in <i>Principles of Modeling</i>, vol. 10760, M. Lohstroh, P. Derler, and M. Sirjani, Eds. Springer, 2018, pp. 143–161.","ama":"Chatterjee K, Henzinger TA, Otop J. Computing average response time. In: Lohstroh M, Derler P, Sirjani M, eds. <i>Principles of Modeling</i>. Vol 10760. Springer; 2018:143-161. doi:<a href=\"https://doi.org/10.1007/978-3-319-95246-8_9\">10.1007/978-3-319-95246-8_9</a>","mla":"Chatterjee, Krishnendu, et al. “Computing Average Response Time.” <i>Principles of Modeling</i>, edited by Marten Lohstroh et al., vol. 10760, Springer, 2018, pp. 143–61, doi:<a href=\"https://doi.org/10.1007/978-3-319-95246-8_9\">10.1007/978-3-319-95246-8_9</a>.","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.","short":"K. Chatterjee, T.A. Henzinger, J. Otop, in:, M. Lohstroh, P. Derler, M. Sirjani (Eds.), Principles of Modeling, Springer, 2018, pp. 143–161.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. “Computing Average Response Time.” In <i>Principles of Modeling</i>, edited by Marten Lohstroh, Patricia Derler, and Marjan Sirjani, 10760:143–61. Springer, 2018. <a href=\"https://doi.org/10.1007/978-3-319-95246-8_9\">https://doi.org/10.1007/978-3-319-95246-8_9</a>."},"file_date_updated":"2020-07-14T12:48:14Z","oa":1,"has_accepted_license":"1","status":"public","project":[{"name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","call_identifier":"FWF"},{"call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407","name":"Game Theory"},{"grant_number":"Z211","name":"Formal methods for the design and analysis of complex systems","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","name":"Efficient Algorithms for Computer Aided Verification","grant_number":"ICT15-003"}],"department":[{"_id":"KrCh"},{"_id":"ToHe"}],"scopus_import":1,"doi":"10.1007/978-3-319-95246-8_9","editor":[{"first_name":"Marten","last_name":"Lohstroh","full_name":"Lohstroh, Marten"},{"last_name":"Derler","full_name":"Derler, Patricia","first_name":"Patricia"},{"first_name":"Marjan","full_name":"Sirjani, Marjan","last_name":"Sirjani"}],"month":"07","ddc":["000"],"file":[{"date_updated":"2020-07-14T12:48:14Z","file_name":"2018_PrinciplesModeling_Chatterjee.pdf","content_type":"application/pdf","checksum":"9995c6ce6957333baf616fc4f20be597","creator":"dernst","file_size":516307,"relation":"main_file","file_id":"7053","access_level":"open_access","date_created":"2019-11-19T08:22:18Z"}],"quality_controlled":"1","oa_version":"Submitted Version","intvolume":"     10760","date_published":"2018-07-20T00:00:00Z","type":"book_chapter","volume":10760,"language":[{"iso":"eng"}]},{"type":"book","date_published":"2018-06-08T00:00:00Z","edition":"1","oa_version":"None","citation":{"ista":"Clarke EM, Henzinger TA, Veith H, Bloem R. 2018. Handbook of Model Checking 1st ed., Cham: Springer Nature, XLVIII, 1212p.","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>","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>.","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>","ieee":"E. M. Clarke, T. A. Henzinger, H. Veith, and R. Bloem, <i>Handbook of Model Checking</i>, 1st ed. Cham: Springer Nature, 2018.","short":"E.M. Clarke, T.A. Henzinger, H. Veith, R. Bloem, Handbook of Model Checking, 1st ed., Springer Nature, Cham, 2018.","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>."},"language":[{"iso":"eng"}],"date_created":"2018-12-11T12:02:32Z","month":"06","publisher":"Springer Nature","user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","quality_controlled":"1","fulldoi":"https://doi.org/10.1007/978-3-319-10575-8","publist_id":"3340","article_processing_charge":"No","day":"08","publication_status":"published","place":"Cham","scopus_import":"1","doi":"10.1007/978-3-319-10575-8","date_updated":"2021-12-21T10:49:36Z","department":[{"_id":"ToHe"}],"title":"Handbook of Model Checking","author":[{"last_name":"Clarke","full_name":"Clarke, Edmund M.","first_name":"Edmund M."},{"full_name":"Henzinger, Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A"},{"full_name":"Veith, Helmut","last_name":"Veith","first_name":"Helmut"},{"last_name":"Bloem","full_name":"Bloem, Roderick","first_name":"Roderick"}],"page":"XLVIII, 1212","status":"public","abstract":[{"lang":"eng","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."}],"_id":"3300","year":"2018","publication_identifier":{"isbn":["978-3-319-10574-1"],"eisbn":["978-3-319-10575-8"]}},{"language":[{"iso":"eng"}],"external_id":{"isi":["000446651100020"]},"volume":19,"type":"journal_article","date_published":"2018-01-01T00:00:00Z","intvolume":"        19","oa_version":"None","quality_controlled":"1","month":"01","related_material":{"record":[{"relation":"earlier_version","id":"1205","status":"public"}]},"doi":"10.1109/TITS.2017.2778077","scopus_import":"1","department":[{"_id":"ToHe"}],"status":"public","issue":"10","citation":{"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.","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>.","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>","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>","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.","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>.","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."},"fulldoi":"https://doi.org/10.1109/TITS.2017.2778077","publist_id":"7389","date_created":"2018-12-11T11:46:27Z","isi":1,"publisher":"IEEE","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","date_updated":"2025-09-22T09:39:54Z","article_processing_charge":"No","day":"01","publication_status":"published","year":"2018","_id":"434","publication":"IEEE Transactions on Intelligent Transportation Systems","author":[{"last_name":"Jiang","full_name":"Jiang, Yu","first_name":"Yu"},{"first_name":"Han","last_name":"Liu","full_name":"Liu, Han"},{"first_name":"Huobing","full_name":"Song, Huobing","last_name":"Song"},{"full_name":"Kong, Hui","last_name":"Kong","orcid":"0000-0002-3066-6941","id":"3BDE25AA-F248-11E8-B48F-1D18A9856A87","first_name":"Hui"},{"first_name":"Rui","last_name":"Wang","full_name":"Wang, Rui"},{"first_name":"Yong","full_name":"Guan, Yong","last_name":"Guan"},{"last_name":"Sha","full_name":"Sha, Lui","first_name":"Lui"}],"title":"Safety-assured model-driven design of the multifunction vehicle bus controller","page":"3320 - 3333","abstract":[{"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.","lang":"eng"}]},{"scopus_import":"1","doi":"10.1145/3178126.3178132","department":[{"_id":"ToHe"}],"project":[{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF"}],"status":"public","has_accepted_license":"1","type":"conference","date_published":"2018-04-11T00:00:00Z","oa_version":"Submitted Version","language":[{"iso":"eng"}],"external_id":{"isi":["000474781600020"]},"month":"04","quality_controlled":"1","file":[{"relation":"main_file","file_size":5900421,"date_created":"2020-05-14T12:18:29Z","access_level":"open_access","file_id":"7833","file_name":"2018_HSCC_Bakhirkin.pdf","date_updated":"2020-07-14T12:45:17Z","creator":"dernst","checksum":"81eabc96430e84336ea88310ac0a1ad0","content_type":"application/pdf"}],"ddc":["000"],"day":"11","article_processing_charge":"No","publication_status":"published","date_updated":"2025-07-10T11:51:21Z","publication":"Proceedings of the 21st International Conference on Hybrid Systems","author":[{"full_name":"Bakhirkin, Alexey","last_name":"Bakhirkin","first_name":"Alexey"},{"orcid":"0000-0001-5199-3143","first_name":"Thomas","id":"40960E6E-F248-11E8-B48F-1D18A9856A87","last_name":"Ferrere","full_name":"Ferrere, Thomas"},{"full_name":"Maler, Oded","last_name":"Maler","first_name":"Oded"}],"title":"Efficient parametric identification for STL","page":"177 - 186","abstract":[{"lang":"eng","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."}],"alternative_title":["HSCC Proceedings"],"year":"2018","_id":"182","conference":{"start_date":"2018-04-11","end_date":"2018-04-13","location":"Porto, Portugal","name":"HSCC: Hybrid Systems - Computation and Control"},"publication_identifier":{"isbn":["978-1-4503-5642-8 "]},"oa":1,"file_date_updated":"2020-07-14T12:45:17Z","citation":{"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>","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>","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>.","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.","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.","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>.","short":"A. Bakhirkin, T. Ferrere, O. Maler, in:, Proceedings of the 21st International Conference on Hybrid Systems, ACM, 2018, pp. 177–186."},"date_created":"2018-12-11T11:45:04Z","isi":1,"publisher":"ACM","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publist_id":"7739","fulldoi":"https://doi.org/10.1145/3178126.3178132"},{"page":"197 - 206","abstract":[{"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.","lang":"eng"}],"author":[{"first_name":"Ezio","last_name":"Bartocci","full_name":"Bartocci, Ezio"},{"last_name":"Ferrere","full_name":"Ferrere, Thomas","id":"40960E6E-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas","orcid":"0000-0001-5199-3143"},{"full_name":"Manjunath, Niveditha","last_name":"Manjunath","first_name":"Niveditha"},{"last_name":"Nickovic","full_name":"Nickovic, Dejan","first_name":"Dejan"}],"title":"Localizing faults in simulink/stateflow models with STL","alternative_title":["HSCC Proceedings"],"_id":"183","year":"2018","conference":{"name":"HSCC: Hybrid Systems - Computation and Control","location":"Porto, Portugal","end_date":"2018-04-13","start_date":"2018-04-11"},"article_processing_charge":"No","day":"11","publication_status":"published","date_updated":"2025-07-10T11:51:22Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_created":"2018-12-11T11:45:04Z","publisher":"Association for Computing Machinery","isi":1,"fulldoi":"https://doi.org/10.1145/3178126.3178131","publist_id":"7738","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.","citation":{"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>.","short":"E. Bartocci, T. Ferrere, N. Manjunath, D. Nickovic, in:, Association for Computing Machinery, 2018, pp. 197–206.","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.","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>.","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>","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."},"status":"public","department":[{"_id":"ToHe"}],"project":[{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF"}],"scopus_import":"1","doi":"10.1145/3178126.3178131","month":"04","quality_controlled":"1","oa_version":"None","date_published":"2018-04-11T00:00:00Z","type":"conference","language":[{"iso":"eng"}],"external_id":{"isi":["000474781600022"]}},{"corr_author":"1","project":[{"_id":"25F5A88A-B435-11E9-9278-68D0E5697425","grant_number":"S11402-N23","name":"Moderne Concurrency Paradigms","call_identifier":"FWF"},{"name":"Formal methods for the design and analysis of complex systems","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"department":[{"_id":"ToHe"}],"status":"public","has_accepted_license":"1","doi":"10.1007/978-3-662-54580-5_10","scopus_import":"1","quality_controlled":"1","ddc":["000"],"file":[{"content_type":"application/pdf","creator":"system","date_updated":"2018-12-12T10:08:37Z","file_name":"IST-2017-758-v1+1_tacas-cr.pdf","file_id":"4698","access_level":"open_access","date_created":"2018-12-12T10:08:37Z","file_size":321800,"relation":"main_file"}],"month":"03","pubrep_id":"758","volume":10206,"external_id":{"isi":["000440733400010"]},"language":[{"iso":"eng"}],"intvolume":"     10206","date_published":"2017-03-31T00:00:00Z","type":"conference","oa_version":"Submitted Version","_id":"1116","conference":{"start_date":"2017-04-22","end_date":"2017-04-29","location":"Uppsala, Sweden","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems"},"year":"2017","alternative_title":["LNCS"],"publication_identifier":{"issn":["0302-9743"]},"author":[{"first_name":"Guy","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-5588-8287","last_name":"Avni","full_name":"Avni, Guy"},{"full_name":"Goel, Shubham","last_name":"Goel","first_name":"Shubham"},{"orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","full_name":"Henzinger, Thomas A","last_name":"Henzinger"},{"full_name":"Rodríguez Navas, Guillermo","last_name":"Rodríguez Navas","first_name":"Guillermo"}],"title":"Computing scores of forwarding schemes in switched networks with probabilistic faults","abstract":[{"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. ","lang":"eng"}],"page":"169 - 187","date_updated":"2026-04-16T09:56:24Z","publication_status":"published","article_processing_charge":"No","day":"31","publist_id":"6246","fulldoi":"https://doi.org/10.1007/978-3-662-54580-5_10","isi":1,"publisher":"Springer","date_created":"2018-12-11T11:50:14Z","user_id":"ba8df636-2132-11f1-aed0-ed93e2281fdd","oa":1,"citation":{"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.","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>","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>","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>.","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.","short":"G. Avni, S. Goel, T.A. Henzinger, G. Rodríguez Navas, in:, Springer, 2017, pp. 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>."},"file_date_updated":"2018-12-12T10:08:37Z"},{"publication_identifier":{"issn":["2663-337X"]},"year":"2017","_id":"1155","alternative_title":["ISTA Thesis"],"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."}],"page":"163","title":"Statistical and logical methods for property checking","author":[{"first_name":"Przemyslaw","id":"49351290-F248-11E8-B48F-1D18A9856A87","full_name":"Daca, Przemyslaw","last_name":"Daca"}],"date_updated":"2026-04-15T10:02:13Z","supervisor":[{"full_name":"Henzinger, Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","orcid":"0000−0002−2985−7724"}],"ec_funded":1,"publication_status":"published","article_processing_charge":"No","day":"02","fulldoi":"https://doi.org/10.15479/AT:ISTA:TH_730","publist_id":"6203","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. ","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publisher":"Institute of Science and Technology Austria","date_created":"2018-12-11T11:50:27Z","citation":{"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>.","short":"P. Daca, Statistical and Logical Methods for Property Checking, Institute of Science and Technology Austria, 2017.","ista":"Daca P. 2017. Statistical and logical methods for property checking. Institute of Science and Technology Austria.","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>","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."},"file_date_updated":"2020-07-14T12:44:34Z","oa":1,"corr_author":"1","has_accepted_license":"1","status":"public","project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling","grant_number":"267989","call_identifier":"FP7"},{"call_identifier":"FWF","name":"Formal methods for the design and analysis of complex systems","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"}],"OA_place":"publisher","department":[{"_id":"ToHe"}],"doi":"10.15479/AT:ISTA:TH_730","related_material":{"record":[{"status":"public","id":"2063","relation":"part_of_dissertation"},{"status":"public","id":"1093","relation":"part_of_dissertation"},{"status":"public","relation":"part_of_dissertation","id":"1391"},{"status":"public","id":"1234","relation":"part_of_dissertation"},{"id":"1230","relation":"part_of_dissertation","status":"public"},{"relation":"part_of_dissertation","id":"1501","status":"public"},{"relation":"part_of_dissertation","id":"1502","status":"public"},{"relation":"part_of_dissertation","id":"2167","status":"public"}]},"ddc":["004","005"],"file":[{"date_created":"2018-12-12T10:11:26Z","file_id":"4880","access_level":"open_access","relation":"main_file","file_size":1028586,"checksum":"1406a681cb737508234fde34766be2c2","creator":"system","content_type":"application/pdf","file_name":"IST-2017-730-v1+1_Statistical_and_Logical_Methods_for_Property_Checking.pdf","date_updated":"2020-07-14T12:44:34Z"}],"month":"01","language":[{"iso":"eng"}],"pubrep_id":"730","oa_version":"Published Version","degree_awarded":"PhD","type":"dissertation","date_published":"2017-01-02T00:00:00Z"},{"scopus_import":"1","doi":"10.1016/j.nahs.2016.09.001","department":[{"_id":"ToHe"}],"project":[{"call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","name":"Quantitative Reactive Modeling"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","call_identifier":"FWF"},{"grant_number":"Z211","name":"Formal methods for the design and analysis of complex systems","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"status":"public","date_published":"2017-02-01T00:00:00Z","type":"journal_article","intvolume":"        23","oa_version":"None","language":[{"iso":"eng"}],"external_id":{"isi":["000390637000011"]},"volume":23,"month":"02","quality_controlled":"1","day":"01","article_processing_charge":"No","publication_status":"published","ec_funded":1,"date_updated":"2025-04-15T06:25:59Z","author":[{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger"},{"id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","first_name":"Jan","full_name":"Otop, Jan","last_name":"Otop"}],"title":"Model measuring for discrete and hybrid systems","publication":"Nonlinear Analysis: Hybrid Systems","page":"166 - 190","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"}],"_id":"1196","year":"2017","citation":{"short":"T.A. Henzinger, J. Otop, Nonlinear Analysis: Hybrid Systems 23 (2017) 166–190.","chicago":"Henzinger, Thomas A, and Jan Otop. “Model Measuring for Discrete and Hybrid Systems.” <i>Nonlinear Analysis: Hybrid Systems</i>. Elsevier, 2017. <a href=\"https://doi.org/10.1016/j.nahs.2016.09.001\">https://doi.org/10.1016/j.nahs.2016.09.001</a>.","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>","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>","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>.","ista":"Henzinger TA, Otop J. 2017. Model measuring for discrete and hybrid systems. Nonlinear Analysis: Hybrid Systems. 23, 166–190.","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."},"date_created":"2018-12-11T11:50:39Z","publisher":"Elsevier","isi":1,"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","fulldoi":"https://doi.org/10.1016/j.nahs.2016.09.001","publist_id":"6154","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/"},{"pubrep_id":"656","external_id":{"isi":["000399888900001"],"pmid":["28490835"]},"volume":50,"language":[{"iso":"eng"}],"intvolume":"        50","date_published":"2017-06-01T00:00:00Z","type":"journal_article","oa_version":"Published Version","quality_controlled":"1","ddc":["000"],"file":[{"file_id":"4985","access_level":"open_access","date_created":"2018-12-12T10:13:05Z","file_size":1416170,"relation":"main_file","content_type":"application/pdf","checksum":"1163dfd997e8212c789525d4178b1653","creator":"system","date_updated":"2020-07-14T12:44:44Z","file_name":"IST-2016-656-v1+1_s10703-016-0256-5.pdf"}],"month":"06","doi":"10.1007/s10703-016-0256-5","related_material":{"record":[{"relation":"earlier_version","id":"1729","status":"public"}]},"pmid":1,"scopus_import":"1","corr_author":"1","project":[{"call_identifier":"FP7","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling"},{"call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"Formal methods for the design and analysis of complex systems"},{"_id":"B67AFEDC-15C9-11EA-A837-991A96BB2854","name":"IST Austria Open Access Fund"}],"department":[{"_id":"ToHe"}],"status":"public","has_accepted_license":"1","issue":"2-3","oa":1,"citation":{"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>.","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>.","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>","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>","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.","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."},"file_date_updated":"2020-07-14T12:44:44Z","tmp":{"short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"publist_id":"5929","fulldoi":"https://doi.org/10.1007/s10703-016-0256-5","publisher":"Springer","isi":1,"date_created":"2018-12-11T11:51:27Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_updated":"2025-09-23T08:54:01Z","publication_status":"published","article_processing_charge":"No","day":"01","ec_funded":1,"_id":"1338","year":"2017","author":[{"last_name":"Cerny","full_name":"Cerny, Pavol","first_name":"Pavol","id":"4DCBEFFE-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Clarke","full_name":"Clarke, Edmund","first_name":"Edmund"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger"},{"first_name":"Arjun","id":"3B51CAC4-F248-11E8-B48F-1D18A9856A87","full_name":"Radhakrishna, Arjun","last_name":"Radhakrishna"},{"first_name":"Leonid","last_name":"Ryzhyk","full_name":"Ryzhyk, Leonid"},{"first_name":"Roopsha","id":"3D2AAC08-F248-11E8-B48F-1D18A9856A87","full_name":"Samanta, Roopsha","last_name":"Samanta"},{"full_name":"Tarrach, Thorsten","last_name":"Tarrach","orcid":"0000-0003-4409-8487","id":"3D6E8F2C-F248-11E8-B48F-1D18A9856A87","first_name":"Thorsten"}],"title":"From non-preemptive to preemptive scheduling using synchronization synthesis","publication":"Formal Methods in System Design","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."}],"page":"97 - 139"},{"scopus_import":"1","related_material":{"record":[{"status":"public","id":"1835","relation":"earlier_version"}]},"doi":"10.1007/s00236-016-0278-x","department":[{"_id":"ToHe"},{"_id":"CaGu"},{"_id":"NiBa"}],"project":[{"name":"Quantitative Reactive Modeling","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"call_identifier":"FWF","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering"},{"call_identifier":"FWF","name":"Formal methods for the design and analysis of complex systems","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425"},{"name":"Speed of Adaptation in Population Genetics and Evolutionary Computation","grant_number":"618091","_id":"25B1EC9E-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"call_identifier":"FP7","_id":"25681D80-B435-11E9-9278-68D0E5697425","grant_number":"291734","name":"International IST Postdoc Fellowship Programme"},{"call_identifier":"FP7","name":"Limits to selection in biology and in evolutionary computation","grant_number":"250152","_id":"25B07788-B435-11E9-9278-68D0E5697425"}],"has_accepted_license":"1","status":"public","corr_author":"1","type":"journal_article","date_published":"2017-12-01T00:00:00Z","intvolume":"        54","oa_version":"Published Version","pubrep_id":"649","language":[{"iso":"eng"}],"volume":54,"external_id":{"isi":["000414343200003"]},"month":"12","quality_controlled":"1","file":[{"relation":"main_file","file_size":755241,"date_created":"2019-01-17T15:57:29Z","access_level":"open_access","file_id":"5841","file_name":"2017_ActaInformatica_Giacobbe.pdf","date_updated":"2020-07-14T12:44:46Z","creator":"dernst","checksum":"4e661d9135d7f8c342e8e258dee76f3e","content_type":"application/pdf"}],"ddc":["006","576"],"article_processing_charge":"No","day":"01","publication_status":"published","ec_funded":1,"date_updated":"2025-07-10T11:50:42Z","publication":"Acta Informatica","title":"Model checking the evolution of gene regulatory networks","author":[{"orcid":"0000-0001-8180-0904","id":"3444EA5E-F248-11E8-B48F-1D18A9856A87","first_name":"Mirco","last_name":"Giacobbe","full_name":"Giacobbe, Mirco"},{"orcid":"0000-0001-6220-2052","first_name":"Calin C","id":"47F8433E-F248-11E8-B48F-1D18A9856A87","full_name":"Guet, Calin C","last_name":"Guet"},{"full_name":"Gupta, Ashutosh","last_name":"Gupta","first_name":"Ashutosh","id":"335E5684-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000−0002−2985−7724","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","last_name":"Henzinger"},{"first_name":"Tiago","id":"2C5658E6-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-2361-3953","last_name":"Paixao","full_name":"Paixao, Tiago"},{"last_name":"Petrov","full_name":"Petrov, Tatjana","orcid":"0000-0002-9041-0905","id":"3D5811FC-F248-11E8-B48F-1D18A9856A87","first_name":"Tatjana"}],"page":"765 - 787","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"}],"_id":"1351","year":"2017","publication_identifier":{"issn":["0001-5903"]},"oa":1,"file_date_updated":"2020-07-14T12:44:46Z","citation":{"short":"M. Giacobbe, C.C. Guet, A. Gupta, T.A. Henzinger, T. Paixao, T. Petrov, Acta Informatica 54 (2017) 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>.","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.","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>","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>","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>.","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."},"issue":"8","date_created":"2018-12-11T11:51:32Z","publisher":"Springer","isi":1,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","tmp":{"short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"publist_id":"5898","fulldoi":"https://doi.org/10.1007/s00236-016-0278-x"},{"related_material":{"record":[{"relation":"earlier_version","id":"1689","status":"public"}]},"doi":"10.1016/j.nahs.2016.04.006","scopus_import":"1","status":"public","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"project":[{"call_identifier":"FP7","_id":"25681D80-B435-11E9-9278-68D0E5697425","grant_number":"291734","name":"International IST Postdoc Fellowship Programme"},{"name":"Quantitative Reactive Modeling","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","call_identifier":"FP7"},{"call_identifier":"FWF","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering"},{"name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23","call_identifier":"FWF"},{"call_identifier":"FWF","grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425","name":"Game Theory"}],"language":[{"iso":"eng"}],"external_id":{"isi":["000390637000014"],"arxiv":["1410.5387"]},"volume":23,"oa_version":"Preprint","type":"journal_article","date_published":"2017-02-01T00:00:00Z","intvolume":"        23","quality_controlled":"1","main_file_link":[{"url":"http://arxiv.org/abs/1410.5387","open_access":"1"}],"month":"02","arxiv":1,"date_updated":"2025-06-11T06:33:00Z","ec_funded":1,"day":"01","article_processing_charge":"No","publication_status":"published","year":"2017","_id":"1407","page":"230 - 253","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."}],"author":[{"first_name":"Mária","last_name":"Svoreňová","full_name":"Svoreňová, Mária"},{"last_name":"Kretinsky","full_name":"Kretinsky, Jan","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","first_name":"Jan","orcid":"0000-0002-8122-2881"},{"id":"3624234E-F248-11E8-B48F-1D18A9856A87","first_name":"Martin","full_name":"Chmelik, Martin","last_name":"Chmelik"},{"first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee"},{"last_name":"Cěrná","full_name":"Cěrná, Ivana","first_name":"Ivana"},{"first_name":"Cǎlin","last_name":"Belta","full_name":"Belta, Cǎlin"}],"publication":"Nonlinear Analysis: Hybrid Systems","title":"Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games","issue":"2","citation":{"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>","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>","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>.","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.","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>.","short":"M. Svoreňová, J. Kretinsky, M. Chmelik, K. Chatterjee, I. Cěrná, C. Belta, Nonlinear Analysis: Hybrid Systems 23 (2017) 230–253."},"oa":1,"fulldoi":"https://doi.org/10.1016/j.nahs.2016.04.006","publist_id":"5800","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","date_created":"2018-12-11T11:51:50Z","publisher":"Elsevier","isi":1},{"year":"2017","_id":"471","publication_identifier":{"issn":["1529-3785"]},"title":"Faster statistical model checking for unbounded temporal properties","publication":"ACM Transactions on Computational Logic","author":[{"first_name":"Przemyslaw","id":"49351290-F248-11E8-B48F-1D18A9856A87","full_name":"Daca, Przemyslaw","last_name":"Daca"},{"orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","full_name":"Henzinger, Thomas A","last_name":"Henzinger"},{"orcid":"0000-0002-8122-2881","first_name":"Jan","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","full_name":"Kretinsky, Jan","last_name":"Kretinsky"},{"first_name":"Tatjana","id":"3D5811FC-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-9041-0905","full_name":"Petrov, Tatjana","last_name":"Petrov"}],"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. "}],"date_updated":"2025-09-22T09:21:16Z","arxiv":1,"publication_status":"published","day":"01","article_processing_charge":"No","ec_funded":1,"publist_id":"7349","fulldoi":"https://doi.org/10.1145/3060139","isi":1,"publisher":"ACM","date_created":"2018-12-11T11:46:39Z","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","issue":"2","article_number":"12","oa":1,"citation":{"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>.","short":"P. Daca, T.A. Henzinger, J. Kretinsky, T. Petrov, ACM Transactions on Computational Logic 18 (2017).","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.","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.","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>","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>","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>."},"corr_author":"1","project":[{"call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","name":"Quantitative Reactive Modeling"},{"grant_number":"S11402-N23","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","name":"Moderne Concurrency Paradigms","call_identifier":"FWF"},{"grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"Formal methods for the design and analysis of complex systems","call_identifier":"FWF"},{"call_identifier":"FP7","grant_number":"291734","name":"International IST Postdoc Fellowship Programme","_id":"25681D80-B435-11E9-9278-68D0E5697425"}],"department":[{"_id":"ToHe"}],"status":"public","doi":"10.1145/3060139","related_material":{"record":[{"relation":"earlier_version","id":"1234","status":"public"}]},"scopus_import":"1","quality_controlled":"1","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1504.05739"}],"month":"05","external_id":{"isi":["000405208400005"],"arxiv":["1504.05739"]},"volume":18,"language":[{"iso":"eng"}],"intvolume":"        18","type":"journal_article","date_published":"2017-05-01T00:00:00Z","oa_version":"Submitted Version"},{"scopus_import":"1","doi":"10.4204/EPTCS.259.3","project":[{"grant_number":"S11402-N23","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","name":"Moderne Concurrency Paradigms","call_identifier":"FWF"},{"call_identifier":"FWF","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"Formal methods for the design and analysis of complex systems"}],"department":[{"_id":"ToHe"}],"status":"public","has_accepted_license":"1","corr_author":"1","intvolume":"       259","date_published":"2017-10-10T00:00:00Z","type":"conference","oa_version":"Submitted Version","pubrep_id":"925","external_id":{"isi":["000439358700004"],"arxiv":["1710.03391"]},"volume":259,"language":[{"iso":"eng"}],"month":"10","quality_controlled":"1","main_file_link":[{"url":"https://arxiv.org/abs/1710.03391","open_access":"1"}],"ddc":["004"],"file":[{"content_type":"application/pdf","checksum":"6274f6c0da3376a7b079180d81568518","creator":"system","date_updated":"2020-07-14T12:47:00Z","file_name":"IST-2018-925-v1+1_1710.03391v1.pdf","file_id":"4939","access_level":"open_access","date_created":"2018-12-12T10:12:21Z","file_size":209294,"relation":"main_file"}],"publication_status":"published","day":"10","article_processing_charge":"No","date_updated":"2025-09-18T09:38:35Z","arxiv":1,"title":"Causality-based model checking","publication":"Electronic Proceedings in Theoretical Computer Science","author":[{"full_name":"Finkbeiner, Bernd","last_name":"Finkbeiner","first_name":"Bernd"},{"last_name":"Kupriyanov","full_name":"Kupriyanov, Andrey","first_name":"Andrey","id":"2C311BF8-F248-11E8-B48F-1D18A9856A87"}],"abstract":[{"text":"Model checking is usually based on a comprehensive traversal of the state space. Causality-based model checking is a radically different approach that instead analyzes the cause-effect relationships in a program. We give an overview on a new class of model checking algorithms that capture the causal relationships in a special data structure called concurrent traces. Concurrent traces identify key events in an execution history and link them through their cause-effect relationships. The model checker builds a tableau of concurrent traces, where the case splits represent different causal explanations of a hypothetical error. Causality-based model checking has been implemented in the ARCTOR tool, and applied to previously intractable multi-threaded benchmarks.","lang":"eng"}],"page":"31 - 38","year":"2017","_id":"549","conference":{"end_date":"2017-04-29","start_date":"2017-04-29","name":"CREST: Causal Reasoning for Embedded and Safety-Critical Systems Technologies","location":"Uppsala, Sweden"},"alternative_title":["EPTCS"],"publication_identifier":{"issn":["2075-2180"]},"oa":1,"citation":{"ieee":"B. Finkbeiner and A. Kupriyanov, “Causality-based model checking,” in <i>Electronic Proceedings in Theoretical Computer Science</i>, Uppsala, Sweden, 2017, vol. 259, pp. 31–38.","mla":"Finkbeiner, Bernd, and Andrey Kupriyanov. “Causality-Based Model Checking.” <i>Electronic Proceedings in Theoretical Computer Science</i>, vol. 259, Open Publishing Association, 2017, pp. 31–38, doi:<a href=\"https://doi.org/10.4204/EPTCS.259.3\">10.4204/EPTCS.259.3</a>.","ama":"Finkbeiner B, Kupriyanov A. Causality-based model checking. In: <i>Electronic Proceedings in Theoretical Computer Science</i>. Vol 259. Open Publishing Association; 2017:31-38. doi:<a href=\"https://doi.org/10.4204/EPTCS.259.3\">10.4204/EPTCS.259.3</a>","apa":"Finkbeiner, B., &#38; Kupriyanov, A. (2017). Causality-based model checking. In <i>Electronic Proceedings in Theoretical Computer Science</i> (Vol. 259, pp. 31–38). Uppsala, Sweden: Open Publishing Association. <a href=\"https://doi.org/10.4204/EPTCS.259.3\">https://doi.org/10.4204/EPTCS.259.3</a>","ista":"Finkbeiner B, Kupriyanov A. 2017. Causality-based model checking. Electronic Proceedings in Theoretical Computer Science. CREST: Causal Reasoning for Embedded and Safety-Critical Systems Technologies, EPTCS, vol. 259, 31–38.","short":"B. Finkbeiner, A. Kupriyanov, in:, Electronic Proceedings in Theoretical Computer Science, Open Publishing Association, 2017, pp. 31–38.","chicago":"Finkbeiner, Bernd, and Andrey Kupriyanov. “Causality-Based Model Checking.” In <i>Electronic Proceedings in Theoretical Computer Science</i>, 259:31–38. Open Publishing Association, 2017. <a href=\"https://doi.org/10.4204/EPTCS.259.3\">https://doi.org/10.4204/EPTCS.259.3</a>."},"file_date_updated":"2020-07-14T12:47:00Z","isi":1,"publisher":"Open Publishing Association","date_created":"2018-12-11T11:47:07Z","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","fulldoi":"https://doi.org/10.4204/EPTCS.259.3","publist_id":"7264"},{"date_published":"2017-07-25T00:00:00Z","type":"book_chapter","intvolume":"     10460","oa_version":"Submitted Version","language":[{"iso":"eng"}],"volume":10460,"month":"07","quality_controlled":"1","file":[{"checksum":"b2402766ec02c79801aac634bd8f9f6c","creator":"dernst","content_type":"application/pdf","file_name":"2017_ModelsAlgorithms_Chatterjee.pdf","date_updated":"2020-07-14T12:47:25Z","date_created":"2019-11-19T08:06:50Z","file_id":"7048","access_level":"open_access","relation":"main_file","file_size":192826}],"ddc":["000"],"scopus_import":"1","series_title":"Theoretical Computer Science and General Issues","editor":[{"first_name":"Luca","last_name":"Aceto","full_name":"Aceto, Luca"},{"first_name":"Giorgio","last_name":"Bacci","full_name":"Bacci, Giorgio"},{"full_name":"Ingólfsdóttir, Anna","last_name":"Ingólfsdóttir","first_name":"Anna"},{"last_name":"Legay","full_name":"Legay, Axel","first_name":"Axel"},{"first_name":"Radu","full_name":"Mardare, Radu","last_name":"Mardare"}],"doi":"10.1007/978-3-319-63121-9_18","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"project":[{"call_identifier":"FWF","name":"Moderne Concurrency Paradigms","grant_number":"S11402-N23","_id":"25F5A88A-B435-11E9-9278-68D0E5697425"},{"name":"Game Theory","grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","name":"Formal methods for the design and analysis of complex systems"},{"call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307"},{"grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification","_id":"25892FC0-B435-11E9-9278-68D0E5697425"}],"has_accepted_license":"1","status":"public","oa":1,"file_date_updated":"2020-07-14T12:47:25Z","citation":{"chicago":"Chatterjee, Krishnendu, Laurent Doyen, and Thomas A Henzinger. “The Cost of Exactness in Quantitative Reachability.” In <i>Models, Algorithms, Logics and Tools</i>, edited by Luca Aceto, Giorgio Bacci, Anna Ingólfsdóttir, Axel Legay, and Radu Mardare, 10460:367–81. Theoretical Computer Science and General Issues. Springer, 2017. <a href=\"https://doi.org/10.1007/978-3-319-63121-9_18\">https://doi.org/10.1007/978-3-319-63121-9_18</a>.","short":"K. Chatterjee, L. Doyen, T.A. Henzinger, in:, L. Aceto, G. Bacci, A. Ingólfsdóttir, A. Legay, R. Mardare (Eds.), Models, Algorithms, Logics and Tools, Springer, 2017, pp. 367–381.","ama":"Chatterjee K, Doyen L, Henzinger TA. The cost of exactness in quantitative reachability. In: Aceto L, Bacci G, Ingólfsdóttir A, Legay A, Mardare R, eds. <i>Models, Algorithms, Logics and Tools</i>. Vol 10460. Theoretical Computer Science and General Issues. Springer; 2017:367-381. doi:<a href=\"https://doi.org/10.1007/978-3-319-63121-9_18\">10.1007/978-3-319-63121-9_18</a>","mla":"Chatterjee, Krishnendu, et al. “The Cost of Exactness in Quantitative Reachability.” <i>Models, Algorithms, Logics and Tools</i>, edited by Luca Aceto et al., vol. 10460, Springer, 2017, pp. 367–81, doi:<a href=\"https://doi.org/10.1007/978-3-319-63121-9_18\">10.1007/978-3-319-63121-9_18</a>.","apa":"Chatterjee, K., Doyen, L., &#38; Henzinger, T. A. (2017). The cost of exactness in quantitative reachability. In L. Aceto, G. Bacci, A. Ingólfsdóttir, A. Legay, &#38; R. Mardare (Eds.), <i>Models, Algorithms, Logics and Tools</i> (Vol. 10460, pp. 367–381). Springer. <a href=\"https://doi.org/10.1007/978-3-319-63121-9_18\">https://doi.org/10.1007/978-3-319-63121-9_18</a>","ista":"Chatterjee K, Doyen L, Henzinger TA. 2017.The cost of exactness in quantitative reachability. In: Models, Algorithms, Logics and Tools. LNCS, vol. 10460, 367–381.","ieee":"K. Chatterjee, L. Doyen, and T. A. Henzinger, “The cost of exactness in quantitative reachability,” in <i>Models, Algorithms, Logics and Tools</i>, vol. 10460, L. Aceto, G. Bacci, A. Ingólfsdóttir, A. Legay, and R. Mardare, Eds. Springer, 2017, pp. 367–381."},"date_created":"2018-12-11T11:47:34Z","publisher":"Springer","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","acknowledgement":"This research was supported in part by the Austrian Science Fund (FWF) under grants S11402-N23 and 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.","fulldoi":"https://doi.org/10.1007/978-3-319-63121-9_18","publist_id":"7170","day":"25","article_processing_charge":"No","publication_status":"published","ec_funded":1,"date_updated":"2025-04-15T06:26:15Z","publication":"Models, Algorithms, Logics and Tools","title":"The cost of exactness in quantitative reachability","author":[{"full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Laurent","full_name":"Doyen, Laurent","last_name":"Doyen"},{"full_name":"Henzinger, Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","orcid":"0000−0002−2985−7724"}],"page":"367 - 381","abstract":[{"text":"In the analysis of reactive systems a quantitative objective assigns a real value to every trace of the system. The value decision problem for a quantitative objective requires a trace whose value is at least a given threshold, and the exact value decision problem requires a trace whose value is exactly the threshold. We compare the computational complexity of the value and exact value decision problems for classical quantitative objectives, such as sum, discounted sum, energy, and mean-payoff for two standard models of reactive systems, namely, graphs and graph games.","lang":"eng"}],"alternative_title":["LNCS"],"_id":"625","year":"2017","publication_identifier":{"issn":["0302-9743"],"isbn":["978-3-319-63120-2"]}},{"status":"public","has_accepted_license":"1","project":[{"grant_number":"S11402-N23","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","name":"Moderne Concurrency Paradigms","call_identifier":"FWF"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"Formal methods for the design and analysis of complex systems","grant_number":"Z211"}],"department":[{"_id":"ToHe"}],"corr_author":"1","scopus_import":"1","doi":"10.1007/978-3-662-54577-5_34","related_material":{"record":[{"id":"6894","relation":"dissertation_contains","status":"public"}]},"month":"03","ddc":["000"],"file":[{"checksum":"f395d0d20102b89aeaad8b4ef4f18f4f","creator":"system","content_type":"application/pdf","file_name":"IST-2017-741-v1+1_main.pdf","date_updated":"2020-07-14T12:47:27Z","date_created":"2018-12-12T10:11:41Z","file_id":"4897","access_level":"open_access","relation":"main_file","file_size":569863},{"content_type":"application/pdf","creator":"system","checksum":"f416ee1ae4497b23ecdf28b1f18bb8df","date_updated":"2020-07-14T12:47:27Z","file_name":"IST-2018-741-v2+2_main.pdf","access_level":"open_access","file_id":"4898","date_created":"2018-12-12T10:11:42Z","file_size":563276,"relation":"main_file"}],"quality_controlled":"1","oa_version":"Submitted Version","intvolume":"     10205","type":"conference","date_published":"2017-03-31T00:00:00Z","external_id":{"isi":["000440734900034"]},"volume":10205,"language":[{"iso":"eng"}],"pubrep_id":"966","abstract":[{"text":"Template polyhedra generalize intervals and octagons to polyhedra whose facets are orthogonal to a given set of arbitrary directions. They have been employed in the abstract interpretation of programs and, with particular success, in the reachability analysis of hybrid automata. While previously, the choice of directions has been left to the user or a heuristic, we present a method for the automatic discovery of directions that generalize and eliminate spurious counterexamples. We show that for the class of convex hybrid automata, i.e., hybrid automata with (possibly nonlinear) convex constraints on derivatives, such directions always exist and can be found using convex optimization. We embed our method inside a CEGAR loop, thus enabling the time-unbounded reachability analysis of an important and richer class of hybrid automata than was previously possible. We evaluate our method on several benchmarks, demonstrating also its superior efficiency for the special case of linear hybrid automata.","lang":"eng"}],"page":"589 - 606","author":[{"full_name":"Bogomolov, Sergiy","last_name":"Bogomolov","orcid":"0000-0002-0686-0365","id":"369D9A44-F248-11E8-B48F-1D18A9856A87","first_name":"Sergiy"},{"last_name":"Frehse","full_name":"Frehse, Goran","first_name":"Goran"},{"last_name":"Giacobbe","full_name":"Giacobbe, Mirco","first_name":"Mirco","id":"3444EA5E-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-8180-0904"},{"orcid":"0000−0002−2985−7724","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","full_name":"Henzinger, Thomas A"}],"title":"Counterexample guided refinement of template polyhedra","publication_identifier":{"isbn":["978-366254576-8"]},"conference":{"location":"Uppsala, Sweden","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","end_date":"2017-04-29","start_date":"2017-04-22"},"_id":"631","year":"2017","alternative_title":["LNCS"],"publication_status":"published","article_processing_charge":"No","day":"31","date_updated":"2026-04-08T07:47:13Z","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","publisher":"Springer","isi":1,"date_created":"2018-12-11T11:47:36Z","fulldoi":"https://doi.org/10.1007/978-3-662-54577-5_34","publist_id":"7162","acknowledgement":"This research was supported in part by the Austrian Science Fund (FWF) under grants S11402-N23 (RiSE/SHiNE) and Z211-N23 (Wittgenstein Award), by the European Commission under grant 643921 (UnCoVerCPS), and by the ARC project DP140104219 (Robust AI Planning for Hybrid Systems).","citation":{"short":"S. Bogomolov, G. Frehse, M. Giacobbe, T.A. Henzinger, in:, Springer, 2017, pp. 589–606.","chicago":"Bogomolov, Sergiy, Goran Frehse, Mirco Giacobbe, and Thomas A Henzinger. “Counterexample Guided Refinement of Template Polyhedra,” 10205:589–606. Springer, 2017. <a href=\"https://doi.org/10.1007/978-3-662-54577-5_34\">https://doi.org/10.1007/978-3-662-54577-5_34</a>.","ieee":"S. Bogomolov, G. Frehse, M. Giacobbe, and T. A. Henzinger, “Counterexample guided refinement of template polyhedra,” presented at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems, Uppsala, Sweden, 2017, vol. 10205, pp. 589–606.","apa":"Bogomolov, S., Frehse, G., Giacobbe, M., &#38; Henzinger, T. A. (2017). Counterexample guided refinement of template polyhedra (Vol. 10205, pp. 589–606). 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-54577-5_34\">https://doi.org/10.1007/978-3-662-54577-5_34</a>","ama":"Bogomolov S, Frehse G, Giacobbe M, Henzinger TA. Counterexample guided refinement of template polyhedra. In: Vol 10205. Springer; 2017:589-606. doi:<a href=\"https://doi.org/10.1007/978-3-662-54577-5_34\">10.1007/978-3-662-54577-5_34</a>","mla":"Bogomolov, Sergiy, et al. <i>Counterexample Guided Refinement of Template Polyhedra</i>. Vol. 10205, Springer, 2017, pp. 589–606, doi:<a href=\"https://doi.org/10.1007/978-3-662-54577-5_34\">10.1007/978-3-662-54577-5_34</a>.","ista":"Bogomolov S, Frehse G, Giacobbe M, Henzinger TA. 2017. Counterexample guided refinement of template polyhedra. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 10205, 589–606."},"file_date_updated":"2020-07-14T12:47:27Z","oa":1},{"project":[{"_id":"25F5A88A-B435-11E9-9278-68D0E5697425","grant_number":"S11402-N23","name":"Moderne Concurrency Paradigms","call_identifier":"FWF"},{"grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"Formal methods for the design and analysis of complex systems","call_identifier":"FWF"}],"department":[{"_id":"ToHe"}],"status":"public","doi":"10.1007/978-3-319-63501-9_6","editor":[{"last_name":"Abate","full_name":"Abate, Alessandro","first_name":"Alessandro"},{"full_name":"Bodo, Sylvie","last_name":"Bodo","first_name":"Sylvie"}],"scopus_import":"1","quality_controlled":"1","month":"01","volume":10381,"external_id":{"isi":["000440724800006"]},"language":[{"iso":"eng"}],"intvolume":"     10381","date_published":"2017-01-01T00:00:00Z","type":"conference","oa_version":"None","conference":{"end_date":"2017-07-23","start_date":"2017-07-22","location":"Heidelberg, Germany","name":"NSV: Numerical Software Verification"},"_id":"633","year":"2017","alternative_title":["LNCS"],"publication_identifier":{"isbn":["978-331963500-2"]},"author":[{"full_name":"Bak, Stanley","last_name":"Bak","first_name":"Stanley"},{"id":"369D9A44-F248-11E8-B48F-1D18A9856A87","first_name":"Sergiy","orcid":"0000-0002-0686-0365","last_name":"Bogomolov","full_name":"Bogomolov, Sergiy"},{"full_name":"Henzinger, Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A"},{"full_name":"Kumar, Aviral","last_name":"Kumar","first_name":"Aviral"}],"title":"Challenges and tool implementation of hybrid rapidly exploring random trees","abstract":[{"lang":"eng","text":"A Rapidly-exploring Random Tree (RRT) is an algorithm which can search a non-convex region of space by incrementally building a space-filling tree. The tree is constructed from random points drawn from system’s state space and is biased to grow towards large unexplored areas in the system. RRT can provide better coverage of a system’s possible behaviors compared with random simulations, but is more lightweight than full reachability analysis. In this paper, we explore some of the design decisions encountered while implementing a hybrid extension of the RRT algorithm, which have not been elaborated on before. In particular, we focus on handling non-determinism, which arises due to discrete transitions. We introduce the notion of important points to account for this phenomena. We showcase our ideas using heater and navigation benchmarks."}],"page":"83 - 89","date_updated":"2025-09-11T07:25:57Z","publication_status":"published","day":"01","article_processing_charge":"No","publist_id":"7159","fulldoi":"https://doi.org/10.1007/978-3-319-63501-9_6","publisher":"Springer","isi":1,"date_created":"2018-12-11T11:47:37Z","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","citation":{"ista":"Bak S, Bogomolov S, Henzinger TA, Kumar A. 2017. Challenges and tool implementation of hybrid rapidly exploring random trees. NSV: Numerical Software Verification, LNCS, vol. 10381, 83–89.","ama":"Bak S, Bogomolov S, Henzinger TA, Kumar A. Challenges and tool implementation of hybrid rapidly exploring random trees. In: Abate A, Bodo S, eds. Vol 10381. Springer; 2017:83-89. doi:<a href=\"https://doi.org/10.1007/978-3-319-63501-9_6\">10.1007/978-3-319-63501-9_6</a>","mla":"Bak, Stanley, et al. <i>Challenges and Tool Implementation of Hybrid Rapidly Exploring Random Trees</i>. Edited by Alessandro Abate and Sylvie Bodo, vol. 10381, Springer, 2017, pp. 83–89, doi:<a href=\"https://doi.org/10.1007/978-3-319-63501-9_6\">10.1007/978-3-319-63501-9_6</a>.","apa":"Bak, S., Bogomolov, S., Henzinger, T. A., &#38; Kumar, A. (2017). Challenges and tool implementation of hybrid rapidly exploring random trees. In A. Abate &#38; S. Bodo (Eds.) (Vol. 10381, pp. 83–89). Presented at the NSV: Numerical Software Verification, Heidelberg, Germany: Springer. <a href=\"https://doi.org/10.1007/978-3-319-63501-9_6\">https://doi.org/10.1007/978-3-319-63501-9_6</a>","ieee":"S. Bak, S. Bogomolov, T. A. Henzinger, and A. Kumar, “Challenges and tool implementation of hybrid rapidly exploring random trees,” presented at the NSV: Numerical Software Verification, Heidelberg, Germany, 2017, vol. 10381, pp. 83–89.","short":"S. Bak, S. Bogomolov, T.A. Henzinger, A. Kumar, in:, A. Abate, S. Bodo (Eds.), Springer, 2017, pp. 83–89.","chicago":"Bak, Stanley, Sergiy Bogomolov, Thomas A Henzinger, and Aviral Kumar. “Challenges and Tool Implementation of Hybrid Rapidly Exploring Random Trees.” edited by Alessandro Abate and Sylvie Bodo, 10381:83–89. Springer, 2017. <a href=\"https://doi.org/10.1007/978-3-319-63501-9_6\">https://doi.org/10.1007/978-3-319-63501-9_6</a>."}},{"doi":"10.1007/978-3-319-65765-3_11","editor":[{"full_name":"Abate, Alessandro","last_name":"Abate","first_name":"Alessandro"},{"first_name":"Gilles","full_name":"Geeraerts, Gilles","last_name":"Geeraerts"}],"scopus_import":"1","department":[{"_id":"ToHe"}],"project":[{"call_identifier":"FWF","grant_number":"S11402-N23","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","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"}],"status":"public","language":[{"iso":"eng"}],"volume":10419,"external_id":{"isi":["000611678300011"]},"date_published":"2017-08-03T00:00:00Z","type":"conference","intvolume":"     10419","oa_version":"Submitted Version","quality_controlled":"1","main_file_link":[{"url":"https://hal.archives-ouvertes.fr/hal-01552132","open_access":"1"}],"month":"08","date_updated":"2025-09-11T07:24:11Z","article_processing_charge":"No","day":"03","publication_status":"published","alternative_title":["LNCS"],"year":"2017","_id":"636","conference":{"name":"FORMATS: Formal Modelling and Analysis of Timed Systems","location":"Berlin, Germany","start_date":"2017-09-05","end_date":"2017-09-07"},"publication_identifier":{"isbn":["978-331965764-6"]},"author":[{"full_name":"Bakhirkin, Alexey","last_name":"Bakhirkin","first_name":"Alexey"},{"orcid":"0000-0001-5199-3143","first_name":"Thomas","id":"40960E6E-F248-11E8-B48F-1D18A9856A87","full_name":"Ferrere, Thomas","last_name":"Ferrere"},{"first_name":"Oded","last_name":"Maler","full_name":"Maler, Oded"},{"first_name":"Dogan","last_name":"Ulus","full_name":"Ulus, Dogan"}],"title":"On the quantitative semantics of regular expressions over real-valued signals","page":"189 - 206","abstract":[{"text":"Signal regular expressions can specify sequential properties of real-valued signals based on threshold conditions, regular operations, and duration constraints. In this paper we endow them with a quantitative semantics which indicates how robustly a signal matches or does not match a given expression. First, we show that this semantics is a safe approximation of a distance between the signal and the language defined by the expression. Then, we consider the robust matching problem, that is, computing the quantitative semantics of every segment of a given signal relative to an expression. We present an algorithm that solves this problem for piecewise-constant and piecewise-linear signals and show that for such signals the robustness map is a piecewise-linear function. The availability of an indicator describing how robustly a signal segment matches some regular pattern provides a general framework for quantitative monitoring of cyber-physical systems.","lang":"eng"}],"oa":1,"citation":{"short":"A. Bakhirkin, T. Ferrere, O. Maler, D. Ulus, in:, A. Abate, G. Geeraerts (Eds.), Springer, 2017, pp. 189–206.","chicago":"Bakhirkin, Alexey, Thomas Ferrere, Oded Maler, and Dogan Ulus. “On the Quantitative Semantics of Regular Expressions over Real-Valued Signals.” edited by Alessandro Abate and Gilles Geeraerts, 10419:189–206. Springer, 2017. <a href=\"https://doi.org/10.1007/978-3-319-65765-3_11\">https://doi.org/10.1007/978-3-319-65765-3_11</a>.","ieee":"A. Bakhirkin, T. Ferrere, O. Maler, and D. Ulus, “On the quantitative semantics of regular expressions over real-valued signals,” presented at the FORMATS: Formal Modelling and Analysis of Timed Systems, Berlin, Germany, 2017, vol. 10419, pp. 189–206.","ama":"Bakhirkin A, Ferrere T, Maler O, Ulus D. On the quantitative semantics of regular expressions over real-valued signals. In: Abate A, Geeraerts G, eds. Vol 10419. Springer; 2017:189-206. doi:<a href=\"https://doi.org/10.1007/978-3-319-65765-3_11\">10.1007/978-3-319-65765-3_11</a>","apa":"Bakhirkin, A., Ferrere, T., Maler, O., &#38; Ulus, D. (2017). On the quantitative semantics of regular expressions over real-valued signals. In A. Abate &#38; G. Geeraerts (Eds.) (Vol. 10419, pp. 189–206). Presented at the FORMATS: Formal Modelling and Analysis of Timed Systems, Berlin, Germany: Springer. <a href=\"https://doi.org/10.1007/978-3-319-65765-3_11\">https://doi.org/10.1007/978-3-319-65765-3_11</a>","mla":"Bakhirkin, Alexey, et al. <i>On the Quantitative Semantics of Regular Expressions over Real-Valued Signals</i>. Edited by Alessandro Abate and Gilles Geeraerts, vol. 10419, Springer, 2017, pp. 189–206, doi:<a href=\"https://doi.org/10.1007/978-3-319-65765-3_11\">10.1007/978-3-319-65765-3_11</a>.","ista":"Bakhirkin A, Ferrere T, Maler O, Ulus D. 2017. On the quantitative semantics of regular expressions over real-valued signals. FORMATS: Formal Modelling and Analysis of Timed Systems, LNCS, vol. 10419, 189–206."},"publist_id":"7152","fulldoi":"https://doi.org/10.1007/978-3-319-65765-3_11","date_created":"2018-12-11T11:47:38Z","isi":1,"publisher":"Springer","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345"}]