[{"project":[{"grant_number":"754411","name":"ISTplus - Postdoctoral Fellowships","call_identifier":"H2020","_id":"260C2330-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","name":"The Wittgenstein Prize"},{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"}],"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","citation":{"ista":"Christakis M, Heizmann M, Mansur MN, Schilling C, Wüstholz V. 2019. Semantic fault localization and suspiciousness ranking. 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems . TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 11427, 226–243.","chicago":"Christakis, Maria, Matthias Heizmann, Muhammad Numair Mansur, Christian Schilling, and Valentin Wüstholz. “Semantic Fault Localization and Suspiciousness Ranking.” In 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems , 11427:226–43. Springer Nature, 2019. https://doi.org/10.1007/978-3-030-17462-0_13.","apa":"Christakis, M., Heizmann, M., Mansur, M. N., Schilling, C., & Wüstholz, V. (2019). Semantic fault localization and suspiciousness ranking. In 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (Vol. 11427, pp. 226–243). Prague, Czech Republic: Springer Nature. https://doi.org/10.1007/978-3-030-17462-0_13","ama":"Christakis M, Heizmann M, Mansur MN, Schilling C, Wüstholz V. Semantic fault localization and suspiciousness ranking. In: 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems . Vol 11427. Springer Nature; 2019:226-243. doi:10.1007/978-3-030-17462-0_13","short":"M. Christakis, M. Heizmann, M.N. Mansur, C. Schilling, V. Wüstholz, in:, 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems , Springer Nature, 2019, pp. 226–243.","ieee":"M. Christakis, M. Heizmann, M. N. Mansur, C. Schilling, and V. Wüstholz, “Semantic fault localization and suspiciousness ranking,” in 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems , Prague, Czech Republic, 2019, vol. 11427, pp. 226–243.","mla":"Christakis, Maria, et al. “Semantic Fault Localization and Suspiciousness Ranking.” 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems , vol. 11427, Springer Nature, 2019, pp. 226–43, doi:10.1007/978-3-030-17462-0_13."},"title":"Semantic fault localization and suspiciousness ranking","external_id":{"isi":["000681166500013"]},"article_processing_charge":"No","author":[{"last_name":"Christakis","full_name":"Christakis, Maria","first_name":"Maria"},{"first_name":"Matthias","full_name":"Heizmann, Matthias","last_name":"Heizmann"},{"full_name":"Mansur, Muhammad Numair","last_name":"Mansur","first_name":"Muhammad Numair"},{"full_name":"Schilling, Christian","orcid":"0000-0003-3658-1065","last_name":"Schilling","first_name":"Christian","id":"3A2F4DCE-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Wüstholz, Valentin","last_name":"Wüstholz","first_name":"Valentin"}],"oa":1,"publisher":"Springer Nature","quality_controlled":"1","publication":"25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems ","day":"04","year":"2019","isi":1,"has_accepted_license":"1","date_created":"2019-02-18T16:44:06Z","date_published":"2019-04-04T00:00:00Z","doi":"10.1007/978-3-030-17462-0_13","page":"226-243","_id":"6042","status":"public","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"conference":{"end_date":"2019-04-11","location":"Prague, Czech Republic","start_date":"2019-04-06","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems"},"type":"conference","ddc":["000"],"date_updated":"2023-08-24T14:47:45Z","department":[{"_id":"ToHe"}],"file_date_updated":"2020-07-14T12:47:17Z","oa_version":"Published Version","abstract":[{"text":"Static program analyzers are increasingly effective in checking correctness properties of programs and reporting any errors found, often in the form of error traces. However, developers still spend a significant amount of time on debugging. This involves processing long error traces in an effort to localize a bug to a relatively small part of the program and to identify its cause. In this paper, we present a technique for automated fault localization that, given a program and an error trace, efficiently narrows down the cause of the error to a few statements. These statements are then ranked in terms of their suspiciousness. Our technique relies only on the semantics of the given program and does not require any test cases or user guidance. In experiments on a set of C benchmarks, we show that our technique is effective in quickly isolating the cause of error while out-performing other state-of-the-art fault-localization techniques.","lang":"eng"}],"intvolume":" 11427","month":"04","alternative_title":["LNCS"],"scopus_import":"1","language":[{"iso":"eng"}],"file":[{"content_type":"application/pdf","access_level":"open_access","relation":"main_file","file_id":"6408","checksum":"9998496f6fe202c0a19124b4209154c6","date_updated":"2020-07-14T12:47:17Z","file_size":773083,"creator":"dernst","date_created":"2019-05-10T14:16:05Z","file_name":"2019_LNCS_Christakis.pdf"}],"publication_status":"published","license":"https://creativecommons.org/licenses/by/4.0/","ec_funded":1,"volume":11427},{"type":"conference","conference":{"name":"HSCC: Hybrid Systems Computation and Control","end_date":"2019-04-18","location":"Montreal, QC, Canada","start_date":"2019-04-16"},"status":"public","keyword":["reachability analysis","hybrid systems","lazy computation"],"_id":"6035","department":[{"_id":"ToHe"}],"file_date_updated":"2020-07-14T12:47:17Z","date_updated":"2023-08-24T14:47:21Z","ddc":["000"],"scopus_import":"1","month":"04","intvolume":" 22","abstract":[{"lang":"eng","text":"We present JuliaReach, a toolbox for set-based reachability analysis of dynamical systems. JuliaReach consists of two main packages: Reachability, containing implementations of reachability algorithms for continuous and hybrid systems, and LazySets, a standalone library that implements state-of-the-art algorithms for calculus with convex sets. The library offers both concrete and lazy set representations, where the latter stands for the ability to delay set computations until they are needed. The choice of the programming language Julia and the accompanying documentation of our toolbox allow researchers to easily translate set-based algorithms from mathematics to software in a platform-independent way, while achieving runtime performance that is comparable to statically compiled languages. Combining lazy operations in high dimensions and explicit computations in low dimensions, JuliaReach can be applied to solve complex, large-scale problems."}],"oa_version":"Submitted Version","volume":22,"ec_funded":1,"publication_identifier":{"isbn":["9781450362825"]},"publication_status":"published","file":[{"content_type":"application/pdf","relation":"main_file","access_level":"open_access","checksum":"28ed56439aea5991c3122d4730fd828f","file_id":"6067","file_size":3784414,"date_updated":"2020-07-14T12:47:17Z","creator":"cschilli","file_name":"hscc19.pdf","date_created":"2019-03-05T09:27:18Z"}],"language":[{"iso":"eng"}],"project":[{"name":"The Wittgenstein Prize","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"name":"ISTplus - Postdoctoral Fellowships","grant_number":"754411","_id":"260C2330-B435-11E9-9278-68D0E5697425","call_identifier":"H2020"}],"author":[{"orcid":"0000-0002-0686-0365","full_name":"Bogomolov, Sergiy","last_name":"Bogomolov","first_name":"Sergiy","id":"369D9A44-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Forets, Marcelo","last_name":"Forets","first_name":"Marcelo"},{"first_name":"Goran","last_name":"Frehse","full_name":"Frehse, Goran"},{"first_name":"Kostiantyn","last_name":"Potomkin","full_name":"Potomkin, Kostiantyn"},{"id":"3A2F4DCE-F248-11E8-B48F-1D18A9856A87","first_name":"Christian","orcid":"0000-0003-3658-1065","full_name":"Schilling, Christian","last_name":"Schilling"}],"external_id":{"isi":["000516713900005"],"arxiv":["1901.10736"]},"article_processing_charge":"No","title":"JuliaReach: A toolbox for set-based reachability","citation":{"mla":"Bogomolov, Sergiy, et al. “JuliaReach: A Toolbox for Set-Based Reachability.” Proceedings of the 22nd International Conference on Hybrid Systems: Computation and Control, vol. 22, ACM, 2019, pp. 39–44, doi:10.1145/3302504.3311804.","apa":"Bogomolov, S., Forets, M., Frehse, G., Potomkin, K., & Schilling, C. (2019). JuliaReach: A toolbox for set-based reachability. In Proceedings of the 22nd International Conference on Hybrid Systems: Computation and Control (Vol. 22, pp. 39–44). Montreal, QC, Canada: ACM. https://doi.org/10.1145/3302504.3311804","ama":"Bogomolov S, Forets M, Frehse G, Potomkin K, Schilling C. JuliaReach: A toolbox for set-based reachability. In: Proceedings of the 22nd International Conference on Hybrid Systems: Computation and Control. Vol 22. ACM; 2019:39-44. doi:10.1145/3302504.3311804","ieee":"S. Bogomolov, M. Forets, G. Frehse, K. Potomkin, and C. Schilling, “JuliaReach: A toolbox for set-based reachability,” in Proceedings of the 22nd International Conference on Hybrid Systems: Computation and Control, Montreal, QC, Canada, 2019, vol. 22, pp. 39–44.","short":"S. Bogomolov, M. Forets, G. Frehse, K. Potomkin, C. Schilling, in:, Proceedings of the 22nd International Conference on Hybrid Systems: Computation and Control, ACM, 2019, pp. 39–44.","chicago":"Bogomolov, Sergiy, Marcelo Forets, Goran Frehse, Kostiantyn Potomkin, and Christian Schilling. “JuliaReach: A Toolbox for Set-Based Reachability.” In Proceedings of the 22nd International Conference on Hybrid Systems: Computation and Control, 22:39–44. ACM, 2019. https://doi.org/10.1145/3302504.3311804.","ista":"Bogomolov S, Forets M, Frehse G, Potomkin K, Schilling C. 2019. JuliaReach: A toolbox for set-based reachability. Proceedings of the 22nd International Conference on Hybrid Systems: Computation and Control. HSCC: Hybrid Systems Computation and Control vol. 22, 39–44."},"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","publisher":"ACM","quality_controlled":"1","oa":1,"page":"39-44","doi":"10.1145/3302504.3311804","date_published":"2019-04-16T00:00:00Z","date_created":"2019-02-18T14:43:28Z","has_accepted_license":"1","isi":1,"year":"2019","day":"16","publication":"Proceedings of the 22nd International Conference on Hybrid Systems: Computation and Control"},{"file_date_updated":"2020-10-08T17:25:45Z","department":[{"_id":"ToHe"}],"ddc":["000"],"date_updated":"2023-08-25T10:19:23Z","status":"public","type":"conference","conference":{"name":"HSCC: Hybrid Systems Computation and Control","start_date":"2019-04-16","end_date":"2019-04-18","location":"Montreal, Canada"},"_id":"6428","file":[{"creator":"dernst","date_updated":"2020-10-08T17:25:45Z","file_size":1055421,"date_created":"2020-10-08T17:25:45Z","file_name":"2019_ACM_Ferrere.pdf","access_level":"open_access","relation":"main_file","content_type":"application/pdf","file_id":"8633","checksum":"b8e967081e051d1c55ca5d18fb187890","success":1}],"language":[{"iso":"eng"}],"publication_identifier":{"isbn":["9781450362825"]},"publication_status":"published","month":"04","scopus_import":"1","oa_version":"Submitted Version","abstract":[{"text":"Safety and security are major concerns in the development of Cyber-Physical Systems (CPS). Signal temporal logic (STL) was proposedas a language to specify and monitor the correctness of CPS relativeto formalized requirements. Incorporating STL into a developmentprocess enables designers to automatically monitor and diagnosetraces, compute robustness estimates based on requirements, andperform requirement falsification, leading to productivity gains inverification and validation activities; however, in its current formSTL is agnostic to the input/output classification of signals, andthis negatively impacts the relevance of the analysis results.In this paper we propose to make the interface explicit in theSTL language by introducing input/output signal declarations. Wethen define new measures of input vacuity and output robustnessthat better reflect the nature of the system and the specification in-tent. The resulting framework, which we call interface-aware signaltemporal logic (IA-STL), aids verification and validation activities.We demonstrate the benefits of IA-STL on several CPS analysisactivities: (1) robustness-driven sensitivity analysis, (2) falsificationand (3) fault localization. We describe an implementation of our en-hancement to STL and associated notions of robustness and vacuityin a prototype extension of Breach, a MATLAB®/Simulink®toolboxfor CPS verification and validation. We explore these methodologi-cal improvements and evaluate our results on two examples fromthe automotive domain: a benchmark powertrain control systemand a hydrogen fuel cell system.","lang":"eng"}],"title":"Interface-aware signal temporal logic","author":[{"id":"40960E6E-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas","last_name":"Ferrere","full_name":"Ferrere, Thomas","orcid":"0000-0001-5199-3143"},{"full_name":"Nickovic, Dejan","last_name":"Nickovic","id":"41BCEE5C-F248-11E8-B48F-1D18A9856A87","first_name":"Dejan"},{"first_name":"Alexandre","last_name":"Donzé","full_name":"Donzé, Alexandre"},{"first_name":"Hisahiro","full_name":"Ito, Hisahiro","last_name":"Ito"},{"first_name":"James","full_name":"Kapinski, James","last_name":"Kapinski"}],"external_id":{"isi":["000516713900007"]},"article_processing_charge":"No","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","citation":{"chicago":"Ferrere, Thomas, Dejan Nickovic, Alexandre Donzé, Hisahiro Ito, and James Kapinski. “Interface-Aware Signal Temporal Logic.” In Proceedings of the 2019 22nd ACM International Conference on Hybrid Systems: Computation and Control, 57–66. ACM, 2019. https://doi.org/10.1145/3302504.3311800.","ista":"Ferrere T, Nickovic D, Donzé A, Ito H, Kapinski J. 2019. Interface-aware signal temporal logic. Proceedings of the 2019 22nd ACM International Conference on Hybrid Systems: Computation and Control. HSCC: Hybrid Systems Computation and Control, 57–66.","mla":"Ferrere, Thomas, et al. “Interface-Aware Signal Temporal Logic.” Proceedings of the 2019 22nd ACM International Conference on Hybrid Systems: Computation and Control, ACM, 2019, pp. 57–66, doi:10.1145/3302504.3311800.","apa":"Ferrere, T., Nickovic, D., Donzé, A., Ito, H., & Kapinski, J. (2019). Interface-aware signal temporal logic. In Proceedings of the 2019 22nd ACM International Conference on Hybrid Systems: Computation and Control (pp. 57–66). Montreal, Canada: ACM. https://doi.org/10.1145/3302504.3311800","ama":"Ferrere T, Nickovic D, Donzé A, Ito H, Kapinski J. Interface-aware signal temporal logic. In: Proceedings of the 2019 22nd ACM International Conference on Hybrid Systems: Computation and Control. ACM; 2019:57-66. doi:10.1145/3302504.3311800","ieee":"T. Ferrere, D. Nickovic, A. Donzé, H. Ito, and J. Kapinski, “Interface-aware signal temporal logic,” in Proceedings of the 2019 22nd ACM International Conference on Hybrid Systems: Computation and Control, Montreal, Canada, 2019, pp. 57–66.","short":"T. Ferrere, D. Nickovic, A. Donzé, H. Ito, J. Kapinski, in:, Proceedings of the 2019 22nd ACM International Conference on Hybrid Systems: Computation and Control, ACM, 2019, pp. 57–66."},"project":[{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"grant_number":"Z211","name":"The Wittgenstein Prize","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"date_published":"2019-04-16T00:00:00Z","doi":"10.1145/3302504.3311800","date_created":"2019-05-13T08:13:46Z","page":"57-66","day":"16","publication":"Proceedings of the 2019 22nd ACM International Conference on Hybrid Systems: Computation and Control","isi":1,"has_accepted_license":"1","year":"2019","quality_controlled":"1","publisher":"ACM","oa":1},{"publication_status":"published","publication_identifier":{"issn":["0302-9743"],"isbn":["9783030255398"]},"language":[{"iso":"eng"}],"file":[{"file_size":659766,"date_updated":"2020-07-14T12:47:31Z","creator":"dernst","file_name":"2019_CAV_Avni.pdf","date_created":"2019-08-14T09:35:24Z","content_type":"application/pdf","relation":"main_file","access_level":"open_access","file_id":"6816","checksum":"c231579f2485c6fd4df17c9443a4d80b"}],"volume":11561,"abstract":[{"text":"A controller is a device that interacts with a plant. At each time point,it reads the plant’s state and issues commands with the goal that the plant oper-ates optimally. Constructing optimal controllers is a fundamental and challengingproblem. Machine learning techniques have recently been successfully applied totrain controllers, yet they have limitations. Learned controllers are monolithic andhard to reason about. In particular, it is difficult to add features without retraining,to guarantee any level of performance, and to achieve acceptable performancewhen encountering untrained scenarios. These limitations can be addressed bydeploying quantitative run-timeshieldsthat serve as a proxy for the controller.At each time point, the shield reads the command issued by the controller andmay choose to alter it before passing it on to the plant. We show how optimalshields that interfere as little as possible while guaranteeing a desired level ofcontroller performance, can be generated systematically and automatically usingreactive synthesis. First, we abstract the plant by building a stochastic model.Second, we consider the learned controller to be a black box. Third, we mea-surecontroller performanceandshield interferenceby two quantitative run-timemeasures that are formally defined using weighted automata. Then, the problemof constructing a shield that guarantees maximal performance with minimal inter-ference is the problem of finding an optimal strategy in a stochastic2-player game“controller versus shield” played on the abstract state space of the plant with aquantitative objective obtained from combining the performance and interferencemeasures. We illustrate the effectiveness of our approach by automatically con-structing lightweight shields for learned traffic-light controllers in various roadnetworks. The shields we generate avoid liveness bugs, improve controller per-formance in untrained and changing traffic situations, and add features to learnedcontrollers, such as giving priority to emergency vehicles.","lang":"eng"}],"oa_version":"Published Version","alternative_title":["LNCS"],"scopus_import":"1","intvolume":" 11561","month":"07","date_updated":"2023-08-25T10:33:27Z","ddc":["000"],"file_date_updated":"2020-07-14T12:47:31Z","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"_id":"6462","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"conference":{"name":"CAV: Computer Aided Verification","start_date":"2019-07-13","location":"New York, NY, United States","end_date":"2019-07-18"},"type":"conference","status":"public","year":"2019","has_accepted_license":"1","isi":1,"publication":"31st International Conference on Computer-Aided Verification","day":"12","page":"630-649","date_created":"2019-05-16T11:22:30Z","doi":"10.1007/978-3-030-25540-4_36","date_published":"2019-07-12T00:00:00Z","oa":1,"publisher":"Springer","quality_controlled":"1","citation":{"ista":"Avni G, Bloem R, Chatterjee K, Henzinger TA, Konighofer B, Pranger S. 2019. Run-time optimization for learned controllers through quantitative games. 31st International Conference on Computer-Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 11561, 630–649.","chicago":"Avni, Guy, Roderick Bloem, Krishnendu Chatterjee, Thomas A Henzinger, Bettina Konighofer, and Stefan Pranger. “Run-Time Optimization for Learned Controllers through Quantitative Games.” In 31st International Conference on Computer-Aided Verification, 11561:630–49. Springer, 2019. https://doi.org/10.1007/978-3-030-25540-4_36.","ieee":"G. Avni, R. Bloem, K. Chatterjee, T. A. Henzinger, B. Konighofer, and S. Pranger, “Run-time optimization for learned controllers through quantitative games,” in 31st International Conference on Computer-Aided Verification, New York, NY, United States, 2019, vol. 11561, pp. 630–649.","short":"G. Avni, R. Bloem, K. Chatterjee, T.A. Henzinger, B. Konighofer, S. Pranger, in:, 31st International Conference on Computer-Aided Verification, Springer, 2019, pp. 630–649.","ama":"Avni G, Bloem R, Chatterjee K, Henzinger TA, Konighofer B, Pranger S. Run-time optimization for learned controllers through quantitative games. In: 31st International Conference on Computer-Aided Verification. Vol 11561. Springer; 2019:630-649. doi:10.1007/978-3-030-25540-4_36","apa":"Avni, G., Bloem, R., Chatterjee, K., Henzinger, T. A., Konighofer, B., & Pranger, S. (2019). Run-time optimization for learned controllers through quantitative games. In 31st International Conference on Computer-Aided Verification (Vol. 11561, pp. 630–649). New York, NY, United States: Springer. https://doi.org/10.1007/978-3-030-25540-4_36","mla":"Avni, Guy, et al. “Run-Time Optimization for Learned Controllers through Quantitative Games.” 31st International Conference on Computer-Aided Verification, vol. 11561, Springer, 2019, pp. 630–49, doi:10.1007/978-3-030-25540-4_36."},"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","external_id":{"isi":["000491468000036"]},"article_processing_charge":"No","author":[{"orcid":"0000-0001-5588-8287","full_name":"Avni, Guy","last_name":"Avni","first_name":"Guy","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Roderick","last_name":"Bloem","full_name":"Bloem, Roderick"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee"},{"last_name":"Henzinger","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Bettina","full_name":"Konighofer, Bettina","last_name":"Konighofer"},{"first_name":"Stefan","full_name":"Pranger, Stefan","last_name":"Pranger"}],"title":"Run-time optimization for learned controllers through quantitative games","project":[{"call_identifier":"FWF","_id":"264B3912-B435-11E9-9278-68D0E5697425","name":"Formal Methods meets Algorithmic Game Theory","grant_number":"M02369"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"Z211","name":"The Wittgenstein Prize"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"}]},{"ec_funded":1,"volume":11561,"publication_status":"published","publication_identifier":{"isbn":["9783030255398"],"issn":["0302-9743"]},"language":[{"iso":"eng"}],"file":[{"content_type":"application/pdf","relation":"main_file","access_level":"open_access","file_id":"6817","checksum":"1f1d61b83a151031745ef70a501da3d6","file_size":674795,"date_updated":"2020-07-14T12:47:32Z","creator":"dernst","file_name":"2019_CAV_GarciaSoto.pdf","date_created":"2019-08-14T11:05:30Z"}],"alternative_title":["LNCS"],"scopus_import":"1","intvolume":" 11561","month":"07","abstract":[{"lang":"eng","text":"We present two algorithmic approaches for synthesizing linear hybrid automata from experimental data. Unlike previous approaches, our algorithms work without a template and generate an automaton with nondeterministic guards and invariants, and with an arbitrary number and topology of modes. They thus construct a succinct model from the data and provide formal guarantees. In particular, (1) the generated automaton can reproduce the data up to a specified tolerance and (2) the automaton is tight, given the first guarantee. Our first approach encodes the synthesis problem as a logical formula in the theory of linear arithmetic, which can then be solved by an SMT solver. This approach minimizes the number of modes in the resulting model but is only feasible for limited data sets. To address scalability, we propose a second approach that does not enforce to find a minimal model. The algorithm constructs an initial automaton and then iteratively extends the automaton based on processing new data. Therefore the algorithm is well-suited for online and synthesis-in-the-loop applications. The core of the algorithm is a membership query that checks whether, within the specified tolerance, a given data set can result from the execution of a given automaton. We solve this membership problem for linear hybrid automata by repeated reachability computations. We demonstrate the effectiveness of the algorithm on synthetic data sets and on cardiac-cell measurements."}],"oa_version":"Published Version","file_date_updated":"2020-07-14T12:47:32Z","department":[{"_id":"ToHe"}],"date_updated":"2023-08-25T10:40:41Z","ddc":["000"],"conference":{"location":"New York City, NY, USA","end_date":"2019-07-18","start_date":"2019-07-15","name":"CAV: Computer-Aided Verification"},"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"type":"conference","keyword":["Synthesis","Linear hybrid automaton","Membership"],"status":"public","_id":"6493","page":"297-314","date_created":"2019-05-27T07:09:53Z","date_published":"2019-07-12T00:00:00Z","doi":"10.1007/978-3-030-25540-4_16","year":"2019","isi":1,"has_accepted_license":"1","publication":"31st International Conference on Computer-Aided Verification","day":"12","oa":1,"quality_controlled":"1","publisher":"Springer","article_processing_charge":"No","external_id":{"isi":["000491468000016"]},"author":[{"first_name":"Miriam","id":"4B3207F6-F248-11E8-B48F-1D18A9856A87","full_name":"Garcia Soto, Miriam","orcid":"0000−0003−2936−5719","last_name":"Garcia Soto"},{"last_name":"Henzinger","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A"},{"full_name":"Schilling, Christian","orcid":"0000-0003-3658-1065","last_name":"Schilling","first_name":"Christian","id":"3A2F4DCE-F248-11E8-B48F-1D18A9856A87"},{"id":"3ADCA2E4-F248-11E8-B48F-1D18A9856A87","first_name":"Luka","last_name":"Zeleznik","full_name":"Zeleznik, Luka"}],"title":"Membership-based synthesis of linear hybrid automata","citation":{"mla":"Garcia Soto, Miriam, et al. “Membership-Based Synthesis of Linear Hybrid Automata.” 31st International Conference on Computer-Aided Verification, vol. 11561, Springer, 2019, pp. 297–314, doi:10.1007/978-3-030-25540-4_16.","ama":"Garcia Soto M, Henzinger TA, Schilling C, Zeleznik L. Membership-based synthesis of linear hybrid automata. In: 31st International Conference on Computer-Aided Verification. Vol 11561. Springer; 2019:297-314. doi:10.1007/978-3-030-25540-4_16","apa":"Garcia Soto, M., Henzinger, T. A., Schilling, C., & Zeleznik, L. (2019). Membership-based synthesis of linear hybrid automata. In 31st International Conference on Computer-Aided Verification (Vol. 11561, pp. 297–314). New York City, NY, USA: Springer. https://doi.org/10.1007/978-3-030-25540-4_16","ieee":"M. Garcia Soto, T. A. Henzinger, C. Schilling, and L. Zeleznik, “Membership-based synthesis of linear hybrid automata,” in 31st International Conference on Computer-Aided Verification, New York City, NY, USA, 2019, vol. 11561, pp. 297–314.","short":"M. Garcia Soto, T.A. Henzinger, C. Schilling, L. Zeleznik, in:, 31st International Conference on Computer-Aided Verification, Springer, 2019, pp. 297–314.","chicago":"Garcia Soto, Miriam, Thomas A Henzinger, Christian Schilling, and Luka Zeleznik. “Membership-Based Synthesis of Linear Hybrid Automata.” In 31st International Conference on Computer-Aided Verification, 11561:297–314. Springer, 2019. https://doi.org/10.1007/978-3-030-25540-4_16.","ista":"Garcia Soto M, Henzinger TA, Schilling C, Zeleznik L. 2019. Membership-based synthesis of linear hybrid automata. 31st International Conference on Computer-Aided Verification. CAV: Computer-Aided Verification, LNCS, vol. 11561, 297–314."},"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","project":[{"call_identifier":"H2020","_id":"260C2330-B435-11E9-9278-68D0E5697425","grant_number":"754411","name":"ISTplus - Postdoctoral Fellowships"},{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize","grant_number":"Z211"}]},{"title":"Infinite-duration bidding games","author":[{"last_name":"Avni","orcid":"0000-0001-5588-8287","full_name":"Avni, Guy","first_name":"Guy","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger"},{"first_name":"Ventsislav K","id":"36CBE2E6-F248-11E8-B48F-1D18A9856A87","last_name":"Chonev","full_name":"Chonev, Ventsislav K"}],"external_id":{"isi":["000487714900008"],"arxiv":["1705.01433"]},"article_processing_charge":"No","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","citation":{"mla":"Avni, Guy, et al. “Infinite-Duration Bidding Games.” Journal of the ACM, vol. 66, no. 4, 31, ACM, 2019, doi:10.1145/3340295.","ama":"Avni G, Henzinger TA, Chonev VK. Infinite-duration bidding games. Journal of the ACM. 2019;66(4). doi:10.1145/3340295","apa":"Avni, G., Henzinger, T. A., & Chonev, V. K. (2019). Infinite-duration bidding games. Journal of the ACM. ACM. https://doi.org/10.1145/3340295","short":"G. Avni, T.A. Henzinger, V.K. Chonev, Journal of the ACM 66 (2019).","ieee":"G. Avni, T. A. Henzinger, and V. K. Chonev, “Infinite-duration bidding games,” Journal of the ACM, vol. 66, no. 4. ACM, 2019.","chicago":"Avni, Guy, Thomas A Henzinger, and Ventsislav K Chonev. “Infinite-Duration Bidding Games.” Journal of the ACM. ACM, 2019. https://doi.org/10.1145/3340295.","ista":"Avni G, Henzinger TA, Chonev VK. 2019. Infinite-duration bidding games. Journal of the ACM. 66(4), 31."},"project":[{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize","grant_number":"Z211"},{"name":"Rigorous Systems Engineering","grant_number":"S11402-N23","call_identifier":"FWF","_id":"25F2ACDE-B435-11E9-9278-68D0E5697425"},{"_id":"264B3912-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"M02369","name":"Formal Methods meets Algorithmic Game Theory"}],"article_number":"31","doi":"10.1145/3340295","date_published":"2019-07-16T00:00:00Z","date_created":"2019-08-04T21:59:16Z","day":"16","publication":"Journal of the ACM","isi":1,"year":"2019","quality_controlled":"1","publisher":"ACM","oa":1,"department":[{"_id":"ToHe"}],"date_updated":"2023-08-29T07:02:13Z","status":"public","type":"journal_article","_id":"6752","volume":66,"issue":"4","related_material":{"record":[{"id":"950","status":"public","relation":"earlier_version"}]},"language":[{"iso":"eng"}],"publication_identifier":{"issn":["00045411"],"eissn":["1557735X"]},"publication_status":"published","month":"07","intvolume":" 66","scopus_import":"1","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1705.01433"}],"oa_version":"Preprint","abstract":[{"text":"Two-player games on graphs are widely studied in formal methods, as they model the interaction between a system and its environment. The game is played by moving a token throughout a graph to produce an infinite path. There are several common modes to determine how the players move the token through the graph; e.g., in turn-based games the players alternate turns in moving the token. We study the bidding mode of moving the token, which, to the best of our knowledge, has never been studied in infinite-duration games. The following bidding rule was previously defined and called Richman bidding. Both players have separate budgets, which sum up to 1. In each turn, a bidding takes place: Both players submit bids simultaneously, where a bid is legal if it does not exceed the available budget, and the higher bidder pays his bid to the other player and moves the token. The central question studied in bidding games is a necessary and sufficient initial budget for winning the game: a threshold budget in a vertex is a value t ∈ [0, 1] such that if Player 1’s budget exceeds t, he can win the game; and if Player 2’s budget exceeds 1 − t, he can win the game. Threshold budgets were previously shown to exist in every vertex of a reachability game, which have an interesting connection with random-turn games—a sub-class of simple stochastic games in which the player who moves is chosen randomly. We show the existence of threshold budgets for a qualitative class of infinite-duration games, namely parity games, and a quantitative class, namely mean-payoff games. The key component of the proof is a quantitative solution to strongly connected mean-payoff bidding games in which we extend the connection with random-turn games to these games, and construct explicit optimal strategies for both players.","lang":"eng"}]},{"article_number":"19","project":[{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"name":"The Wittgenstein Prize","grant_number":"Z211","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425"}],"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","citation":{"chicago":"Ferrere, Thomas, Oded Maler, Dejan Ničković, and Amir Pnueli. “From Real-Time Logic to Timed Automata.” Journal of the ACM. ACM, 2019. https://doi.org/10.1145/3286976.","ista":"Ferrere T, Maler O, Ničković D, Pnueli A. 2019. From real-time logic to timed automata. Journal of the ACM. 66(3), 19.","mla":"Ferrere, Thomas, et al. “From Real-Time Logic to Timed Automata.” Journal of the ACM, vol. 66, no. 3, 19, ACM, 2019, doi:10.1145/3286976.","ieee":"T. Ferrere, O. Maler, D. Ničković, and A. Pnueli, “From real-time logic to timed automata,” Journal of the ACM, vol. 66, no. 3. ACM, 2019.","short":"T. Ferrere, O. Maler, D. Ničković, A. Pnueli, Journal of the ACM 66 (2019).","apa":"Ferrere, T., Maler, O., Ničković, D., & Pnueli, A. (2019). From real-time logic to timed automata. Journal of the ACM. ACM. https://doi.org/10.1145/3286976","ama":"Ferrere T, Maler O, Ničković D, Pnueli A. From real-time logic to timed automata. Journal of the ACM. 2019;66(3). doi:10.1145/3286976"},"title":"From real-time logic to timed automata","author":[{"first_name":"Thomas","id":"40960E6E-F248-11E8-B48F-1D18A9856A87","last_name":"Ferrere","orcid":"0000-0001-5199-3143","full_name":"Ferrere, Thomas"},{"first_name":"Oded","last_name":"Maler","full_name":"Maler, Oded"},{"first_name":"Dejan","last_name":"Ničković","full_name":"Ničković, Dejan"},{"full_name":"Pnueli, Amir","last_name":"Pnueli","first_name":"Amir"}],"external_id":{"isi":["000495406300005"]},"article_processing_charge":"No","publisher":"ACM","quality_controlled":"1","day":"01","publication":"Journal of the ACM","isi":1,"year":"2019","date_published":"2019-05-01T00:00:00Z","doi":"10.1145/3286976","date_created":"2019-11-26T10:22:32Z","_id":"7109","status":"public","article_type":"original","type":"journal_article","date_updated":"2023-09-06T11:11:56Z","department":[{"_id":"ToHe"}],"oa_version":"None","abstract":[{"text":"We show how to construct temporal testers for the logic MITL, a prominent linear-time logic for real-time systems. A temporal tester is a transducer that inputs a signal holding the Boolean value of atomic propositions and outputs the truth value of a formula along time. Here we consider testers over continuous-time Boolean signals that use clock variables to enforce duration constraints, as in timed automata. We first rewrite the MITL formula into a “simple” formula using a limited set of temporal modalities. We then build testers for these specific modalities and show how to compose testers for simple formulae into complex ones. Temporal testers can be turned into acceptors, yielding a compositional translation from MITL to timed automata. This construction is much simpler than previously known and remains asymptotically optimal. It supports both past and future operators and can easily be extended.","lang":"eng"}],"month":"05","intvolume":" 66","scopus_import":"1","language":[{"iso":"eng"}],"publication_identifier":{"issn":["0004-5411"]},"publication_status":"published","volume":66,"issue":"3"},{"date_updated":"2023-09-06T11:18:08Z","department":[{"_id":"CaGu"},{"_id":"ToHe"}],"_id":"7147","type":"conference","conference":{"name":"CMSB: Computational Methods in Systems Biology","start_date":"2019-09-18","location":"Trieste, Italy","end_date":"2019-09-20"},"status":"public","publication_identifier":{"isbn":["9783030313036","9783030313043"],"eissn":["1611-3349"],"issn":["0302-9743"]},"publication_status":"published","language":[{"iso":"eng"}],"volume":11773,"abstract":[{"lang":"eng","text":"The expression of a gene is characterised by its transcription factors and the function processing them. If the transcription factors are not affected by gene products, the regulating function is often represented as a combinational logic circuit, where the outputs (product) are determined by current input values (transcription factors) only, and are hence independent on their relative arrival times. However, the simultaneous arrival of transcription factors (TFs) in genetic circuits is a strong assumption, given that the processes of transcription and translation of a gene into a protein introduce intrinsic time delays and that there is no global synchronisation among the arrival times of different molecular species at molecular targets.\r\n\r\nIn this paper, we construct an experimentally implementable genetic circuit with two inputs and a single output, such that, in presence of small delays in input arrival, the circuit exhibits qualitatively distinct observable phenotypes. In particular, these phenotypes are long lived transients: they all converge to a single value, but so slowly, that they seem stable for an extended time period, longer than typical experiment duration. We used rule-based language to prototype our circuit, and we implemented a search for finding the parameter combinations raising the phenotypes of interest.\r\n\r\nThe behaviour of our prototype circuit has wide implications. First, it suggests that GRNs can exploit event timing to create phenotypes. Second, it opens the possibility that GRNs are using event timing to react to stimuli and memorise events, without explicit feedback in regulation. From the modelling perspective, our prototype circuit demonstrates the critical importance of analysing the transient dynamics at the promoter binding sites of the DNA, before applying rapid equilibrium assumptions."}],"oa_version":"None","scopus_import":"1","alternative_title":["LNCS"],"month":"09","intvolume":" 11773","citation":{"chicago":"Guet, Calin C, Thomas A Henzinger, Claudia Igler, Tatjana Petrov, and Ali Sezgin. “Transient Memory in Gene Regulation.” In 17th International Conference on Computational Methods in Systems Biology, 11773:155–87. Springer Nature, 2019. https://doi.org/10.1007/978-3-030-31304-3_9.","ista":"Guet CC, Henzinger TA, Igler C, Petrov T, Sezgin A. 2019. Transient memory in gene regulation. 17th International Conference on Computational Methods in Systems Biology. CMSB: Computational Methods in Systems Biology, LNCS, vol. 11773, 155–187.","mla":"Guet, Calin C., et al. “Transient Memory in Gene Regulation.” 17th International Conference on Computational Methods in Systems Biology, vol. 11773, Springer Nature, 2019, pp. 155–87, doi:10.1007/978-3-030-31304-3_9.","ieee":"C. C. Guet, T. A. Henzinger, C. Igler, T. Petrov, and A. Sezgin, “Transient memory in gene regulation,” in 17th International Conference on Computational Methods in Systems Biology, Trieste, Italy, 2019, vol. 11773, pp. 155–187.","short":"C.C. Guet, T.A. Henzinger, C. Igler, T. Petrov, A. Sezgin, in:, 17th International Conference on Computational Methods in Systems Biology, Springer Nature, 2019, pp. 155–187.","apa":"Guet, C. C., Henzinger, T. A., Igler, C., Petrov, T., & Sezgin, A. (2019). Transient memory in gene regulation. In 17th International Conference on Computational Methods in Systems Biology (Vol. 11773, pp. 155–187). Trieste, Italy: Springer Nature. https://doi.org/10.1007/978-3-030-31304-3_9","ama":"Guet CC, Henzinger TA, Igler C, Petrov T, Sezgin A. Transient memory in gene regulation. In: 17th International Conference on Computational Methods in Systems Biology. Vol 11773. Springer Nature; 2019:155-187. doi:10.1007/978-3-030-31304-3_9"},"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","author":[{"first_name":"Calin C","id":"47F8433E-F248-11E8-B48F-1D18A9856A87","last_name":"Guet","full_name":"Guet, Calin C","orcid":"0000-0001-6220-2052"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A"},{"last_name":"Igler","full_name":"Igler, Claudia","id":"46613666-F248-11E8-B48F-1D18A9856A87","first_name":"Claudia"},{"id":"3D5811FC-F248-11E8-B48F-1D18A9856A87","first_name":"Tatjana","orcid":"0000-0002-9041-0905","full_name":"Petrov, Tatjana","last_name":"Petrov"},{"id":"4C7638DA-F248-11E8-B48F-1D18A9856A87","first_name":"Ali","full_name":"Sezgin, Ali","last_name":"Sezgin"}],"external_id":{"isi":["000557875100009"]},"article_processing_charge":"No","title":"Transient memory in gene regulation","project":[{"grant_number":"Z211","name":"The Wittgenstein Prize","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"name":"Design principles underlying genetic switch architecture","grant_number":"24573","_id":"251EE76E-B435-11E9-9278-68D0E5697425"}],"isi":1,"year":"2019","day":"17","publication":"17th International Conference on Computational Methods in Systems Biology","page":"155-187","doi":"10.1007/978-3-030-31304-3_9","date_published":"2019-09-17T00:00:00Z","date_created":"2019-12-04T16:07:50Z","quality_controlled":"1","publisher":"Springer Nature"},{"language":[{"iso":"eng"}],"publication_identifier":{"isbn":["9783030320782","9783030320799"],"issn":["0302-9743"]},"publication_status":"published","volume":11757,"oa_version":"None","abstract":[{"text":"Cyber-physical systems (CPS) and the Internet-of-Things (IoT) result in a tremendous amount of generated, measured and recorded time-series data. Extracting temporal segments that encode patterns with useful information out of these huge amounts of data is an extremely difficult problem. We propose shape expressions as a declarative formalism for specifying, querying and extracting sophisticated temporal patterns from possibly noisy data. Shape expressions are regular expressions with arbitrary (linear, exponential, sinusoidal, etc.) shapes with parameters as atomic predicates and additional constraints on these parameters. We equip shape expressions with a novel noisy semantics that combines regular expression matching semantics with statistical regression. We characterize essential properties of the formalism and propose an efficient approximate shape expression matching procedure. We demonstrate the wide applicability of this technique on two case studies. ","lang":"eng"}],"month":"10","intvolume":" 11757","alternative_title":["LNCS"],"scopus_import":"1","date_updated":"2023-09-06T11:24:10Z","department":[{"_id":"ToHe"}],"_id":"7159","status":"public","type":"conference","conference":{"location":"Porto, Portugal","end_date":"2019-10-11","start_date":"2019-10-08","name":"RV: Runtime Verification"},"day":"01","publication":"19th International Conference on Runtime Verification","isi":1,"year":"2019","date_published":"2019-10-01T00:00:00Z","doi":"10.1007/978-3-030-32079-9_17","date_created":"2019-12-09T08:47:55Z","page":"292-309","publisher":"Springer Nature","quality_controlled":"1","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","citation":{"ama":"Ničković D, Qin X, Ferrere T, Mateis C, Deshmukh J. Shape expressions for specifying and extracting signal features. In: 19th International Conference on Runtime Verification. Vol 11757. Springer Nature; 2019:292-309. doi:10.1007/978-3-030-32079-9_17","apa":"Ničković, D., Qin, X., Ferrere, T., Mateis, C., & Deshmukh, J. (2019). Shape expressions for specifying and extracting signal features. In 19th International Conference on Runtime Verification (Vol. 11757, pp. 292–309). Porto, Portugal: Springer Nature. https://doi.org/10.1007/978-3-030-32079-9_17","short":"D. Ničković, X. Qin, T. Ferrere, C. Mateis, J. Deshmukh, in:, 19th International Conference on Runtime Verification, Springer Nature, 2019, pp. 292–309.","ieee":"D. Ničković, X. Qin, T. Ferrere, C. Mateis, and J. Deshmukh, “Shape expressions for specifying and extracting signal features,” in 19th International Conference on Runtime Verification, Porto, Portugal, 2019, vol. 11757, pp. 292–309.","mla":"Ničković, Dejan, et al. “Shape Expressions for Specifying and Extracting Signal Features.” 19th International Conference on Runtime Verification, vol. 11757, Springer Nature, 2019, pp. 292–309, doi:10.1007/978-3-030-32079-9_17.","ista":"Ničković D, Qin X, Ferrere T, Mateis C, Deshmukh J. 2019. Shape expressions for specifying and extracting signal features. 19th International Conference on Runtime Verification. RV: Runtime Verification, LNCS, vol. 11757, 292–309.","chicago":"Ničković, Dejan, Xin Qin, Thomas Ferrere, Cristinel Mateis, and Jyotirmoy Deshmukh. “Shape Expressions for Specifying and Extracting Signal Features.” In 19th International Conference on Runtime Verification, 11757:292–309. Springer Nature, 2019. https://doi.org/10.1007/978-3-030-32079-9_17."},"title":"Shape expressions for specifying and extracting signal features","author":[{"full_name":"Ničković, Dejan","last_name":"Ničković","first_name":"Dejan"},{"full_name":"Qin, Xin","last_name":"Qin","first_name":"Xin"},{"first_name":"Thomas","id":"40960E6E-F248-11E8-B48F-1D18A9856A87","last_name":"Ferrere","full_name":"Ferrere, Thomas","orcid":"0000-0001-5199-3143"},{"first_name":"Cristinel","last_name":"Mateis","full_name":"Mateis, Cristinel"},{"first_name":"Jyotirmoy","full_name":"Deshmukh, Jyotirmoy","last_name":"Deshmukh"}],"article_processing_charge":"No","external_id":{"isi":["000570006300017"]},"project":[{"name":"The Wittgenstein Prize","grant_number":"Z211","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425"},{"name":"Rigorous Systems Engineering","grant_number":"S11402-N23","call_identifier":"FWF","_id":"25F2ACDE-B435-11E9-9278-68D0E5697425"}]},{"quality_controlled":"1","publisher":"Springer Nature","oa":1,"doi":"10.1007/978-3-030-29662-9_8","date_published":"2019-08-13T00:00:00Z","date_created":"2020-01-05T23:00:47Z","page":"123-141","day":"13","publication":"17th International Conference on Formal Modeling and Analysis of Timed Systems","isi":1,"year":"2019","project":[{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"},{"name":"Game Theory","grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"Z211","name":"The Wittgenstein Prize"}],"title":"Piecewise robust barrier tubes for nonlinear hybrid systems with uncertainty","author":[{"last_name":"Kong","full_name":"Kong, Hui","orcid":"0000-0002-3066-6941","id":"3BDE25AA-F248-11E8-B48F-1D18A9856A87","first_name":"Hui"},{"first_name":"Ezio","last_name":"Bartocci","full_name":"Bartocci, Ezio"},{"first_name":"Yu","full_name":"Jiang, Yu","last_name":"Jiang"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger"}],"external_id":{"isi":["000611677700008"],"arxiv":["1907.11514"]},"article_processing_charge":"No","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","citation":{"mla":"Kong, Hui, et al. “Piecewise Robust Barrier Tubes for Nonlinear Hybrid Systems with Uncertainty.” 17th International Conference on Formal Modeling and Analysis of Timed Systems, vol. 11750, Springer Nature, 2019, pp. 123–41, doi:10.1007/978-3-030-29662-9_8.","apa":"Kong, H., Bartocci, E., Jiang, Y., & Henzinger, T. A. (2019). Piecewise robust barrier tubes for nonlinear hybrid systems with uncertainty. In 17th International Conference on Formal Modeling and Analysis of Timed Systems (Vol. 11750, pp. 123–141). Amsterdam, The Netherlands: Springer Nature. https://doi.org/10.1007/978-3-030-29662-9_8","ama":"Kong H, Bartocci E, Jiang Y, Henzinger TA. Piecewise robust barrier tubes for nonlinear hybrid systems with uncertainty. In: 17th International Conference on Formal Modeling and Analysis of Timed Systems. Vol 11750. Springer Nature; 2019:123-141. doi:10.1007/978-3-030-29662-9_8","ieee":"H. Kong, E. Bartocci, Y. Jiang, and T. A. Henzinger, “Piecewise robust barrier tubes for nonlinear hybrid systems with uncertainty,” in 17th International Conference on Formal Modeling and Analysis of Timed Systems, Amsterdam, The Netherlands, 2019, vol. 11750, pp. 123–141.","short":"H. Kong, E. Bartocci, Y. Jiang, T.A. Henzinger, in:, 17th International Conference on Formal Modeling and Analysis of Timed Systems, Springer Nature, 2019, pp. 123–141.","chicago":"Kong, Hui, Ezio Bartocci, Yu Jiang, and Thomas A Henzinger. “Piecewise Robust Barrier Tubes for Nonlinear Hybrid Systems with Uncertainty.” In 17th International Conference on Formal Modeling and Analysis of Timed Systems, 11750:123–41. Springer Nature, 2019. https://doi.org/10.1007/978-3-030-29662-9_8.","ista":"Kong H, Bartocci E, Jiang Y, Henzinger TA. 2019. Piecewise robust barrier tubes for nonlinear hybrid systems with uncertainty. 17th International Conference on Formal Modeling and Analysis of Timed Systems. FORMATS: Formal Modeling and Analysis of Timed Systems, LNCS, vol. 11750, 123–141."},"month":"08","intvolume":" 11750","alternative_title":["LNCS"],"scopus_import":"1","main_file_link":[{"url":"https://arxiv.org/abs/1907.11514","open_access":"1"}],"oa_version":"Preprint","abstract":[{"lang":"eng","text":"Piecewise Barrier Tubes (PBT) is a new technique for flowpipe overapproximation for nonlinear systems with polynomial dynamics, which leverages a combination of barrier certificates. PBT has advantages over traditional time-step based methods in dealing with those nonlinear dynamical systems in which there is a large difference in speed between trajectories, producing an overapproximation that is time independent. However, the existing approach for PBT is not efficient due to the application of interval methods for enclosure-box computation, and it can only deal with continuous dynamical systems without uncertainty. In this paper, we extend the approach with the ability to handle both continuous and hybrid dynamical systems with uncertainty that can reside in parameters and/or noise. We also improve the efficiency of the method significantly, by avoiding the use of interval-based methods for the enclosure-box computation without loosing soundness. We have developed a C++ prototype implementing the proposed approach and we evaluate it on several benchmarks. The experiments show that our approach is more efficient and precise than other methods in the literature."}],"volume":11750,"language":[{"iso":"eng"}],"publication_identifier":{"eissn":["1611-3349"],"isbn":["978-3-0302-9661-2"],"issn":["0302-9743"]},"publication_status":"published","status":"public","type":"conference","conference":{"name":"FORMATS: Formal Modeling and Analysis of Timed Systems","start_date":"2019-08-27","location":"Amsterdam, The Netherlands","end_date":"2019-08-29"},"_id":"7231","department":[{"_id":"ToHe"}],"date_updated":"2023-09-06T14:55:15Z"},{"intvolume":" 11750","month":"08","alternative_title":["LNCS"],"scopus_import":"1","oa_version":"None","abstract":[{"lang":"eng","text":"We present Mixed-time Signal Temporal Logic (STL−MX), a specification formalism which extends STL by capturing the discrete/ continuous time duality found in many cyber-physical systems (CPS), as well as mixed-signal electronic designs. In STL−MX, properties of components with continuous dynamics are expressed in STL, while specifications of components with discrete dynamics are written in LTL. To combine the two layers, we evaluate formulas on two traces, discrete- and continuous-time, and introduce two interface operators that map signals, properties and their satisfaction signals across the two time domains. We show that STL-mx has the expressive power of STL supplemented with an implicit T-periodic clock signal. We develop and implement an algorithm for monitoring STL-mx formulas and illustrate the approach using a mixed-signal example. "}],"volume":11750,"language":[{"iso":"eng"}],"publication_status":"published","publication_identifier":{"issn":["0302-9743"],"eissn":["1611-3349"],"isbn":["978-3-0302-9661-2"]},"status":"public","conference":{"start_date":"2019-08-27","location":"Amsterdam, The Netherlands","end_date":"2019-08-29","name":"FORMATS: Formal Modeling and Anaysis of Timed Systems"},"type":"conference","_id":"7232","department":[{"_id":"ToHe"}],"date_updated":"2023-09-06T14:57:17Z","quality_controlled":"1","publisher":"Springer Nature","date_created":"2020-01-05T23:00:48Z","doi":"10.1007/978-3-030-29662-9_4","date_published":"2019-08-13T00:00:00Z","page":"59-75","publication":"17th International Conference on Formal Modeling and Analysis of Timed Systems","day":"13","year":"2019","isi":1,"project":[{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize","grant_number":"Z211"}],"title":"Mixed-time signal temporal logic","article_processing_charge":"No","external_id":{"isi":["000611677700004"]},"author":[{"first_name":"Thomas","id":"40960E6E-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-5199-3143","full_name":"Ferrere, Thomas","last_name":"Ferrere"},{"first_name":"Oded","last_name":"Maler","full_name":"Maler, Oded"},{"last_name":"Nickovic","full_name":"Nickovic, Dejan","id":"41BCEE5C-F248-11E8-B48F-1D18A9856A87","first_name":"Dejan"}],"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","citation":{"short":"T. Ferrere, O. Maler, D. Nickovic, in:, 17th International Conference on Formal Modeling and Analysis of Timed Systems, Springer Nature, 2019, pp. 59–75.","ieee":"T. Ferrere, O. Maler, and D. Nickovic, “Mixed-time signal temporal logic,” in 17th International Conference on Formal Modeling and Analysis of Timed Systems, Amsterdam, The Netherlands, 2019, vol. 11750, pp. 59–75.","ama":"Ferrere T, Maler O, Nickovic D. Mixed-time signal temporal logic. In: 17th International Conference on Formal Modeling and Analysis of Timed Systems. Vol 11750. Springer Nature; 2019:59-75. doi:10.1007/978-3-030-29662-9_4","apa":"Ferrere, T., Maler, O., & Nickovic, D. (2019). Mixed-time signal temporal logic. In 17th International Conference on Formal Modeling and Analysis of Timed Systems (Vol. 11750, pp. 59–75). Amsterdam, The Netherlands: Springer Nature. https://doi.org/10.1007/978-3-030-29662-9_4","mla":"Ferrere, Thomas, et al. “Mixed-Time Signal Temporal Logic.” 17th International Conference on Formal Modeling and Analysis of Timed Systems, vol. 11750, Springer Nature, 2019, pp. 59–75, doi:10.1007/978-3-030-29662-9_4.","ista":"Ferrere T, Maler O, Nickovic D. 2019. Mixed-time signal temporal logic. 17th International Conference on Formal Modeling and Analysis of Timed Systems. FORMATS: Formal Modeling and Anaysis of Timed Systems, LNCS, vol. 11750, 59–75.","chicago":"Ferrere, Thomas, Oded Maler, and Dejan Nickovic. “Mixed-Time Signal Temporal Logic.” In 17th International Conference on Formal Modeling and Analysis of Timed Systems, 11750:59–75. Springer Nature, 2019. https://doi.org/10.1007/978-3-030-29662-9_4."}},{"_id":"6894","status":"public","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"type":"dissertation","ddc":["000"],"date_updated":"2023-09-19T09:30:43Z","supervisor":[{"full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"file_date_updated":"2020-07-14T12:47:43Z","department":[{"_id":"ToHe"}],"oa_version":"Published Version","abstract":[{"lang":"eng","text":"Hybrid automata combine finite automata and dynamical systems, and model the interaction of digital with physical systems. Formal analysis that can guarantee the safety of all behaviors or rigorously witness failures, while unsolvable in general, has been tackled algorithmically using, e.g., abstraction, bounded model-checking, assisted theorem proving.\r\nNevertheless, very few methods have addressed the time-unbounded reachability analysis of hybrid automata and, for current sound and automatic tools, scalability remains critical. We develop methods for the polyhedral abstraction of hybrid automata, which construct coarse overapproximations and tightens them incrementally, in a CEGAR fashion. We use template polyhedra, i.e., polyhedra whose facets are normal to a given set of directions.\r\nWhile, previously, directions were given by the user, we introduce (1) the first method\r\nfor computing template directions from spurious counterexamples, so as to generalize and\r\neliminate them. The method applies naturally to convex hybrid automata, i.e., hybrid\r\nautomata with (possibly non-linear) convex constraints on derivatives only, while for linear\r\nODE requires further abstraction. Specifically, we introduce (2) the conic abstractions,\r\nwhich, partitioning the state space into appropriate (possibly non-uniform) cones, divide\r\ncurvy trajectories into relatively straight sections, suitable for polyhedral abstractions.\r\nFinally, we introduce (3) space-time interpolation, which, combining interval arithmetic\r\nand template refinement, computes appropriate (possibly non-uniform) time partitioning\r\nand template directions along spurious trajectories, so as to eliminate them.\r\nWe obtain sound and automatic methods for the reachability analysis over dense\r\nand unbounded time of convex hybrid automata and hybrid automata with linear ODE.\r\nWe build prototype tools and compare—favorably—our methods against the respective\r\nstate-of-the-art tools, on several benchmarks."}],"month":"09","alternative_title":["ISTA Thesis"],"language":[{"iso":"eng"}],"file":[{"access_level":"open_access","relation":"main_file","content_type":"application/pdf","file_id":"6916","checksum":"773beaf4a85dc2acc2c12b578fbe1965","creator":"mgiacobbe","date_updated":"2020-07-14T12:47:43Z","file_size":4100685,"date_created":"2019-09-27T14:15:05Z","file_name":"giacobbe_thesis.pdf"},{"file_size":7959732,"date_updated":"2020-07-14T12:47:43Z","creator":"mgiacobbe","file_name":"giacobbe_thesis_src.tar.gz","date_created":"2019-09-27T14:22:04Z","content_type":"application/gzip","relation":"source_file","access_level":"closed","file_id":"6917","checksum":"97f1c3da71feefd27e6e625d32b4c75b"}],"publication_status":"published","degree_awarded":"PhD","publication_identifier":{"eissn":["2663-337X"]},"related_material":{"record":[{"relation":"part_of_dissertation","id":"631","status":"public"},{"status":"public","id":"647","relation":"part_of_dissertation"},{"id":"140","status":"public","relation":"part_of_dissertation"}]},"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","citation":{"ista":"Giacobbe M. 2019. Automatic time-unbounded reachability analysis of hybrid systems. Institute of Science and Technology Austria.","chicago":"Giacobbe, Mirco. “Automatic Time-Unbounded Reachability Analysis of Hybrid Systems.” Institute of Science and Technology Austria, 2019. https://doi.org/10.15479/AT:ISTA:6894.","ama":"Giacobbe M. Automatic time-unbounded reachability analysis of hybrid systems. 2019. doi:10.15479/AT:ISTA:6894","apa":"Giacobbe, M. (2019). Automatic time-unbounded reachability analysis of hybrid systems. Institute of Science and Technology Austria. https://doi.org/10.15479/AT:ISTA:6894","short":"M. Giacobbe, Automatic Time-Unbounded Reachability Analysis of Hybrid Systems, Institute of Science and Technology Austria, 2019.","ieee":"M. Giacobbe, “Automatic time-unbounded reachability analysis of hybrid systems,” Institute of Science and Technology Austria, 2019.","mla":"Giacobbe, Mirco. Automatic Time-Unbounded Reachability Analysis of Hybrid Systems. Institute of Science and Technology Austria, 2019, doi:10.15479/AT:ISTA:6894."},"title":"Automatic time-unbounded reachability analysis of hybrid systems","article_processing_charge":"No","author":[{"id":"3444EA5E-F248-11E8-B48F-1D18A9856A87","first_name":"Mirco","orcid":"0000-0001-8180-0904","full_name":"Giacobbe, Mirco","last_name":"Giacobbe"}],"oa":1,"publisher":"Institute of Science and Technology Austria","day":"30","year":"2019","has_accepted_license":"1","date_created":"2019-09-22T14:08:44Z","doi":"10.15479/AT:ISTA:6894","date_published":"2019-09-30T00:00:00Z","page":"132"},{"_id":"3300","status":"public","type":"book","user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","date_updated":"2021-12-21T10:49:36Z","citation":{"mla":"Clarke, Edmund M., et al. Handbook of Model Checking. 1st ed., Springer Nature, 2018, doi:10.1007/978-3-319-10575-8.","apa":"Clarke, E. M., Henzinger, T. A., Veith, H., & Bloem, R. (2018). Handbook of Model Checking (1st ed.). Cham: Springer Nature. https://doi.org/10.1007/978-3-319-10575-8","ama":"Clarke EM, Henzinger TA, Veith H, Bloem R. Handbook of Model Checking. 1st ed. Cham: Springer Nature; 2018. doi:10.1007/978-3-319-10575-8","short":"E.M. Clarke, T.A. Henzinger, H. Veith, R. Bloem, Handbook of Model Checking, 1st ed., Springer Nature, Cham, 2018.","ieee":"E. M. Clarke, T. A. Henzinger, H. Veith, and R. Bloem, Handbook of Model Checking, 1st ed. Cham: Springer Nature, 2018.","chicago":"Clarke, Edmund M., Thomas A Henzinger, Helmut Veith, and Roderick Bloem. Handbook of Model Checking. 1st ed. Cham: Springer Nature, 2018. https://doi.org/10.1007/978-3-319-10575-8.","ista":"Clarke EM, Henzinger TA, Veith H, Bloem R. 2018. Handbook of Model Checking 1st ed., Cham: Springer Nature, XLVIII, 1212p."},"title":"Handbook of Model Checking","department":[{"_id":"ToHe"}],"author":[{"full_name":"Clarke, Edmund M.","last_name":"Clarke","first_name":"Edmund M."},{"last_name":"Henzinger","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A"},{"full_name":"Veith, Helmut","last_name":"Veith","first_name":"Helmut"},{"first_name":"Roderick","full_name":"Bloem, Roderick","last_name":"Bloem"}],"publist_id":"3340","article_processing_charge":"No","oa_version":"None","abstract":[{"text":"This book first explores the origins of this idea, grounded in theoretical work on temporal logic and automata. The editors and authors are among the world's leading researchers in this domain, and they contributed 32 chapters representing a thorough view of the development and application of the technique. Topics covered include binary decision diagrams, symbolic model checking, satisfiability modulo theories, partial-order reduction, abstraction, interpolation, concurrency, security protocols, games, probabilistic model checking, and process algebra, and chapters on the transfer of theory to industrial practice, property specification languages for hardware, and verification of real-time systems and hybrid systems.\r\n\r\nThe book will be valuable for researchers and graduate students engaged with the development of formal methods and verification tools.","lang":"eng"}],"place":"Cham","month":"06","scopus_import":"1","publisher":"Springer Nature","quality_controlled":"1","edition":"1","day":"08","language":[{"iso":"eng"}],"publication_identifier":{"eisbn":["978-3-319-10575-8"],"isbn":["978-3-319-10574-1"]},"publication_status":"published","year":"2018","doi":"10.1007/978-3-319-10575-8","date_published":"2018-06-08T00:00:00Z","date_created":"2018-12-11T12:02:32Z","page":"XLVIII, 1212"},{"page":"1 - 26","date_created":"2018-12-11T11:44:25Z","date_published":"2018-05-19T00:00:00Z","doi":"10.1007/978-3-319-10575-8_1","year":"2018","publication_status":"published","language":[{"iso":"eng"}],"publication":"Handbook of Model Checking","day":"19","publisher":"Springer","scopus_import":1,"quality_controlled":"1","month":"05","abstract":[{"lang":"eng","text":"Model checking is a computer-assisted method for the analysis of dynamical systems that can be modeled by state-transition systems. Drawing from research traditions in mathematical logic, programming languages, hardware design, and theoretical computer science, model checking is now widely used for the verification of hardware and software in industry. This chapter is an introduction and short survey of model checking. The chapter aims to motivate and link the individual chapters of the handbook, and to provide context for readers who are not familiar with model checking."}],"oa_version":"None","publist_id":"7994","author":[{"last_name":"Clarke","full_name":"Clarke, Edmund","first_name":"Edmund"},{"last_name":"Henzinger","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Helmut","full_name":"Veith, Helmut","last_name":"Veith"}],"title":"Introduction to model checking","editor":[{"first_name":"Thomas A","last_name":"Henzinger","full_name":"Henzinger, Thomas A"}],"department":[{"_id":"ToHe"}],"citation":{"chicago":"Clarke, Edmund, Thomas A Henzinger, and Helmut Veith. “Introduction to Model Checking.” In Handbook of Model Checking, edited by Thomas A Henzinger, 1–26. Handbook of Model Checking. Springer, 2018. https://doi.org/10.1007/978-3-319-10575-8_1.","ista":"Clarke E, Henzinger TA, Veith H. 2018.Introduction to model checking. In: Handbook of Model Checking. , 1–26.","mla":"Clarke, Edmund, et al. “Introduction to Model Checking.” Handbook of Model Checking, edited by Thomas A Henzinger, Springer, 2018, pp. 1–26, doi:10.1007/978-3-319-10575-8_1.","short":"E. Clarke, T.A. Henzinger, H. Veith, in:, T.A. Henzinger (Ed.), Handbook of Model Checking, Springer, 2018, pp. 1–26.","ieee":"E. Clarke, T. A. Henzinger, and H. Veith, “Introduction to model checking,” in Handbook of Model Checking, T. A. Henzinger, Ed. Springer, 2018, pp. 1–26.","apa":"Clarke, E., Henzinger, T. A., & Veith, H. (2018). Introduction to model checking. In T. A. Henzinger (Ed.), Handbook of Model Checking (pp. 1–26). Springer. https://doi.org/10.1007/978-3-319-10575-8_1","ama":"Clarke E, Henzinger TA, Veith H. Introduction to model checking. In: Henzinger TA, ed. Handbook of Model Checking. Handbook of Model Checking. Springer; 2018:1-26. doi:10.1007/978-3-319-10575-8_1"},"date_updated":"2021-01-12T08:05:35Z","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","type":"book_chapter","status":"public","series_title":"Handbook of Model Checking","_id":"60"},{"file_date_updated":"2020-07-14T12:48:14Z","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"ddc":["000"],"date_updated":"2021-01-12T08:20:14Z","status":"public","type":"book_chapter","_id":"86","ec_funded":1,"volume":10760,"language":[{"iso":"eng"}],"file":[{"file_size":516307,"date_updated":"2020-07-14T12:48:14Z","creator":"dernst","file_name":"2018_PrinciplesModeling_Chatterjee.pdf","date_created":"2019-11-19T08:22:18Z","content_type":"application/pdf","relation":"main_file","access_level":"open_access","checksum":"9995c6ce6957333baf616fc4f20be597","file_id":"7053"}],"publication_status":"published","intvolume":" 10760","month":"07","scopus_import":1,"alternative_title":["LNCS"],"oa_version":"Submitted Version","abstract":[{"text":"Responsiveness—the requirement that every request to a system be eventually handled—is one of the fundamental liveness properties of a reactive system. Average response time is a quantitative measure for the responsiveness requirement used commonly in performance evaluation. We show how average response time can be computed on state-transition graphs, on Markov chains, and on game graphs. In all three cases, we give polynomial-time algorithms.","lang":"eng"}],"title":"Computing average response time","editor":[{"first_name":"Marten","last_name":"Lohstroh","full_name":"Lohstroh, Marten"},{"first_name":"Patricia","last_name":"Derler","full_name":"Derler, Patricia"},{"first_name":"Marjan","full_name":"Sirjani, Marjan","last_name":"Sirjani"}],"author":[{"orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Henzinger","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Otop","full_name":"Otop, Jan","first_name":"Jan","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87"}],"publist_id":"7968","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. “Computing Average Response Time.” In Principles of Modeling, edited by Marten Lohstroh, Patricia Derler, and Marjan Sirjani, 10760:143–61. Springer, 2018. https://doi.org/10.1007/978-3-319-95246-8_9.","ista":"Chatterjee K, Henzinger TA, Otop J. 2018.Computing average response time. In: Principles of Modeling. LNCS, vol. 10760, 143–161.","mla":"Chatterjee, Krishnendu, et al. “Computing Average Response Time.” Principles of Modeling, edited by Marten Lohstroh et al., vol. 10760, Springer, 2018, pp. 143–61, doi:10.1007/978-3-319-95246-8_9.","ama":"Chatterjee K, Henzinger TA, Otop J. Computing average response time. In: Lohstroh M, Derler P, Sirjani M, eds. Principles of Modeling. Vol 10760. Springer; 2018:143-161. doi:10.1007/978-3-319-95246-8_9","apa":"Chatterjee, K., Henzinger, T. A., & Otop, J. (2018). Computing average response time. In M. Lohstroh, P. Derler, & M. Sirjani (Eds.), Principles of Modeling (Vol. 10760, pp. 143–161). Springer. https://doi.org/10.1007/978-3-319-95246-8_9","ieee":"K. Chatterjee, T. A. Henzinger, and J. Otop, “Computing average response time,” in Principles of Modeling, vol. 10760, M. Lohstroh, P. Derler, and M. Sirjani, Eds. Springer, 2018, pp. 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."},"project":[{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S11407","name":"Game Theory"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize","grant_number":"Z211"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications"},{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","name":"Efficient Algorithms for Computer Aided Verification","grant_number":"ICT15-003"}],"date_created":"2018-12-11T11:44:33Z","date_published":"2018-07-20T00:00:00Z","doi":"10.1007/978-3-319-95246-8_9","page":"143 - 161","publication":"Principles of Modeling","day":"20","year":"2018","has_accepted_license":"1","oa":1,"quality_controlled":"1","publisher":"Springer","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."},{"project":[{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","name":"The Wittgenstein Prize"},{"name":"Formal Methods meets Algorithmic Game Theory","grant_number":"M02369","_id":"264B3912-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"article_number":"23","title":"Timed network games with clocks","article_processing_charge":"No","author":[{"first_name":"Guy","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","last_name":"Avni","orcid":"0000-0001-5588-8287","full_name":"Avni, Guy"},{"last_name":"Guha","full_name":"Guha, Shibashis","first_name":"Shibashis"},{"last_name":"Kupferman","full_name":"Kupferman, Orna","first_name":"Orna"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"mla":"Avni, Guy, et al. Timed Network Games with Clocks. Vol. 117, 23, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018, doi:10.4230/LIPICS.MFCS.2018.23.","ieee":"G. Avni, S. Guha, and O. Kupferman, “Timed network games with clocks,” presented at the MFCS: Mathematical Foundations of Computer Science, Liverpool, United Kingdom, 2018, vol. 117.","short":"G. Avni, S. Guha, O. Kupferman, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018.","ama":"Avni G, Guha S, Kupferman O. Timed network games with clocks. In: Vol 117. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2018. doi:10.4230/LIPICS.MFCS.2018.23","apa":"Avni, G., Guha, S., & Kupferman, O. (2018). Timed network games with clocks (Vol. 117). Presented at the MFCS: Mathematical Foundations of Computer Science, Liverpool, United Kingdom: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPICS.MFCS.2018.23","chicago":"Avni, Guy, Shibashis Guha, and Orna Kupferman. “Timed Network Games with Clocks,” Vol. 117. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. https://doi.org/10.4230/LIPICS.MFCS.2018.23.","ista":"Avni G, Guha S, Kupferman O. 2018. Timed network games with clocks. MFCS: Mathematical Foundations of Computer Science, LIPIcs, vol. 117, 23."},"oa":1,"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","quality_controlled":"1","date_created":"2019-02-14T14:12:09Z","doi":"10.4230/LIPICS.MFCS.2018.23","date_published":"2018-08-01T00:00:00Z","day":"01","year":"2018","has_accepted_license":"1","status":"public","conference":{"location":"Liverpool, United Kingdom","end_date":"2018-08-31","start_date":"2018-08-27","name":"MFCS: Mathematical Foundations of Computer Science"},"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"type":"conference","_id":"6005","file_date_updated":"2020-07-14T12:47:15Z","department":[{"_id":"ToHe"}],"ddc":["000"],"date_updated":"2023-02-23T14:02:58Z","intvolume":" 117","month":"08","alternative_title":["LIPIcs"],"scopus_import":"1","oa_version":"Published Version","abstract":[{"text":"Network games are widely used as a model for selfish resource-allocation problems. In the classicalmodel, each player selects a path connecting her source and target vertices. The cost of traversingan edge depends on theload; namely, number of players that traverse it. Thus, it abstracts the factthat different users may use a resource at different times and for different durations, which playsan important role in determining the costs of the users in reality. For example, when transmittingpackets in a communication network, routing traffic in a road network, or processing a task in aproduction system, actual sharing and congestion of resources crucially depends on time.In [13], we introducedtimed network games, which add a time component to network games.Each vertexvin the network is associated with a cost function, mapping the load onvto theprice that a player pays for staying invfor one time unit with this load. Each edge in thenetwork is guarded by the time intervals in which it can be traversed, which forces the players tospend time in the vertices. In this work we significantly extend the way time can be referred toin timed network games. In the model we study, the network is equipped withclocks, and, as intimed automata, edges are guarded by constraints on the values of the clocks, and their traversalmay involve a reset of some clocks. We argue that the stronger model captures many realisticnetworks. The addition of clocks breaks the techniques we developed in [13] and we developnew techniques in order to show that positive results on classic network games carry over to thestronger timed setting.","lang":"eng"}],"volume":117,"related_material":{"record":[{"relation":"earlier_version","id":"963","status":"public"}]},"language":[{"iso":"eng"}],"file":[{"creator":"dernst","date_updated":"2020-07-14T12:47:15Z","file_size":542889,"date_created":"2019-02-14T14:22:04Z","file_name":"2018_LIPIcs_Avni.pdf","access_level":"open_access","relation":"main_file","content_type":"application/pdf","checksum":"41ab2ae9b63f5eb49fa995250c0ba128","file_id":"6007"}],"publication_status":"published","publication_identifier":{"issn":["1868-8969"]}},{"oa_version":"Published Version","abstract":[{"text":"Synchronous programs are easy to specify because the side effects of an operation are finished by the time the invocation of the operation returns to the caller. Asynchronous programs, on the other hand, are difficult to specify because there are side effects due to pending computation scheduled as a result of the invocation of an operation. They are also difficult to verify because of the large number of possible interleavings of concurrent computation threads. We present synchronization, a new proof rule that simplifies the verification of asynchronous programs by introducing the fiction, for proof purposes, that asynchronous operations complete synchronously. Synchronization summarizes an asynchronous computation as immediate atomic effect. Modular verification is enabled via pending asynchronous calls in atomic summaries, and a complementary proof rule that eliminates pending asynchronous calls when components and their specifications are composed. We evaluate synchronization in the context of a multi-layer refinement verification methodology on a collection of benchmark programs.","lang":"eng"}],"month":"08","intvolume":" 118","scopus_import":1,"alternative_title":["LIPIcs"],"file":[{"file_name":"IST-2018-853-v2+2_concur2018.pdf","date_created":"2018-12-12T10:18:46Z","creator":"system","file_size":745438,"date_updated":"2020-07-14T12:44:44Z","checksum":"c90895f4c5fafc18ddc54d1c8848077e","file_id":"5368","relation":"main_file","access_level":"open_access","content_type":"application/pdf"}],"language":[{"iso":"eng"}],"publication_identifier":{"issn":["18688969"]},"publication_status":"published","volume":118,"related_material":{"record":[{"id":"6426","status":"public","relation":"earlier_version"},{"relation":"dissertation_contains","id":"8332","status":"public"}]},"_id":"133","status":"public","pubrep_id":"1039","type":"conference","conference":{"name":"CONCUR: International Conference on Concurrency Theory","end_date":"2018-09-07","location":"Beijing, China","start_date":"2018-09-04"},"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"ddc":["000"],"date_updated":"2023-09-07T13:18:00Z","department":[{"_id":"ToHe"}],"file_date_updated":"2020-07-14T12:44:44Z","quality_controlled":"1","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","oa":1,"day":"13","has_accepted_license":"1","year":"2018","date_published":"2018-08-13T00:00:00Z","doi":"10.4230/LIPIcs.CONCUR.2018.21","date_created":"2018-12-11T11:44:48Z","article_number":"21","project":[{"_id":"25F2ACDE-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S11402-N23"},{"call_identifier":"FWF","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","name":"Moderne Concurrency Paradigms","grant_number":"S11402-N23"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"ista":"Kragl B, Qadeer S, Henzinger TA. 2018. Synchronizing the asynchronous. CONCUR: International Conference on Concurrency Theory, LIPIcs, vol. 118, 21.","chicago":"Kragl, Bernhard, Shaz Qadeer, and Thomas A Henzinger. “Synchronizing the Asynchronous,” Vol. 118. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. https://doi.org/10.4230/LIPIcs.CONCUR.2018.21.","ieee":"B. Kragl, S. Qadeer, and T. A. Henzinger, “Synchronizing the asynchronous,” presented at the CONCUR: International Conference on Concurrency Theory, Beijing, China, 2018, vol. 118.","short":"B. Kragl, S. Qadeer, T.A. Henzinger, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018.","ama":"Kragl B, Qadeer S, Henzinger TA. Synchronizing the asynchronous. In: Vol 118. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2018. doi:10.4230/LIPIcs.CONCUR.2018.21","apa":"Kragl, B., Qadeer, S., & Henzinger, T. A. (2018). Synchronizing the asynchronous (Vol. 118). Presented at the CONCUR: International Conference on Concurrency Theory, Beijing, China: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2018.21","mla":"Kragl, Bernhard, et al. Synchronizing the Asynchronous. Vol. 118, 21, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018, doi:10.4230/LIPIcs.CONCUR.2018.21."},"title":"Synchronizing the asynchronous","publist_id":"7790","author":[{"orcid":"0000-0001-7745-9117","full_name":"Kragl, Bernhard","last_name":"Kragl","id":"320FC952-F248-11E8-B48F-1D18A9856A87","first_name":"Bernhard"},{"first_name":"Shaz","full_name":"Qadeer, Shaz","last_name":"Qadeer"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","last_name":"Henzinger","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724"}]},{"isi":1,"has_accepted_license":"1","year":"2018","day":"14","page":"303 - 319","date_published":"2018-04-14T00:00:00Z","doi":"10.1007/978-3-319-89963-3_18","date_created":"2018-12-11T11:45:41Z","publisher":"Springer","quality_controlled":"1","oa":1,"citation":{"chicago":"Nickovic, Dejan, Olivier Lebeltel, Oded Maler, Thomas Ferrere, and Dogan Ulus. “AMT 2.0: Qualitative and Quantitative Trace Analysis with Extended Signal Temporal Logic.” edited by Dirk Beyer and Marieke Huisman, 10806:303–19. Springer, 2018. https://doi.org/10.1007/978-3-319-89963-3_18.","ista":"Nickovic D, Lebeltel O, Maler O, Ferrere T, Ulus D. 2018. AMT 2.0: Qualitative and quantitative trace analysis with extended signal temporal logic. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 10806, 303–319.","mla":"Nickovic, Dejan, et al. AMT 2.0: Qualitative and Quantitative Trace Analysis with Extended Signal Temporal Logic. Edited by Dirk Beyer and Marieke Huisman, vol. 10806, Springer, 2018, pp. 303–19, doi:10.1007/978-3-319-89963-3_18.","apa":"Nickovic, D., Lebeltel, O., Maler, O., Ferrere, T., & Ulus, D. (2018). AMT 2.0: Qualitative and quantitative trace analysis with extended signal temporal logic. In D. Beyer & M. Huisman (Eds.) (Vol. 10806, pp. 303–319). Presented at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems, Thessaloniki, Greece: Springer. https://doi.org/10.1007/978-3-319-89963-3_18","ama":"Nickovic D, Lebeltel O, Maler O, Ferrere T, Ulus D. AMT 2.0: Qualitative and quantitative trace analysis with extended signal temporal logic. In: Beyer D, Huisman M, eds. Vol 10806. Springer; 2018:303-319. doi:10.1007/978-3-319-89963-3_18","short":"D. Nickovic, O. Lebeltel, O. Maler, T. Ferrere, D. Ulus, in:, D. Beyer, M. Huisman (Eds.), Springer, 2018, pp. 303–319.","ieee":"D. Nickovic, O. Lebeltel, O. Maler, T. Ferrere, and D. Ulus, “AMT 2.0: Qualitative and quantitative trace analysis with extended signal temporal logic,” presented at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems, Thessaloniki, Greece, 2018, vol. 10806, pp. 303–319."},"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","publist_id":"7582","author":[{"full_name":"Nickovic, Dejan","last_name":"Nickovic","id":"41BCEE5C-F248-11E8-B48F-1D18A9856A87","first_name":"Dejan"},{"first_name":"Olivier","full_name":"Lebeltel, Olivier","last_name":"Lebeltel"},{"last_name":"Maler","full_name":"Maler, Oded","first_name":"Oded"},{"orcid":"0000-0001-5199-3143","full_name":"Ferrere, Thomas","last_name":"Ferrere","id":"40960E6E-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas"},{"first_name":"Dogan","full_name":"Ulus, Dogan","last_name":"Ulus"}],"external_id":{"isi":["00445822600018"]},"article_processing_charge":"No","editor":[{"last_name":"Beyer","full_name":"Beyer, Dirk","first_name":"Dirk"},{"full_name":"Huisman, Marieke","last_name":"Huisman","first_name":"Marieke"}],"title":"AMT 2.0: Qualitative and quantitative trace analysis with extended signal temporal logic","publication_status":"published","file":[{"file_size":3267209,"date_updated":"2020-07-14T12:45:58Z","creator":"dernst","file_name":"2018_LNCS_Nickovic.pdf","date_created":"2019-02-06T07:33:05Z","content_type":"application/pdf","relation":"main_file","access_level":"open_access","checksum":"e11db3b9c8e27a1c7d1c738cc5e4d25a","file_id":"5928"}],"language":[{"iso":"eng"}],"related_material":{"record":[{"id":"10861","status":"public","relation":"later_version"}]},"volume":10806,"abstract":[{"text":"We introduce in this paper AMT 2.0 , a tool for qualitative and quantitative analysis of hybrid continuous and Boolean signals that combine numerical values and discrete events. The evaluation of the signals is based on rich temporal specifications expressed in extended Signal Temporal Logic (xSTL), which integrates Timed Regular Expressions (TRE) within Signal Temporal Logic (STL). The tool features qualitative monitoring (property satisfaction checking), trace diagnostics for explaining and justifying property violations and specification-driven measurement of quantitative features of the signal.","lang":"eng"}],"oa_version":"Published Version","alternative_title":["LNCS"],"scopus_import":"1","month":"04","intvolume":" 10806","date_updated":"2023-09-08T11:52:02Z","ddc":["000"],"department":[{"_id":"ToHe"}],"file_date_updated":"2020-07-14T12:45:58Z","_id":"299","type":"conference","conference":{"start_date":"2018-04-14","location":"Thessaloniki, Greece","end_date":"2018-04-20","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems"},"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"status":"public"},{"date_created":"2018-12-11T11:44:52Z","volume":"Part F138033","doi":"10.1145/3209108.3209194","date_published":"2018-07-09T00:00:00Z","page":"394 - 403","language":[{"iso":"eng"}],"day":"09","publication_status":"published","year":"2018","isi":1,"month":"07","alternative_title":["ACM/IEEE Symposium on Logic in Computer Science"],"quality_controlled":"1","scopus_import":"1","publisher":"IEEE","oa_version":"None","abstract":[{"lang":"eng","text":"The task of a monitor is to watch, at run-time, the execution of a reactive system, and signal the occurrence of a safety violation in the observed sequence of events. While finite-state monitors have been studied extensively, in practice, monitoring software also makes use of unbounded memory. We define a model of automata equipped with integer-valued registers which can execute only a bounded number of instructions between consecutive events, and thus can form the theoretical basis for the study of infinite-state monitors. We classify these register monitors according to the number k of available registers, and the type of register instructions. In stark contrast to the theory of computability for register machines, we prove that for every k 1, monitors with k + 1 counters (with instruction set 〈+1, =〉) are strictly more expressive than monitors with k counters. We also show that adder monitors (with instruction set 〈1, +, =〉) are strictly more expressive than counter monitors, but are complete for monitoring all computable safety -languages for k = 6. Real-time monitors are further required to signal the occurrence of a safety violation as soon as it occurs. The expressiveness hierarchy for counter monitors carries over to real-time monitors. We then show that 2 adders cannot simulate 3 counters in real-time. Finally, we show that real-time adder monitors with inequalities are as expressive as real-time Turing machines."}],"department":[{"_id":"ToHe"}],"title":"A theory of register monitors","article_processing_charge":"No","external_id":{"isi":["000545262800041"]},"author":[{"last_name":"Ferrere","full_name":"Ferrere, Thomas","orcid":"0000-0001-5199-3143","id":"40960E6E-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","last_name":"Henzinger","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724"},{"last_name":"Saraç","full_name":"Saraç, Ege","first_name":"Ege"}],"publist_id":"7779","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","date_updated":"2023-09-08T11:49:13Z","citation":{"ieee":"T. Ferrere, T. A. Henzinger, and E. Saraç, “A theory of register monitors,” presented at the LICS: Logic in Computer Science, Oxford, UK, 2018, vol. Part F138033, pp. 394–403.","short":"T. Ferrere, T.A. Henzinger, E. Saraç, in:, IEEE, 2018, pp. 394–403.","ama":"Ferrere T, Henzinger TA, Saraç E. A theory of register monitors. In: Vol Part F138033. IEEE; 2018:394-403. doi:10.1145/3209108.3209194","apa":"Ferrere, T., Henzinger, T. A., & Saraç, E. (2018). A theory of register monitors (Vol. Part F138033, pp. 394–403). Presented at the LICS: Logic in Computer Science, Oxford, UK: IEEE. https://doi.org/10.1145/3209108.3209194","mla":"Ferrere, Thomas, et al. A Theory of Register Monitors. Vol. Part F138033, IEEE, 2018, pp. 394–403, doi:10.1145/3209108.3209194.","ista":"Ferrere T, Henzinger TA, Saraç E. 2018. A theory of register monitors. LICS: Logic in Computer Science, ACM/IEEE Symposium on Logic in Computer Science, vol. Part F138033, 394–403.","chicago":"Ferrere, Thomas, Thomas A Henzinger, and Ege Saraç. “A Theory of Register Monitors,” Part F138033:394–403. IEEE, 2018. https://doi.org/10.1145/3209108.3209194."},"status":"public","conference":{"name":"LICS: Logic in Computer Science","end_date":"2018-07-12","location":"Oxford, UK","start_date":"2018-07-09"},"type":"conference","_id":"144"},{"publication_status":"published","publication_identifier":{"isbn":["978-1-4503-5642-8 "]},"language":[{"iso":"eng"}],"file":[{"date_created":"2020-05-14T12:18:29Z","file_name":"2018_HSCC_Bakhirkin.pdf","creator":"dernst","date_updated":"2020-07-14T12:45:17Z","file_size":5900421,"file_id":"7833","checksum":"81eabc96430e84336ea88310ac0a1ad0","access_level":"open_access","relation":"main_file","content_type":"application/pdf"}],"abstract":[{"text":"We describe a new algorithm for the parametric identification problem for signal temporal logic (STL), stated as follows. Given a densetime real-valued signal w and a parameterized temporal logic formula φ, compute the subset of the parameter space that renders the formula satisfied by the signal. Unlike previous solutions, which were based on search in the parameter space or quantifier elimination, our procedure works recursively on φ and computes the evolution over time of the set of valid parameter assignments. This procedure is similar to that of monitoring or computing the robustness of φ relative to w. Our implementation and experiments demonstrate that this approach can work well in practice.","lang":"eng"}],"oa_version":"Submitted Version","alternative_title":["HSCC Proceedings"],"scopus_import":"1","month":"04","date_updated":"2023-09-11T13:30:51Z","ddc":["000"],"department":[{"_id":"ToHe"}],"file_date_updated":"2020-07-14T12:45:17Z","_id":"182","conference":{"location":"Porto, Portugal","end_date":"2018-04-13","start_date":"2018-04-11","name":"HSCC: Hybrid Systems: Computation and Control"},"type":"conference","status":"public","year":"2018","isi":1,"has_accepted_license":"1","publication":"Proceedings of the 21st International Conference on Hybrid Systems","day":"11","page":"177 - 186","date_created":"2018-12-11T11:45:04Z","doi":"10.1145/3178126.3178132","date_published":"2018-04-11T00:00:00Z","oa":1,"publisher":"ACM","quality_controlled":"1","citation":{"mla":"Bakhirkin, Alexey, et al. “Efficient Parametric Identification for STL.” Proceedings of the 21st International Conference on Hybrid Systems, ACM, 2018, pp. 177–86, doi:10.1145/3178126.3178132.","apa":"Bakhirkin, A., Ferrere, T., & Maler, O. (2018). Efficient parametric identification for STL. In Proceedings of the 21st International Conference on Hybrid Systems (pp. 177–186). Porto, Portugal: ACM. https://doi.org/10.1145/3178126.3178132","ama":"Bakhirkin A, Ferrere T, Maler O. Efficient parametric identification for STL. In: Proceedings of the 21st International Conference on Hybrid Systems. ACM; 2018:177-186. doi:10.1145/3178126.3178132","ieee":"A. Bakhirkin, T. Ferrere, and O. Maler, “Efficient parametric identification for STL,” in Proceedings of the 21st International Conference on Hybrid Systems, Porto, Portugal, 2018, pp. 177–186.","short":"A. Bakhirkin, T. Ferrere, O. Maler, in:, Proceedings of the 21st International Conference on Hybrid Systems, ACM, 2018, pp. 177–186.","chicago":"Bakhirkin, Alexey, Thomas Ferrere, and Oded Maler. “Efficient Parametric Identification for STL.” In Proceedings of the 21st International Conference on Hybrid Systems, 177–86. ACM, 2018. https://doi.org/10.1145/3178126.3178132.","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."},"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","article_processing_charge":"No","external_id":{"isi":["000474781600020"]},"author":[{"full_name":"Bakhirkin, Alexey","last_name":"Bakhirkin","first_name":"Alexey"},{"first_name":"Thomas","id":"40960E6E-F248-11E8-B48F-1D18A9856A87","last_name":"Ferrere","full_name":"Ferrere, Thomas","orcid":"0000-0001-5199-3143"},{"full_name":"Maler, Oded","last_name":"Maler","first_name":"Oded"}],"publist_id":"7739","title":"Efficient parametric identification for STL","project":[{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"}]}]