[{"department":[{"_id":"ToHe"}],"publisher":"Springer Nature","publication_status":"published","year":"2020","volume":22,"date_created":"2022-03-18T10:10:53Z","date_updated":"2023-09-08T11:52:02Z","related_material":{"record":[{"relation":"earlier_version","status":"public","id":"299"}]},"author":[{"id":"41BCEE5C-F248-11E8-B48F-1D18A9856A87","last_name":"Nickovic","first_name":"Dejan","full_name":"Nickovic, Dejan"},{"first_name":"Olivier","last_name":"Lebeltel","full_name":"Lebeltel, Olivier"},{"full_name":"Maler, Oded","last_name":"Maler","first_name":"Oded"},{"last_name":"Ferrere","first_name":"Thomas","orcid":"0000-0001-5199-3143","id":"40960E6E-F248-11E8-B48F-1D18A9856A87","full_name":"Ferrere, Thomas"},{"last_name":"Ulus","first_name":"Dogan","full_name":"Ulus, Dogan"}],"publication_identifier":{"eissn":["1433-2787"],"issn":["1433-2779"]},"month":"08","isi":1,"quality_controlled":"1","external_id":{"isi":["000555398600001"]},"language":[{"iso":"eng"}],"doi":"10.1007/s10009-020-00582-z","type":"journal_article","issue":"6","abstract":[{"text":"We introduce in this paper AMT2.0, a tool for qualitative and quantitative analysis of hybrid continuous and Boolean signals that combine numerical values and discrete events. The evaluation of the signals is based on rich temporal specifications expressed in extended signal temporal logic, which integrates timed regular expressions within signal temporal logic. The tool features qualitative monitoring (property satisfaction checking), trace diagnostics for explaining and justifying property violations and specification-driven measurement of quantitative features of the signal. We demonstrate the tool functionality on several running examples and case studies, and evaluate its performance.","lang":"eng"}],"intvolume":" 22","title":"AMT 2.0: Qualitative and quantitative trace analysis with extended signal temporal logic","status":"public","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","_id":"10861","oa_version":"None","keyword":["Information Systems","Software"],"scopus_import":"1","article_processing_charge":"No","day":"03","page":"741-758","article_type":"original","citation":{"short":"D. Nickovic, O. Lebeltel, O. Maler, T. Ferrere, D. Ulus, International Journal on Software Tools for Technology Transfer 22 (2020) 741–758.","mla":"Nickovic, Dejan, et al. “AMT 2.0: Qualitative and Quantitative Trace Analysis with Extended Signal Temporal Logic.” International Journal on Software Tools for Technology Transfer, vol. 22, no. 6, Springer Nature, 2020, pp. 741–58, doi:10.1007/s10009-020-00582-z.","chicago":"Nickovic, Dejan, Olivier Lebeltel, Oded Maler, Thomas Ferrere, and Dogan Ulus. “AMT 2.0: Qualitative and Quantitative Trace Analysis with Extended Signal Temporal Logic.” International Journal on Software Tools for Technology Transfer. Springer Nature, 2020. https://doi.org/10.1007/s10009-020-00582-z.","ama":"Nickovic D, Lebeltel O, Maler O, Ferrere T, Ulus D. AMT 2.0: Qualitative and quantitative trace analysis with extended signal temporal logic. International Journal on Software Tools for Technology Transfer. 2020;22(6):741-758. doi:10.1007/s10009-020-00582-z","ieee":"D. Nickovic, O. Lebeltel, O. Maler, T. Ferrere, and D. Ulus, “AMT 2.0: Qualitative and quantitative trace analysis with extended signal temporal logic,” International Journal on Software Tools for Technology Transfer, vol. 22, no. 6. Springer Nature, pp. 741–758, 2020.","apa":"Nickovic, D., Lebeltel, O., Maler, O., Ferrere, T., & Ulus, D. (2020). AMT 2.0: Qualitative and quantitative trace analysis with extended signal temporal logic. International Journal on Software Tools for Technology Transfer. Springer Nature. https://doi.org/10.1007/s10009-020-00582-z","ista":"Nickovic D, Lebeltel O, Maler O, Ferrere T, Ulus D. 2020. AMT 2.0: Qualitative and quantitative trace analysis with extended signal temporal logic. International Journal on Software Tools for Technology Transfer. 22(6), 741–758."},"publication":"International Journal on Software Tools for Technology Transfer","date_published":"2020-08-03T00:00:00Z"},{"author":[{"id":"320FC952-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-7745-9117","first_name":"Bernhard","last_name":"Kragl","full_name":"Kragl, Bernhard"}],"related_material":{"record":[{"status":"public","relation":"part_of_dissertation","id":"133"},{"id":"8012","status":"public","relation":"part_of_dissertation"},{"id":"8195","relation":"part_of_dissertation","status":"public"},{"id":"160","relation":"part_of_dissertation","status":"public"}]},"date_updated":"2023-09-13T08:45:08Z","date_created":"2020-09-04T12:24:12Z","year":"2020","publication_status":"published","department":[{"_id":"ToHe"}],"publisher":"Institute of Science and Technology Austria","file_date_updated":"2020-09-04T13:00:17Z","doi":"10.15479/AT:ISTA:8332","supervisor":[{"full_name":"Henzinger, Thomas A","last_name":"Henzinger","first_name":"Thomas A","orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"degree_awarded":"PhD","language":[{"iso":"eng"}],"oa":1,"month":"09","publication_identifier":{"issn":["2663-337X"]},"file":[{"file_name":"kragl-thesis.pdf","access_level":"open_access","creator":"bkragl","file_size":1348815,"content_type":"application/pdf","file_id":"8333","relation":"main_file","date_created":"2020-09-04T12:17:47Z","date_updated":"2020-09-04T12:17:47Z","checksum":"26fe261550f691280bda4c454bf015c7"},{"checksum":"b9694ce092b7c55557122adba8337ebc","date_created":"2020-09-04T13:00:17Z","date_updated":"2020-09-04T13:00:17Z","relation":"source_file","file_id":"8335","content_type":"application/zip","file_size":372312,"creator":"bkragl","access_level":"closed","file_name":"kragl-thesis.zip"}],"oa_version":"Published Version","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","_id":"8332","ddc":["000"],"status":"public","title":"Verifying concurrent programs: Refinement, synchronization, sequentialization","abstract":[{"lang":"eng","text":"Designing and verifying concurrent programs is a notoriously challenging, time consuming, and error prone task, even for experts. This is due to the sheer number of possible interleavings of a concurrent program, all of which have to be tracked and accounted for in a formal proof. Inventing an inductive invariant that captures all interleavings of a low-level implementation is theoretically possible, but practically intractable. We develop a refinement-based verification framework that provides mechanisms to simplify proof construction by decomposing the verification task into smaller subtasks.\r\n\r\nIn a first line of work, we present a foundation for refinement reasoning over structured concurrent programs. We introduce layered concurrent programs as a compact notation to represent multi-layer refinement proofs. A layered concurrent program specifies a sequence of connected concurrent programs, from most concrete to most abstract, such that common parts of different programs are written exactly once. Each program in this sequence is expressed as structured concurrent program, i.e., a program over (potentially recursive) procedures, imperative control flow, gated atomic actions, structured parallelism, and asynchronous concurrency. This is in contrast to existing refinement-based verifiers, which represent concurrent systems as flat transition relations. We present a powerful refinement proof rule that decomposes refinement checking over structured programs into modular verification conditions. Refinement checking is supported by a new form of modular, parameterized invariants, called yield invariants, and a linear permission system to enhance local reasoning.\r\n\r\nIn a second line of work, we present two new reduction-based program transformations that target asynchronous programs. These transformations reduce the number of interleavings that need to be considered, thus reducing the complexity of invariants. Synchronization 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. Inductive sequentialization establishes sequential reductions that captures every behavior of the original program up to reordering of coarse-grained commutative actions. A sequential reduction of a concurrent program is easy to reason about since it corresponds to a simple execution of the program in an idealized synchronous environment, where processes act in a fixed order and at the same speed.\r\n\r\nOur approach is implemented the CIVL verifier, which has been successfully used for the verification of several complex concurrent programs. In our methodology, the overall correctness of a program is established piecemeal by focusing on the invariant required for each refinement step separately. While the programmer does the creative work of specifying the chain of programs and the inductive invariant justifying each link in the chain, the tool automatically constructs the verification conditions underlying each refinement step."}],"type":"dissertation","alternative_title":["ISTA Thesis"],"date_published":"2020-09-03T00:00:00Z","citation":{"chicago":"Kragl, Bernhard. “Verifying Concurrent Programs: Refinement, Synchronization, Sequentialization.” Institute of Science and Technology Austria, 2020. https://doi.org/10.15479/AT:ISTA:8332.","short":"B. Kragl, Verifying Concurrent Programs: Refinement, Synchronization, Sequentialization, Institute of Science and Technology Austria, 2020.","mla":"Kragl, Bernhard. Verifying Concurrent Programs: Refinement, Synchronization, Sequentialization. Institute of Science and Technology Austria, 2020, doi:10.15479/AT:ISTA:8332.","apa":"Kragl, B. (2020). Verifying concurrent programs: Refinement, synchronization, sequentialization. Institute of Science and Technology Austria. https://doi.org/10.15479/AT:ISTA:8332","ieee":"B. Kragl, “Verifying concurrent programs: Refinement, synchronization, sequentialization,” Institute of Science and Technology Austria, 2020.","ista":"Kragl B. 2020. Verifying concurrent programs: Refinement, synchronization, sequentialization. Institute of Science and Technology Austria.","ama":"Kragl B. Verifying concurrent programs: Refinement, synchronization, sequentialization. 2020. doi:10.15479/AT:ISTA:8332"},"page":"120","day":"03","has_accepted_license":"1","article_processing_charge":"No"},{"date_published":"2020-12-01T00:00:00Z","page":"244-256","citation":{"chicago":"Garcia Soto, Miriam, and Pavithra Prabhakar. “Hybridization for Stability Verification of Nonlinear Switched Systems.” In 2020 IEEE Real-Time Systems Symposium, 244–56. IEEE, 2020. https://doi.org/10.1109/RTSS49844.2020.00031.","short":"M. Garcia Soto, P. Prabhakar, in:, 2020 IEEE Real-Time Systems Symposium, IEEE, 2020, pp. 244–256.","mla":"Garcia Soto, Miriam, and Pavithra Prabhakar. “Hybridization for Stability Verification of Nonlinear Switched Systems.” 2020 IEEE Real-Time Systems Symposium, IEEE, 2020, pp. 244–56, doi:10.1109/RTSS49844.2020.00031.","apa":"Garcia Soto, M., & Prabhakar, P. (2020). Hybridization for stability verification of nonlinear switched systems. In 2020 IEEE Real-Time Systems Symposium (pp. 244–256). Houston, TX, USA : IEEE. https://doi.org/10.1109/RTSS49844.2020.00031","ieee":"M. Garcia Soto and P. Prabhakar, “Hybridization for stability verification of nonlinear switched systems,” in 2020 IEEE Real-Time Systems Symposium, Houston, TX, USA , 2020, pp. 244–256.","ista":"Garcia Soto M, Prabhakar P. 2020. Hybridization for stability verification of nonlinear switched systems. 2020 IEEE Real-Time Systems Symposium. RTTS: Real-Time Systems Symposium, 244–256.","ama":"Garcia Soto M, Prabhakar P. Hybridization for stability verification of nonlinear switched systems. In: 2020 IEEE Real-Time Systems Symposium. IEEE; 2020:244-256. doi:10.1109/RTSS49844.2020.00031"},"publication":"2020 IEEE Real-Time Systems Symposium","has_accepted_license":"1","article_processing_charge":"No","day":"01","file":[{"checksum":"8f97f229316c3b3a6f0cf99297aa0941","date_updated":"2021-02-26T16:38:14Z","date_created":"2021-02-26T16:38:14Z","file_id":"9203","relation":"main_file","creator":"mgarcias","file_size":1125794,"content_type":"application/pdf","access_level":"open_access","file_name":"main.pdf"}],"oa_version":"Submitted Version","title":"Hybridization for stability verification of nonlinear switched systems","ddc":["000"],"status":"public","_id":"9202","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","abstract":[{"text":"We propose a novel hybridization method for stability analysis that over-approximates nonlinear dynamical systems by switched systems with linear inclusion dynamics. We observe that existing hybridization techniques for safety analysis that over-approximate nonlinear dynamical systems by switched affine inclusion dynamics and provide fixed approximation error, do not suffice for stability analysis. Hence, we propose a hybridization method that provides a state-dependent error which converges to zero as the state tends to the equilibrium point. The crux of our hybridization computation is an elegant recursive algorithm that uses partial derivatives of a given function to obtain upper and lower bound matrices for the over-approximating linear inclusion. We illustrate our method on some examples to demonstrate the application of the theory for stability analysis. In particular, our method is able to establish stability of a nonlinear system which does not admit a polynomial Lyapunov function.","lang":"eng"}],"type":"conference","language":[{"iso":"eng"}],"doi":"10.1109/RTSS49844.2020.00031","conference":{"end_date":"2020-12-04","start_date":"2020-12-01","location":"Houston, TX, USA ","name":"RTTS: Real-Time Systems Symposium"},"project":[{"call_identifier":"FWF","name":"The Wittgenstein Prize","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211"}],"quality_controlled":"1","isi":1,"external_id":{"isi":["000680435100021"]},"oa":1,"publication_identifier":{"eissn":["2576-3172"],"eisbn":["9781728183244"]},"month":"12","date_updated":"2024-02-22T13:25:19Z","date_created":"2021-02-26T16:38:24Z","author":[{"full_name":"Garcia Soto, Miriam","orcid":"0000-0003-2936-5719","id":"4B3207F6-F248-11E8-B48F-1D18A9856A87","last_name":"Garcia Soto","first_name":"Miriam"},{"full_name":"Prabhakar, Pavithra","last_name":"Prabhakar","first_name":"Pavithra"}],"publisher":"IEEE","department":[{"_id":"ToHe"}],"publication_status":"published","acknowledgement":"Miriam Garc´ıa Soto was partially supported by the Austrian Science Fund (FWF) under grant Z211-N23 (Wittgenstein Award). Pavithra Prabhakar was partially supported by NSF CAREER Award No. 1552668, NSF Award No. 2008957 and ONR YIP Award No. N000141712577.","year":"2020","file_date_updated":"2021-02-26T16:38:14Z"},{"intvolume":" 36","title":"Abstraction based verification of stability of polyhedral switched systems","status":"public","ddc":["000"],"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","_id":"7426","oa_version":"Submitted Version","file":[{"content_type":"application/pdf","file_size":818774,"creator":"dernst","file_name":"2020_NAHS_GarciaSoto.pdf","access_level":"open_access","date_created":"2020-10-21T13:16:45Z","date_updated":"2022-05-16T22:30:04Z","checksum":"560abfddb53f9fe921b6744f59f2cfaa","relation":"main_file","file_id":"8688","embargo":"2022-05-15"}],"type":"journal_article","issue":"5","abstract":[{"lang":"eng","text":"This paper presents a novel abstraction technique for analyzing Lyapunov and asymptotic stability of polyhedral switched systems. A polyhedral switched system is a hybrid system in which the continuous dynamics is specified by polyhedral differential inclusions, the invariants and guards are specified by polyhedral sets and the switching between the modes do not involve reset of variables. A finite state weighted graph abstracting the polyhedral switched system is constructed from a finite partition of the state–space, such that the satisfaction of certain graph conditions, such as the absence of cycles with product of weights on the edges greater than (or equal) to 1, implies the stability of the system. However, the graph is in general conservative and hence, the violation of the graph conditions does not imply instability. If the analysis fails to establish stability due to the conservativeness in the approximation, a counterexample (cycle with product of edge weights greater than or equal to 1) indicating a potential reason for the failure is returned. Further, a more precise approximation of the switched system can be constructed by considering a finer partition of the state–space in the construction of the finite weighted graph. We present experimental results on analyzing stability of switched systems using the above method."}],"article_type":"original","citation":{"ama":"Garcia Soto M, Prabhakar P. Abstraction based verification of stability of polyhedral switched systems. Nonlinear Analysis: Hybrid Systems. 2020;36(5). doi:10.1016/j.nahs.2020.100856","ista":"Garcia Soto M, Prabhakar P. 2020. Abstraction based verification of stability of polyhedral switched systems. Nonlinear Analysis: Hybrid Systems. 36(5), 100856.","ieee":"M. Garcia Soto and P. Prabhakar, “Abstraction based verification of stability of polyhedral switched systems,” Nonlinear Analysis: Hybrid Systems, vol. 36, no. 5. Elsevier, 2020.","apa":"Garcia Soto, M., & Prabhakar, P. (2020). Abstraction based verification of stability of polyhedral switched systems. Nonlinear Analysis: Hybrid Systems. Elsevier. https://doi.org/10.1016/j.nahs.2020.100856","mla":"Garcia Soto, Miriam, and Pavithra Prabhakar. “Abstraction Based Verification of Stability of Polyhedral Switched Systems.” Nonlinear Analysis: Hybrid Systems, vol. 36, no. 5, 100856, Elsevier, 2020, doi:10.1016/j.nahs.2020.100856.","short":"M. Garcia Soto, P. Prabhakar, Nonlinear Analysis: Hybrid Systems 36 (2020).","chicago":"Garcia Soto, Miriam, and Pavithra Prabhakar. “Abstraction Based Verification of Stability of Polyhedral Switched Systems.” Nonlinear Analysis: Hybrid Systems. Elsevier, 2020. https://doi.org/10.1016/j.nahs.2020.100856."},"publication":"Nonlinear Analysis: Hybrid Systems","date_published":"2020-05-01T00:00:00Z","scopus_import":"1","article_processing_charge":"No","has_accepted_license":"1","day":"01","publisher":"Elsevier","department":[{"_id":"ToHe"}],"publication_status":"published","year":"2020","volume":36,"date_created":"2020-02-02T23:00:59Z","date_updated":"2023-08-17T14:32:54Z","author":[{"full_name":"Garcia Soto, Miriam","id":"4B3207F6-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0003−2936−5719","first_name":"Miriam","last_name":"Garcia Soto"},{"full_name":"Prabhakar, Pavithra","first_name":"Pavithra","last_name":"Prabhakar"}],"article_number":"100856","license":"https://creativecommons.org/licenses/by-nc-nd/4.0/","file_date_updated":"2022-05-16T22:30:04Z","project":[{"_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407","call_identifier":"FWF","name":"Game Theory"},{"call_identifier":"FWF","name":"The Wittgenstein Prize","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211"}],"isi":1,"quality_controlled":"1","tmp":{"name":"Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International (CC BY-NC-ND 4.0)","legal_code_url":"https://creativecommons.org/licenses/by-nc-nd/4.0/legalcode","short":"CC BY-NC-ND (4.0)","image":"/images/cc_by_nc_nd.png"},"oa":1,"external_id":{"isi":["000528828600003"]},"language":[{"iso":"eng"}],"doi":"10.1016/j.nahs.2020.100856","publication_identifier":{"issn":["1751-570X"]},"month":"05"},{"abstract":[{"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.","lang":"eng"}],"type":"conference","alternative_title":["EPiC Series in Computing"],"file":[{"file_name":"2019_EPiCs_Frehse.pdf","access_level":"open_access","creator":"dernst","content_type":"application/pdf","file_size":346415,"file_id":"11391","relation":"main_file","date_updated":"2022-05-17T06:55:49Z","date_created":"2022-05-17T06:55:49Z","success":1,"checksum":"4b92e333db7b4e2349501a804dfede69"}],"oa_version":"Published Version","_id":"10877","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","intvolume":" 61","ddc":["000"],"title":"ARCH-COMP19 Category Report: Hybrid systems with piecewise constant dynamics","status":"public","article_processing_charge":"No","has_accepted_license":"1","day":"25","scopus_import":"1","date_published":"2019-05-25T00:00:00Z","citation":{"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.","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","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.","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","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.","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.","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."},"publication":"ARCH19. 6th International Workshop on Applied Verification of Continuous and Hybrid Systems","page":"1-13","file_date_updated":"2022-05-17T06:55:49Z","author":[{"full_name":"Frehse, Goran","first_name":"Goran","last_name":"Frehse"},{"first_name":"Alessandro","last_name":"Abate","full_name":"Abate, Alessandro"},{"last_name":"Adzkiya","first_name":"Dieky","full_name":"Adzkiya, Dieky"},{"first_name":"Anna","last_name":"Becchi","full_name":"Becchi, Anna"},{"last_name":"Bu","first_name":"Lei","full_name":"Bu, Lei"},{"first_name":"Alessandro","last_name":"Cimatti","full_name":"Cimatti, Alessandro"},{"first_name":"Mirco","last_name":"Giacobbe","id":"3444EA5E-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-8180-0904","full_name":"Giacobbe, Mirco"},{"full_name":"Griggio, Alberto","first_name":"Alberto","last_name":"Griggio"},{"full_name":"Mover, Sergio","first_name":"Sergio","last_name":"Mover"},{"full_name":"Mufid, Muhammad Syifa'ul","first_name":"Muhammad Syifa'ul","last_name":"Mufid"},{"last_name":"Riouak","first_name":"Idriss","full_name":"Riouak, Idriss"},{"full_name":"Tonetta, Stefano","last_name":"Tonetta","first_name":"Stefano"},{"full_name":"Zaffanella, Enea","last_name":"Zaffanella","first_name":"Enea"}],"volume":61,"date_created":"2022-03-18T12:29:23Z","date_updated":"2022-05-17T07:09:47Z","year":"2019","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).","editor":[{"first_name":"Goran","last_name":"Frehse","full_name":"Frehse, Goran"},{"full_name":"Althoff, Matthias","first_name":"Matthias","last_name":"Althoff"}],"publisher":"EasyChair","department":[{"_id":"ToHe"}],"publication_status":"published","publication_identifier":{"issn":["2398-7340"]},"month":"05","doi":"10.29007/rjwn","conference":{"end_date":"2019-04-15","location":"Montreal, Canada","start_date":"2019-04-15","name":"ARCH: International Workshop on Applied Verification on Continuous and Hybrid Systems"},"language":[{"iso":"eng"}],"oa":1,"quality_controlled":"1"},{"abstract":[{"lang":"eng","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."}],"type":"conference","file":[{"file_size":396031,"content_type":"application/pdf","creator":"dernst","access_level":"open_access","file_name":"2019_ICC_Kundu.pdf","checksum":"d622a91af1e427f6b1e0ba8e18a2b767","success":1,"date_created":"2020-10-21T13:13:49Z","date_updated":"2020-10-21T13:13:49Z","relation":"main_file","file_id":"8687"}],"oa_version":"Submitted Version","ddc":["000"],"title":"Formal synthesis of stabilizing controllers for periodically controlled linear switched systems","status":"public","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"6565","has_accepted_license":"1","article_processing_charge":"No","day":"16","scopus_import":"1","date_published":"2019-05-16T00:00:00Z","citation":{"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","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.","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","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.","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.","short":"A. Kundu, M. Garcia Soto, P. Prabhakar, in:, 5th Indian Control Conference Proceedings, IEEE, 2019."},"publication":"5th Indian Control Conference Proceedings","file_date_updated":"2020-10-21T13:13:49Z","article_number":"8715598","date_created":"2019-06-17T06:57:33Z","date_updated":"2021-01-12T08:08:01Z","author":[{"first_name":"Atreyee","last_name":"Kundu","full_name":"Kundu, Atreyee"},{"orcid":"0000−0003−2936−5719","id":"4B3207F6-F248-11E8-B48F-1D18A9856A87","last_name":"Garcia Soto","first_name":"Miriam","full_name":"Garcia Soto, Miriam"},{"first_name":"Pavithra","last_name":"Prabhakar","full_name":"Prabhakar, Pavithra"}],"department":[{"_id":"ToHe"}],"publisher":"IEEE","publication_status":"published","year":"2019","publication_identifier":{"isbn":["978-153866246-5"]},"month":"05","language":[{"iso":"eng"}],"doi":"10.1109/INDIANCC.2019.8715598","conference":{"end_date":"2019-01-11","start_date":"2019-01-09","location":"Delhi, India","name":"ICC 2019 - Indian Control Conference"},"project":[{"name":"Rigorous Systems Engineering","call_identifier":"FWF","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","name":"The Wittgenstein Prize","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211"}],"quality_controlled":"1","oa":1},{"file_date_updated":"2020-07-14T12:47:41Z","year":"2019","publisher":"Springer","department":[{"_id":"ToHe"}],"publication_status":"published","author":[{"full_name":"Avni, Guy","orcid":"0000-0001-5588-8287","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","last_name":"Avni","first_name":"Guy"},{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"},{"full_name":"Ibsen-Jensen, Rasmus","first_name":"Rasmus","last_name":"Ibsen-Jensen","id":"3B699956-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-4783-0389"},{"first_name":"Petr","last_name":"Novotny","full_name":"Novotny, Petr"}],"volume":11674,"date_created":"2019-08-19T07:58:10Z","date_updated":"2021-01-12T08:09:12Z","publication_identifier":{"issn":["0302-9743"],"isbn":["978-303030805-6"]},"month":"09","oa":1,"project":[{"call_identifier":"FWF","name":"Formal Methods meets Algorithmic Game Theory","grant_number":"M02369","_id":"264B3912-B435-11E9-9278-68D0E5697425"},{"name":"Rigorous Systems Engineering","call_identifier":"FWF","grant_number":"S11402-N23","_id":"25F2ACDE-B435-11E9-9278-68D0E5697425"},{"name":"The Wittgenstein Prize","call_identifier":"FWF","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425"}],"quality_controlled":"1","doi":"10.1007/978-3-030-30806-3_1","conference":{"name":"RP: Reachability Problems","end_date":"2019-09-13","location":"Brussels, Belgium","start_date":"2019-09-11"},"language":[{"iso":"eng"}],"type":"conference","alternative_title":["LNCS"],"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."}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"6822","intvolume":" 11674","ddc":["000"],"title":"Bidding games on Markov decision processes","status":"public","oa_version":"Submitted Version","file":[{"file_id":"6823","relation":"main_file","checksum":"45ebbc709af2b247d28c7c293c01504b","date_created":"2019-08-19T07:56:40Z","date_updated":"2020-07-14T12:47:41Z","access_level":"open_access","file_name":"prob.pdf","creator":"gavni","content_type":"application/pdf","file_size":436635}],"scopus_import":1,"has_accepted_license":"1","day":"06","citation":{"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.","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.","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","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","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.","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.","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."},"publication":" Proceedings of the 13th International Conference of Reachability Problems","page":"1-12","date_published":"2019-09-06T00:00:00Z"},{"file":[{"creator":"dernst","content_type":"application/pdf","file_size":3265107,"access_level":"open_access","file_name":"2019_ICRA_Lechner.pdf","success":1,"checksum":"f5545a6b60c3ffd01feb3613f81d03b6","date_updated":"2020-10-08T17:30:38Z","date_created":"2020-10-08T17:30:38Z","file_id":"8636","relation":"main_file"}],"oa_version":"Submitted Version","_id":"6888","user_id":"D865714E-FA4E-11E9-B85B-F5C5E5697425","title":"Designing worm-inspired neural networks for interpretable robotic control","ddc":["000"],"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."}],"type":"conference","alternative_title":["ICRA"],"date_published":"2019-05-01T00:00:00Z","publication":"Proceedings - IEEE International Conference on Robotics and Automation","citation":{"short":"M. Lechner, R. Hasani, M. Zimmer, T.A. Henzinger, R. Grosu, in:, Proceedings - IEEE International Conference on Robotics and Automation, IEEE, 2019.","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.","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","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.","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","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."},"day":"01","article_processing_charge":"No","has_accepted_license":"1","scopus_import":"1","author":[{"full_name":"Lechner, Mathias","first_name":"Mathias","last_name":"Lechner","id":"3DC22916-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Hasani, Ramin","first_name":"Ramin","last_name":"Hasani"},{"last_name":"Zimmer","first_name":"Manuel","full_name":"Zimmer, Manuel"},{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"},{"last_name":"Grosu","first_name":"Radu","full_name":"Grosu, Radu"}],"date_updated":"2021-01-12T08:09:28Z","date_created":"2019-09-18T08:09:51Z","volume":"2019-May","year":"2019","publication_status":"published","department":[{"_id":"ToHe"}],"publisher":"IEEE","file_date_updated":"2020-10-08T17:30:38Z","article_number":"8793840","conference":{"end_date":"2019-05-24","location":"Montreal, QC, Canada","start_date":"2019-05-20","name":"ICRA: International Conference on Robotics and Automation"},"doi":"10.1109/icra.2019.8793840","language":[{"iso":"eng"}],"oa":1,"quality_controlled":"1","project":[{"grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"The Wittgenstein Prize"}],"month":"05","publication_identifier":{"isbn":["9781538660270"]}},{"scopus_import":"1","has_accepted_license":"1","article_processing_charge":"No","day":"01","citation":{"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","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.","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","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.","short":"M. Aghajohari, G. Avni, T.A. Henzinger, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019.","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.","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."},"date_published":"2019-08-01T00:00:00Z","alternative_title":["LIPIcs"],"type":"conference","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"}],"intvolume":" 140","title":"Determinacy in discrete-bidding infinite-duration games","status":"public","ddc":["000"],"user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","_id":"6886","oa_version":"Published Version","file":[{"checksum":"4df6d3575c506edb17215adada03cc8e","date_updated":"2020-07-14T12:47:43Z","date_created":"2019-09-27T12:21:38Z","relation":"main_file","file_id":"6915","content_type":"application/pdf","file_size":741425,"creator":"kschuh","access_level":"open_access","file_name":"2019_LIPIcs_Aghajohari.pdf"}],"month":"08","project":[{"name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25F2ACDE-B435-11E9-9278-68D0E5697425","grant_number":"S11402-N23"},{"grant_number":"M02369","_id":"264B3912-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Formal Methods meets Algorithmic Game Theory"}],"quality_controlled":"1","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/3.0/legalcode","name":"Creative Commons Attribution 3.0 Unported (CC BY 3.0)","short":"CC BY (3.0)","image":"/images/cc_by.png"},"oa":1,"external_id":{"arxiv":["1905.03588"]},"language":[{"iso":"eng"}],"doi":"10.4230/LIPICS.CONCUR.2019.20","conference":{"end_date":"2019-08-30","start_date":"2019-08-27","location":"Amsterdam, Netherlands","name":"CONCUR: International Conference on Concurrency Theory"},"article_number":"20","license":"https://creativecommons.org/licenses/by/3.0/","file_date_updated":"2020-07-14T12:47:43Z","department":[{"_id":"ToHe"}],"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","publication_status":"published","year":"2019","volume":140,"date_updated":"2022-01-26T08:27:10Z","date_created":"2019-09-18T08:06:58Z","author":[{"full_name":"Aghajohari, Milad","first_name":"Milad","last_name":"Aghajohari"},{"full_name":"Avni, Guy","last_name":"Avni","first_name":"Guy","orcid":"0000-0001-5588-8287","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Henzinger, Thomas A","last_name":"Henzinger","first_name":"Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}]},{"citation":{"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.","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.","short":"K. Chatterjee, T.A. Henzinger, J. Otop, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019.","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.","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","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.","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"},"date_published":"2019-08-01T00:00:00Z","scopus_import":1,"has_accepted_license":"1","day":"01","intvolume":" 140","title":"Long-run average behavior of vector addition systems with states","ddc":["000"],"status":"public","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","_id":"6885","file":[{"checksum":"4985e26e1572d1575d64d38acabd71d6","date_created":"2019-09-27T12:09:35Z","date_updated":"2020-07-14T12:47:43Z","file_id":"6914","relation":"main_file","creator":"kschuh","content_type":"application/pdf","file_size":538120,"access_level":"open_access","file_name":"2019_LIPIcs_Chatterjee.pdf"}],"oa_version":"Published Version","alternative_title":["LIPIcs"],"type":"conference","abstract":[{"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. ","lang":"eng"}],"project":[{"call_identifier":"FWF","name":"Game Theory","_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407"},{"name":"Rigorous Systems Engineering","call_identifier":"FWF","grant_number":"S11402-N23","_id":"25F2ACDE-B435-11E9-9278-68D0E5697425"}],"quality_controlled":"1","oa":1,"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"language":[{"iso":"eng"}],"doi":"10.4230/LIPICS.CONCUR.2019.27","conference":{"end_date":"2019-08-30","location":"Amsterdam, Netherlands","start_date":"2019-08-27","name":"CONCUR: International Conference on Concurrency Theory"},"month":"08","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"publication_status":"published","year":"2019","volume":140,"date_created":"2019-09-18T08:06:14Z","date_updated":"2021-01-12T08:09:27Z","author":[{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A"},{"first_name":"Jan","last_name":"Otop","full_name":"Otop, Jan"}],"article_number":"27","file_date_updated":"2020-07-14T12:47:43Z"}]