[{"_id":"1391","month":"07","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","publication_status":"published","related_material":{"record":[{"status":"public","relation":"dissertation_contains","id":"1155"}]},"oa":1,"title":"Array folds logic","department":[{"_id":"ToHe"}],"alternative_title":["LNCS"],"ec_funded":1,"abstract":[{"text":"We present an extension to the quantifier-free theory of integer arrays which allows us to express counting. The properties expressible in Array Folds Logic (AFL) include statements such as &quot;the first array cell contains the array length,&quot; and &quot;the array contains equally many minimal and maximal elements.&quot; These properties cannot be expressed in quantified fragments of the theory of arrays, nor in the theory of concatenation. Using reduction to counter machines, we show that the satisfiability problem of AFL is PSPACE-complete, and with a natural restriction the complexity decreases to NP. We also show that adding either universal quantifiers or concatenation leads to undecidability.\r\nAFL contains terms that fold a function over an array. We demonstrate that folding, a well-known concept from functional languages, allows us to concisely summarize loops that count over arrays, which occurs frequently in real-life programs. We provide a tool that can discharge proof obligations in AFL, and we demonstrate on practical examples that our decision procedure can solve a broad range of problems in symbolic testing and program verification.","lang":"eng"}],"status":"public","day":"13","citation":{"ama":"Daca P, Henzinger TA, Kupriyanov A. Array folds logic. In: Vol 9780. Springer; 2016:230-248. doi:<a href=\"https://doi.org/10.1007/978-3-319-41540-6_13\">10.1007/978-3-319-41540-6_13</a>","short":"P. Daca, T.A. Henzinger, A. Kupriyanov, in:, Springer, 2016, pp. 230–248.","ieee":"P. Daca, T. A. Henzinger, and A. Kupriyanov, “Array folds logic,” presented at the CAV: Computer Aided Verification, Toronto, Canada, 2016, vol. 9780, pp. 230–248.","mla":"Daca, Przemyslaw, et al. <i>Array Folds Logic</i>. Vol. 9780, Springer, 2016, pp. 230–48, doi:<a href=\"https://doi.org/10.1007/978-3-319-41540-6_13\">10.1007/978-3-319-41540-6_13</a>.","ista":"Daca P, Henzinger TA, Kupriyanov A. 2016. Array folds logic. CAV: Computer Aided Verification, LNCS, vol. 9780, 230–248.","chicago":"Daca, Przemyslaw, Thomas A Henzinger, and Andrey Kupriyanov. “Array Folds Logic,” 9780:230–48. Springer, 2016. <a href=\"https://doi.org/10.1007/978-3-319-41540-6_13\">https://doi.org/10.1007/978-3-319-41540-6_13</a>.","apa":"Daca, P., Henzinger, T. A., &#38; Kupriyanov, A. (2016). Array folds logic (Vol. 9780, pp. 230–248). Presented at the CAV: Computer Aided Verification, Toronto, Canada: Springer. <a href=\"https://doi.org/10.1007/978-3-319-41540-6_13\">https://doi.org/10.1007/978-3-319-41540-6_13</a>"},"intvolume":"      9780","publisher":"Springer","doi":"10.1007/978-3-319-41540-6_13","type":"conference","language":[{"iso":"eng"}],"date_published":"2016-07-13T00:00:00Z","conference":{"location":"Toronto, Canada","end_date":"2016-07-23","name":"CAV: Computer Aided Verification","start_date":"2016-07-17"},"oa_version":"Preprint","author":[{"last_name":"Daca","first_name":"Przemyslaw","full_name":"Daca, Przemyslaw","id":"49351290-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Henzinger","full_name":"Henzinger, Thomas A","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"},{"id":"2C311BF8-F248-11E8-B48F-1D18A9856A87","full_name":"Kupriyanov, Andrey","first_name":"Andrey","last_name":"Kupriyanov"}],"publist_id":"5818","project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","name":"Quantitative Reactive Modeling","call_identifier":"FP7"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","call_identifier":"FWF"},{"name":"The Wittgenstein Prize","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"date_updated":"2023-09-07T11:58:33Z","year":"2016","date_created":"2018-12-11T11:51:45Z","page":"230 - 248","quality_controlled":"1","volume":9780,"main_file_link":[{"url":"http://arxiv.org/abs/1603.06850","open_access":"1"}],"scopus_import":1},{"type":"conference","title":"Scalable static hybridization methods for analysis of nonlinear systems","publication_status":"published","language":[{"iso":"eng"}],"publisher":"Springer","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","doi":"10.1145/2883817.2883837","_id":"1421","month":"04","author":[{"last_name":"Bak","full_name":"Bak, Stanley","first_name":"Stanley"},{"orcid":"0000-0002-0686-0365","id":"369D9A44-F248-11E8-B48F-1D18A9856A87","last_name":"Bogomolov","first_name":"Sergiy","full_name":"Bogomolov, Sergiy"},{"last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"},{"first_name":"Taylor","full_name":"Johnson, Taylor","last_name":"Johnson"},{"last_name":"Prakash","full_name":"Prakash, Pradyot","first_name":"Pradyot"}],"publist_id":"5786","date_published":"2016-04-11T00:00:00Z","department":[{"_id":"ToHe"}],"oa_version":"None","conference":{"location":"Vienna, Austria","end_date":"2016-04-14","name":"HSCC 2016: International Conference on Hybrid Systems: Computation and Control","start_date":"2016-04-12"},"abstract":[{"lang":"eng","text":"Hybridization methods enable the analysis of hybrid automata with complex, nonlinear dynamics through a sound abstraction process. Complex dynamics are converted to simpler ones with added noise, and then analysis is done using a reachability method for the simpler dynamics. Several such recent approaches advocate that only &quot;dynamic&quot; hybridization techniquesi.e., those where the dynamics are abstracted on-The-fly during a reachability computation are effective. In this paper, we demonstrate this is not the case, and create static hybridization methods that are more scalable than earlier approaches. The main insight in our approach is that quick, numeric simulations can be used to guide the process, eliminating the need for an exponential number of hybridization domains. Transitions between domains are generally timetriggered, avoiding accumulated error from geometric intersections. We enhance our static technique by combining time-Triggered transitions with occasional space-Triggered transitions, and demonstrate the benefits of the combined approach in what we call mixed-Triggered hybridization. Finally, error modes are inserted to confirm that the reachable states stay within the hybridized regions. The developed techniques can scale to higher dimensions than previous static approaches, while enabling the parallelization of the main performance bottleneck for many dynamic hybridization approaches: The nonlinear optimization required for sound dynamics abstraction. We implement our method as a model transformation pass in the HYST tool, and perform reachability analysis and evaluation using an unmodified version of SpaceEx on nonlinear models with up to six dimensions."}],"status":"public","ec_funded":1,"date_updated":"2021-01-12T06:50:37Z","project":[{"call_identifier":"FP7","name":"Quantitative Reactive Modeling","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","name":"The Wittgenstein Prize","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"}],"quality_controlled":"1","page":"155 - 164","year":"2016","date_created":"2018-12-11T11:51:55Z","scopus_import":1,"citation":{"ieee":"S. Bak, S. Bogomolov, T. A. Henzinger, T. Johnson, and P. Prakash, “Scalable static hybridization methods for analysis of nonlinear systems,” presented at the HSCC 2016: International Conference on Hybrid Systems: Computation and Control, Vienna, Austria, 2016, pp. 155–164.","mla":"Bak, Stanley, et al. <i>Scalable Static Hybridization Methods for Analysis of Nonlinear Systems</i>. Springer, 2016, pp. 155–64, doi:<a href=\"https://doi.org/10.1145/2883817.2883837\">10.1145/2883817.2883837</a>.","ista":"Bak S, Bogomolov S, Henzinger TA, Johnson T, Prakash P. 2016. Scalable static hybridization methods for analysis of nonlinear systems. HSCC 2016: International Conference on Hybrid Systems: Computation and Control, 155–164.","chicago":"Bak, Stanley, Sergiy Bogomolov, Thomas A Henzinger, Taylor Johnson, and Pradyot Prakash. “Scalable Static Hybridization Methods for Analysis of Nonlinear Systems,” 155–64. Springer, 2016. <a href=\"https://doi.org/10.1145/2883817.2883837\">https://doi.org/10.1145/2883817.2883837</a>.","apa":"Bak, S., Bogomolov, S., Henzinger, T. A., Johnson, T., &#38; Prakash, P. (2016). Scalable static hybridization methods for analysis of nonlinear systems (pp. 155–164). Presented at the HSCC 2016: International Conference on Hybrid Systems: Computation and Control, Vienna, Austria: Springer. <a href=\"https://doi.org/10.1145/2883817.2883837\">https://doi.org/10.1145/2883817.2883837</a>","ama":"Bak S, Bogomolov S, Henzinger TA, Johnson T, Prakash P. Scalable static hybridization methods for analysis of nonlinear systems. In: Springer; 2016:155-164. doi:<a href=\"https://doi.org/10.1145/2883817.2883837\">10.1145/2883817.2883837</a>","short":"S. Bak, S. Bogomolov, T.A. Henzinger, T. Johnson, P. Prakash, in:, Springer, 2016, pp. 155–164."},"day":"11"},{"date_updated":"2021-01-12T06:50:45Z","project":[{"grant_number":"267989","name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize","grant_number":"Z211","call_identifier":"FWF"},{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"quality_controlled":"1","page":"400 - 415","year":"2016","date_created":"2018-12-11T11:52:01Z","volume":"20-22","scopus_import":1,"main_file_link":[{"url":"https://hal.inria.fr/hal-01251199/","open_access":"1"}],"publisher":"ACM","doi":"10.1145/2837614.2837650","type":"conference","language":[{"iso":"eng"}],"date_published":"2016-01-11T00:00:00Z","oa_version":"Preprint","conference":{"start_date":"2016-01-20","name":"POPL: Principles of Programming Languages","end_date":"2016-01-22","location":"St. Petersburg, FL, USA"},"author":[{"id":"2B2B5ED0-F248-11E8-B48F-1D18A9856A87","first_name":"Cezara","full_name":"Dragoi, Cezara","last_name":"Dragoi"},{"orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","full_name":"Henzinger, Thomas A","last_name":"Henzinger"},{"last_name":"Zufferey","first_name":"Damien","full_name":"Zufferey, Damien","id":"4397AC76-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-3197-8736"}],"publist_id":"5759","ec_funded":1,"abstract":[{"lang":"eng","text":"Fault-tolerant distributed algorithms play an important role in many critical/high-availability applications. These algorithms are notoriously difficult to implement correctly, due to asynchronous communication and the occurrence of faults, such as the network dropping messages or computers crashing. We introduce PSYNC, a domain specific language based on the Heard-Of model, which views asynchronous faulty systems as synchronous ones with an adversarial environment that simulates asynchrony and faults by dropping messages. We define a runtime system for PSYNC that efficiently executes on asynchronous networks. We formalize the relation between the runtime system and PSYNC in terms of observational refinement. The high-level lockstep abstraction introduced by PSYNC simplifies the design and implementation of fault-tolerant distributed algorithms and enables automated formal verification. We have implemented an embedding of PSYNC in the SCALA programming language with a runtime system for asynchronous networks. We show the applicability of PSYNC by implementing several important fault-tolerant distributed algorithms and we compare the implementation of consensus algorithms in PSYNC against implementations in other languages in terms of code size, runtime efficiency, and verification."}],"status":"public","day":"11","citation":{"short":"C. Dragoi, T.A. Henzinger, D. Zufferey, in:, ACM, 2016, pp. 400–415.","ama":"Dragoi C, Henzinger TA, Zufferey D. PSYNC: A partially synchronous language for fault-tolerant distributed algorithms. In: Vol 20-22. ACM; 2016:400-415. doi:<a href=\"https://doi.org/10.1145/2837614.2837650\">10.1145/2837614.2837650</a>","chicago":"Dragoi, Cezara, Thomas A Henzinger, and Damien Zufferey. “PSYNC: A Partially Synchronous Language for Fault-Tolerant Distributed Algorithms,” 20–22:400–415. ACM, 2016. <a href=\"https://doi.org/10.1145/2837614.2837650\">https://doi.org/10.1145/2837614.2837650</a>.","ista":"Dragoi C, Henzinger TA, Zufferey D. 2016. PSYNC: A partially synchronous language for fault-tolerant distributed algorithms. POPL: Principles of Programming Languages, ACM SIGPLAN Notices, vol. 20–22, 400–415.","apa":"Dragoi, C., Henzinger, T. A., &#38; Zufferey, D. (2016). PSYNC: A partially synchronous language for fault-tolerant distributed algorithms (Vol. 20–22, pp. 400–415). Presented at the POPL: Principles of Programming Languages, St. Petersburg, FL, USA: ACM. <a href=\"https://doi.org/10.1145/2837614.2837650\">https://doi.org/10.1145/2837614.2837650</a>","ieee":"C. Dragoi, T. A. Henzinger, and D. Zufferey, “PSYNC: A partially synchronous language for fault-tolerant distributed algorithms,” presented at the POPL: Principles of Programming Languages, St. Petersburg, FL, USA, 2016, vol. 20–22, pp. 400–415.","mla":"Dragoi, Cezara, et al. <i>PSYNC: A Partially Synchronous Language for Fault-Tolerant Distributed Algorithms</i>. Vol. 20–22, ACM, 2016, pp. 400–15, doi:<a href=\"https://doi.org/10.1145/2837614.2837650\">10.1145/2837614.2837650</a>."},"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","_id":"1439","month":"01","title":"PSYNC: A partially synchronous language for fault-tolerant distributed algorithms","oa":1,"publication_status":"published","acknowledgement":"Damien Zufferey was supported by DARPA (Grants FA8650-11-C-7192 and FA8650-15-C-7564) and NSF (Grant CCF-1138967). ","department":[{"_id":"ToHe"}],"alternative_title":["ACM SIGPLAN Notices"]},{"volume":58,"file":[{"creator":"system","file_size":564560,"relation":"main_file","date_updated":"2018-12-12T10:17:31Z","access_level":"open_access","content_type":"application/pdf","date_created":"2018-12-12T10:17:31Z","file_id":"5286","file_name":"IST-2017-795-v1+1_LIPIcs-MFCS-2016-24.pdf"}],"quality_controlled":"1","year":"2016","date_created":"2018-12-11T11:50:05Z","date_updated":"2021-01-12T06:48:12Z","project":[{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"},{"call_identifier":"FWF","grant_number":"Z211","name":"The Wittgenstein Prize","_id":"25F42A32-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications"},{"grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification","_id":"25892FC0-B435-11E9-9278-68D0E5697425"}],"scopus_import":1,"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)"},"language":[{"iso":"eng"}],"file_date_updated":"2018-12-12T10:17:31Z","type":"conference","doi":"10.4230/LIPIcs.MFCS.2016.24","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","publist_id":"6286","ddc":["004"],"author":[{"last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A"},{"id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","last_name":"Otop","full_name":"Otop, Jan","first_name":"Jan"}],"oa_version":"Published Version","conference":{"end_date":"2016-08-26","location":"Krakow; Poland","start_date":"2016-08-22","name":"MFCS: Mathematical Foundations of Computer Science (SG)"},"date_published":"2016-08-01T00:00:00Z","article_number":"24","status":"public","abstract":[{"lang":"eng","text":" While weighted automata provide a natural framework to express quantitative properties, many basic properties like average response time cannot be expressed with weighted automata. Nested weighted automata extend weighted automata and consist of a master automaton and a set of slave automata that are invoked by the master automaton. Nested weighted automata are strictly more expressive than weighted automata (e.g., average response time can be expressed with nested weighted automata), but the basic decision questions have higher complexity (e.g., for deterministic automata, the emptiness question for nested weighted automata is PSPACE-hard, whereas the corresponding complexity for weighted automata is PTIME). We consider a natural subclass of nested weighted automata where at any point at most a bounded number k of slave automata can be active. We focus on automata whose master value function is the limit average. We show that these nested weighted automata with bounded width are strictly more expressive than weighted automata (e.g., average response time with no overlapping requests can be expressed with bound k=1, but not with non-nested weighted automata). We show that the complexity of the basic decision problems (i.e., emptiness and universality) for the subclass with k constant matches the complexity for weighted automata. Moreover, when k is part of the input given in unary we establish PSPACE-completeness."}],"ec_funded":1,"citation":{"short":"K. Chatterjee, T.A. Henzinger, J. Otop, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016.","ama":"Chatterjee K, Henzinger TA, Otop J. Nested weighted limit-average automata of bounded width. In: Vol 58. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2016. doi:<a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2016.24\">10.4230/LIPIcs.MFCS.2016.24</a>","apa":"Chatterjee, K., Henzinger, T. A., &#38; Otop, J. (2016). Nested weighted limit-average automata of bounded width (Vol. 58). Presented at the MFCS: Mathematical Foundations of Computer Science (SG), Krakow; Poland: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2016.24\">https://doi.org/10.4230/LIPIcs.MFCS.2016.24</a>","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. “Nested Weighted Limit-Average Automata of Bounded Width,” Vol. 58. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. <a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2016.24\">https://doi.org/10.4230/LIPIcs.MFCS.2016.24</a>.","ista":"Chatterjee K, Henzinger TA, Otop J. 2016. Nested weighted limit-average automata of bounded width. MFCS: Mathematical Foundations of Computer Science (SG), LIPIcs, vol. 58, 24.","ieee":"K. Chatterjee, T. A. Henzinger, and J. Otop, “Nested weighted limit-average automata of bounded width,” presented at the MFCS: Mathematical Foundations of Computer Science (SG), Krakow; Poland, 2016, vol. 58.","mla":"Chatterjee, Krishnendu, et al. <i>Nested Weighted Limit-Average Automata of Bounded Width</i>. Vol. 58, 24, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016, doi:<a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2016.24\">10.4230/LIPIcs.MFCS.2016.24</a>."},"intvolume":"        58","day":"01","has_accepted_license":"1","title":"Nested weighted limit-average automata of bounded width","oa":1,"publication_status":"published","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","_id":"1090","month":"08","pubrep_id":"795","alternative_title":["LIPIcs"],"department":[{"_id":"KrCh"},{"_id":"ToHe"}],"acknowledgement":"This research was supported in part by the Austrian Science Fund (FWF) under grants S11402-N23\r\n(RiSE/SHiNE) and Z211-N23 (Wittgenstein Award), ERC Start grant (279307: Graph Games), Vienna\r\nScience and Technology Fund (WWTF) through project ICT15-003 and by the National Science Centre\r\n(NCN), Poland under grant 2014/15/D/ST6/04543."},{"department":[{"_id":"ToHe"},{"_id":"KrCh"},{"_id":"CaGu"}],"acknowledgement":"This research was funded in part by the European Research Council (ERC) under grant agreement 267989\r\n(QUAREM), the Austrian Science Fund (FWF) under grants project S11402-N23 (RiSE and SHiNE)\r\nand Z211-N23 (Wittgenstein Award), by the Czech Science Foundation Grant No. P202/12/G061, and\r\nby the SNSF Advanced Postdoc. Mobility Fellowship – grant number P300P2_161067.","pubrep_id":"794","alternative_title":["LIPIcs"],"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","_id":"1093","month":"08","title":"Linear distances between Markov chains","oa":1,"related_material":{"record":[{"status":"public","relation":"dissertation_contains","id":"1155"}]},"publication_status":"published","day":"01","has_accepted_license":"1","intvolume":"        59","citation":{"ama":"Daca P, Henzinger TA, Kretinsky J, Petrov T. Linear distances between Markov chains. In: Vol 59. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2016. doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2016.20\">10.4230/LIPIcs.CONCUR.2016.20</a>","short":"P. Daca, T.A. Henzinger, J. Kretinsky, T. Petrov, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016.","ieee":"P. Daca, T. A. Henzinger, J. Kretinsky, and T. Petrov, “Linear distances between Markov chains,” presented at the CONCUR: Concurrency Theory, Quebec City; Canada, 2016, vol. 59.","mla":"Daca, Przemyslaw, et al. <i>Linear Distances between Markov Chains</i>. Vol. 59, 20, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016, doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2016.20\">10.4230/LIPIcs.CONCUR.2016.20</a>.","ista":"Daca P, Henzinger TA, Kretinsky J, Petrov T. 2016. Linear distances between Markov chains. CONCUR: Concurrency Theory, LIPIcs, vol. 59, 20.","chicago":"Daca, Przemyslaw, Thomas A Henzinger, Jan Kretinsky, and Tatjana Petrov. “Linear Distances between Markov Chains,” Vol. 59. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2016.20\">https://doi.org/10.4230/LIPIcs.CONCUR.2016.20</a>.","apa":"Daca, P., Henzinger, T. A., Kretinsky, J., &#38; Petrov, T. (2016). Linear distances between Markov chains (Vol. 59). Presented at the CONCUR: Concurrency Theory, Quebec City; Canada: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2016.20\">https://doi.org/10.4230/LIPIcs.CONCUR.2016.20</a>"},"ec_funded":1,"article_number":"20","status":"public","abstract":[{"lang":"eng","text":"We introduce a general class of distances (metrics) between Markov chains, which are based on linear behaviour. This class encompasses distances given topologically (such as the total variation distance or trace distance) as well as by temporal logics or automata. We investigate which of the distances can be approximated by observing the systems, i.e. by black-box testing or simulation, and we provide both negative and positive results. "}],"oa_version":"Published Version","conference":{"name":"CONCUR: Concurrency Theory","start_date":"2016-08-23","location":"Quebec City; Canada","end_date":"2016-08-26"},"date_published":"2016-08-01T00:00:00Z","publist_id":"6283","ddc":["004"],"author":[{"id":"49351290-F248-11E8-B48F-1D18A9856A87","last_name":"Daca","full_name":"Daca, Przemyslaw","first_name":"Przemyslaw"},{"orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A"},{"last_name":"Kretinsky","full_name":"Kretinsky, Jan","first_name":"Jan","orcid":"0000-0002-8122-2881","id":"44CEF464-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000-0002-9041-0905","id":"3D5811FC-F248-11E8-B48F-1D18A9856A87","first_name":"Tatjana","full_name":"Petrov, Tatjana","last_name":"Petrov"}],"doi":"10.4230/LIPIcs.CONCUR.2016.20","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","language":[{"iso":"eng"}],"file_date_updated":"2018-12-12T10:11:39Z","type":"conference","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,"quality_controlled":"1","year":"2016","date_created":"2018-12-11T11:50:06Z","date_updated":"2023-09-07T11:58:33Z","project":[{"call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling","grant_number":"267989"},{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","name":"The Wittgenstein Prize"}],"volume":59,"file":[{"relation":"main_file","creator":"system","file_size":501827,"file_name":"IST-2017-794-v1+1_LIPIcs-CONCUR-2016-20.pdf","access_level":"open_access","date_updated":"2018-12-12T10:11:39Z","content_type":"application/pdf","file_id":"4895","date_created":"2018-12-12T10:11:39Z"}]},{"date_published":"2016-08-01T00:00:00Z","conference":{"location":"Quebec City; Canada","end_date":"2016-08-26","name":"CONCUR: Concurrency Theory","start_date":"2016-08-23"},"oa_version":"Published Version","author":[{"first_name":"Andreas","full_name":"Haas, Andreas","last_name":"Haas"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger"},{"first_name":"Andreas","full_name":"Holzer, Andreas","last_name":"Holzer"},{"last_name":"Kirsch","first_name":"Christoph","full_name":"Kirsch, Christoph"},{"last_name":"Lippautz","first_name":"Michael","full_name":"Lippautz, Michael"},{"last_name":"Payer","first_name":"Hannes","full_name":"Payer, Hannes"},{"id":"4C7638DA-F248-11E8-B48F-1D18A9856A87","last_name":"Sezgin","first_name":"Ali","full_name":"Sezgin, Ali"},{"last_name":"Sokolova","full_name":"Sokolova, Ana","first_name":"Ana"},{"full_name":"Veith, Helmut","first_name":"Helmut","last_name":"Veith"}],"ddc":["004"],"publication":"Leibniz International Proceedings in Informatics","publist_id":"6280","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","doi":"10.4230/LIPIcs.CONCUR.2016.6","type":"conference","file_date_updated":"2018-12-12T10:10:10Z","language":[{"iso":"eng"}],"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,"project":[{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","name":"Quantitative Reactive Modeling","call_identifier":"FP7"},{"name":"The Wittgenstein Prize","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"date_updated":"2021-01-12T06:48:14Z","year":"2016","date_created":"2018-12-11T11:50:07Z","quality_controlled":"1","file":[{"file_name":"IST-2017-793-v1+1_LIPIcs-CONCUR-2016-6.pdf","date_created":"2018-12-12T10:10:10Z","file_id":"4795","content_type":"application/pdf","access_level":"open_access","date_updated":"2018-12-12T10:10:10Z","relation":"main_file","file_size":589747,"creator":"system"}],"volume":59,"acknowledgement":"This work has been supported by the National Research Network RiSE on Rigorous Systems Engineering\r\n(Austrian Science Fund (FWF): S11402-N23, S11403-N23, S11404-N23, S11411-N23), a Google\r\nPhD Fellowship, an Erwin Schrödinger Fellowship (Austrian Science Fund (FWF): J3696-N26), EPSRC\r\ngrants EP/H005633/1 and EP/K008528/1, the Vienna Science and Technology Fund (WWTF) trough\r\ngrant PROSEED, the European Research Council (ERC) under grant 267989 (QUAREM) and by the\r\nAustrian Science Fund (FWF) under grant Z211-N23 (Wittgenstein Award).","department":[{"_id":"ToHe"}],"alternative_title":["LIPIcs"],"pubrep_id":"793","_id":"1095","month":"08","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","publication_status":"published","oa":1,"title":"Local linearizability for concurrent container-type data structures","has_accepted_license":"1","day":"01","intvolume":"        59","citation":{"chicago":"Haas, Andreas, Thomas A Henzinger, Andreas Holzer, Christoph Kirsch, Michael Lippautz, Hannes Payer, Ali Sezgin, Ana Sokolova, and Helmut Veith. “Local Linearizability for Concurrent Container-Type Data Structures.” In <i>Leibniz International Proceedings in Informatics</i>, Vol. 59. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2016.6\">https://doi.org/10.4230/LIPIcs.CONCUR.2016.6</a>.","ista":"Haas A, Henzinger TA, Holzer A, Kirsch C, Lippautz M, Payer H, Sezgin A, Sokolova A, Veith H. 2016. Local linearizability for concurrent container-type data structures. Leibniz International Proceedings in Informatics. CONCUR: Concurrency Theory, LIPIcs, vol. 59, 6.","apa":"Haas, A., Henzinger, T. A., Holzer, A., Kirsch, C., Lippautz, M., Payer, H., … Veith, H. (2016). Local linearizability for concurrent container-type data structures. In <i>Leibniz International Proceedings in Informatics</i> (Vol. 59). Quebec City; Canada: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2016.6\">https://doi.org/10.4230/LIPIcs.CONCUR.2016.6</a>","ieee":"A. Haas <i>et al.</i>, “Local linearizability for concurrent container-type data structures,” in <i>Leibniz International Proceedings in Informatics</i>, Quebec City; Canada, 2016, vol. 59.","mla":"Haas, Andreas, et al. “Local Linearizability for Concurrent Container-Type Data Structures.” <i>Leibniz International Proceedings in Informatics</i>, vol. 59, 6, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016, doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2016.6\">10.4230/LIPIcs.CONCUR.2016.6</a>.","short":"A. Haas, T.A. Henzinger, A. Holzer, C. Kirsch, M. Lippautz, H. Payer, A. Sezgin, A. Sokolova, H. Veith, in:, Leibniz International Proceedings in Informatics, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016.","ama":"Haas A, Henzinger TA, Holzer A, et al. Local linearizability for concurrent container-type data structures. In: <i>Leibniz International Proceedings in Informatics</i>. Vol 59. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2016. doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2016.6\">10.4230/LIPIcs.CONCUR.2016.6</a>"},"ec_funded":1,"abstract":[{"text":" The semantics of concurrent data structures is usually given by a sequential specification and a consistency condition. Linearizability is the most popular consistency condition due to its simplicity and general applicability. Nevertheless, for applications that do not require all guarantees offered by linearizability, recent research has focused on improving performance and scalability of concurrent data structures by relaxing their semantics. In this paper, we present local linearizability, a relaxed consistency condition that is applicable to container-type concurrent data structures like pools, queues, and stacks. While linearizability requires that the effect of each operation is observed by all threads at the same time, local linearizability only requires that for each thread T, the effects of its local insertion operations and the effects of those removal operations that remove values inserted by T are observed by all threads at the same time. We investigate theoretical and practical properties of local linearizability and its relationship to many existing consistency conditions. We present a generic implementation method for locally linearizable data structures that uses existing linearizable data structures as building blocks. Our implementations show performance and scalability improvements over the original building blocks and outperform the fastest existing container-type implementations. ","lang":"eng"}],"status":"public","article_number":"6"},{"scopus_import":1,"citation":{"mla":"Gurung, Amit, et al. <i>Parallel Reachability Analysis for Hybrid Systems</i>. 7797741, IEEE, 2016, doi:<a href=\"https://doi.org/10.1109/MEMCOD.2016.7797741\">10.1109/MEMCOD.2016.7797741</a>.","ieee":"A. Gurung, A. Deka, E. Bartocci, S. Bogomolov, R. Grosu, and R. Ray, “Parallel reachability analysis for hybrid systems,” presented at the MEMOCODE: International Conference on Formal Methods and Models for System Design, Kanpur, India , 2016.","chicago":"Gurung, Amit, Arup Deka, Ezio Bartocci, Sergiy Bogomolov, Radu Grosu, and Rajarshi Ray. “Parallel Reachability Analysis for Hybrid Systems.” IEEE, 2016. <a href=\"https://doi.org/10.1109/MEMCOD.2016.7797741\">https://doi.org/10.1109/MEMCOD.2016.7797741</a>.","apa":"Gurung, A., Deka, A., Bartocci, E., Bogomolov, S., Grosu, R., &#38; Ray, R. (2016). Parallel reachability analysis for hybrid systems. Presented at the MEMOCODE: International Conference on Formal Methods and Models for System Design, Kanpur, India : IEEE. <a href=\"https://doi.org/10.1109/MEMCOD.2016.7797741\">https://doi.org/10.1109/MEMCOD.2016.7797741</a>","ista":"Gurung A, Deka A, Bartocci E, Bogomolov S, Grosu R, Ray R. 2016. Parallel reachability analysis for hybrid systems. MEMOCODE: International Conference on Formal Methods and Models for System Design, 7797741.","ama":"Gurung A, Deka A, Bartocci E, Bogomolov S, Grosu R, Ray R. Parallel reachability analysis for hybrid systems. In: IEEE; 2016. doi:<a href=\"https://doi.org/10.1109/MEMCOD.2016.7797741\">10.1109/MEMCOD.2016.7797741</a>","short":"A. Gurung, A. Deka, E. Bartocci, S. Bogomolov, R. Grosu, R. Ray, in:, IEEE, 2016."},"main_file_link":[{"url":"https://arxiv.org/abs/1606.05473","open_access":"1"}],"day":"27","abstract":[{"text":"We propose two parallel state-space-exploration algorithms for hybrid automaton (HA), with the goal of enhancing performance on multi-core shared-memory systems. The first uses the parallel, breadth-first-search algorithm (PBFS) of the SPIN model checker, when traversing the discrete modes of the HA, and enhances it with a parallel exploration of the continuous states within each mode. We show that this simple-minded extension of PBFS does not provide the desired load balancing in many HA benchmarks. The second algorithm is a task-parallel BFS algorithm (TP-BFS), which uses a cheap precomputation of the cost associated with the post operations (both continuous and discrete) in order to improve load balancing. We illustrate the TP-BFS and the cost precomputation of the post operators on a support-function-based algorithm for state-space exploration. The performance comparison of the two algorithms shows that, in general, TP-BFS provides a better utilization/load-balancing of the CPU. Both algorithms are implemented in the model checker XSpeed. Our experiments show a maximum speed-up of more than 2000 χ on a navigation benchmark, with respect to SpaceEx LGG scenario. In order to make the comparison fair, we employed an equal number of post operations in both tools. To the best of our knowledge, this paper represents the first attempt to provide parallel, reachability-analysis algorithms for HA.","lang":"eng"}],"article_number":"7797741","status":"public","ec_funded":1,"date_updated":"2021-01-12T06:48:18Z","project":[{"call_identifier":"FP7","name":"Quantitative Reactive Modeling","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"grant_number":"Z211","name":"The Wittgenstein Prize","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"}],"quality_controlled":"1","year":"2016","date_created":"2018-12-11T11:50:09Z","author":[{"last_name":"Gurung","first_name":"Amit","full_name":"Gurung, Amit"},{"full_name":"Deka, Arup","first_name":"Arup","last_name":"Deka"},{"last_name":"Bartocci","first_name":"Ezio","full_name":"Bartocci, Ezio"},{"orcid":"0000-0002-0686-0365","id":"369D9A44-F248-11E8-B48F-1D18A9856A87","last_name":"Bogomolov","full_name":"Bogomolov, Sergiy","first_name":"Sergiy"},{"last_name":"Grosu","first_name":"Radu","full_name":"Grosu, Radu"},{"last_name":"Ray","full_name":"Ray, Rajarshi","first_name":"Rajarshi"}],"publist_id":"6272","date_published":"2016-12-27T00:00:00Z","acknowledgement":"This work was supported in part by DST-SERB, GoI under Project No. YSS/2014/000623 and by the European Research Council (ERC) under grant 267989 (QUAREM) and by the Austrian Science Fund (FWF) under grants S11402-N23, S11405-N23 and S11412-N23 (RiSE/SHiNE) and Z211-N23 (Wittgenstein Award).","department":[{"_id":"ToHe"}],"conference":{"end_date":"2016-11-20","location":"Kanpur, India ","start_date":"2016-11-18","name":"MEMOCODE: International Conference on Formal Methods and Models for System Design"},"oa_version":"Preprint","type":"conference","oa":1,"title":"Parallel reachability analysis for hybrid systems","language":[{"iso":"eng"}],"publication_status":"published","publisher":"IEEE","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","_id":"1103","doi":"10.1109/MEMCOD.2016.7797741","month":"12"},{"degree_awarded":"PhD","ec_funded":1,"status":"public","abstract":[{"lang":"eng","text":"In this thesis we present a computer-aided programming approach to concurrency. Our approach helps the programmer by automatically fixing concurrency-related bugs, i.e. bugs that occur when the program is executed using an aggressive preemptive scheduler, but not when using a non-preemptive (cooperative) scheduler. Bugs are program behaviours that are incorrect w.r.t. a specification. We consider both user-provided explicit specifications in the form of assertion\r\nstatements in the code as well as an implicit specification. The implicit specification is inferred from the non-preemptive behaviour. Let us consider sequences of calls that the program makes to an external interface. The implicit specification requires that any such sequence produced under a preemptive scheduler should be included in the set of sequences produced under a non-preemptive scheduler. We consider several semantics-preserving fixes that go beyond atomic sections typically explored in the synchronisation synthesis literature. Our synthesis is able to place locks, barriers and wait-signal statements and last, but not least reorder independent statements. The latter may be useful if a thread is released to early, e.g., before some initialisation is completed. We guarantee that our synthesis does not introduce deadlocks and that the synchronisation inserted is optimal w.r.t. a given objective function. We dub our solution trace-based synchronisation synthesis and it is loosely based on counterexample-guided inductive synthesis (CEGIS). The synthesis works by discovering a trace that is incorrect w.r.t. the specification and identifying ordering constraints crucial to trigger the specification violation. Synchronisation may be placed immediately (greedy approach) or delayed until all incorrect traces are found (non-greedy approach). For the non-greedy approach we construct a set of global constraints over synchronisation placements. Each model of the global constraints set corresponds to a correctness-ensuring synchronisation placement. The placement that is optimal w.r.t. the given objective function is chosen as the synchronisation solution. We evaluate our approach on a number of realistic (albeit simplified) Linux device-driver\r\nbenchmarks. The benchmarks are versions of the drivers with known concurrency-related bugs. For the experiments with an explicit specification we added assertions that would detect the bugs in the experiments. Device drivers lend themselves to implicit specification, where the device and the operating system are the external interfaces. Our experiments demonstrate that our synthesis method is precise and efficient. We implemented objective functions for coarse-grained and fine-grained locking and observed that different synchronisation placements are produced for our experiments, favouring e.g. a minimal number of synchronisation operations or maximum concurrency."}],"day":"07","has_accepted_license":"1","supervisor":[{"orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger"}],"citation":{"ama":"Tarrach T. Automatic synthesis of synchronisation primitives for concurrent programs. 2016. doi:<a href=\"https://doi.org/10.15479/at:ista:1130\">10.15479/at:ista:1130</a>","short":"T. Tarrach, Automatic Synthesis of Synchronisation Primitives for Concurrent Programs, Institute of Science and Technology Austria, 2016.","ieee":"T. Tarrach, “Automatic synthesis of synchronisation primitives for concurrent programs,” Institute of Science and Technology Austria, 2016.","mla":"Tarrach, Thorsten. <i>Automatic Synthesis of Synchronisation Primitives for Concurrent Programs</i>. Institute of Science and Technology Austria, 2016, doi:<a href=\"https://doi.org/10.15479/at:ista:1130\">10.15479/at:ista:1130</a>.","chicago":"Tarrach, Thorsten. “Automatic Synthesis of Synchronisation Primitives for Concurrent Programs.” Institute of Science and Technology Austria, 2016. <a href=\"https://doi.org/10.15479/at:ista:1130\">https://doi.org/10.15479/at:ista:1130</a>.","apa":"Tarrach, T. (2016). <i>Automatic synthesis of synchronisation primitives for concurrent programs</i>. Institute of Science and Technology Austria. <a href=\"https://doi.org/10.15479/at:ista:1130\">https://doi.org/10.15479/at:ista:1130</a>","ista":"Tarrach T. 2016. Automatic synthesis of synchronisation primitives for concurrent programs. Institute of Science and Technology Austria."},"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","_id":"1130","month":"07","oa":1,"title":"Automatic synthesis of synchronisation primitives for concurrent programs","related_material":{"record":[{"relation":"part_of_dissertation","status":"public","id":"1729"},{"id":"2218","status":"public","relation":"part_of_dissertation"},{"id":"2445","status":"public","relation":"part_of_dissertation"}]},"publication_status":"published","department":[{"_id":"ToHe"},{"_id":"GradSch"}],"alternative_title":["ISTA Thesis"],"page":"151","year":"2016","date_created":"2018-12-11T11:50:19Z","date_updated":"2023-09-07T11:57:01Z","project":[{"call_identifier":"FP7","name":"Quantitative Reactive Modeling","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize","grant_number":"Z211","call_identifier":"FWF"}],"file":[{"file_size":1523935,"creator":"dernst","relation":"main_file","checksum":"319a506831650327e85376db41fc1094","content_type":"application/pdf","date_created":"2021-02-22T11:39:32Z","file_id":"9179","access_level":"open_access","success":1,"date_updated":"2021-02-22T11:39:32Z","file_name":"2016_Tarrach_Thesis.pdf"},{"content_type":"application/pdf","date_created":"2021-11-16T14:14:38Z","file_id":"10296","date_updated":"2021-11-17T13:46:55Z","access_level":"closed","file_name":"2016_Tarrach_Thesispdfa.pdf","file_size":1306068,"creator":"cchlebak","relation":"main_file","checksum":"39efcd789f0ad859ff15652cb7afc412"}],"article_processing_charge":"No","publication_identifier":{"issn":["2663-337X"]},"main_file_link":[{"url":"http://thorstent.github.io/theses/phd_thorsten_tarrach.pdf","open_access":"1"}],"doi":"10.15479/at:ista:1130","publisher":"Institute of Science and Technology Austria","language":[{"iso":"eng"}],"file_date_updated":"2021-11-17T13:46:55Z","type":"dissertation","oa_version":"Published Version","date_published":"2016-07-07T00:00:00Z","publist_id":"6230","ddc":["000"],"author":[{"orcid":"0000-0003-4409-8487","id":"3D6E8F2C-F248-11E8-B48F-1D18A9856A87","last_name":"Tarrach","full_name":"Tarrach, Thorsten","first_name":"Thorsten"}]},{"day":"10","citation":{"ista":"Duggirala P, Fan C, Potok M, Qi B, Mitra S, Viswanathan M, Bak S, Bogomolov S, Johnson T, Nguyen L, Schilling C, Sogokon A, Tran H, Xiang W. 2016. Tutorial: Software tools for hybrid systems verification transformation and synthesis C2E2 HyST and TuLiP. 2016 IEEE Conference on Control Applications. CCA: Control Applications , 7587948.","apa":"Duggirala, P., Fan, C., Potok, M., Qi, B., Mitra, S., Viswanathan, M., … Xiang, W. (2016). Tutorial: Software tools for hybrid systems verification transformation and synthesis C2E2 HyST and TuLiP. In <i>2016 IEEE Conference on Control Applications</i>. Buenos Aires, Argentina : IEEE. <a href=\"https://doi.org/10.1109/CCA.2016.7587948\">https://doi.org/10.1109/CCA.2016.7587948</a>","chicago":"Duggirala, Parasara, Chuchu Fan, Matthew Potok, Bolun Qi, Sayan Mitra, Mahesh Viswanathan, Stanley Bak, et al. “Tutorial: Software Tools for Hybrid Systems Verification Transformation and Synthesis C2E2 HyST and TuLiP.” In <i>2016 IEEE Conference on Control Applications</i>. IEEE, 2016. <a href=\"https://doi.org/10.1109/CCA.2016.7587948\">https://doi.org/10.1109/CCA.2016.7587948</a>.","ieee":"P. Duggirala <i>et al.</i>, “Tutorial: Software tools for hybrid systems verification transformation and synthesis C2E2 HyST and TuLiP,” in <i>2016 IEEE Conference on Control Applications</i>, Buenos Aires, Argentina , 2016.","mla":"Duggirala, Parasara, et al. “Tutorial: Software Tools for Hybrid Systems Verification Transformation and Synthesis C2E2 HyST and TuLiP.” <i>2016 IEEE Conference on Control Applications</i>, 7587948, IEEE, 2016, doi:<a href=\"https://doi.org/10.1109/CCA.2016.7587948\">10.1109/CCA.2016.7587948</a>.","short":"P. Duggirala, C. Fan, M. Potok, B. Qi, S. Mitra, M. Viswanathan, S. Bak, S. Bogomolov, T. Johnson, L. Nguyen, C. Schilling, A. Sogokon, H. Tran, W. Xiang, in:, 2016 IEEE Conference on Control Applications, IEEE, 2016.","ama":"Duggirala P, Fan C, Potok M, et al. Tutorial: Software tools for hybrid systems verification transformation and synthesis C2E2 HyST and TuLiP. In: <i>2016 IEEE Conference on Control Applications</i>. IEEE; 2016. doi:<a href=\"https://doi.org/10.1109/CCA.2016.7587948\">10.1109/CCA.2016.7587948</a>"},"scopus_import":1,"date_updated":"2021-01-12T06:48:32Z","year":"2016","date_created":"2018-12-11T11:50:20Z","quality_controlled":"1","abstract":[{"text":"Hybrid systems have both continuous and discrete dynamics and are useful for modeling a variety of control systems, from air traffic control protocols to robotic maneuvers and beyond. Recently, numerous powerful and scalable tools for analyzing hybrid systems have emerged. Several of these tools implement automated formal methods for mathematically proving a system meets a specification. This tutorial session will present three recent hybrid systems tools: C2E2, HyST, and TuLiP. C2E2 is a simulated-based verification tool for hybrid systems, and uses validated numerical solvers and bloating of simulation traces to verify systems meet specifications. HyST is a hybrid systems model transformation and translation tool, and uses a canonical intermediate representation to support most of the recent verification tools, as well as automated sound abstractions that simplify verification of a given hybrid system. TuLiP is a controller synthesis tool for hybrid systems, where given a temporal logic specification to be satisfied for a system (plant) model, TuLiP will find a controller that meets a given specification. © 2016 IEEE.","lang":"eng"}],"status":"public","article_number":"7587948","department":[{"_id":"ToHe"}],"date_published":"2016-10-10T00:00:00Z","conference":{"end_date":"2016-09-22","location":"Buenos Aires, Argentina ","start_date":"2016-09-19","name":"CCA: Control Applications "},"oa_version":"None","author":[{"first_name":"Parasara","full_name":"Duggirala, Parasara","last_name":"Duggirala"},{"first_name":"Chuchu","full_name":"Fan, Chuchu","last_name":"Fan"},{"full_name":"Potok, Matthew","first_name":"Matthew","last_name":"Potok"},{"first_name":"Bolun","full_name":"Qi, Bolun","last_name":"Qi"},{"full_name":"Mitra, Sayan","first_name":"Sayan","last_name":"Mitra"},{"full_name":"Viswanathan, Mahesh","first_name":"Mahesh","last_name":"Viswanathan"},{"last_name":"Bak","first_name":"Stanley","full_name":"Bak, Stanley"},{"id":"369D9A44-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-0686-0365","last_name":"Bogomolov","first_name":"Sergiy","full_name":"Bogomolov, Sergiy"},{"first_name":"Taylor","full_name":"Johnson, Taylor","last_name":"Johnson"},{"first_name":"Luan","full_name":"Nguyen, Luan","last_name":"Nguyen"},{"last_name":"Schilling","full_name":"Schilling, Christian","first_name":"Christian","id":"3A2F4DCE-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-3658-1065"},{"first_name":"Andrew","full_name":"Sogokon, Andrew","last_name":"Sogokon"},{"last_name":"Tran","full_name":"Tran, Hoang","first_name":"Hoang"},{"first_name":"Weiming","full_name":"Xiang, Weiming","last_name":"Xiang"}],"publication":"2016 IEEE Conference on Control Applications","publist_id":"6224","publisher":"IEEE","doi":"10.1109/CCA.2016.7587948","_id":"1134","month":"10","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","type":"conference","publication_status":"published","language":[{"iso":"eng"}],"title":"Tutorial: Software tools for hybrid systems verification transformation and synthesis C2E2 HyST and TuLiP"},{"publication":"Proceedings of the 13th International Conference on Embedded Software ","publist_id":"6223","author":[{"id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-5588-8287","first_name":"Guy","full_name":"Avni, Guy","last_name":"Avni"},{"full_name":"Guha, Shibashis","first_name":"Shibashis","last_name":"Guha"},{"full_name":"Rodríguez Navas, Guillermo","first_name":"Guillermo","last_name":"Rodríguez Navas"}],"ddc":["000"],"oa_version":"Submitted Version","conference":{"name":"EMSOFT: Embedded Software ","start_date":"2016-10-01","location":"Pittsburgh, PA, USA","end_date":"2016-10-07"},"date_published":"2016-10-01T00:00:00Z","language":[{"iso":"eng"}],"type":"conference","file_date_updated":"2018-12-12T10:09:31Z","doi":"10.1145/2968478.2968499","publisher":"ACM","scopus_import":1,"file":[{"file_size":279240,"creator":"system","relation":"main_file","content_type":"application/pdf","date_created":"2018-12-12T10:09:31Z","file_id":"4755","access_level":"open_access","date_updated":"2018-12-12T10:09:31Z","file_name":"IST-2016-644-v1+1_emsoft-no-format.pdf"}],"year":"2016","date_created":"2018-12-11T11:50:20Z","quality_controlled":"1","project":[{"call_identifier":"FP7","name":"Quantitative Reactive Modeling","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"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"}],"date_updated":"2021-01-12T06:48:33Z","pubrep_id":"644","department":[{"_id":"ToHe"}],"publication_status":"published","oa":1,"title":"Synthesizing time triggered schedules for switched networks with faulty links","month":"10","_id":"1135","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","citation":{"ama":"Avni G, Guha S, Rodríguez Navas G. Synthesizing time triggered schedules for switched networks with faulty links. In: <i>Proceedings of the 13th International Conference on Embedded Software </i>. ACM; 2016. doi:<a href=\"https://doi.org/10.1145/2968478.2968499\">10.1145/2968478.2968499</a>","short":"G. Avni, S. Guha, G. Rodríguez Navas, in:, Proceedings of the 13th International Conference on Embedded Software , ACM, 2016.","mla":"Avni, Guy, et al. “Synthesizing Time Triggered Schedules for Switched Networks with Faulty Links.” <i>Proceedings of the 13th International Conference on Embedded Software </i>, 26, ACM, 2016, doi:<a href=\"https://doi.org/10.1145/2968478.2968499\">10.1145/2968478.2968499</a>.","ieee":"G. Avni, S. Guha, and G. Rodríguez Navas, “Synthesizing time triggered schedules for switched networks with faulty links,” in <i>Proceedings of the 13th International Conference on Embedded Software </i>, Pittsburgh, PA, USA, 2016.","ista":"Avni G, Guha S, Rodríguez Navas G. 2016. Synthesizing time triggered schedules for switched networks with faulty links. Proceedings of the 13th International Conference on Embedded Software . EMSOFT: Embedded Software , 26.","chicago":"Avni, Guy, Shibashis Guha, and Guillermo Rodríguez Navas. “Synthesizing Time Triggered Schedules for Switched Networks with Faulty Links.” In <i>Proceedings of the 13th International Conference on Embedded Software </i>. ACM, 2016. <a href=\"https://doi.org/10.1145/2968478.2968499\">https://doi.org/10.1145/2968478.2968499</a>.","apa":"Avni, G., Guha, S., &#38; Rodríguez Navas, G. (2016). Synthesizing time triggered schedules for switched networks with faulty links. In <i>Proceedings of the 13th International Conference on Embedded Software </i>. Pittsburgh, PA, USA: ACM. <a href=\"https://doi.org/10.1145/2968478.2968499\">https://doi.org/10.1145/2968478.2968499</a>"},"day":"01","has_accepted_license":"1","status":"public","article_number":"26","abstract":[{"lang":"eng","text":"Time-triggered (TT) switched networks are a deterministic communication infrastructure used by real-time distributed embedded systems. These networks rely on the notion of globally discretized time (i.e. time slots) and a static TT schedule that prescribes which message is sent through which link at every time slot, such that all messages reach their destination before a global timeout. These schedules are generated offline, assuming a static network with fault-free links, and entrusting all error-handling functions to the end user. Assuming the network is static is an over-optimistic view, and indeed links tend to fail in practice. We study synthesis of TT schedules on a network in which links fail over time and we assume the switches run a very simple error-recovery protocol once they detect a crashed link. We address the problem of finding a pk; qresistant schedule; namely, one that, assuming the switches run a fixed error-recovery protocol, guarantees that the number of messages that arrive at their destination by the timeout is at least no matter what sequence of at most k links fail. Thus, we maintain the simplicity of the switches while giving a guarantee on the number of messages that meet the timeout. We show how a pk; q-resistant schedule can be obtained using a CEGAR-like approach: find a schedule, decide whether it is pk; q-resistant, and if it is not, use the witnessing fault sequence to generate a constraint that is added to the program. The newly added constraint disallows the schedule to be regenerated in a future iteration while also eliminating several other schedules that are not pk; q-resistant. We illustrate the applicability of our approach using an SMT-based implementation. © 2016 ACM."}],"ec_funded":1},{"publication":"Proceedings of the 31st Annual ACM/IEEE Symposium","publist_id":"6220","author":[{"first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","last_name":"Henzinger","full_name":"Henzinger, Thomas A","first_name":"Thomas A"},{"id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","last_name":"Otop","full_name":"Otop, Jan","first_name":"Jan"}],"oa_version":"Preprint","conference":{"start_date":"2016-07-05","name":"LICS: Logic in Computer Science","end_date":"2016-07-08","location":"New York, NY, USA"},"external_id":{"arxiv":["1604.06764"]},"date_published":"2016-07-05T00:00:00Z","language":[{"iso":"eng"}],"arxiv":1,"type":"conference","doi":"10.1145/2933575.2933588","publisher":"IEEE","scopus_import":1,"main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1604.06764"}],"page":"76 - 85","quality_controlled":"1","date_created":"2018-12-11T11:50:21Z","year":"2016","date_updated":"2021-01-12T06:48:34Z","project":[{"call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","name":"Quantitative Reactive Modeling"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"grant_number":"Z211","name":"The Wittgenstein Prize","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23","call_identifier":"FWF"},{"grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification"}],"acknowledgement":"This research was funded in part by the European Research Council (ERC) under grant agreement 267989 (QUAREM), by the Austrian Science Fund (FWF) projects S11402-N23 (RiSE) and Z211-N23 (Wittgenstein Award), FWF Grant No P23499- N23, FWF NFN Grant No S114","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"oa":1,"title":"Quantitative automata under probabilistic semantics","publication_status":"published","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"1138","month":"07","citation":{"apa":"Chatterjee, K., Henzinger, T. A., &#38; Otop, J. (2016). Quantitative automata under probabilistic semantics. In <i>Proceedings of the 31st Annual ACM/IEEE Symposium</i> (pp. 76–85). New York, NY, USA: IEEE. <a href=\"https://doi.org/10.1145/2933575.2933588\">https://doi.org/10.1145/2933575.2933588</a>","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. “Quantitative Automata under Probabilistic Semantics.” In <i>Proceedings of the 31st Annual ACM/IEEE Symposium</i>, 76–85. IEEE, 2016. <a href=\"https://doi.org/10.1145/2933575.2933588\">https://doi.org/10.1145/2933575.2933588</a>.","ista":"Chatterjee K, Henzinger TA, Otop J. 2016. Quantitative automata under probabilistic semantics. Proceedings of the 31st Annual ACM/IEEE Symposium. LICS: Logic in Computer Science, 76–85.","ieee":"K. Chatterjee, T. A. Henzinger, and J. Otop, “Quantitative automata under probabilistic semantics,” in <i>Proceedings of the 31st Annual ACM/IEEE Symposium</i>, New York, NY, USA, 2016, pp. 76–85.","mla":"Chatterjee, Krishnendu, et al. “Quantitative Automata under Probabilistic Semantics.” <i>Proceedings of the 31st Annual ACM/IEEE Symposium</i>, IEEE, 2016, pp. 76–85, doi:<a href=\"https://doi.org/10.1145/2933575.2933588\">10.1145/2933575.2933588</a>.","short":"K. Chatterjee, T.A. Henzinger, J. Otop, in:, Proceedings of the 31st Annual ACM/IEEE Symposium, IEEE, 2016, pp. 76–85.","ama":"Chatterjee K, Henzinger TA, Otop J. Quantitative automata under probabilistic semantics. In: <i>Proceedings of the 31st Annual ACM/IEEE Symposium</i>. IEEE; 2016:76-85. doi:<a href=\"https://doi.org/10.1145/2933575.2933588\">10.1145/2933575.2933588</a>"},"day":"05","status":"public","abstract":[{"lang":"eng","text":"Automata with monitor counters, where the transitions do not depend on counter values, and nested weighted automata are two expressive automata-theoretic frameworks for quantitative properties. For a well-studied and wide class of quantitative functions, we establish that automata with monitor counters and nested weighted automata are equivalent. We study for the first time such quantitative automata under probabilistic semantics. We show that several problems that are undecidable for the classical questions of emptiness and universality become decidable under the probabilistic semantics. We present a complete picture of decidability for such automata, and even an almost-complete picture of computational complexity, for the probabilistic questions we consider. © 2016 ACM."}],"ec_funded":1},{"acknowledgement":"This work is based on the CMSB 2015 paper “Adaptive moment closure for parameter inference of biochemical reaction networks” (Bogomolov et al., 2015). The work was partly supported by the German Research Foundation (DFG) as part of the Transregional Collaborative Research Center “Automatic Verification and Analysis of Complex Systems” (SFB/TR 14 AVACS1), by the European Research Council (ERC) under grant 267989 (QUAREM) and by the Austrian Science Fund (FWF) under grants S11402-N23 (RiSE) and Z211-N23 (Wittgenstein Award). J.R. acknowledges support from the People Programme (Marie Curie Actions) of the European Union's Seventh Framework Programme (FP7/2007-2013) under REA grant agreement no. 291734.","department":[{"_id":"ToHe"},{"_id":"GaTk"}],"publication_status":"published","related_material":{"record":[{"relation":"earlier_version","status":"public","id":"1658"}]},"title":"Adaptive moment closure for parameter inference of biochemical reaction networks","_id":"1148","month":"11","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","intvolume":"       149","citation":{"chicago":"Schilling, Christian, Sergiy Bogomolov, Thomas A Henzinger, Andreas Podelski, and Jakob Ruess. “Adaptive Moment Closure for Parameter Inference of Biochemical Reaction Networks.” <i>Biosystems</i>. Elsevier, 2016. <a href=\"https://doi.org/10.1016/j.biosystems.2016.07.005\">https://doi.org/10.1016/j.biosystems.2016.07.005</a>.","apa":"Schilling, C., Bogomolov, S., Henzinger, T. A., Podelski, A., &#38; Ruess, J. (2016). Adaptive moment closure for parameter inference of biochemical reaction networks. <i>Biosystems</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.biosystems.2016.07.005\">https://doi.org/10.1016/j.biosystems.2016.07.005</a>","ista":"Schilling C, Bogomolov S, Henzinger TA, Podelski A, Ruess J. 2016. Adaptive moment closure for parameter inference of biochemical reaction networks. Biosystems. 149, 15–25.","ieee":"C. Schilling, S. Bogomolov, T. A. Henzinger, A. Podelski, and J. Ruess, “Adaptive moment closure for parameter inference of biochemical reaction networks,” <i>Biosystems</i>, vol. 149. Elsevier, pp. 15–25, 2016.","mla":"Schilling, Christian, et al. “Adaptive Moment Closure for Parameter Inference of Biochemical Reaction Networks.” <i>Biosystems</i>, vol. 149, Elsevier, 2016, pp. 15–25, doi:<a href=\"https://doi.org/10.1016/j.biosystems.2016.07.005\">10.1016/j.biosystems.2016.07.005</a>.","short":"C. Schilling, S. Bogomolov, T.A. Henzinger, A. Podelski, J. Ruess, Biosystems 149 (2016) 15–25.","ama":"Schilling C, Bogomolov S, Henzinger TA, Podelski A, Ruess J. Adaptive moment closure for parameter inference of biochemical reaction networks. <i>Biosystems</i>. 2016;149:15-25. doi:<a href=\"https://doi.org/10.1016/j.biosystems.2016.07.005\">10.1016/j.biosystems.2016.07.005</a>"},"day":"01","status":"public","abstract":[{"lang":"eng","text":"Continuous-time Markov chain (CTMC) models have become a central tool for understanding the dynamics of complex reaction networks and the importance of stochasticity in the underlying biochemical processes. When such models are employed to answer questions in applications, in order to ensure that the model provides a sufficiently accurate representation of the real system, it is of vital importance that the model parameters are inferred from real measured data. This, however, is often a formidable task and all of the existing methods fail in one case or the other, usually because the underlying CTMC model is high-dimensional and computationally difficult to analyze. The parameter inference methods that tend to scale best in the dimension of the CTMC are based on so-called moment closure approximations. However, there exists a large number of different moment closure approximations and it is typically hard to say a priori which of the approximations is the most suitable for the inference procedure. Here, we propose a moment-based parameter inference method that automatically chooses the most appropriate moment closure method. Accordingly, contrary to existing methods, the user is not required to be experienced in moment closure techniques. In addition to that, our method adaptively changes the approximation during the parameter inference to ensure that always the best approximation is used, even in cases where different approximations are best in different regions of the parameter space. © 2016 Elsevier Ireland Ltd"}],"ec_funded":1,"publist_id":"6210","publication":"Biosystems","author":[{"last_name":"Schilling","full_name":"Schilling, Christian","first_name":"Christian"},{"full_name":"Bogomolov, Sergiy","first_name":"Sergiy","last_name":"Bogomolov","orcid":"0000-0002-0686-0365","id":"369D9A44-F248-11E8-B48F-1D18A9856A87"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","last_name":"Henzinger","full_name":"Henzinger, Thomas A","first_name":"Thomas A"},{"last_name":"Podelski","first_name":"Andreas","full_name":"Podelski, Andreas"},{"id":"4A245D00-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-1615-3282","last_name":"Ruess","first_name":"Jakob","full_name":"Ruess, Jakob"}],"oa_version":"None","date_published":"2016-11-01T00:00:00Z","language":[{"iso":"eng"}],"type":"journal_article","doi":"10.1016/j.biosystems.2016.07.005","publisher":"Elsevier","scopus_import":1,"volume":149,"date_created":"2018-12-11T11:50:24Z","year":"2016","quality_controlled":"1","page":"15 - 25","project":[{"call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","name":"Quantitative Reactive Modeling"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize","grant_number":"Z211"},{"call_identifier":"FP7","_id":"25681D80-B435-11E9-9278-68D0E5697425","name":"International IST Postdoc Fellowship Programme","grant_number":"291734"}],"date_updated":"2023-02-23T10:08:46Z"},{"oa_version":"None","conference":{"start_date":"2016-02-12","name":"AAAI: Conference on Artificial Intelligence","end_date":"2016-02-17","location":"Phoenix, AZ, USA"},"department":[{"_id":"KrCh"},{"_id":"ToHe"}],"date_published":"2016-12-02T00:00:00Z","publication":"Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence","publist_id":"6191","author":[{"first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Chmelik, Martin","first_name":"Martin","last_name":"Chmelik","id":"3624234E-F248-11E8-B48F-1D18A9856A87"},{"id":"378E0060-F248-11E8-B48F-1D18A9856A87","first_name":"Jessica","full_name":"Davies, Jessica","last_name":"Davies"}],"_id":"1166","month":"12","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","publisher":"AAAI Press","language":[{"iso":"eng"}],"publication_status":"published","related_material":{"link":[{"relation":"table_of_contents","url":"https://dl.acm.org/citation.cfm?id=3016355"}],"record":[{"id":"5443","status":"public","relation":"earlier_version"}]},"title":"A symbolic SAT based algorithm for almost sure reachability with small strategies in pomdps","type":"conference","day":"02","intvolume":"      2016","citation":{"ista":"Chatterjee K, Chmelik M, Davies J. 2016. A symbolic SAT based algorithm for almost sure reachability with small strategies in pomdps. Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence. AAAI: Conference on Artificial Intelligence vol. 2016, 3225–3232.","apa":"Chatterjee, K., Chmelik, M., &#38; Davies, J. (2016). A symbolic SAT based algorithm for almost sure reachability with small strategies in pomdps. In <i>Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence</i> (Vol. 2016, pp. 3225–3232). Phoenix, AZ, USA: AAAI Press.","chicago":"Chatterjee, Krishnendu, Martin Chmelik, and Jessica Davies. “A Symbolic SAT Based Algorithm for Almost Sure Reachability with Small Strategies in Pomdps.” In <i>Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence</i>, 2016:3225–32. AAAI Press, 2016.","ieee":"K. Chatterjee, M. Chmelik, and J. Davies, “A symbolic SAT based algorithm for almost sure reachability with small strategies in pomdps,” in <i>Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence</i>, Phoenix, AZ, USA, 2016, vol. 2016, pp. 3225–3232.","mla":"Chatterjee, Krishnendu, et al. “A Symbolic SAT Based Algorithm for Almost Sure Reachability with Small Strategies in Pomdps.” <i>Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence</i>, vol. 2016, AAAI Press, 2016, pp. 3225–32.","short":"K. Chatterjee, M. Chmelik, J. Davies, in:, Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence, AAAI Press, 2016, pp. 3225–3232.","ama":"Chatterjee K, Chmelik M, Davies J. A symbolic SAT based algorithm for almost sure reachability with small strategies in pomdps. In: <i>Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence</i>. Vol 2016. AAAI Press; 2016:3225-3232."},"year":"2016","date_created":"2018-12-11T11:50:30Z","quality_controlled":"1","page":"3225 - 3232","project":[{"_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"},{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications"}],"date_updated":"2023-02-23T12:26:41Z","ec_funded":1,"status":"public","volume":2016,"abstract":[{"lang":"eng","text":"POMDPs are standard models for probabilistic planning problems, where an agent interacts with an uncertain environment. We study the problem of almost-sure reachability, where given a set of target states, the question is to decide whether there is a policy to ensure that the target set is reached with probability 1 (almost-surely). While in general the problem is EXPTIMEcomplete, in many practical cases policies with a small amount of memory suffice. Moreover, the existing solution to the problem is explicit, which first requires to construct explicitly an exponential reduction to a belief-support MDP. In this work, we first study the existence of observation-stationary strategies, which is NP-complete, and then small-memory strategies. We present a symbolic algorithm by an efficient encoding to SAT and using a SAT solver for the problem. We report experimental results demonstrating the scalability of our symbolic (SAT-based) approach. © 2016, Association for the Advancement of Artificial Intelligence (www.aaai.org). All rights reserved."}]},{"abstract":[{"lang":"eng","text":"In this paper, we present a formal model-driven engineering approach to establishing a safety-assured implementation of Multifunction vehicle bus controller (MVBC) based on the generic reference models and requirements described in the International Electrotechnical Commission (IEC) standard IEC-61375. First, the generic models described in IEC-61375 are translated into a network of timed automata, and some safety requirements tested in IEC-61375 are formalized as timed computation tree logic (TCTL) formulas. With the help of Uppaal, we check and debug whether the timed automata satisfy the formulas or not. Within this step, several logic inconsistencies in the original standard are detected and corrected. Then, we apply the tool Times to generate C code from the verified model, which was later synthesized into a real MVBC chip. Finally, the runtime verification tool RMOR is applied to verify some safety requirements at the implementation level. We set up a real platform with worldwide mostly used MVBC D113, and verify the correctness and the scalability of the synthesized MVBC chip more comprehensively. The errors in the standard has been confirmed and the resulted MVBC has been deployed in real train communication network."}],"status":"public","has_accepted_license":"1","day":"08","citation":{"ieee":"Y. Jiang <i>et al.</i>, “Safety assured formal model driven design of the multifunction vehicle bus controller,” presented at the FM: International Symposium on Formal Methods, Limassol, Cyprus, 2016, vol. 9995, pp. 757–763.","mla":"Jiang, Yu, et al. <i>Safety Assured Formal Model Driven Design of the Multifunction Vehicle Bus Controller</i>. Vol. 9995, Springer, 2016, pp. 757–63, doi:<a href=\"https://doi.org/10.1007/978-3-319-48989-6_47\">10.1007/978-3-319-48989-6_47</a>.","apa":"Jiang, Y., Liu, H., Song, H., Kong, H., Gu, M., Sun, J., &#38; Sha, L. (2016). Safety assured formal model driven design of the multifunction vehicle bus controller (Vol. 9995, pp. 757–763). Presented at the FM: International Symposium on Formal Methods, Limassol, Cyprus: Springer. <a href=\"https://doi.org/10.1007/978-3-319-48989-6_47\">https://doi.org/10.1007/978-3-319-48989-6_47</a>","ista":"Jiang Y, Liu H, Song H, Kong H, Gu M, Sun J, Sha L. 2016. Safety assured formal model driven design of the multifunction vehicle bus controller. FM: International Symposium on Formal Methods, LNCS, vol. 9995, 757–763.","chicago":"Jiang, Yu, Han Liu, Houbing Song, Hui Kong, Ming Gu, Jiaguang Sun, and Lui Sha. “Safety Assured Formal Model Driven Design of the Multifunction Vehicle Bus Controller,” 9995:757–63. Springer, 2016. <a href=\"https://doi.org/10.1007/978-3-319-48989-6_47\">https://doi.org/10.1007/978-3-319-48989-6_47</a>.","ama":"Jiang Y, Liu H, Song H, et al. Safety assured formal model driven design of the multifunction vehicle bus controller. In: Vol 9995. Springer; 2016:757-763. doi:<a href=\"https://doi.org/10.1007/978-3-319-48989-6_47\">10.1007/978-3-319-48989-6_47</a>","short":"Y. Jiang, H. Liu, H. Song, H. Kong, M. Gu, J. Sun, L. Sha, in:, Springer, 2016, pp. 757–763."},"intvolume":"      9995","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","month":"11","_id":"1205","oa":1,"related_material":{"record":[{"id":"434","status":"public","relation":"later_version"}]},"title":"Safety assured formal model driven design of the multifunction vehicle bus controller","publication_status":"published","department":[{"_id":"ToHe"}],"acknowledgement":"This research is sponsored in part by NSFC Program (No. 91218302, No. 61527812), National Science and Technology Major Project (No. 2016ZX01038101), Tsinghua University Initiative Scientific Research Program (20131089331), MIIT IT funds (Research and application of TCN key technologies) of China, and the National Key Technology R&D Program (No. 2015BAG14B01-02), Austrian Science Fund (FWF) under grants S11402-N23 (RiSE/SHiNE) and Z211-N23.\r\n","alternative_title":["LNCS"],"pubrep_id":"783","date_updated":"2023-09-18T08:12:48Z","project":[{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize","grant_number":"Z211"}],"quality_controlled":"1","page":"757 - 763","year":"2016","date_created":"2018-12-11T11:50:42Z","volume":9995,"file":[{"file_size":281501,"creator":"system","relation":"main_file","checksum":"fea0b3fae9a2a42e8bfec59840e30d8c","file_id":"4673","content_type":"application/pdf","date_created":"2018-12-12T10:08:13Z","date_updated":"2020-07-14T12:44:39Z","access_level":"open_access","file_name":"IST-2017-783-v1+1_FM-Safety-Assured-Development-of-MVBC.pdf"}],"scopus_import":1,"publisher":"Springer","doi":"10.1007/978-3-319-48989-6_47","file_date_updated":"2020-07-14T12:44:39Z","type":"conference","language":[{"iso":"eng"}],"date_published":"2016-11-08T00:00:00Z","conference":{"name":"FM: International Symposium on Formal Methods","start_date":"2016-11-09","location":"Limassol, Cyprus","end_date":"2016-11-11"},"oa_version":"Submitted Version","ddc":["004"],"author":[{"last_name":"Jiang","full_name":"Jiang, Yu","first_name":"Yu"},{"first_name":"Han","full_name":"Liu, Han","last_name":"Liu"},{"last_name":"Song","first_name":"Houbing","full_name":"Song, Houbing"},{"id":"3BDE25AA-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-3066-6941","full_name":"Kong, Hui","first_name":"Hui","last_name":"Kong"},{"first_name":"Ming","full_name":"Gu, Ming","last_name":"Gu"},{"first_name":"Jiaguang","full_name":"Sun, Jiaguang","last_name":"Sun"},{"last_name":"Sha","first_name":"Lui","full_name":"Sha, Lui"}],"publist_id":"6144"},{"alternative_title":["Proceedings International Conference on Software Engineering"],"publication":"Proceedings of the 38th International Conference on Software Engineering Companion ","publist_id":"7341","author":[{"last_name":"Jiang","first_name":"Yu","full_name":"Jiang, Yu"},{"first_name":"Han","full_name":"Liu, Han","last_name":"Liu"},{"id":"3BDE25AA-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-3066-6941","last_name":"Kong","first_name":"Hui","full_name":"Kong, Hui"},{"last_name":"Wang","first_name":"Rui","full_name":"Wang, Rui"},{"last_name":"Hosseini","full_name":"Hosseini, Mohamad","first_name":"Mohamad"},{"full_name":"Sun, Jiaguang","first_name":"Jiaguang","last_name":"Sun"},{"last_name":"Sha","first_name":"Lui","full_name":"Sha, Lui"}],"oa_version":"None","conference":{"start_date":"2016-05-14","name":"ICSE: International Conference on Software Engineering","end_date":"2016-05-22","location":"Austin, TX, USA"},"date_published":"2016-05-14T00:00:00Z","department":[{"_id":"ToHe"}],"acknowledgement":"This work is supported by NSF CNS 13-30077, NSF CNS 13-29886, NSF CNS 15-45002, and NSFC 61303014.\r\nThe authors thank Dr.  Bobby and Dr.  Hill at Carle Hospital, Urbana, IL for their help with the discussion on medical  knowledge.\r\n\r\n","title":"Use runtime verification to improve the quality of medical care practice","language":[{"iso":"eng"}],"publication_status":"published","type":"conference","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","_id":"479","month":"05","doi":"10.1145/2889160.2889233","publisher":"IEEE","scopus_import":1,"citation":{"chicago":"Jiang, Yu, Han Liu, Hui Kong, Rui Wang, Mohamad Hosseini, Jiaguang Sun, and Lui Sha. “Use Runtime Verification to Improve the Quality of Medical Care Practice.” In <i>Proceedings of the 38th International Conference on Software Engineering Companion </i>, 112–21. IEEE, 2016. <a href=\"https://doi.org/10.1145/2889160.2889233\">https://doi.org/10.1145/2889160.2889233</a>.","apa":"Jiang, Y., Liu, H., Kong, H., Wang, R., Hosseini, M., Sun, J., &#38; Sha, L. (2016). Use runtime verification to improve the quality of medical care practice. In <i>Proceedings of the 38th International Conference on Software Engineering Companion </i> (pp. 112–121). Austin, TX, USA: IEEE. <a href=\"https://doi.org/10.1145/2889160.2889233\">https://doi.org/10.1145/2889160.2889233</a>","ista":"Jiang Y, Liu H, Kong H, Wang R, Hosseini M, Sun J, Sha L. 2016. Use runtime verification to improve the quality of medical care practice. Proceedings of the 38th International Conference on Software Engineering Companion . ICSE: International Conference on Software Engineering, Proceedings International Conference on Software Engineering, , 112–121.","mla":"Jiang, Yu, et al. “Use Runtime Verification to Improve the Quality of Medical Care Practice.” <i>Proceedings of the 38th International Conference on Software Engineering Companion </i>, IEEE, 2016, pp. 112–21, doi:<a href=\"https://doi.org/10.1145/2889160.2889233\">10.1145/2889160.2889233</a>.","ieee":"Y. Jiang <i>et al.</i>, “Use runtime verification to improve the quality of medical care practice,” in <i>Proceedings of the 38th International Conference on Software Engineering Companion </i>, Austin, TX, USA, 2016, pp. 112–121.","short":"Y. Jiang, H. Liu, H. Kong, R. Wang, M. Hosseini, J. Sun, L. Sha, in:, Proceedings of the 38th International Conference on Software Engineering Companion , IEEE, 2016, pp. 112–121.","ama":"Jiang Y, Liu H, Kong H, et al. Use runtime verification to improve the quality of medical care practice. In: <i>Proceedings of the 38th International Conference on Software Engineering Companion </i>. IEEE; 2016:112-121. doi:<a href=\"https://doi.org/10.1145/2889160.2889233\">10.1145/2889160.2889233</a>"},"day":"14","status":"public","abstract":[{"text":"Clinical guidelines and decision support systems (DSS) play an important role in daily practices of medicine. Many text-based guidelines have been encoded for work-flow simulation of DSS to automate health care. During the collaboration with Carle hospital to develop a DSS, we identify that, for some complex and life-critical diseases, it is highly desirable to automatically rigorously verify some complex temporal properties in guidelines, which brings new challenges to current simulation based DSS with limited support of automatical formal verification and real-time data analysis. In this paper, we conduct the first study on applying runtime verification to cooperate with current DSS based on real-time data. Within the proposed technique, a user-friendly domain specific language, named DRTV, is designed to specify vital real-time data sampled by medical devices and temporal properties originated from clinical guidelines. Some interfaces are developed for data acquisition and communication. Then, for medical practice scenarios described in DRTV model, we will automatically generate event sequences and runtime property verifier automata. If a temporal property violates, real-time warnings will be produced by the formal verifier and passed to medical DSS. We have used DRTV to specify different kinds of medical care scenarios, and applied the proposed technique to assist existing DSS. As presented in experiment results, in terms of warning detection, it outperforms the only use of DSS or human inspection, and improves the quality of clinical health care of hospital","lang":"eng"}],"quality_controlled":"1","page":"112 - 121","date_created":"2018-12-11T11:46:42Z","year":"2016","date_updated":"2021-01-12T08:00:55Z"},{"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","month":"01","_id":"1498","oa":1,"title":"The need for language support for fault-tolerant distributed systems","publication_status":"published","department":[{"_id":"ToHe"}],"alternative_title":["LIPIcs"],"pubrep_id":"499","ec_funded":1,"status":"public","abstract":[{"lang":"eng","text":"Fault-tolerant distributed algorithms play an important role in many critical/high-availability applications. These algorithms are notoriously difficult to implement correctly, due to asynchronous communication and the occurrence of faults, such as the network dropping messages or computers crashing. Nonetheless there is surprisingly little language and verification support to build distributed systems based on fault-tolerant algorithms. In this paper, we present some of the challenges that a designer has to overcome to implement a fault-tolerant distributed system. Then we review different models that have been proposed to reason about distributed algorithms and sketch how such a model can form the basis for a domain-specific programming language. Adopting a high-level programming model can simplify the programmer's life and make the code amenable to automated verification, while still compiling to efficiently executable code. We conclude by summarizing the current status of an ongoing language design and implementation project that is based on this idea."}],"day":"01","has_accepted_license":"1","citation":{"apa":"Dragoi, C., Henzinger, T. A., &#38; Zufferey, D. (2015). The need for language support for fault-tolerant distributed systems. Presented at the SNAPL: Summit oN Advances in Programming Languages, Asilomar, CA, United States: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.SNAPL.2015.90\">https://doi.org/10.4230/LIPIcs.SNAPL.2015.90</a>","chicago":"Dragoi, Cezara, Thomas A Henzinger, and Damien Zufferey. “The Need for Language Support for Fault-Tolerant Distributed Systems.” Leibniz International Proceedings in Informatics. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015. <a href=\"https://doi.org/10.4230/LIPIcs.SNAPL.2015.90\">https://doi.org/10.4230/LIPIcs.SNAPL.2015.90</a>.","ista":"Dragoi C, Henzinger TA, Zufferey D. 2015. The need for language support for fault-tolerant distributed systems. 32, 90–102.","ieee":"C. Dragoi, T. A. Henzinger, and D. Zufferey, “The need for language support for fault-tolerant distributed systems,” vol. 32. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, pp. 90–102, 2015.","mla":"Dragoi, Cezara, et al. <i>The Need for Language Support for Fault-Tolerant Distributed Systems</i>. Vol. 32, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015, pp. 90–102, doi:<a href=\"https://doi.org/10.4230/LIPIcs.SNAPL.2015.90\">10.4230/LIPIcs.SNAPL.2015.90</a>.","short":"C. Dragoi, T.A. Henzinger, D. Zufferey, 32 (2015) 90–102.","ama":"Dragoi C, Henzinger TA, Zufferey D. The need for language support for fault-tolerant distributed systems. 2015;32:90-102. doi:<a href=\"https://doi.org/10.4230/LIPIcs.SNAPL.2015.90\">10.4230/LIPIcs.SNAPL.2015.90</a>"},"intvolume":"        32","doi":"10.4230/LIPIcs.SNAPL.2015.90","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","language":[{"iso":"eng"}],"file_date_updated":"2020-07-14T12:44:58Z","type":"conference","oa_version":"Published Version","conference":{"end_date":"2015-05-06","location":"Asilomar, CA, United States","start_date":"2015-05-03","name":"SNAPL: Summit oN Advances in Programming Languages"},"date_published":"2015-01-01T00:00:00Z","publist_id":"5681","ddc":["005"],"author":[{"id":"2B2B5ED0-F248-11E8-B48F-1D18A9856A87","full_name":"Dragoi, Cezara","first_name":"Cezara","last_name":"Dragoi"},{"last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"},{"orcid":"0000-0002-3197-8736","id":"4397AC76-F248-11E8-B48F-1D18A9856A87","first_name":"Damien","full_name":"Zufferey, Damien","last_name":"Zufferey"}],"quality_controlled":"1","page":"90 - 102","date_created":"2018-12-11T11:52:22Z","series_title":"Leibniz International Proceedings in Informatics","year":"2015","date_updated":"2020-08-11T10:09:14Z","project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling","grant_number":"267989","call_identifier":"FP7"},{"_id":"25F5A88A-B435-11E9-9278-68D0E5697425","name":"Moderne Concurrency Paradigms","grant_number":"S11402-N23","call_identifier":"FWF"},{"call_identifier":"FWF","name":"The Wittgenstein Prize","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425"}],"volume":32,"file":[{"file_id":"5050","content_type":"application/pdf","date_created":"2018-12-12T10:14:02Z","access_level":"open_access","date_updated":"2020-07-14T12:44:58Z","file_name":"IST-2016-499-v1+1_9.pdf","file_size":489362,"creator":"system","relation":"main_file","checksum":"cf5e94baa89a2dc4c5de01abc676eda8"}],"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_identifier":{"isbn":["978-3-939897-80-4 "]},"scopus_import":1},{"status":"public","abstract":[{"lang":"eng","text":"We consider weighted automata with both positive and negative integer weights on edges and\r\nstudy the problem of synchronization using adaptive strategies that may only observe whether\r\nthe current weight-level is negative or nonnegative. We show that the synchronization problem is decidable in polynomial time for deterministic weighted automata."}],"ec_funded":1,"intvolume":"        42","citation":{"apa":"Kretinsky, J., Larsen, K., Laursen, S., &#38; Srba, J. (2015). Polynomial time decidability of weighted synchronization under partial observability (Vol. 42, pp. 142–154). Presented at the CONCUR: Concurrency Theory, Madrid, Spain: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2015.142\">https://doi.org/10.4230/LIPIcs.CONCUR.2015.142</a>","ista":"Kretinsky J, Larsen K, Laursen S, Srba J. 2015. Polynomial time decidability of weighted synchronization under partial observability. CONCUR: Concurrency Theory, LIPIcs, vol. 42, 142–154.","chicago":"Kretinsky, Jan, Kim Larsen, Simon Laursen, and Jiří Srba. “Polynomial Time Decidability of Weighted Synchronization under Partial Observability,” 42:142–54. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2015.142\">https://doi.org/10.4230/LIPIcs.CONCUR.2015.142</a>.","mla":"Kretinsky, Jan, et al. <i>Polynomial Time Decidability of Weighted Synchronization under Partial Observability</i>. Vol. 42, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015, pp. 142–54, doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2015.142\">10.4230/LIPIcs.CONCUR.2015.142</a>.","ieee":"J. Kretinsky, K. Larsen, S. Laursen, and J. Srba, “Polynomial time decidability of weighted synchronization under partial observability,” presented at the CONCUR: Concurrency Theory, Madrid, Spain, 2015, vol. 42, pp. 142–154.","short":"J. Kretinsky, K. Larsen, S. Laursen, J. Srba, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015, pp. 142–154.","ama":"Kretinsky J, Larsen K, Laursen S, Srba J. Polynomial time decidability of weighted synchronization under partial observability. In: Vol 42. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2015:142-154. doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2015.142\">10.4230/LIPIcs.CONCUR.2015.142</a>"},"day":"01","has_accepted_license":"1","publication_status":"published","title":"Polynomial time decidability of weighted synchronization under partial observability","oa":1,"month":"01","_id":"1499","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","alternative_title":["LIPIcs"],"pubrep_id":"498","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"acknowledgement":"The research leading to these results has received funding from the European Union Seventh Framework Programme (FP7/2007-2013) under grant agreement 601148 (CASSTING), EU FP7 FET project SENSATION, Sino-Danish Basic Research Center IDAE4CPS, the European Research Council (ERC) under grant agreement 267989 (QUAREM), the Austrian Science Fund (FWF) project S11402-N23 (RiSE) and Z211-N23 (Wittgenstein Award), the Czech Science Foundation under grant agreement P202/12/G061, and People Programme (Marie Curie Actions) of the European Union’s Seventh Framework\r\nProgramme (FP7/2007-2013) REA Grant No 291734.","file":[{"access_level":"open_access","date_updated":"2020-07-14T12:44:58Z","file_id":"4672","content_type":"application/pdf","date_created":"2018-12-12T10:08:12Z","file_name":"IST-2016-498-v1+1_32.pdf","creator":"system","file_size":623563,"checksum":"49eb5021caafaabe5356c65b9c5f8c9c","relation":"main_file"}],"volume":42,"date_created":"2018-12-11T11:52:22Z","year":"2015","quality_controlled":"1","page":"142 - 154","project":[{"call_identifier":"FP7","grant_number":"267989","name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"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"},{"call_identifier":"FP7","grant_number":"291734","name":"International IST Postdoc Fellowship Programme","_id":"25681D80-B435-11E9-9278-68D0E5697425"}],"date_updated":"2021-01-12T06:51:10Z","scopus_import":1,"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)"},"language":[{"iso":"eng"}],"type":"conference","file_date_updated":"2020-07-14T12:44:58Z","doi":"10.4230/LIPIcs.CONCUR.2015.142","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","publist_id":"5680","author":[{"orcid":"0000-0002-8122-2881","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","full_name":"Kretinsky, Jan","first_name":"Jan","last_name":"Kretinsky"},{"last_name":"Larsen","full_name":"Larsen, Kim","first_name":"Kim"},{"full_name":"Laursen, Simon","first_name":"Simon","last_name":"Laursen"},{"full_name":"Srba, Jiří","first_name":"Jiří","last_name":"Srba"}],"ddc":["000","003"],"oa_version":"Published Version","conference":{"location":"Madrid, Spain","end_date":"2015-09-04","name":"CONCUR: Concurrency Theory","start_date":"2015-09-01"},"date_published":"2015-01-01T00:00:00Z"},{"author":[{"last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"full_name":"Chmelik, Martin","first_name":"Martin","last_name":"Chmelik","id":"3624234E-F248-11E8-B48F-1D18A9856A87"},{"id":"49351290-F248-11E8-B48F-1D18A9856A87","first_name":"Przemyslaw","full_name":"Daca, Przemyslaw","last_name":"Daca"}],"publist_id":"5677","publication":"Formal Methods in System Design","issue":"2","date_published":"2015-10-01T00:00:00Z","oa_version":"Preprint","type":"journal_article","language":[{"iso":"eng"}],"publisher":"Springer","doi":"10.1007/s10703-015-0235-2","scopus_import":1,"main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1405.0835"}],"volume":47,"date_updated":"2023-09-07T11:58:33Z","project":[{"grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"},{"name":"Quantitative Reactive Modeling","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"}],"page":"230 - 264","quality_controlled":"1","date_created":"2018-12-11T11:52:23Z","year":"2015","acknowledgement":"The research was partly supported by Austrian Science Fund (FWF) Grant No. P23499- N23, FWF NFN Grant No. S11407-N23, FWF Grant S11403-N23 (RiSE), and FWF Grant Z211-N23 (Wittgenstein Award), ERC Start Grant (279307: Graph Games), Microsoft faculty fellows award, the ERC Advanced Grant QUAREM (Quantitative Reactive Modeling).","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"title":"CEGAR for compositional analysis of qualitative properties in Markov decision processes","related_material":{"record":[{"id":"1155","relation":"dissertation_contains","status":"public"}]},"oa":1,"publication_status":"published","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","month":"10","_id":"1501","citation":{"ieee":"K. Chatterjee, M. Chmelik, and P. Daca, “CEGAR for compositional analysis of qualitative properties in Markov decision processes,” <i>Formal Methods in System Design</i>, vol. 47, no. 2. Springer, pp. 230–264, 2015.","mla":"Chatterjee, Krishnendu, et al. “CEGAR for Compositional Analysis of Qualitative Properties in Markov Decision Processes.” <i>Formal Methods in System Design</i>, vol. 47, no. 2, Springer, 2015, pp. 230–64, doi:<a href=\"https://doi.org/10.1007/s10703-015-0235-2\">10.1007/s10703-015-0235-2</a>.","chicago":"Chatterjee, Krishnendu, Martin Chmelik, and Przemyslaw Daca. “CEGAR for Compositional Analysis of Qualitative Properties in Markov Decision Processes.” <i>Formal Methods in System Design</i>. Springer, 2015. <a href=\"https://doi.org/10.1007/s10703-015-0235-2\">https://doi.org/10.1007/s10703-015-0235-2</a>.","apa":"Chatterjee, K., Chmelik, M., &#38; Daca, P. (2015). CEGAR for compositional analysis of qualitative properties in Markov decision processes. <i>Formal Methods in System Design</i>. Springer. <a href=\"https://doi.org/10.1007/s10703-015-0235-2\">https://doi.org/10.1007/s10703-015-0235-2</a>","ista":"Chatterjee K, Chmelik M, Daca P. 2015. CEGAR for compositional analysis of qualitative properties in Markov decision processes. Formal Methods in System Design. 47(2), 230–264.","ama":"Chatterjee K, Chmelik M, Daca P. CEGAR for compositional analysis of qualitative properties in Markov decision processes. <i>Formal Methods in System Design</i>. 2015;47(2):230-264. doi:<a href=\"https://doi.org/10.1007/s10703-015-0235-2\">10.1007/s10703-015-0235-2</a>","short":"K. Chatterjee, M. Chmelik, P. Daca, Formal Methods in System Design 47 (2015) 230–264."},"intvolume":"        47","day":"01","abstract":[{"lang":"eng","text":"We consider Markov decision processes (MDPs) which are a standard model for probabilistic systems. We focus on qualitative properties for MDPs that can express that desired behaviors of the system arise almost-surely (with probability 1) or with positive probability. We introduce a new simulation relation to capture the refinement relation of MDPs with respect to qualitative properties, and present discrete graph algorithms with quadratic complexity to compute the simulation relation. We present an automated technique for assume-guarantee style reasoning for compositional analysis of two-player games by giving a counterexample guided abstraction-refinement approach to compute our new simulation relation. We show a tight link between two-player games and MDPs, and as a consequence the results for games are lifted to MDPs with qualitative properties. We have implemented our algorithms and show that the compositional analysis leads to significant improvements. "}],"status":"public","ec_funded":1},{"status":"public","abstract":[{"lang":"eng","text":"We extend the theory of input-output conformance with operators for merge and quotient. The former is useful when testing against multiple requirements or views. The latter can be used to generate tests for patches of an already tested system. Both operators can combine systems with different action alphabets, which is usually the case when constructing complex systems and specifications from parts, for instance different views as well as newly defined functionality of a~previous version of the system."}],"ec_funded":1,"citation":{"short":"N. Beneš, P. Daca, T.A. Henzinger, J. Kretinsky, D. Nickovic, in:, ACM, 2015, pp. 101–110.","ama":"Beneš N, Daca P, Henzinger TA, Kretinsky J, Nickovic D. Complete composition operators for IOCO-testing theory. In: ACM; 2015:101-110. doi:<a href=\"https://doi.org/10.1145/2737166.2737175\">10.1145/2737166.2737175</a>","chicago":"Beneš, Nikola, Przemyslaw Daca, Thomas A Henzinger, Jan Kretinsky, and Dejan Nickovic. “Complete Composition Operators for IOCO-Testing Theory,” 101–10. ACM, 2015. <a href=\"https://doi.org/10.1145/2737166.2737175\">https://doi.org/10.1145/2737166.2737175</a>.","ista":"Beneš N, Daca P, Henzinger TA, Kretinsky J, Nickovic D. 2015. Complete composition operators for IOCO-testing theory. CBSE: Component-Based Software Engineering , Proceedings of the 18th International ACM SIGSOFT Symposium on Component-Based Software Engineering , , 101–110.","apa":"Beneš, N., Daca, P., Henzinger, T. A., Kretinsky, J., &#38; Nickovic, D. (2015). Complete composition operators for IOCO-testing theory (pp. 101–110). Presented at the CBSE: Component-Based Software Engineering , Montreal, QC, Canada: ACM. <a href=\"https://doi.org/10.1145/2737166.2737175\">https://doi.org/10.1145/2737166.2737175</a>","ieee":"N. Beneš, P. Daca, T. A. Henzinger, J. Kretinsky, and D. Nickovic, “Complete composition operators for IOCO-testing theory,” presented at the CBSE: Component-Based Software Engineering , Montreal, QC, Canada, 2015, pp. 101–110.","mla":"Beneš, Nikola, et al. <i>Complete Composition Operators for IOCO-Testing Theory</i>. ACM, 2015, pp. 101–10, doi:<a href=\"https://doi.org/10.1145/2737166.2737175\">10.1145/2737166.2737175</a>."},"day":"01","has_accepted_license":"1","oa":1,"title":"Complete composition operators for IOCO-testing theory","related_material":{"record":[{"id":"1155","status":"public","relation":"dissertation_contains"}]},"publication_status":"published","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"1502","month":"05","pubrep_id":"625","alternative_title":["Proceedings of the 18th International ACM SIGSOFT Symposium on Component-Based Software Engineering "],"department":[{"_id":"ToHe"},{"_id":"KrCh"}],"acknowledgement":"This research was funded in part by the European Research Council (ERC) under grant agreement 267989 (QUAREM), by the Austrian Science Fund (FWF) projects S11402-N23(RiSE) and Z211-N23 (Wittgestein Award), by People Programme (Marie Curie Actions) of the European Union's Seventh Framework Programme (FP7/2007-2013) under REA grant agreement 291734, and by the ARTEMIS JU under grant agreement 295373 (nSafeCer).  Jan Křetínský has been partially supported by the Czech Science Foundation, grant No.  P202/12/G061.  Nikola Beneš has been supported by the\r\nMEYS project No. CZ.1.07/2.3.00/30.0009 Employment of Newly Graduated Doctors of Science for Scientific Excellence.","file":[{"date_updated":"2020-07-14T12:44:59Z","access_level":"open_access","content_type":"application/pdf","date_created":"2018-12-12T10:17:46Z","file_id":"5303","file_name":"IST-2016-625-v1+1_conf-cbse-BenesDHKN15.pdf","creator":"system","file_size":467561,"checksum":"c6ce681035c163a158751f240cb7d389","relation":"main_file"}],"page":"101 - 110","quality_controlled":"1","year":"2015","date_created":"2018-12-11T11:52:24Z","date_updated":"2023-09-07T11:58:33Z","project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","name":"Quantitative Reactive Modeling","call_identifier":"FP7"},{"call_identifier":"FWF","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","name":"The Wittgenstein Prize","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425"},{"_id":"25681D80-B435-11E9-9278-68D0E5697425","grant_number":"291734","name":"International IST Postdoc Fellowship Programme","call_identifier":"FP7"}],"publication_identifier":{"isbn":["978-1-4503-3471-6"]},"scopus_import":1,"language":[{"iso":"eng"}],"file_date_updated":"2020-07-14T12:44:59Z","type":"conference","doi":"10.1145/2737166.2737175","publisher":"ACM","publist_id":"5676","ddc":["000"],"author":[{"last_name":"Beneš","full_name":"Beneš, Nikola","first_name":"Nikola"},{"full_name":"Daca, Przemyslaw","first_name":"Przemyslaw","last_name":"Daca","id":"49351290-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A"},{"last_name":"Kretinsky","first_name":"Jan","full_name":"Kretinsky, Jan","orcid":"0000-0002-8122-2881","id":"44CEF464-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Dejan","full_name":"Nickovic, Dejan","last_name":"Nickovic"}],"conference":{"location":"Montreal, QC, Canada","end_date":"2015-05-08","name":"CBSE: Component-Based Software Engineering ","start_date":"2015-05-04"},"oa_version":"Submitted Version","date_published":"2015-05-01T00:00:00Z"},{"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","month":"06","_id":"1538","title":"Iterative experiment design guides the characterization of a light-inducible gene expression circuit","oa":1,"publication_status":"published","department":[{"_id":"ToHe"},{"_id":"GaTk"}],"acknowledgement":"J.R., F.P., and J.L. acknowledge support from the European Commission under the Network of Excellence HYCON2 (highly-complex and networked control systems) and SystemsX.ch under the SignalX Project. J.R. acknowledges support from the People Programme (Marie Curie Actions) of the European Union’s Seventh Framework Programme FP7/2007-2013 under REA (Research Executive Agency) Grant 291734. M.K. acknowledges support from Human Frontier Science Program Grant RP0061/2011 (www.hfsp.org). ","ec_funded":1,"abstract":[{"lang":"eng","text":"Systems biology rests on the idea that biological complexity can be better unraveled through the interplay of modeling and experimentation. However, the success of this approach depends critically on the informativeness of the chosen experiments, which is usually unknown a priori. Here, we propose a systematic scheme based on iterations of optimal experiment design, flow cytometry experiments, and Bayesian parameter inference to guide the discovery process in the case of stochastic biochemical reaction networks. To illustrate the benefit of our methodology, we apply it to the characterization of an engineered light-inducible gene expression circuit in yeast and compare the performance of the resulting model with models identified from nonoptimal experiments. In particular, we compare the parameter posterior distributions and the precision to which the outcome of future experiments can be predicted. Moreover, we illustrate how the identified stochastic model can be used to determine light induction patterns that make either the average amount of protein or the variability in a population of cells follow a desired profile. Our results show that optimal experiment design allows one to derive models that are accurate enough to precisely predict and regulate the protein expression in heterogeneous cell populations over extended periods of time."}],"status":"public","day":"30","intvolume":"       112","citation":{"ama":"Ruess J, Parise F, Milias Argeitis A, Khammash M, Lygeros J. Iterative experiment design guides the characterization of a light-inducible gene expression circuit. <i>PNAS</i>. 2015;112(26):8148-8153. doi:<a href=\"https://doi.org/10.1073/pnas.1423947112\">10.1073/pnas.1423947112</a>","short":"J. Ruess, F. Parise, A. Milias Argeitis, M. Khammash, J. Lygeros, PNAS 112 (2015) 8148–8153.","ieee":"J. Ruess, F. Parise, A. Milias Argeitis, M. Khammash, and J. Lygeros, “Iterative experiment design guides the characterization of a light-inducible gene expression circuit,” <i>PNAS</i>, vol. 112, no. 26. National Academy of Sciences, pp. 8148–8153, 2015.","mla":"Ruess, Jakob, et al. “Iterative Experiment Design Guides the Characterization of a Light-Inducible Gene Expression Circuit.” <i>PNAS</i>, vol. 112, no. 26, National Academy of Sciences, 2015, pp. 8148–53, doi:<a href=\"https://doi.org/10.1073/pnas.1423947112\">10.1073/pnas.1423947112</a>.","ista":"Ruess J, Parise F, Milias Argeitis A, Khammash M, Lygeros J. 2015. Iterative experiment design guides the characterization of a light-inducible gene expression circuit. PNAS. 112(26), 8148–8153.","apa":"Ruess, J., Parise, F., Milias Argeitis, A., Khammash, M., &#38; Lygeros, J. (2015). Iterative experiment design guides the characterization of a light-inducible gene expression circuit. <i>PNAS</i>. National Academy of Sciences. <a href=\"https://doi.org/10.1073/pnas.1423947112\">https://doi.org/10.1073/pnas.1423947112</a>","chicago":"Ruess, Jakob, Francesca Parise, Andreas Milias Argeitis, Mustafa Khammash, and John Lygeros. “Iterative Experiment Design Guides the Characterization of a Light-Inducible Gene Expression Circuit.” <i>PNAS</i>. National Academy of Sciences, 2015. <a href=\"https://doi.org/10.1073/pnas.1423947112\">https://doi.org/10.1073/pnas.1423947112</a>."},"publisher":"National Academy of Sciences","doi":"10.1073/pnas.1423947112","type":"journal_article","language":[{"iso":"eng"}],"date_published":"2015-06-30T00:00:00Z","oa_version":"Submitted Version","external_id":{"pmid":["26085136"]},"author":[{"last_name":"Ruess","full_name":"Ruess, Jakob","first_name":"Jakob","orcid":"0000-0003-1615-3282","id":"4A245D00-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Parise","first_name":"Francesca","full_name":"Parise, Francesca"},{"last_name":"Milias Argeitis","first_name":"Andreas","full_name":"Milias Argeitis, Andreas"},{"last_name":"Khammash","first_name":"Mustafa","full_name":"Khammash, Mustafa"},{"last_name":"Lygeros","full_name":"Lygeros, John","first_name":"John"}],"issue":"26","publication":"PNAS","publist_id":"5633","date_updated":"2021-01-12T06:51:27Z","project":[{"name":"International IST Postdoc Fellowship Programme","grant_number":"291734","_id":"25681D80-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"}],"page":"8148 - 8153","quality_controlled":"1","date_created":"2018-12-11T11:52:36Z","year":"2015","volume":112,"scopus_import":1,"pmid":1,"main_file_link":[{"open_access":"1","url":"http://www.ncbi.nlm.nih.gov/pmc/articles/PMC4491780/"}]}]