[{"status":"public","type":"book_chapter","_id":"7453","series_title":"LNCS","department":[{"_id":"ToHe"}],"date_updated":"2022-09-06T08:25:52Z","month":"10","intvolume":" 10000","scopus_import":"1","alternative_title":["Lecture Notes in Computer Science"],"main_file_link":[{"open_access":"1","url":"https://doi.org/10.1007/978-3-319-91908-9_22"}],"oa_version":"Published Version","abstract":[{"text":"We illustrate the ingredients of the state-of-the-art of model-based approach for the formal design and verification of cyber-physical systems. To capture the interaction between a discrete controller and its continuously evolving environment, we use the formal models of timed and hybrid automata. We explain the steps of modeling and verification in the tools Uppaal and SpaceEx using a case study based on a dual-chamber implantable pacemaker monitoring a human heart. We show how to design a model as a composition of components, how to construct models at varying levels of detail, how to establish that one model is an abstraction of another, how to specify correctness requirements using temporal logic, and how to verify that a model satisfies a logical requirement.","lang":"eng"}],"volume":10000,"language":[{"iso":"eng"}],"publication_identifier":{"eissn":["0302-9743"],"isbn":["9783319919072"],"issn":["1611-3349"],"eisbn":["9783319919089"]},"publication_status":"published","project":[{"name":"Rigorous Systems Engineering","grant_number":"S11402-N23","_id":"25F2ACDE-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize","grant_number":"Z211"}],"editor":[{"first_name":"Bernhard","full_name":"Steffen, Bernhard","last_name":"Steffen"},{"last_name":"Woeginger","full_name":"Woeginger, Gerhard","first_name":"Gerhard"}],"title":"Continuous-time models for system design and analysis","author":[{"last_name":"Alur","full_name":"Alur, Rajeev","first_name":"Rajeev"},{"orcid":"0000-0001-8180-0904","full_name":"Giacobbe, Mirco","last_name":"Giacobbe","id":"3444EA5E-F248-11E8-B48F-1D18A9856A87","first_name":"Mirco"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger"},{"last_name":"Larsen","full_name":"Larsen, Kim G.","first_name":"Kim G."},{"first_name":"Marius","last_name":"Mikučionis","full_name":"Mikučionis, Marius"}],"article_processing_charge":"No","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"mla":"Alur, Rajeev, et al. “Continuous-Time Models for System Design and Analysis.” Computing and Software Science, edited by Bernhard Steffen and Gerhard Woeginger, vol. 10000, Springer Nature, 2019, pp. 452–77, doi:10.1007/978-3-319-91908-9_22.","ieee":"R. Alur, M. Giacobbe, T. A. Henzinger, K. G. Larsen, and M. Mikučionis, “Continuous-time models for system design and analysis,” in Computing and Software Science, vol. 10000, B. Steffen and G. Woeginger, Eds. Springer Nature, 2019, pp. 452–477.","short":"R. Alur, M. Giacobbe, T.A. Henzinger, K.G. Larsen, M. Mikučionis, in:, B. Steffen, G. Woeginger (Eds.), Computing and Software Science, Springer Nature, 2019, pp. 452–477.","ama":"Alur R, Giacobbe M, Henzinger TA, Larsen KG, Mikučionis M. Continuous-time models for system design and analysis. In: Steffen B, Woeginger G, eds. Computing and Software Science. Vol 10000. LNCS. Springer Nature; 2019:452-477. doi:10.1007/978-3-319-91908-9_22","apa":"Alur, R., Giacobbe, M., Henzinger, T. A., Larsen, K. G., & Mikučionis, M. (2019). Continuous-time models for system design and analysis. In B. Steffen & G. Woeginger (Eds.), Computing and Software Science (Vol. 10000, pp. 452–477). Springer Nature. https://doi.org/10.1007/978-3-319-91908-9_22","chicago":"Alur, Rajeev, Mirco Giacobbe, Thomas A Henzinger, Kim G. Larsen, and Marius Mikučionis. “Continuous-Time Models for System Design and Analysis.” In Computing and Software Science, edited by Bernhard Steffen and Gerhard Woeginger, 10000:452–77. LNCS. Springer Nature, 2019. https://doi.org/10.1007/978-3-319-91908-9_22.","ista":"Alur R, Giacobbe M, Henzinger TA, Larsen KG, Mikučionis M. 2019.Continuous-time models for system design and analysis. In: Computing and Software Science. Lecture Notes in Computer Science, vol. 10000, 452–477."},"quality_controlled":"1","publisher":"Springer Nature","oa":1,"acknowledgement":"This research was supported in part by the Austrian Science Fund (FWF) under grants S11402-N23(RiSE/SHiNE) and Z211-N23 (Wittgenstein Award). This research has received funding from the Sino-Danish Basic Research Centre, IDEA4CPS, funded by the Danish National Research Foundation and the National Science Foundation, China, the Innovation Fund Denmark centre DiCyPS, as well as the ERC Advanced Grant LASSO.","doi":"10.1007/978-3-319-91908-9_22","date_published":"2019-10-05T00:00:00Z","date_created":"2020-02-05T10:51:44Z","page":"452-477","day":"05","publication":"Computing and Software Science","year":"2019"},{"department":[{"_id":"JaMa"}],"date_updated":"2022-06-17T07:52:41Z","type":"journal_article","article_type":"original","status":"public","_id":"7550","issue":"2","volume":28,"publication_identifier":{"issn":["1343-4373"]},"publication_status":"published","language":[{"iso":"eng"}],"main_file_link":[{"open_access":"1","url":" https://doi.org/10.48550/arXiv.1910.10050"}],"month":"10","intvolume":" 28","abstract":[{"text":"We consider an optimal control problem for an abstract nonlinear dissipative evolution equation. The differential constraint is penalized by augmenting the target functional by a nonnegative global-in-time functional which is null-minimized in the evolution equation is satisfied. Different variational settings are presented, leading to the convergence of the penalization method for gradient flows, noncyclic and semimonotone flows, doubly nonlinear evolutions, and GENERIC systems. ","lang":"eng"}],"oa_version":"Preprint","author":[{"first_name":"Lorenzo","id":"30AD2CBC-F248-11E8-B48F-1D18A9856A87","full_name":"Portinale, Lorenzo","last_name":"Portinale"},{"full_name":"Stefanelli, Ulisse","last_name":"Stefanelli","first_name":"Ulisse"}],"article_processing_charge":"No","external_id":{"arxiv":["1910.10050"]},"title":"Penalization via global functionals of optimal-control problems for dissipative evolution","citation":{"chicago":"Portinale, Lorenzo, and Ulisse Stefanelli. “Penalization via Global Functionals of Optimal-Control Problems for Dissipative Evolution.” Advances in Mathematical Sciences and Applications. Gakko Tosho, 2019.","ista":"Portinale L, Stefanelli U. 2019. Penalization via global functionals of optimal-control problems for dissipative evolution. Advances in Mathematical Sciences and Applications. 28(2), 425–447.","mla":"Portinale, Lorenzo, and Ulisse Stefanelli. “Penalization via Global Functionals of Optimal-Control Problems for Dissipative Evolution.” Advances in Mathematical Sciences and Applications, vol. 28, no. 2, Gakko Tosho, 2019, pp. 425–47.","short":"L. Portinale, U. Stefanelli, Advances in Mathematical Sciences and Applications 28 (2019) 425–447.","ieee":"L. Portinale and U. Stefanelli, “Penalization via global functionals of optimal-control problems for dissipative evolution,” Advances in Mathematical Sciences and Applications, vol. 28, no. 2. Gakko Tosho, pp. 425–447, 2019.","apa":"Portinale, L., & Stefanelli, U. (2019). Penalization via global functionals of optimal-control problems for dissipative evolution. Advances in Mathematical Sciences and Applications. Gakko Tosho.","ama":"Portinale L, Stefanelli U. Penalization via global functionals of optimal-control problems for dissipative evolution. Advances in Mathematical Sciences and Applications. 2019;28(2):425-447."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","project":[{"_id":"fc31cba2-9c52-11eb-aca3-ff467d239cd2","name":"Taming Complexity in Partial Differential Systems","grant_number":"F6504"}],"page":"425-447","date_published":"2019-10-22T00:00:00Z","date_created":"2020-02-28T10:54:41Z","year":"2019","day":"22","publication":"Advances in Mathematical Sciences and Applications","quality_controlled":"1","publisher":"Gakko Tosho","oa":1,"acknowledgement":"This work is supported by Vienna Science and Technology Fund (WWTF) through Project MA14-009 and by the Austrian Science Fund (FWF) projects F 65 and I 2375."},{"year":"2019","publication_status":"submitted","language":[{"iso":"eng"}],"publication":"arXiv:1912.08579","day":"18","page":"5","date_created":"2020-02-28T10:57:08Z","date_published":"2019-12-18T00:00:00Z","abstract":[{"text":"There is increasing evidence that protein binding to specific sites along DNA can activate the reading out of genetic information without coming into direct physical contact with the gene. There also is evidence that these distant but interacting sites are embedded in a liquid droplet of proteins which condenses out of the surrounding solution. We argue that droplet-mediated interactions can account for crucial features of gene regulation only if the droplet is poised at a non-generic point in its phase diagram. We explore a minimal model that embodies this idea, show that this model has a natural mechanism for self-tuning, and suggest direct experimental tests. ","lang":"eng"}],"oa_version":"Preprint","oa":1,"main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1912.08579"}],"publisher":"ArXiv","month":"12","date_updated":"2021-01-12T08:14:09Z","citation":{"apa":"Bialek, W., Gregor, T., & Tkačik, G. (n.d.). Action at a distance in transcriptional regulation. arXiv:1912.08579. ArXiv.","ama":"Bialek W, Gregor T, Tkačik G. Action at a distance in transcriptional regulation. arXiv:191208579.","ieee":"W. Bialek, T. Gregor, and G. Tkačik, “Action at a distance in transcriptional regulation,” arXiv:1912.08579. ArXiv.","short":"W. Bialek, T. Gregor, G. Tkačik, ArXiv:1912.08579 (n.d.).","mla":"Bialek, William, et al. “Action at a Distance in Transcriptional Regulation.” ArXiv:1912.08579, ArXiv.","ista":"Bialek W, Gregor T, Tkačik G. Action at a distance in transcriptional regulation. arXiv:1912.08579, .","chicago":"Bialek, William, Thomas Gregor, and Gašper Tkačik. “Action at a Distance in Transcriptional Regulation.” ArXiv:1912.08579. ArXiv, n.d."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","article_processing_charge":"No","external_id":{"arxiv":["1912.08579"]},"author":[{"full_name":"Bialek, William","last_name":"Bialek","first_name":"William"},{"last_name":"Gregor","full_name":"Gregor, Thomas","first_name":"Thomas"},{"orcid":"0000-0002-6699-1455","full_name":"Tkačik, Gašper","last_name":"Tkačik","id":"3D494DCA-F248-11E8-B48F-1D18A9856A87","first_name":"Gašper"}],"department":[{"_id":"GaTk"}],"title":"Action at a distance in transcriptional regulation","_id":"7552","type":"preprint","project":[{"_id":"254E9036-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Biophysics of information processing in gene regulation","grant_number":"P28844-B27"}],"status":"public"},{"oa_version":"Published Version","abstract":[{"lang":"eng","text":"We present the results of a friendly competition for formal verification of continuous and hybrid systems with nonlinear continuous dynamics. The friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in 2019. In this year, 6 tools Ariadne, CORA, DynIbex, Flow*, Isabelle/HOL, and JuliaReach (in alphabetic order) participated. They are applied to solve reachability analysis problems on four benchmark problems, one of them with hybrid dynamics. We do not rank the tools based on the results, but show the current status and discover the potential advantages of different tools."}],"intvolume":" 61","month":"05","scopus_import":1,"language":[{"iso":"eng"}],"file":[{"date_created":"2020-03-24T07:36:36Z","file_name":"2019_ARCH19_Immler.pdf","date_updated":"2020-07-14T12:48:00Z","file_size":1934830,"creator":"dernst","file_id":"7617","checksum":"9138977a06fcd6a95976eb4bca875f0c","content_type":"application/pdf","access_level":"open_access","relation":"main_file"}],"publication_status":"published","publication_identifier":{"eissn":["23987340"]},"volume":61,"_id":"7576","status":"public","conference":{"end_date":"2019-04-15","location":"Montreal, Canada","start_date":"2019-04-15","name":"ARCH: International Workshop on Applied Verification on Continuous and Hybrid Systems"},"type":"conference","ddc":["000"],"date_updated":"2021-01-12T08:14:17Z","file_date_updated":"2020-07-14T12:48:00Z","department":[{"_id":"ToHe"}],"oa":1,"publisher":"EasyChair Publications","quality_controlled":"1","publication":"EPiC Series in Computing","day":"25","year":"2019","has_accepted_license":"1","date_created":"2020-03-08T23:00:49Z","date_published":"2019-05-25T00:00:00Z","doi":"10.29007/m75b","page":"41-61","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"mla":"Immler, Fabian, et al. “ARCH-COMP19 Category Report: Continuous and Hybrid Systems with Nonlinear Dynamics.” EPiC Series in Computing, vol. 61, EasyChair Publications, 2019, pp. 41–61, doi:10.29007/m75b.","apa":"Immler, F., Althoff, M., Benet, L., Chapoutot, A., Chen, X., Forets, M., … Schilling, C. (2019). ARCH-COMP19 Category Report: Continuous and hybrid systems with nonlinear dynamics. In EPiC Series in Computing (Vol. 61, pp. 41–61). Montreal, Canada: EasyChair Publications. https://doi.org/10.29007/m75b","ama":"Immler F, Althoff M, Benet L, et al. ARCH-COMP19 Category Report: Continuous and hybrid systems with nonlinear dynamics. In: EPiC Series in Computing. Vol 61. EasyChair Publications; 2019:41-61. doi:10.29007/m75b","short":"F. Immler, M. Althoff, L. Benet, A. Chapoutot, X. Chen, M. Forets, L. Geretti, N. Kochdumper, D.P. Sanders, C. Schilling, in:, EPiC Series in Computing, EasyChair Publications, 2019, pp. 41–61.","ieee":"F. Immler et al., “ARCH-COMP19 Category Report: Continuous and hybrid systems with nonlinear dynamics,” in EPiC Series in Computing, Montreal, Canada, 2019, vol. 61, pp. 41–61.","chicago":"Immler, Fabian, Matthias Althoff, Luis Benet, Alexandre Chapoutot, Xin Chen, Marcelo Forets, Luca Geretti, Niklas Kochdumper, David P. Sanders, and Christian Schilling. “ARCH-COMP19 Category Report: Continuous and Hybrid Systems with Nonlinear Dynamics.” In EPiC Series in Computing, 61:41–61. EasyChair Publications, 2019. https://doi.org/10.29007/m75b.","ista":"Immler F, Althoff M, Benet L, Chapoutot A, Chen X, Forets M, Geretti L, Kochdumper N, Sanders DP, Schilling C. 2019. ARCH-COMP19 Category Report: Continuous and hybrid systems with nonlinear dynamics. EPiC Series in Computing. ARCH: International Workshop on Applied Verification on Continuous and Hybrid Systems vol. 61, 41–61."},"title":"ARCH-COMP19 Category Report: Continuous and hybrid systems with nonlinear dynamics","article_processing_charge":"No","author":[{"full_name":"Immler, Fabian","last_name":"Immler","first_name":"Fabian"},{"full_name":"Althoff, Matthias","last_name":"Althoff","first_name":"Matthias"},{"first_name":"Luis","full_name":"Benet, Luis","last_name":"Benet"},{"first_name":"Alexandre","last_name":"Chapoutot","full_name":"Chapoutot, Alexandre"},{"full_name":"Chen, Xin","last_name":"Chen","first_name":"Xin"},{"first_name":"Marcelo","full_name":"Forets, Marcelo","last_name":"Forets"},{"first_name":"Luca","full_name":"Geretti, Luca","last_name":"Geretti"},{"last_name":"Kochdumper","full_name":"Kochdumper, Niklas","first_name":"Niklas"},{"last_name":"Sanders","full_name":"Sanders, David P.","first_name":"David P."},{"first_name":"Christian","id":"3A2F4DCE-F248-11E8-B48F-1D18A9856A87","full_name":"Schilling, Christian","orcid":"0000-0003-3658-1065","last_name":"Schilling"}]},{"year":"2019","publication":"Proceedings on the 31st International Conference on Formal Power Series and Algebraic Combinatorics","day":"01","date_created":"2020-07-26T22:01:04Z","date_published":"2019-07-01T00:00:00Z","acknowledgement":"D.B. is especially grateful to Patrik Ferrari for suggesting simplifications in Section 3 and\r\nto Alessandra Occelli for suggesting the name for the models of Section 2.\r\n","oa":1,"publisher":"Formal Power Series and Algebraic Combinatorics","quality_controlled":"1","citation":{"ama":"Betea D, Bouttier J, Nejjar P, Vuletíc M. New edge asymptotics of skew Young diagrams via free boundaries. In: Proceedings on the 31st International Conference on Formal Power Series and Algebraic Combinatorics. Formal Power Series and Algebraic Combinatorics; 2019.","apa":"Betea, D., Bouttier, J., Nejjar, P., & Vuletíc, M. (2019). New edge asymptotics of skew Young diagrams via free boundaries. In Proceedings on the 31st International Conference on Formal Power Series and Algebraic Combinatorics. Ljubljana, Slovenia: Formal Power Series and Algebraic Combinatorics.","short":"D. Betea, J. Bouttier, P. Nejjar, M. Vuletíc, in:, Proceedings on the 31st International Conference on Formal Power Series and Algebraic Combinatorics, Formal Power Series and Algebraic Combinatorics, 2019.","ieee":"D. Betea, J. Bouttier, P. Nejjar, and M. Vuletíc, “New edge asymptotics of skew Young diagrams via free boundaries,” in Proceedings on the 31st International Conference on Formal Power Series and Algebraic Combinatorics, Ljubljana, Slovenia, 2019.","mla":"Betea, Dan, et al. “New Edge Asymptotics of Skew Young Diagrams via Free Boundaries.” Proceedings on the 31st International Conference on Formal Power Series and Algebraic Combinatorics, 34, Formal Power Series and Algebraic Combinatorics, 2019.","ista":"Betea D, Bouttier J, Nejjar P, Vuletíc M. 2019. New edge asymptotics of skew Young diagrams via free boundaries. Proceedings on the 31st International Conference on Formal Power Series and Algebraic Combinatorics. FPSAC: International Conference on Formal Power Series and Algebraic Combinatorics, 34.","chicago":"Betea, Dan, Jérémie Bouttier, Peter Nejjar, and Mirjana Vuletíc. “New Edge Asymptotics of Skew Young Diagrams via Free Boundaries.” In Proceedings on the 31st International Conference on Formal Power Series and Algebraic Combinatorics. Formal Power Series and Algebraic Combinatorics, 2019."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","article_processing_charge":"No","external_id":{"arxiv":["1902.08750"]},"author":[{"full_name":"Betea, Dan","last_name":"Betea","first_name":"Dan"},{"first_name":"Jérémie","full_name":"Bouttier, Jérémie","last_name":"Bouttier"},{"last_name":"Nejjar","full_name":"Nejjar, Peter","id":"4BF426E2-F248-11E8-B48F-1D18A9856A87","first_name":"Peter"},{"last_name":"Vuletíc","full_name":"Vuletíc, Mirjana","first_name":"Mirjana"}],"title":"New edge asymptotics of skew Young diagrams via free boundaries","article_number":"34","project":[{"call_identifier":"FP7","_id":"258DCDE6-B435-11E9-9278-68D0E5697425","name":"Random matrices, universality and disordered quantum systems","grant_number":"338804"},{"name":"Optimal Transport and Stochastic Dynamics","grant_number":"716117","_id":"256E75B8-B435-11E9-9278-68D0E5697425","call_identifier":"H2020"}],"publication_status":"published","language":[{"iso":"eng"}],"ec_funded":1,"abstract":[{"lang":"eng","text":"We study edge asymptotics of poissonized Plancherel-type measures on skew Young diagrams (integer partitions). These measures can be seen as generalizations of those studied by Baik--Deift--Johansson and Baik--Rains in resolving Ulam's problem on longest increasing subsequences of random permutations and the last passage percolation (corner growth) discrete versions thereof. Moreover they interpolate between said measures and the uniform measure on partitions. In the new KPZ-like 1/3 exponent edge scaling limit with logarithmic corrections, we find new probability distributions generalizing the classical Tracy--Widom GUE, GOE and GSE distributions from the theory of random matrices."}],"oa_version":"Preprint","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1902.08750"}],"scopus_import":"1","month":"07","date_updated":"2021-01-12T08:17:18Z","department":[{"_id":"LaEr"}],"_id":"8175","conference":{"start_date":"2019-07-01","location":"Ljubljana, Slovenia","end_date":"2019-07-05","name":"FPSAC: International Conference on Formal Power Series and Algebraic Combinatorics"},"type":"conference","status":"public"}]