[{"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","month":"08","_id":"7232","title":"Mixed-time signal temporal logic","publication_status":"published","department":[{"_id":"ToHe"}],"alternative_title":["LNCS"],"status":"public","abstract":[{"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. ","lang":"eng"}],"day":"13","intvolume":" 11750","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.","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","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.","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.","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."},"doi":"10.1007/978-3-030-29662-9_4","publisher":"Springer Nature","language":[{"iso":"eng"}],"type":"conference","conference":{"location":"Amsterdam, The Netherlands","end_date":"2019-08-29","name":"FORMATS: Formal Modeling and Anaysis of Timed Systems","start_date":"2019-08-27"},"external_id":{"isi":["000611677700004"]},"oa_version":"None","date_published":"2019-08-13T00:00:00Z","publication":"17th International Conference on Formal Modeling and Analysis of Timed Systems","author":[{"id":"40960E6E-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-5199-3143","first_name":"Thomas","full_name":"Ferrere, Thomas","last_name":"Ferrere"},{"first_name":"Oded","full_name":"Maler, Oded","last_name":"Maler"},{"id":"41BCEE5C-F248-11E8-B48F-1D18A9856A87","last_name":"Nickovic","full_name":"Nickovic, Dejan","first_name":"Dejan"}],"page":"59-75","quality_controlled":"1","year":"2019","date_created":"2020-01-05T23:00:48Z","date_updated":"2023-09-06T14:57:17Z","project":[{"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"}],"volume":11750,"isi":1,"article_processing_charge":"No","publication_identifier":{"isbn":["978-3-0302-9661-2"],"issn":["0302-9743"],"eissn":["1611-3349"]},"scopus_import":"1"},{"acknowledgement":"This research was supported in part by the Austrian Science Fund (FWF) under grants S11402-N23(RiSE/SHiNE) and Z211-N23 (Wittgenstein Award). This research has received funding from the Sino-Danish Basic Research Centre, IDEA4CPS, funded by the Danish National Research Foundation and the National Science Foundation, China, the Innovation Fund Denmark centre DiCyPS, as well as the ERC Advanced Grant LASSO.","department":[{"_id":"ToHe"}],"alternative_title":["Lecture Notes in Computer Science"],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","month":"10","_id":"7453","title":"Continuous-time models for system design and analysis","oa":1,"publication_status":"published","day":"05","intvolume":" 10000","citation":{"short":"R. Alur, M. Giacobbe, T.A. Henzinger, K.G. Larsen, M. Mikučionis, in:, B. Steffen, G. Woeginger (Eds.), Computing and Software Science, Springer Nature, 2019, pp. 452–477.","ama":"Alur R, Giacobbe M, Henzinger TA, Larsen KG, Mikučionis M. Continuous-time models for system design and analysis. In: Steffen B, Woeginger G, eds. Computing and Software Science. Vol 10000. LNCS. Springer Nature; 2019:452-477. doi:10.1007/978-3-319-91908-9_22","chicago":"Alur, Rajeev, Mirco Giacobbe, Thomas A Henzinger, Kim G. Larsen, and Marius Mikučionis. “Continuous-Time Models for System Design and Analysis.” In Computing and Software Science, edited by Bernhard Steffen and Gerhard Woeginger, 10000:452–77. LNCS. Springer Nature, 2019. https://doi.org/10.1007/978-3-319-91908-9_22.","apa":"Alur, R., Giacobbe, M., Henzinger, T. A., Larsen, K. G., & Mikučionis, M. (2019). Continuous-time models for system design and analysis. In B. Steffen & G. Woeginger (Eds.), Computing and Software Science (Vol. 10000, pp. 452–477). Springer Nature. https://doi.org/10.1007/978-3-319-91908-9_22","ista":"Alur R, Giacobbe M, Henzinger TA, Larsen KG, Mikučionis M. 2019.Continuous-time models for system design and analysis. In: Computing and Software Science. Lecture Notes in Computer Science, vol. 10000, 452–477.","ieee":"R. Alur, M. Giacobbe, T. A. Henzinger, K. G. Larsen, and M. Mikučionis, “Continuous-time models for system design and analysis,” in Computing and Software Science, vol. 10000, B. Steffen and G. Woeginger, Eds. Springer Nature, 2019, pp. 452–477.","mla":"Alur, Rajeev, et al. “Continuous-Time Models for System Design and Analysis.” Computing and Software Science, edited by Bernhard Steffen and Gerhard Woeginger, vol. 10000, Springer Nature, 2019, pp. 452–77, doi:10.1007/978-3-319-91908-9_22."},"editor":[{"last_name":"Steffen","full_name":"Steffen, Bernhard","first_name":"Bernhard"},{"last_name":"Woeginger","first_name":"Gerhard","full_name":"Woeginger, Gerhard"}],"abstract":[{"text":"We illustrate the ingredients of the state-of-the-art of model-based approach for the formal design and verification of cyber-physical systems. To capture the interaction between a discrete controller and its continuously evolving environment, we use the formal models of timed and hybrid automata. We explain the steps of modeling and verification in the tools Uppaal and SpaceEx using a case study based on a dual-chamber implantable pacemaker monitoring a human heart. We show how to design a model as a composition of components, how to construct models at varying levels of detail, how to establish that one model is an abstraction of another, how to specify correctness requirements using temporal logic, and how to verify that a model satisfies a logical requirement.","lang":"eng"}],"status":"public","date_published":"2019-10-05T00:00:00Z","oa_version":"Published Version","author":[{"full_name":"Alur, Rajeev","first_name":"Rajeev","last_name":"Alur"},{"orcid":"0000-0001-8180-0904","id":"3444EA5E-F248-11E8-B48F-1D18A9856A87","last_name":"Giacobbe","first_name":"Mirco","full_name":"Giacobbe, Mirco"},{"last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Larsen, Kim G.","first_name":"Kim G.","last_name":"Larsen"},{"last_name":"Mikučionis","first_name":"Marius","full_name":"Mikučionis, Marius"}],"publication":"Computing and Software Science","publisher":"Springer Nature","doi":"10.1007/978-3-319-91908-9_22","type":"book_chapter","language":[{"iso":"eng"}],"article_processing_charge":"No","scopus_import":"1","main_file_link":[{"url":"https://doi.org/10.1007/978-3-319-91908-9_22","open_access":"1"}],"publication_identifier":{"isbn":["9783319919072"],"eisbn":["9783319919089"],"eissn":["0302-9743"],"issn":["1611-3349"]},"date_updated":"2022-09-06T08:25:52Z","project":[{"call_identifier":"FWF","_id":"25F2ACDE-B435-11E9-9278-68D0E5697425","grant_number":"S11402-N23","name":"Rigorous Systems Engineering"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize","grant_number":"Z211"}],"quality_controlled":"1","page":"452-477","year":"2019","date_created":"2020-02-05T10:51:44Z","series_title":"LNCS","volume":10000},{"file":[{"date_updated":"2020-07-14T12:48:00Z","access_level":"open_access","date_created":"2020-03-24T07:36:36Z","file_id":"7617","content_type":"application/pdf","file_name":"2019_ARCH19_Immler.pdf","creator":"dernst","file_size":1934830,"checksum":"9138977a06fcd6a95976eb4bca875f0c","relation":"main_file"}],"volume":61,"date_updated":"2021-01-12T08:14:17Z","year":"2019","date_created":"2020-03-08T23:00:49Z","page":"41-61","quality_controlled":"1","scopus_import":1,"publication_identifier":{"eissn":["23987340"]},"article_processing_charge":"No","type":"conference","file_date_updated":"2020-07-14T12:48:00Z","language":[{"iso":"eng"}],"publisher":"EasyChair Publications","doi":"10.29007/m75b","author":[{"last_name":"Immler","full_name":"Immler, Fabian","first_name":"Fabian"},{"last_name":"Althoff","first_name":"Matthias","full_name":"Althoff, Matthias"},{"last_name":"Benet","full_name":"Benet, Luis","first_name":"Luis"},{"first_name":"Alexandre","full_name":"Chapoutot, Alexandre","last_name":"Chapoutot"},{"full_name":"Chen, Xin","first_name":"Xin","last_name":"Chen"},{"last_name":"Forets","first_name":"Marcelo","full_name":"Forets, Marcelo"},{"full_name":"Geretti, Luca","first_name":"Luca","last_name":"Geretti"},{"full_name":"Kochdumper, Niklas","first_name":"Niklas","last_name":"Kochdumper"},{"last_name":"Sanders","first_name":"David P.","full_name":"Sanders, David P."},{"id":"3A2F4DCE-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-3658-1065","full_name":"Schilling, Christian","first_name":"Christian","last_name":"Schilling"}],"ddc":["000"],"publication":"EPiC Series in Computing","date_published":"2019-05-25T00:00:00Z","conference":{"start_date":"2019-04-15","name":"ARCH: International Workshop on Applied Verification on Continuous and Hybrid Systems","end_date":"2019-04-15","location":"Montreal, Canada"},"oa_version":"Published Version","abstract":[{"text":"We present the results of a friendly competition for formal verification of continuous and hybrid systems with nonlinear continuous dynamics. The friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in 2019. In this year, 6 tools Ariadne, CORA, DynIbex, Flow*, Isabelle/HOL, and JuliaReach (in alphabetic order) participated. They are applied to solve reachability analysis problems on four benchmark problems, one of them with hybrid dynamics. We do not rank the tools based on the results, but show the current status and discover the potential advantages of different tools.","lang":"eng"}],"status":"public","citation":{"short":"F. Immler, M. Althoff, L. Benet, A. Chapoutot, X. Chen, M. Forets, L. Geretti, N. Kochdumper, D.P. Sanders, C. Schilling, in:, EPiC Series in Computing, EasyChair Publications, 2019, pp. 41–61.","ama":"Immler F, Althoff M, Benet L, et al. ARCH-COMP19 Category Report: Continuous and hybrid systems with nonlinear dynamics. In: EPiC Series in Computing. Vol 61. EasyChair Publications; 2019:41-61. doi:10.29007/m75b","apa":"Immler, F., Althoff, M., Benet, L., Chapoutot, A., Chen, X., Forets, M., … Schilling, C. (2019). ARCH-COMP19 Category Report: Continuous and hybrid systems with nonlinear dynamics. In EPiC Series in Computing (Vol. 61, pp. 41–61). Montreal, Canada: EasyChair Publications. https://doi.org/10.29007/m75b","chicago":"Immler, Fabian, Matthias Althoff, Luis Benet, Alexandre Chapoutot, Xin Chen, Marcelo Forets, Luca Geretti, Niklas Kochdumper, David P. Sanders, and Christian Schilling. “ARCH-COMP19 Category Report: Continuous and Hybrid Systems with Nonlinear Dynamics.” In EPiC Series in Computing, 61:41–61. EasyChair Publications, 2019. https://doi.org/10.29007/m75b.","ista":"Immler F, Althoff M, Benet L, Chapoutot A, Chen X, Forets M, Geretti L, Kochdumper N, Sanders DP, Schilling C. 2019. ARCH-COMP19 Category Report: Continuous and hybrid systems with nonlinear dynamics. EPiC Series in Computing. ARCH: International Workshop on Applied Verification on Continuous and Hybrid Systems vol. 61, 41–61.","mla":"Immler, Fabian, et al. “ARCH-COMP19 Category Report: Continuous and Hybrid Systems with Nonlinear Dynamics.” EPiC Series in Computing, vol. 61, EasyChair Publications, 2019, pp. 41–61, doi:10.29007/m75b.","ieee":"F. Immler et al., “ARCH-COMP19 Category Report: Continuous and hybrid systems with nonlinear dynamics,” in EPiC Series in Computing, Montreal, Canada, 2019, vol. 61, pp. 41–61."},"intvolume":" 61","has_accepted_license":"1","day":"25","publication_status":"published","oa":1,"title":"ARCH-COMP19 Category Report: Continuous and hybrid systems with nonlinear dynamics","_id":"7576","month":"05","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","department":[{"_id":"ToHe"}]},{"ddc":["000"],"author":[{"orcid":"0000-0002-0686-0365","id":"369D9A44-F248-11E8-B48F-1D18A9856A87","first_name":"Sergiy","full_name":"Bogomolov, Sergiy","last_name":"Bogomolov"},{"last_name":"Forets","first_name":"Marcelo","full_name":"Forets, Marcelo"},{"first_name":"Goran","full_name":"Frehse, Goran","last_name":"Frehse"},{"full_name":"Potomkin, Kostiantyn","first_name":"Kostiantyn","last_name":"Potomkin"},{"orcid":"0000-0003-3658-1065","id":"3A2F4DCE-F248-11E8-B48F-1D18A9856A87","last_name":"Schilling","first_name":"Christian","full_name":"Schilling, Christian"}],"publication":"Proceedings of the 22nd International Conference on Hybrid Systems: Computation and Control","date_published":"2019-04-16T00:00:00Z","oa_version":"Submitted Version","external_id":{"arxiv":["1901.10736"],"isi":["000516713900005"]},"conference":{"location":"Montreal, QC, Canada","end_date":"2019-04-18","name":"HSCC: Hybrid Systems Computation and Control","start_date":"2019-04-16"},"file_date_updated":"2020-07-14T12:47:17Z","type":"conference","language":[{"iso":"eng"}],"arxiv":1,"publisher":"ACM","doi":"10.1145/3302504.3311804","scopus_import":"1","publication_identifier":{"isbn":["9781450362825"]},"article_processing_charge":"No","volume":22,"file":[{"file_name":"hscc19.pdf","date_updated":"2020-07-14T12:47:17Z","access_level":"open_access","content_type":"application/pdf","date_created":"2019-03-05T09:27:18Z","file_id":"6067","checksum":"28ed56439aea5991c3122d4730fd828f","relation":"main_file","creator":"cschilli","file_size":3784414}],"isi":1,"date_updated":"2023-08-24T14:47:21Z","project":[{"call_identifier":"FWF","grant_number":"Z211","name":"The Wittgenstein Prize","_id":"25F42A32-B435-11E9-9278-68D0E5697425"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","call_identifier":"FWF"},{"call_identifier":"H2020","grant_number":"754411","name":"ISTplus - Postdoctoral Fellowships","_id":"260C2330-B435-11E9-9278-68D0E5697425"}],"page":"39-44","quality_controlled":"1","year":"2019","date_created":"2019-02-18T14:43:28Z","department":[{"_id":"ToHe"}],"title":"JuliaReach: A toolbox for set-based reachability","oa":1,"publication_status":"published","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","_id":"6035","month":"04","citation":{"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","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.","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.","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.","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.","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","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."},"intvolume":" 22","keyword":["reachability analysis","hybrid systems","lazy computation"],"has_accepted_license":"1","day":"16","abstract":[{"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.","lang":"eng"}],"status":"public","ec_funded":1},{"language":[{"iso":"eng"}],"type":"conference","file_date_updated":"2020-07-14T12:47:17Z","doi":"10.1007/978-3-030-17462-0_13","publisher":"Springer Nature","publication":"25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems ","author":[{"last_name":"Christakis","full_name":"Christakis, Maria","first_name":"Maria"},{"full_name":"Heizmann, Matthias","first_name":"Matthias","last_name":"Heizmann"},{"last_name":"Mansur","first_name":"Muhammad Numair","full_name":"Mansur, Muhammad Numair"},{"last_name":"Schilling","first_name":"Christian","full_name":"Schilling, Christian","id":"3A2F4DCE-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-3658-1065"},{"last_name":"Wüstholz","first_name":"Valentin","full_name":"Wüstholz, Valentin"}],"ddc":["000"],"conference":{"start_date":"2019-04-06","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","end_date":"2019-04-11","location":"Prague, Czech Republic"},"external_id":{"isi":["000681166500013"]},"oa_version":"Published Version","date_published":"2019-04-04T00:00:00Z","isi":1,"file":[{"file_name":"2019_LNCS_Christakis.pdf","date_created":"2019-05-10T14:16:05Z","content_type":"application/pdf","file_id":"6408","date_updated":"2020-07-14T12:47:17Z","access_level":"open_access","relation":"main_file","checksum":"9998496f6fe202c0a19124b4209154c6","file_size":773083,"creator":"dernst"}],"volume":11427,"year":"2019","date_created":"2019-02-18T16:44:06Z","quality_controlled":"1","page":"226-243","project":[{"_id":"260C2330-B435-11E9-9278-68D0E5697425","grant_number":"754411","name":"ISTplus - Postdoctoral Fellowships","call_identifier":"H2020"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize","grant_number":"Z211","call_identifier":"FWF"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"}],"date_updated":"2023-08-24T14:47:45Z","scopus_import":"1","article_processing_charge":"No","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)"},"publication_status":"published","title":"Semantic fault localization and suspiciousness ranking","oa":1,"month":"04","_id":"6042","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","alternative_title":["LNCS"],"department":[{"_id":"ToHe"}],"status":"public","abstract":[{"lang":"eng","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."}],"ec_funded":1,"citation":{"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.","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.","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.","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.","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","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."},"intvolume":" 11427","day":"04","has_accepted_license":"1"},{"language":[{"iso":"eng"}],"file_date_updated":"2020-10-08T17:25:45Z","type":"conference","doi":"10.1145/3302504.3311800","publisher":"ACM","publication":"Proceedings of the 2019 22nd ACM International Conference on Hybrid Systems: Computation and Control","ddc":["000"],"author":[{"last_name":"Ferrere","full_name":"Ferrere, Thomas","first_name":"Thomas","orcid":"0000-0001-5199-3143","id":"40960E6E-F248-11E8-B48F-1D18A9856A87"},{"id":"41BCEE5C-F248-11E8-B48F-1D18A9856A87","last_name":"Nickovic","full_name":"Nickovic, Dejan","first_name":"Dejan"},{"full_name":"Donzé, Alexandre","first_name":"Alexandre","last_name":"Donzé"},{"full_name":"Ito, Hisahiro","first_name":"Hisahiro","last_name":"Ito"},{"first_name":"James","full_name":"Kapinski, James","last_name":"Kapinski"}],"conference":{"end_date":"2019-04-18","location":"Montreal, Canada","start_date":"2019-04-16","name":"HSCC: Hybrid Systems Computation and Control"},"external_id":{"isi":["000516713900007"]},"oa_version":"Submitted Version","date_published":"2019-04-16T00:00:00Z","file":[{"file_size":1055421,"creator":"dernst","relation":"main_file","checksum":"b8e967081e051d1c55ca5d18fb187890","date_created":"2020-10-08T17:25:45Z","content_type":"application/pdf","file_id":"8633","access_level":"open_access","date_updated":"2020-10-08T17:25:45Z","success":1,"file_name":"2019_ACM_Ferrere.pdf"}],"isi":1,"quality_controlled":"1","page":"57-66","date_created":"2019-05-13T08:13:46Z","year":"2019","date_updated":"2023-08-25T10:19:23Z","project":[{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"name":"The Wittgenstein Prize","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"publication_identifier":{"isbn":["9781450362825"]},"scopus_import":"1","article_processing_charge":"No","title":"Interface-aware signal temporal logic","oa":1,"publication_status":"published","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","month":"04","_id":"6428","department":[{"_id":"ToHe"}],"status":"public","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"}],"citation":{"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","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.","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.","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.","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","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.","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."},"day":"16","has_accepted_license":"1"},{"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","month":"07","_id":"6462","oa":1,"title":"Run-time optimization for learned controllers through quantitative games","publication_status":"published","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"alternative_title":["LNCS"],"abstract":[{"lang":"eng","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."}],"status":"public","has_accepted_license":"1","day":"12","intvolume":" 11561","citation":{"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.","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.","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.","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"},"publisher":"Springer","doi":"10.1007/978-3-030-25540-4_36","file_date_updated":"2020-07-14T12:47:31Z","type":"conference","language":[{"iso":"eng"}],"date_published":"2019-07-12T00:00:00Z","conference":{"location":"New York, NY, United States","end_date":"2019-07-18","name":"CAV: Computer Aided Verification","start_date":"2019-07-13"},"oa_version":"Published Version","external_id":{"isi":["000491468000036"]},"ddc":["000"],"author":[{"full_name":"Avni, Guy","first_name":"Guy","last_name":"Avni","orcid":"0000-0001-5588-8287","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Bloem","full_name":"Bloem, Roderick","first_name":"Roderick"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee"},{"orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger"},{"last_name":"Konighofer","full_name":"Konighofer, Bettina","first_name":"Bettina"},{"first_name":"Stefan","full_name":"Pranger, Stefan","last_name":"Pranger"}],"publication":"31st International Conference on Computer-Aided Verification","date_updated":"2023-08-25T10:33:27Z","project":[{"name":"Formal Methods meets Algorithmic Game Theory","grant_number":"M02369","_id":"264B3912-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"name":"The Wittgenstein Prize","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"page":"630-649","quality_controlled":"1","date_created":"2019-05-16T11:22:30Z","year":"2019","volume":11561,"isi":1,"file":[{"relation":"main_file","checksum":"c231579f2485c6fd4df17c9443a4d80b","file_size":659766,"creator":"dernst","file_name":"2019_CAV_Avni.pdf","file_id":"6816","content_type":"application/pdf","date_created":"2019-08-14T09:35:24Z","access_level":"open_access","date_updated":"2020-07-14T12:47:31Z"}],"article_processing_charge":"No","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)"},"scopus_import":"1","publication_identifier":{"isbn":["9783030255398"],"issn":["0302-9743"]}},{"publication":"31st International Conference on Computer-Aided Verification","ddc":["000"],"author":[{"orcid":"0000−0003−2936−5719","id":"4B3207F6-F248-11E8-B48F-1D18A9856A87","last_name":"Garcia Soto","full_name":"Garcia Soto, Miriam","first_name":"Miriam"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger"},{"last_name":"Schilling","full_name":"Schilling, Christian","first_name":"Christian","id":"3A2F4DCE-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-3658-1065"},{"last_name":"Zeleznik","full_name":"Zeleznik, Luka","first_name":"Luka","id":"3ADCA2E4-F248-11E8-B48F-1D18A9856A87"}],"oa_version":"Published Version","external_id":{"isi":["000491468000016"]},"conference":{"start_date":"2019-07-15","name":"CAV: Computer-Aided Verification","end_date":"2019-07-18","location":"New York City, NY, USA"},"date_published":"2019-07-12T00:00:00Z","language":[{"iso":"eng"}],"file_date_updated":"2020-07-14T12:47:32Z","type":"conference","doi":"10.1007/978-3-030-25540-4_16","publisher":"Springer","publication_identifier":{"issn":["0302-9743"],"isbn":["9783030255398"]},"scopus_import":"1","article_processing_charge":"No","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)"},"volume":11561,"isi":1,"file":[{"file_name":"2019_CAV_GarciaSoto.pdf","date_created":"2019-08-14T11:05:30Z","content_type":"application/pdf","file_id":"6817","access_level":"open_access","date_updated":"2020-07-14T12:47:32Z","relation":"main_file","checksum":"1f1d61b83a151031745ef70a501da3d6","file_size":674795,"creator":"dernst"}],"quality_controlled":"1","page":"297-314","year":"2019","date_created":"2019-05-27T07:09:53Z","date_updated":"2023-08-25T10:40:41Z","project":[{"call_identifier":"H2020","_id":"260C2330-B435-11E9-9278-68D0E5697425","name":"ISTplus - Postdoctoral Fellowships","grant_number":"754411"},{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","name":"The Wittgenstein Prize","call_identifier":"FWF"}],"alternative_title":["LNCS"],"department":[{"_id":"ToHe"}],"oa":1,"title":"Membership-based synthesis of linear hybrid automata","publication_status":"published","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","_id":"6493","month":"07","keyword":["Synthesis","Linear hybrid automaton","Membership"],"intvolume":" 11561","citation":{"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.","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","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.","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.","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.","short":"M. Garcia Soto, T.A. Henzinger, C. Schilling, L. Zeleznik, in:, 31st International Conference on Computer-Aided Verification, Springer, 2019, pp. 297–314.","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"},"day":"12","has_accepted_license":"1","status":"public","abstract":[{"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.","lang":"eng"}],"ec_funded":1},{"abstract":[{"text":"In this paper, we address the problem of synthesizing periodic switching controllers for stabilizing a family of linear systems. Our broad approach consists of constructing a finite game graph based on the family of linear systems such that every winning strategy on the game graph corresponds to a stabilizing switching controller for the family of linear systems. The construction of a (finite) game graph, the synthesis of a winning strategy and the extraction of a stabilizing controller are all computationally feasible. We illustrate our method on an example.","lang":"eng"}],"status":"public","article_number":"8715598","has_accepted_license":"1","day":"16","citation":{"short":"A. Kundu, M. Garcia Soto, P. Prabhakar, in:, 5th Indian Control Conference Proceedings, IEEE, 2019.","ama":"Kundu A, Garcia Soto M, Prabhakar P. Formal synthesis of stabilizing controllers for periodically controlled linear switched systems. In: 5th Indian Control Conference Proceedings. IEEE; 2019. doi:10.1109/INDIANCC.2019.8715598","ista":"Kundu A, Garcia Soto M, Prabhakar P. 2019. Formal synthesis of stabilizing controllers for periodically controlled linear switched systems. 5th Indian Control Conference Proceedings. ICC 2019 - Indian Control Conference, 8715598.","apa":"Kundu, A., Garcia Soto, M., & Prabhakar, P. (2019). Formal synthesis of stabilizing controllers for periodically controlled linear switched systems. In 5th Indian Control Conference Proceedings. Delhi, India: IEEE. https://doi.org/10.1109/INDIANCC.2019.8715598","chicago":"Kundu, Atreyee, Miriam Garcia Soto, and Pavithra Prabhakar. “Formal Synthesis of Stabilizing Controllers for Periodically Controlled Linear Switched Systems.” In 5th Indian Control Conference Proceedings. IEEE, 2019. https://doi.org/10.1109/INDIANCC.2019.8715598.","ieee":"A. Kundu, M. Garcia Soto, and P. Prabhakar, “Formal synthesis of stabilizing controllers for periodically controlled linear switched systems,” in 5th Indian Control Conference Proceedings, Delhi, India, 2019.","mla":"Kundu, Atreyee, et al. “Formal Synthesis of Stabilizing Controllers for Periodically Controlled Linear Switched Systems.” 5th Indian Control Conference Proceedings, 8715598, IEEE, 2019, doi:10.1109/INDIANCC.2019.8715598."},"_id":"6565","month":"05","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publication_status":"published","oa":1,"title":"Formal synthesis of stabilizing controllers for periodically controlled linear switched systems","department":[{"_id":"ToHe"}],"project":[{"call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","name":"The Wittgenstein Prize"}],"date_updated":"2021-01-12T08:08:01Z","date_created":"2019-06-17T06:57:33Z","year":"2019","quality_controlled":"1","file":[{"access_level":"open_access","date_updated":"2020-10-21T13:13:49Z","success":1,"file_id":"8687","content_type":"application/pdf","date_created":"2020-10-21T13:13:49Z","file_name":"2019_ICC_Kundu.pdf","creator":"dernst","file_size":396031,"checksum":"d622a91af1e427f6b1e0ba8e18a2b767","relation":"main_file"}],"article_processing_charge":"No","scopus_import":"1","publication_identifier":{"isbn":["978-153866246-5"]},"publisher":"IEEE","doi":"10.1109/INDIANCC.2019.8715598","type":"conference","file_date_updated":"2020-10-21T13:13:49Z","language":[{"iso":"eng"}],"date_published":"2019-05-16T00:00:00Z","conference":{"start_date":"2019-01-09","name":"ICC 2019 - Indian Control Conference","end_date":"2019-01-11","location":"Delhi, India"},"oa_version":"Submitted Version","author":[{"last_name":"Kundu","full_name":"Kundu, Atreyee","first_name":"Atreyee"},{"id":"4B3207F6-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0003−2936−5719","last_name":"Garcia Soto","full_name":"Garcia Soto, Miriam","first_name":"Miriam"},{"last_name":"Prabhakar","full_name":"Prabhakar, Pavithra","first_name":"Pavithra"}],"ddc":["000"],"publication":"5th Indian Control Conference Proceedings"},{"issue":"4","publication":"Journal of the ACM","author":[{"full_name":"Avni, Guy","first_name":"Guy","last_name":"Avni","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-5588-8287"},{"last_name":"Henzinger","full_name":"Henzinger, Thomas A","first_name":"Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"id":"36CBE2E6-F248-11E8-B48F-1D18A9856A87","first_name":"Ventsislav K","full_name":"Chonev, Ventsislav K","last_name":"Chonev"}],"external_id":{"arxiv":["1705.01433"],"isi":["000487714900008"]},"oa_version":"Preprint","date_published":"2019-07-16T00:00:00Z","arxiv":1,"language":[{"iso":"eng"}],"type":"journal_article","doi":"10.1145/3340295","publisher":"ACM","publication_identifier":{"issn":["00045411"],"eissn":["1557735X"]},"main_file_link":[{"url":"https://arxiv.org/abs/1705.01433","open_access":"1"}],"scopus_import":"1","article_processing_charge":"No","isi":1,"volume":66,"date_created":"2019-08-04T21:59:16Z","year":"2019","quality_controlled":"1","project":[{"grant_number":"Z211","name":"The Wittgenstein Prize","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"call_identifier":"FWF","grant_number":"S11402-N23","name":"Rigorous Systems Engineering","_id":"25F2ACDE-B435-11E9-9278-68D0E5697425"},{"_id":"264B3912-B435-11E9-9278-68D0E5697425","grant_number":"M02369","name":"Formal Methods meets Algorithmic Game Theory","call_identifier":"FWF"}],"date_updated":"2023-08-29T07:02:13Z","department":[{"_id":"ToHe"}],"publication_status":"published","title":"Infinite-duration bidding games","oa":1,"related_material":{"record":[{"id":"950","status":"public","relation":"earlier_version"}]},"month":"07","_id":"6752","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","intvolume":" 66","citation":{"short":"G. Avni, T.A. Henzinger, V.K. Chonev, Journal of the ACM 66 (2019).","ama":"Avni G, Henzinger TA, Chonev VK. Infinite-duration bidding games. Journal of the ACM. 2019;66(4). doi:10.1145/3340295","ista":"Avni G, Henzinger TA, Chonev VK. 2019. Infinite-duration bidding games. Journal of the ACM. 66(4), 31.","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.","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","ieee":"G. Avni, T. A. Henzinger, and V. K. Chonev, “Infinite-duration bidding games,” Journal of the ACM, vol. 66, no. 4. ACM, 2019.","mla":"Avni, Guy, et al. “Infinite-Duration Bidding Games.” Journal of the ACM, vol. 66, no. 4, 31, ACM, 2019, doi:10.1145/3340295."},"day":"16","status":"public","article_number":"31","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"}]},{"scopus_import":1,"publication_identifier":{"issn":["0302-9743"],"isbn":["978-303030805-6"]},"file":[{"file_size":436635,"creator":"gavni","relation":"main_file","checksum":"45ebbc709af2b247d28c7c293c01504b","content_type":"application/pdf","date_created":"2019-08-19T07:56:40Z","file_id":"6823","access_level":"open_access","date_updated":"2020-07-14T12:47:41Z","file_name":"prob.pdf"}],"volume":11674,"project":[{"call_identifier":"FWF","grant_number":"M02369","name":"Formal Methods meets Algorithmic Game Theory","_id":"264B3912-B435-11E9-9278-68D0E5697425"},{"_id":"25F2ACDE-B435-11E9-9278-68D0E5697425","grant_number":"S11402-N23","name":"Rigorous Systems Engineering","call_identifier":"FWF"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize","grant_number":"Z211","call_identifier":"FWF"}],"date_updated":"2021-01-12T08:09:12Z","year":"2019","date_created":"2019-08-19T07:58:10Z","quality_controlled":"1","page":"1-12","author":[{"orcid":"0000-0001-5588-8287","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","first_name":"Guy","full_name":"Avni, Guy","last_name":"Avni"},{"first_name":"Thomas A","full_name":"Henzinger, Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000-0003-4783-0389","id":"3B699956-F248-11E8-B48F-1D18A9856A87","last_name":"Ibsen-Jensen","first_name":"Rasmus","full_name":"Ibsen-Jensen, Rasmus"},{"last_name":"Novotny","first_name":"Petr","full_name":"Novotny, Petr"}],"ddc":["000"],"publication":" Proceedings of the 13th International Conference of Reachability Problems","date_published":"2019-09-06T00:00:00Z","conference":{"name":"RP: Reachability Problems","start_date":"2019-09-11","location":"Brussels, Belgium","end_date":"2019-09-13"},"oa_version":"Submitted Version","type":"conference","file_date_updated":"2020-07-14T12:47:41Z","language":[{"iso":"eng"}],"publisher":"Springer","doi":"10.1007/978-3-030-30806-3_1","citation":{"apa":"Avni, G., Henzinger, T. A., Ibsen-Jensen, R., & Novotny, P. (2019). Bidding games on Markov decision processes. In Proceedings of the 13th International Conference of Reachability Problems (Vol. 11674, pp. 1–12). Brussels, Belgium: Springer. https://doi.org/10.1007/978-3-030-30806-3_1","chicago":"Avni, Guy, Thomas A Henzinger, Rasmus Ibsen-Jensen, and Petr Novotny. “Bidding Games on Markov Decision Processes.” In Proceedings of the 13th International Conference of Reachability Problems, 11674:1–12. Springer, 2019. https://doi.org/10.1007/978-3-030-30806-3_1.","ista":"Avni G, Henzinger TA, Ibsen-Jensen R, Novotny P. 2019. Bidding games on Markov decision processes. Proceedings of the 13th International Conference of Reachability Problems. RP: Reachability Problems, LNCS, vol. 11674, 1–12.","mla":"Avni, Guy, et al. “Bidding Games on Markov Decision Processes.” Proceedings of the 13th International Conference of Reachability Problems, vol. 11674, Springer, 2019, pp. 1–12, doi:10.1007/978-3-030-30806-3_1.","ieee":"G. Avni, T. A. Henzinger, R. Ibsen-Jensen, and P. Novotny, “Bidding games on Markov decision processes,” in Proceedings of the 13th International Conference of Reachability Problems, Brussels, Belgium, 2019, vol. 11674, pp. 1–12.","short":"G. Avni, T.A. Henzinger, R. Ibsen-Jensen, P. Novotny, in:, Proceedings of the 13th International Conference of Reachability Problems, Springer, 2019, pp. 1–12.","ama":"Avni G, Henzinger TA, Ibsen-Jensen R, Novotny P. Bidding games on Markov decision processes. In: Proceedings of the 13th International Conference of Reachability Problems. Vol 11674. Springer; 2019:1-12. doi:10.1007/978-3-030-30806-3_1"},"intvolume":" 11674","has_accepted_license":"1","day":"06","abstract":[{"lang":"eng","text":"In two-player games on graphs, the players move a token through a graph to produce an infinite path, which determines the qualitative winner or quantitative payoff of the game. In bidding games, in each turn, we hold an auction between the two players to determine which player moves the token. Bidding games have largely been studied with concrete bidding mechanisms that are variants of a first-price auction: in each turn both players simultaneously submit bids, the higher\r\nbidder moves the token, and pays his bid to the lower bidder in Richman bidding, to the bank in poorman bidding, and in taxman bidding, the bid is split between the other player and the bank according to a predefined constant factor. Bidding games are deterministic games. They have an intriguing connection with a fragment of stochastic games called \r\n randomturn games. We study, for the first time, a combination of bidding games with probabilistic behavior; namely, we study bidding games that are played on Markov decision processes, where the players bid for the right to choose the next action, which determines the probability distribution according to which the next vertex is chosen. We study parity and meanpayoff bidding games on MDPs and extend results from the deterministic bidding setting to the probabilistic one."}],"status":"public","alternative_title":["LNCS"],"department":[{"_id":"ToHe"}],"publication_status":"published","title":"Bidding games on Markov decision processes","oa":1,"_id":"6822","month":"09","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87"},{"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)"},"scopus_import":1,"date_updated":"2023-08-07T14:08:34Z","project":[{"name":"International IST Doctoral Program","grant_number":"665385","_id":"2564DBCA-B435-11E9-9278-68D0E5697425","call_identifier":"H2020"},{"call_identifier":"FWF","_id":"264B3912-B435-11E9-9278-68D0E5697425","grant_number":"M02369","name":"Formal Methods meets Algorithmic Game Theory"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","name":"The Wittgenstein Prize"},{"call_identifier":"FWF","_id":"25F2ACDE-B435-11E9-9278-68D0E5697425","grant_number":"S11402-N23","name":"Rigorous Systems Engineering"}],"quality_controlled":"1","year":"2019","date_created":"2019-09-18T08:04:26Z","volume":138,"file":[{"date_created":"2019-09-27T11:45:15Z","file_id":"6913","content_type":"application/pdf","access_level":"open_access","date_updated":"2020-07-14T12:47:42Z","file_name":"2019_LIPIcs_Avni.pdf","file_size":554457,"creator":"kschuh","relation":"main_file","checksum":"6346e116a4f4ed1414174d96d2c4fbd7"}],"date_published":"2019-08-01T00:00:00Z","conference":{"end_date":"2019-08-30","location":"Aachen, Germany","start_date":"2019-08-26","name":"MFCS: nternational Symposium on Mathematical Foundations of Computer Science"},"oa_version":"Published Version","external_id":{"arxiv":["1905.03835"]},"ddc":["004"],"author":[{"id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-5588-8287","first_name":"Guy","full_name":"Avni, Guy","last_name":"Avni"},{"orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","full_name":"Henzinger, Thomas A","first_name":"Thomas A"},{"id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","last_name":"Zikelic","full_name":"Zikelic, Dorde","first_name":"Dorde"}],"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","doi":"10.4230/LIPICS.MFCS.2019.11","file_date_updated":"2020-07-14T12:47:42Z","type":"conference","language":[{"iso":"eng"}],"arxiv":1,"has_accepted_license":"1","day":"01","citation":{"short":"G. Avni, T.A. Henzinger, D. Zikelic, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019.","ama":"Avni G, Henzinger TA, Zikelic D. Bidding mechanisms in graph games. In: Vol 138. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2019. doi:10.4230/LIPICS.MFCS.2019.11","ista":"Avni G, Henzinger TA, Zikelic D. 2019. Bidding mechanisms in graph games. MFCS: nternational Symposium on Mathematical Foundations of Computer Science, LIPIcs, vol. 138, 11.","apa":"Avni, G., Henzinger, T. A., & Zikelic, D. (2019). Bidding mechanisms in graph games (Vol. 138). Presented at the MFCS: nternational Symposium on Mathematical Foundations of Computer Science, Aachen, Germany: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPICS.MFCS.2019.11","chicago":"Avni, Guy, Thomas A Henzinger, and Dorde Zikelic. “Bidding Mechanisms in Graph Games,” Vol. 138. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. https://doi.org/10.4230/LIPICS.MFCS.2019.11.","ieee":"G. Avni, T. A. Henzinger, and D. Zikelic, “Bidding mechanisms in graph games,” presented at the MFCS: nternational Symposium on Mathematical Foundations of Computer Science, Aachen, Germany, 2019, vol. 138.","mla":"Avni, Guy, et al. Bidding Mechanisms in Graph Games. Vol. 138, 11, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019, doi:10.4230/LIPICS.MFCS.2019.11."},"intvolume":" 138","ec_funded":1,"abstract":[{"text":"In two-player games on graphs, the players move a token through a graph to produce a finite or infinite path, which determines the qualitative winner or quantitative payoff of the game. We study bidding games in which the players bid for the right to move the token. Several bidding rules were studied previously. In Richman bidding, in each round, the players simultaneously submit bids, and the higher bidder moves the token and pays the other player. Poorman bidding is similar except that the winner of the bidding pays the \"bank\" rather than the other player. Taxman bidding spans the spectrum between Richman and poorman bidding. They are parameterized by a constant tau in [0,1]: portion tau of the winning bid is paid to the other player, and portion 1-tau to the bank. While finite-duration (reachability) taxman games have been studied before, we present, for the first time, results on infinite-duration taxman games. It was previously shown that both Richman and poorman infinite-duration games with qualitative objectives reduce to reachability games, and we show a similar result here. Our most interesting results concern quantitative taxman games, namely mean-payoff games, where poorman and Richman bidding differ significantly. A central quantity in these games is the ratio between the two players' initial budgets. While in poorman mean-payoff games, the optimal payoff of a player depends on the initial ratio, in Richman bidding, the payoff depends only on the structure of the game. In both games the optimal payoffs can be found using (different) probabilistic connections with random-turn games in which in each turn, instead of bidding, a coin is tossed to determine which player moves. While the value with Richman bidding equals the value of a random-turn game with an un-biased coin, with poorman bidding, the bias in the coin is the initial ratio of the budgets. We give a complete classification of mean-payoff taxman games that is based on a probabilistic connection: the value of a taxman bidding game with parameter tau and initial ratio r, equals the value of a random-turn game that uses a coin with bias F(tau, r) = (r+tau * (1-r))/(1+tau). Thus, we show that Richman bidding is the exception; namely, for every tau <1, the value of the game depends on the initial ratio. Our proof technique simplifies and unifies the previous proof techniques for both Richman and poorman bidding. ","lang":"eng"}],"article_number":"11","status":"public","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"alternative_title":["LIPIcs"],"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","month":"08","_id":"6884","title":"Bidding mechanisms in graph games","oa":1,"related_material":{"record":[{"status":"public","relation":"later_version","id":"9239"}]},"publication_status":"published"},{"year":"2019","date_created":"2019-09-18T08:06:14Z","quality_controlled":"1","project":[{"_id":"25863FF4-B435-11E9-9278-68D0E5697425","name":"Game Theory","grant_number":"S11407","call_identifier":"FWF"},{"call_identifier":"FWF","_id":"25F2ACDE-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S11402-N23"}],"date_updated":"2021-01-12T08:09:27Z","file":[{"file_size":538120,"creator":"kschuh","relation":"main_file","checksum":"4985e26e1572d1575d64d38acabd71d6","content_type":"application/pdf","date_created":"2019-09-27T12:09:35Z","file_id":"6914","access_level":"open_access","date_updated":"2020-07-14T12:47:43Z","file_name":"2019_LIPIcs_Chatterjee.pdf"}],"volume":140,"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)"},"scopus_import":1,"doi":"10.4230/LIPICS.CONCUR.2019.27","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","language":[{"iso":"eng"}],"type":"conference","file_date_updated":"2020-07-14T12:47:43Z","conference":{"start_date":"2019-08-27","name":"CONCUR: International Conference on Concurrency Theory","end_date":"2019-08-30","location":"Amsterdam, Netherlands"},"oa_version":"Published Version","date_published":"2019-08-01T00:00:00Z","author":[{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu"},{"first_name":"Thomas A","full_name":"Henzinger, Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"},{"full_name":"Otop, Jan","first_name":"Jan","last_name":"Otop"}],"ddc":["000"],"status":"public","article_number":"27","abstract":[{"lang":"eng","text":"A vector addition system with states (VASS) consists of a finite set of states and counters. A configuration is a state and a value for each counter; a transition changes the state and each counter is incremented, decremented, or left unchanged. While qualitative properties such as state and configuration reachability have been studied for VASS, we consider the long-run average cost of infinite computations of VASS. The cost of a configuration is for each state, a linear combination of the counter values. In the special case of uniform cost functions, the linear combination is the same for all states. The (regular) long-run emptiness problem is, given a VASS, a cost function, and a threshold value, if there is a (lasso-shaped) computation such that the long-run average value of the cost function does not exceed the threshold. For uniform cost functions, we show that the regular long-run emptiness problem is (a) decidable in polynomial time for integer-valued VASS, and (b) decidable but nonelementarily hard for natural-valued VASS (i.e., nonnegative counters). For general cost functions, we show that the problem is (c) NP-complete for integer-valued VASS, and (d) undecidable for natural-valued VASS. Our most interesting result is for (c) integer-valued VASS with general cost functions, where we establish a connection between the regular long-run emptiness problem and quadratic Diophantine inequalities. The general (nonregular) long-run emptiness problem is equally hard as the regular problem in all cases except (c), where it remains open. "}],"day":"01","has_accepted_license":"1","intvolume":" 140","citation":{"ama":"Chatterjee K, Henzinger TA, Otop J. Long-run average behavior of vector addition systems with states. In: Vol 140. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2019. doi:10.4230/LIPICS.CONCUR.2019.27","short":"K. Chatterjee, T.A. Henzinger, J. Otop, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019.","mla":"Chatterjee, Krishnendu, et al. Long-Run Average Behavior of Vector Addition Systems with States. Vol. 140, 27, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019, doi:10.4230/LIPICS.CONCUR.2019.27.","ieee":"K. Chatterjee, T. A. Henzinger, and J. Otop, “Long-run average behavior of vector addition systems with states,” presented at the CONCUR: International Conference on Concurrency Theory, Amsterdam, Netherlands, 2019, vol. 140.","apa":"Chatterjee, K., Henzinger, T. A., & Otop, J. (2019). Long-run average behavior of vector addition systems with states (Vol. 140). Presented at the CONCUR: International Conference on Concurrency Theory, Amsterdam, Netherlands: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPICS.CONCUR.2019.27","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. “Long-Run Average Behavior of Vector Addition Systems with States,” Vol. 140. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. https://doi.org/10.4230/LIPICS.CONCUR.2019.27.","ista":"Chatterjee K, Henzinger TA, Otop J. 2019. Long-run average behavior of vector addition systems with states. CONCUR: International Conference on Concurrency Theory, LIPIcs, vol. 140, 27."},"month":"08","_id":"6885","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","publication_status":"published","title":"Long-run average behavior of vector addition systems with states","oa":1,"department":[{"_id":"ToHe"},{"_id":"KrCh"}],"alternative_title":["LIPIcs"]},{"has_accepted_license":"1","day":"01","intvolume":" 140","citation":{"chicago":"Aghajohari, Milad, Guy Avni, and Thomas A Henzinger. “Determinacy in Discrete-Bidding Infinite-Duration Games,” Vol. 140. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. https://doi.org/10.4230/LIPICS.CONCUR.2019.20.","ista":"Aghajohari M, Avni G, Henzinger TA. 2019. Determinacy in discrete-bidding infinite-duration games. CONCUR: International Conference on Concurrency Theory, LIPIcs, vol. 140, 20.","apa":"Aghajohari, M., Avni, G., & Henzinger, T. A. (2019). Determinacy in discrete-bidding infinite-duration games (Vol. 140). Presented at the CONCUR: International Conference on Concurrency Theory, Amsterdam, Netherlands: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPICS.CONCUR.2019.20","mla":"Aghajohari, Milad, et al. Determinacy in Discrete-Bidding Infinite-Duration Games. Vol. 140, 20, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019, doi:10.4230/LIPICS.CONCUR.2019.20.","ieee":"M. Aghajohari, G. Avni, and T. A. Henzinger, “Determinacy in discrete-bidding infinite-duration games,” presented at the CONCUR: International Conference on Concurrency Theory, Amsterdam, Netherlands, 2019, vol. 140.","short":"M. Aghajohari, G. Avni, T.A. Henzinger, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019.","ama":"Aghajohari M, Avni G, Henzinger TA. Determinacy in discrete-bidding infinite-duration games. In: Vol 140. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2019. doi:10.4230/LIPICS.CONCUR.2019.20"},"abstract":[{"text":"In two-player games on graphs, the players move a token through a graph to produce an infinite path, which determines the winner of the game. Such games are central in formal methods since they model the interaction between a non-terminating system and its environment. In bidding games the players bid for the right to move the token: in each round, the players simultaneously submit bids, and the higher bidder moves the token and pays the other player. Bidding games are known to have a clean and elegant mathematical structure that relies on the ability of the players to submit arbitrarily small bids. Many applications, however, require a fixed granularity for the bids, which can represent, for example, the monetary value expressed in cents. We study, for the first time, the combination of discrete-bidding and infinite-duration games. Our most important result proves that these games form a large determined subclass of concurrent games, where determinacy is the strong property that there always exists exactly one player who can guarantee winning the game. In particular, we show that, in contrast to non-discrete bidding games, the mechanism with which tied bids are resolved plays an important role in discrete-bidding games. We study several natural tie-breaking mechanisms and show that, while some do not admit determinacy, most natural mechanisms imply determinacy for every pair of initial budgets. ","lang":"eng"}],"article_number":"20","status":"public","department":[{"_id":"ToHe"}],"alternative_title":["LIPIcs"],"user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","month":"08","_id":"6886","oa":1,"title":"Determinacy in discrete-bidding infinite-duration games","publication_status":"published","article_processing_charge":"No","tmp":{"short":"CC BY (3.0)","legal_code_url":"https://creativecommons.org/licenses/by/3.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 3.0 Unported (CC BY 3.0)"},"scopus_import":"1","date_updated":"2022-01-26T08:27:10Z","project":[{"_id":"25F2ACDE-B435-11E9-9278-68D0E5697425","grant_number":"S11402-N23","name":"Rigorous Systems Engineering","call_identifier":"FWF"},{"grant_number":"M02369","name":"Formal Methods meets Algorithmic Game Theory","_id":"264B3912-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"quality_controlled":"1","year":"2019","date_created":"2019-09-18T08:06:58Z","volume":140,"file":[{"access_level":"open_access","date_updated":"2020-07-14T12:47:43Z","date_created":"2019-09-27T12:21:38Z","file_id":"6915","content_type":"application/pdf","file_name":"2019_LIPIcs_Aghajohari.pdf","creator":"kschuh","file_size":741425,"checksum":"4df6d3575c506edb17215adada03cc8e","relation":"main_file"}],"date_published":"2019-08-01T00:00:00Z","license":"https://creativecommons.org/licenses/by/3.0/","external_id":{"arxiv":["1905.03588"]},"oa_version":"Published Version","conference":{"location":"Amsterdam, Netherlands","end_date":"2019-08-30","name":"CONCUR: International Conference on Concurrency Theory","start_date":"2019-08-27"},"ddc":["000"],"author":[{"last_name":"Aghajohari","first_name":"Milad","full_name":"Aghajohari, Milad"},{"id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-5588-8287","full_name":"Avni, Guy","first_name":"Guy","last_name":"Avni"},{"orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger"}],"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","doi":"10.4230/LIPICS.CONCUR.2019.20","file_date_updated":"2020-07-14T12:47:43Z","type":"conference","arxiv":1,"language":[{"iso":"eng"}]},{"doi":"10.1109/icra.2019.8793840","publisher":"IEEE","language":[{"iso":"eng"}],"file_date_updated":"2020-10-08T17:30:38Z","type":"conference","oa_version":"Submitted Version","conference":{"start_date":"2019-05-20","name":"ICRA: International Conference on Robotics and Automation","end_date":"2019-05-24","location":"Montreal, QC, Canada"},"date_published":"2019-05-01T00:00:00Z","publication":"Proceedings - IEEE International Conference on Robotics and Automation","ddc":["000"],"author":[{"id":"3DC22916-F248-11E8-B48F-1D18A9856A87","first_name":"Mathias","full_name":"Lechner, Mathias","last_name":"Lechner"},{"last_name":"Hasani","full_name":"Hasani, Ramin","first_name":"Ramin"},{"last_name":"Zimmer","full_name":"Zimmer, Manuel","first_name":"Manuel"},{"first_name":"Thomas A","full_name":"Henzinger, Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Radu","full_name":"Grosu, Radu","last_name":"Grosu"}],"quality_controlled":"1","date_created":"2019-09-18T08:09:51Z","year":"2019","date_updated":"2021-01-12T08:09:28Z","project":[{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","name":"The Wittgenstein Prize"}],"volume":"2019-May","file":[{"file_id":"8636","content_type":"application/pdf","date_created":"2020-10-08T17:30:38Z","date_updated":"2020-10-08T17:30:38Z","access_level":"open_access","success":1,"file_name":"2019_ICRA_Lechner.pdf","file_size":3265107,"creator":"dernst","relation":"main_file","checksum":"f5545a6b60c3ffd01feb3613f81d03b6"}],"article_processing_charge":"No","publication_identifier":{"isbn":["9781538660270"]},"scopus_import":"1","user_id":"D865714E-FA4E-11E9-B85B-F5C5E5697425","_id":"6888","month":"05","oa":1,"title":"Designing worm-inspired neural networks for interpretable robotic control","publication_status":"published","department":[{"_id":"ToHe"}],"alternative_title":["ICRA"],"article_number":"8793840","status":"public","abstract":[{"lang":"eng","text":"In this paper, we design novel liquid time-constant recurrent neural networks for robotic control, inspired by the brain of the nematode, C. elegans. In the worm's nervous system, neurons communicate through nonlinear time-varying synaptic links established amongst them by their particular wiring structure. This property enables neurons to express liquid time-constants dynamics and therefore allows the network to originate complex behaviors with a small number of neurons. We identify neuron-pair communication motifs as design operators and use them to configure compact neuronal network structures to govern sequential robotic tasks. The networks are systematically designed to map the environmental observations to motor actions, by their hierarchical topology from sensory neurons, through recurrently-wired interneurons, to motor neurons. The networks are then parametrized in a supervised-learning scheme by a search-based algorithm. We demonstrate that obtained networks realize interpretable dynamics. We evaluate their performance in controlling mobile and arm robots, and compare their attributes to other artificial neural network-based control agents. Finally, we experimentally show their superior resilience to environmental noise, compared to the existing machine learning-based methods."}],"day":"01","has_accepted_license":"1","citation":{"ieee":"M. Lechner, R. Hasani, M. Zimmer, T. A. Henzinger, and R. Grosu, “Designing worm-inspired neural networks for interpretable robotic control,” in Proceedings - IEEE International Conference on Robotics and Automation, Montreal, QC, Canada, 2019, vol. 2019–May.","mla":"Lechner, Mathias, et al. “Designing Worm-Inspired Neural Networks for Interpretable Robotic Control.” Proceedings - IEEE International Conference on Robotics and Automation, vol. 2019–May, 8793840, IEEE, 2019, doi:10.1109/icra.2019.8793840.","chicago":"Lechner, Mathias, Ramin Hasani, Manuel Zimmer, Thomas A Henzinger, and Radu Grosu. “Designing Worm-Inspired Neural Networks for Interpretable Robotic Control.” In Proceedings - IEEE International Conference on Robotics and Automation, Vol. 2019–May. IEEE, 2019. https://doi.org/10.1109/icra.2019.8793840.","ista":"Lechner M, Hasani R, Zimmer M, Henzinger TA, Grosu R. 2019. Designing worm-inspired neural networks for interpretable robotic control. Proceedings - IEEE International Conference on Robotics and Automation. ICRA: International Conference on Robotics and Automation, ICRA, vol. 2019–May, 8793840.","apa":"Lechner, M., Hasani, R., Zimmer, M., Henzinger, T. A., & Grosu, R. (2019). Designing worm-inspired neural networks for interpretable robotic control. In Proceedings - IEEE International Conference on Robotics and Automation (Vol. 2019–May). Montreal, QC, Canada: IEEE. https://doi.org/10.1109/icra.2019.8793840","ama":"Lechner M, Hasani R, Zimmer M, Henzinger TA, Grosu R. Designing worm-inspired neural networks for interpretable robotic control. In: Proceedings - IEEE International Conference on Robotics and Automation. Vol 2019-May. IEEE; 2019. doi:10.1109/icra.2019.8793840","short":"M. Lechner, R. Hasani, M. Zimmer, T.A. Henzinger, R. Grosu, in:, Proceedings - IEEE International Conference on Robotics and Automation, IEEE, 2019."}},{"degree_awarded":"PhD","status":"public","abstract":[{"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.","lang":"eng"}],"day":"30","has_accepted_license":"1","supervisor":[{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A","full_name":"Henzinger, Thomas A","last_name":"Henzinger"}],"citation":{"ama":"Giacobbe M. Automatic time-unbounded reachability analysis of hybrid systems. 2019. doi: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.","ista":"Giacobbe M. 2019. Automatic time-unbounded reachability analysis of hybrid systems. Institute of Science and Technology Austria.","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","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."},"_id":"6894","month":"09","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","publication_status":"published","title":"Automatic time-unbounded reachability analysis of hybrid systems","related_material":{"record":[{"relation":"part_of_dissertation","status":"public","id":"631"},{"status":"public","relation":"part_of_dissertation","id":"647"},{"status":"public","relation":"part_of_dissertation","id":"140"}]},"oa":1,"department":[{"_id":"ToHe"}],"alternative_title":["ISTA Thesis"],"year":"2019","date_created":"2019-09-22T14:08:44Z","page":"132","date_updated":"2023-09-19T09:30:43Z","file":[{"checksum":"773beaf4a85dc2acc2c12b578fbe1965","relation":"main_file","creator":"mgiacobbe","file_size":4100685,"file_name":"giacobbe_thesis.pdf","date_updated":"2020-07-14T12:47:43Z","access_level":"open_access","date_created":"2019-09-27T14:15:05Z","file_id":"6916","content_type":"application/pdf"},{"creator":"mgiacobbe","file_size":7959732,"checksum":"97f1c3da71feefd27e6e625d32b4c75b","relation":"source_file","date_updated":"2020-07-14T12:47:43Z","access_level":"closed","content_type":"application/gzip","file_id":"6917","date_created":"2019-09-27T14:22:04Z","file_name":"giacobbe_thesis_src.tar.gz"}],"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)"},"article_processing_charge":"No","publication_identifier":{"eissn":["2663-337X"]},"doi":"10.15479/AT:ISTA:6894","publisher":"Institute of Science and Technology Austria","language":[{"iso":"eng"}],"type":"dissertation","file_date_updated":"2020-07-14T12:47:43Z","oa_version":"Published Version","date_published":"2019-09-30T00:00:00Z","author":[{"last_name":"Giacobbe","first_name":"Mirco","full_name":"Giacobbe, Mirco","orcid":"0000-0001-8180-0904","id":"3444EA5E-F248-11E8-B48F-1D18A9856A87"}],"ddc":["000"]},{"file":[{"success":1,"access_level":"open_access","date_updated":"2022-05-17T06:55:49Z","file_id":"11391","date_created":"2022-05-17T06:55:49Z","content_type":"application/pdf","file_name":"2019_EPiCs_Frehse.pdf","creator":"dernst","file_size":346415,"checksum":"4b92e333db7b4e2349501a804dfede69","relation":"main_file"}],"volume":61,"year":"2019","date_created":"2022-03-18T12:29:23Z","page":"1-13","quality_controlled":"1","date_updated":"2022-05-17T07:09:47Z","publication_identifier":{"issn":["2398-7340"]},"scopus_import":"1","article_processing_charge":"No","language":[{"iso":"eng"}],"type":"conference","file_date_updated":"2022-05-17T06:55:49Z","doi":"10.29007/rjwn","publisher":"EasyChair","publication":"ARCH19. 6th International Workshop on Applied Verification of Continuous and Hybrid Systems","author":[{"full_name":"Frehse, Goran","first_name":"Goran","last_name":"Frehse"},{"full_name":"Abate, Alessandro","first_name":"Alessandro","last_name":"Abate"},{"full_name":"Adzkiya, Dieky","first_name":"Dieky","last_name":"Adzkiya"},{"last_name":"Becchi","first_name":"Anna","full_name":"Becchi, Anna"},{"first_name":"Lei","full_name":"Bu, Lei","last_name":"Bu"},{"full_name":"Cimatti, Alessandro","first_name":"Alessandro","last_name":"Cimatti"},{"orcid":"0000-0001-8180-0904","id":"3444EA5E-F248-11E8-B48F-1D18A9856A87","first_name":"Mirco","full_name":"Giacobbe, Mirco","last_name":"Giacobbe"},{"full_name":"Griggio, Alberto","first_name":"Alberto","last_name":"Griggio"},{"first_name":"Sergio","full_name":"Mover, Sergio","last_name":"Mover"},{"last_name":"Mufid","full_name":"Mufid, Muhammad Syifa'ul","first_name":"Muhammad Syifa'ul"},{"first_name":"Idriss","full_name":"Riouak, Idriss","last_name":"Riouak"},{"last_name":"Tonetta","first_name":"Stefano","full_name":"Tonetta, Stefano"},{"last_name":"Zaffanella","full_name":"Zaffanella, Enea","first_name":"Enea"}],"ddc":["000"],"conference":{"start_date":"2019-04-15","name":"ARCH: International Workshop on Applied Verification on Continuous and Hybrid Systems","end_date":"2019-04-15","location":"Montreal, Canada"},"oa_version":"Published Version","date_published":"2019-05-25T00:00:00Z","status":"public","abstract":[{"lang":"eng","text":"This report presents the results of a friendly competition for formal verification of continuous and hybrid systems with piecewise constant dynamics. The friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in 2019. In this third edition, six tools have been applied to solve five different benchmark problems in the category for piecewise constant dynamics: BACH, Lyse, Hy- COMP, PHAVer/SX, PHAVerLite, and VeriSiMPL. Compared to last year, a new tool has participated (HyCOMP) and PHAVerLite has replaced PHAVer-lite. The result is a snap- shot of the current landscape of tools and the types of benchmarks they are particularly suited for. Due to the diversity of problems, we are not ranking tools, yet the presented results probably provide the most complete assessment of tools for the safety verification of continuous and hybrid systems with piecewise constant dynamics up to this date."}],"editor":[{"full_name":"Frehse, Goran","first_name":"Goran","last_name":"Frehse"},{"last_name":"Althoff","full_name":"Althoff, Matthias","first_name":"Matthias"}],"intvolume":" 61","citation":{"chicago":"Frehse, Goran, Alessandro Abate, Dieky Adzkiya, Anna Becchi, Lei Bu, Alessandro Cimatti, Mirco Giacobbe, et al. “ARCH-COMP19 Category Report: Hybrid Systems with Piecewise Constant Dynamics.” In ARCH19. 6th International Workshop on Applied Verification of Continuous and Hybrid Systems, edited by Goran Frehse and Matthias Althoff, 61:1–13. EasyChair, 2019. https://doi.org/10.29007/rjwn.","ista":"Frehse G, Abate A, Adzkiya D, Becchi A, Bu L, Cimatti A, Giacobbe M, Griggio A, Mover S, Mufid MS, Riouak I, Tonetta S, Zaffanella E. 2019. ARCH-COMP19 Category Report: Hybrid systems with piecewise constant dynamics. ARCH19. 6th International Workshop on Applied Verification of Continuous and Hybrid Systems. ARCH: International Workshop on Applied Verification on Continuous and Hybrid Systems, EPiC Series in Computing, vol. 61, 1–13.","apa":"Frehse, G., Abate, A., Adzkiya, D., Becchi, A., Bu, L., Cimatti, A., … Zaffanella, E. (2019). ARCH-COMP19 Category Report: Hybrid systems with piecewise constant dynamics. In G. Frehse & M. Althoff (Eds.), ARCH19. 6th International Workshop on Applied Verification of Continuous and Hybrid Systems (Vol. 61, pp. 1–13). Montreal, Canada: EasyChair. https://doi.org/10.29007/rjwn","mla":"Frehse, Goran, et al. “ARCH-COMP19 Category Report: Hybrid Systems with Piecewise Constant Dynamics.” ARCH19. 6th International Workshop on Applied Verification of Continuous and Hybrid Systems, edited by Goran Frehse and Matthias Althoff, vol. 61, EasyChair, 2019, pp. 1–13, doi:10.29007/rjwn.","ieee":"G. Frehse et al., “ARCH-COMP19 Category Report: Hybrid systems with piecewise constant dynamics,” in ARCH19. 6th International Workshop on Applied Verification of Continuous and Hybrid Systems, Montreal, Canada, 2019, vol. 61, pp. 1–13.","short":"G. Frehse, A. Abate, D. Adzkiya, A. Becchi, L. Bu, A. Cimatti, M. Giacobbe, A. Griggio, S. Mover, M.S. Mufid, I. Riouak, S. Tonetta, E. Zaffanella, in:, G. Frehse, M. Althoff (Eds.), ARCH19. 6th International Workshop on Applied Verification of Continuous and Hybrid Systems, EasyChair, 2019, pp. 1–13.","ama":"Frehse G, Abate A, Adzkiya D, et al. ARCH-COMP19 Category Report: Hybrid systems with piecewise constant dynamics. In: Frehse G, Althoff M, eds. ARCH19. 6th International Workshop on Applied Verification of Continuous and Hybrid Systems. Vol 61. EasyChair; 2019:1-13. doi:10.29007/rjwn"},"day":"25","has_accepted_license":"1","publication_status":"published","oa":1,"title":"ARCH-COMP19 Category Report: Hybrid systems with piecewise constant dynamics","_id":"10877","month":"05","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","alternative_title":["EPiC Series in Computing"],"acknowledgement":"The authors gratefully acknowledge \fnancial support by the European Commission project\r\nUnCoVerCPS under grant number 643921. Lei Bu is supported by the National Natural Science\r\nFoundation of China (No.61572249).","department":[{"_id":"ToHe"}]},{"publication_status":"published","oa":1,"related_material":{"record":[{"id":"6426","status":"public","relation":"earlier_version"},{"id":"8332","relation":"dissertation_contains","status":"public"}]},"title":"Synchronizing the asynchronous","_id":"133","month":"08","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","alternative_title":["LIPIcs"],"pubrep_id":"1039","department":[{"_id":"ToHe"}],"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"}],"status":"public","article_number":"21","intvolume":" 118","citation":{"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.","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.","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.","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","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","short":"B. Kragl, S. Qadeer, T.A. Henzinger, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018."},"has_accepted_license":"1","day":"13","type":"conference","file_date_updated":"2020-07-14T12:44:44Z","language":[{"iso":"eng"}],"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","doi":"10.4230/LIPIcs.CONCUR.2018.21","author":[{"last_name":"Kragl","first_name":"Bernhard","full_name":"Kragl, Bernhard","orcid":"0000-0001-7745-9117","id":"320FC952-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Qadeer, Shaz","first_name":"Shaz","last_name":"Qadeer"},{"first_name":"Thomas A","full_name":"Henzinger, Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"}],"ddc":["000"],"publist_id":"7790","date_published":"2018-08-13T00:00:00Z","conference":{"start_date":"2018-09-04","name":"CONCUR: International Conference on Concurrency Theory","end_date":"2018-09-07","location":"Beijing, China"},"oa_version":"Published Version","file":[{"date_created":"2018-12-12T10:18:46Z","content_type":"application/pdf","file_id":"5368","date_updated":"2020-07-14T12:44:44Z","access_level":"open_access","file_name":"IST-2018-853-v2+2_concur2018.pdf","file_size":745438,"creator":"system","relation":"main_file","checksum":"c90895f4c5fafc18ddc54d1c8848077e"}],"volume":118,"project":[{"call_identifier":"FWF","_id":"25F2ACDE-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S11402-N23"},{"grant_number":"S11402-N23","name":"Moderne Concurrency Paradigms","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"date_updated":"2023-09-07T13:18:00Z","year":"2018","date_created":"2018-12-11T11:44:48Z","quality_controlled":"1","scopus_import":1,"publication_identifier":{"issn":["18688969"]},"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)"}},{"department":[{"_id":"KrCh"},{"_id":"ToHe"}],"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.","alternative_title":["LNCS"],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"86","month":"07","title":"Computing average response time","oa":1,"publication_status":"published","has_accepted_license":"1","day":"20","citation":{"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.","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.","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","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.","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","short":"K. Chatterjee, T.A. Henzinger, J. Otop, in:, M. Lohstroh, P. Derler, M. Sirjani (Eds.), Principles of Modeling, Springer, 2018, pp. 143–161."},"intvolume":" 10760","ec_funded":1,"editor":[{"full_name":"Lohstroh, Marten","first_name":"Marten","last_name":"Lohstroh"},{"full_name":"Derler, Patricia","first_name":"Patricia","last_name":"Derler"},{"last_name":"Sirjani","first_name":"Marjan","full_name":"Sirjani, Marjan"}],"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"}],"status":"public","date_published":"2018-07-20T00:00:00Z","oa_version":"Submitted Version","ddc":["000"],"author":[{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","last_name":"Otop","first_name":"Jan","full_name":"Otop, Jan"}],"publist_id":"7968","publication":"Principles of Modeling","publisher":"Springer","doi":"10.1007/978-3-319-95246-8_9","file_date_updated":"2020-07-14T12:48:14Z","type":"book_chapter","language":[{"iso":"eng"}],"scopus_import":1,"date_updated":"2021-01-12T08:20:14Z","project":[{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","call_identifier":"FWF"},{"call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407","name":"Game Theory"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize","grant_number":"Z211","call_identifier":"FWF"},{"call_identifier":"FP7","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification","_id":"25892FC0-B435-11E9-9278-68D0E5697425"}],"quality_controlled":"1","page":"143 - 161","year":"2018","date_created":"2018-12-11T11:44:33Z","volume":10760,"file":[{"relation":"main_file","checksum":"9995c6ce6957333baf616fc4f20be597","file_size":516307,"creator":"dernst","file_name":"2018_PrinciplesModeling_Chatterjee.pdf","date_created":"2019-11-19T08:22:18Z","content_type":"application/pdf","file_id":"7053","date_updated":"2020-07-14T12:48:14Z","access_level":"open_access"}]},{"date_created":"2018-12-11T11:44:31Z","year":"2018","quality_controlled":"1","page":"215 - 232","project":[{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","call_identifier":"FWF"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize","grant_number":"Z211"}],"date_updated":"2023-09-13T09:35:46Z","isi":1,"file":[{"file_name":"2018_LNCS_Bakhirkin.pdf","file_id":"7831","date_created":"2020-05-14T11:34:34Z","content_type":"application/pdf","date_updated":"2020-07-14T12:48:03Z","access_level":"open_access","relation":"main_file","checksum":"436b7574934324cfa7d1d3986fddc65b","file_size":374851,"creator":"dernst"}],"volume":11022,"article_processing_charge":"No","publication_identifier":{"isbn":["978-3-030-00150-6"]},"scopus_import":"1","doi":"10.1007/978-3-030-00151-3_13","publisher":"Springer","language":[{"iso":"eng"}],"type":"conference","file_date_updated":"2020-07-14T12:48:03Z","external_id":{"isi":["000884993200013"]},"conference":{"location":"Bejing, China","end_date":"2018-09-06","name":"FORMATS: Formal Modeling and Analysis of Timed Systems","start_date":"2018-09-04"},"oa_version":"Submitted Version","date_published":"2018-08-26T00:00:00Z","publist_id":"7976","author":[{"full_name":"Bakhirkin, Alexey","first_name":"Alexey","last_name":"Bakhirkin"},{"first_name":"Thomas","full_name":"Ferrere, Thomas","last_name":"Ferrere","id":"40960E6E-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-5199-3143"},{"first_name":"Dejan","full_name":"Nickovic, Dejan","last_name":"Nickovic"},{"first_name":"Oded","full_name":"Maler, Oded","last_name":"Maler"},{"last_name":"Asarin","first_name":"Eugene","full_name":"Asarin, Eugene"}],"ddc":["000"],"status":"public","abstract":[{"lang":"eng","text":"We provide a procedure for detecting the sub-segments of an incrementally observed Boolean signal ω that match a given temporal pattern ϕ. As a pattern specification language, we use timed regular expressions, a formalism well-suited for expressing properties of concurrent asynchronous behaviors embedded in metric time. We construct a timed automaton accepting the timed language denoted by ϕ and modify it slightly for the purpose of matching. We then apply zone-based reachability computation to this automaton while it reads ω, and retrieve all the matching segments from the results. Since the procedure is automaton based, it can be applied to patterns specified by other formalisms such as timed temporal logics reducible to timed automata or directly encoded as timed automata. The procedure has been implemented and its performance on synthetic examples is demonstrated."}],"day":"26","has_accepted_license":"1","intvolume":" 11022","citation":{"mla":"Bakhirkin, Alexey, et al. Online Timed Pattern Matching Using Automata. Vol. 11022, Springer, 2018, pp. 215–32, doi:10.1007/978-3-030-00151-3_13.","ieee":"A. Bakhirkin, T. Ferrere, D. Nickovic, O. Maler, and E. Asarin, “Online timed pattern matching using automata,” presented at the FORMATS: Formal Modeling and Analysis of Timed Systems, Bejing, China, 2018, vol. 11022, pp. 215–232.","apa":"Bakhirkin, A., Ferrere, T., Nickovic, D., Maler, O., & Asarin, E. (2018). Online timed pattern matching using automata (Vol. 11022, pp. 215–232). Presented at the FORMATS: Formal Modeling and Analysis of Timed Systems, Bejing, China: Springer. https://doi.org/10.1007/978-3-030-00151-3_13","chicago":"Bakhirkin, Alexey, Thomas Ferrere, Dejan Nickovic, Oded Maler, and Eugene Asarin. “Online Timed Pattern Matching Using Automata,” 11022:215–32. Springer, 2018. https://doi.org/10.1007/978-3-030-00151-3_13.","ista":"Bakhirkin A, Ferrere T, Nickovic D, Maler O, Asarin E. 2018. Online timed pattern matching using automata. FORMATS: Formal Modeling and Analysis of Timed Systems, LNCS, vol. 11022, 215–232.","ama":"Bakhirkin A, Ferrere T, Nickovic D, Maler O, Asarin E. Online timed pattern matching using automata. In: Vol 11022. Springer; 2018:215-232. doi:10.1007/978-3-030-00151-3_13","short":"A. Bakhirkin, T. Ferrere, D. Nickovic, O. Maler, E. Asarin, in:, Springer, 2018, pp. 215–232."},"month":"08","_id":"78","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","publication_status":"published","oa":1,"title":"Online timed pattern matching using automata","department":[{"_id":"ToHe"}],"alternative_title":["LNCS"]}]