{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,1]],"date-time":"2025-11-01T12:29:17Z","timestamp":1762000157397,"version":"build-2065373602"},"publisher-location":"New York, NY, USA","reference-count":36,"publisher":"ACM","license":[{"start":{"date-parts":[[2017,9,29]],"date-time":"2017-09-29T00:00:00Z","timestamp":1506643200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"DARPA"},{"name":"MARCO"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2017,9,29]]},"DOI":"10.1145\/3127041.3127045","type":"proceedings-article","created":{"date-parts":[[2017,9,27]],"date-time":"2017-09-27T12:34:00Z","timestamp":1506515640000},"page":"5-14","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":25,"title":["Stochastic contracts for cyber-physical system design under probabilistic requirements"],"prefix":"10.1145","author":[{"given":"Jiwei","family":"Li","sequence":"first","affiliation":[{"name":"Shanghai Jiao Tong University"}]},{"given":"Pierluigi","family":"Nuzzo","sequence":"additional","affiliation":[{"name":"University of Southern California"}]},{"given":"Alberto","family":"Sangiovanni-Vincentelli","sequence":"additional","affiliation":[{"name":"University of California"}]},{"given":"Yugeng","family":"Xi","sequence":"additional","affiliation":[{"name":"Shanghai Jiao Tong University"}]},{"given":"Dewei","family":"Li","sequence":"additional","affiliation":[{"name":"Shanghai Jiao Tong University"}]}],"member":"320","published-online":{"date-parts":[[2017,9,29]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0005-1098(98)00178-2"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-92188-2_9"},{"key":"e_1_3_2_1_3_1","unstructured":"Albert Benveniste Beno\u00eet Caillaud Dejan Nickovic Roberto Passerone Jean-Baptiste Raclet Philipp Reinkemeier Alberto Sangiovanni-Vincentelli Werner Damm Thomas Henzinger and Kim Guldstrand Larsen. 2012. Contracts for System Design. Rapport de recherche RR-8147. INRIA. 65 pages.  Albert Benveniste Beno\u00eet Caillaud Dejan Nickovic Roberto Passerone Jean-Baptiste Raclet Philipp Reinkemeier Alberto Sangiovanni-Vincentelli Werner Damm Thomas Henzinger and Kim Guldstrand Larsen. 2012. Contracts for System Design. Rapport de recherche RR-8147. INRIA. 65 pages."},{"volume-title":"Applied mathematical programming","author":"Bradley Stephen","key":"e_1_3_2_1_4_1","unstructured":"Stephen Bradley , Arnoldo Hax , and Thomas Magnanti . 1977. Applied mathematical programming . Addison Wesley . Stephen Bradley, Arnoldo Hax, and Thomas Magnanti. 1977. Applied mathematical programming. Addison Wesley."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2010.23"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"crossref","unstructured":"M. Cannon P. Couchman and B. Kouvaritakis. 2007. MPC for stochastic systems. Assessment and Future Directions of Nonlinear Model Predictive Control (2007) 255--268.  M. Cannon P. Couchman and B. Kouvaritakis. 2007. MPC for stochastic systems. Assessment and Future Directions of Nonlinear Model Predictive Control (2007) 255--268.","DOI":"10.1007\/978-3-540-72699-9_20"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/5397.5399"},{"key":"e_1_3_2_1_8_1","unstructured":"E. M. Clarke O. Grumberg and D. A. Peled. 2008. Model Checking. The MIT Press Cambridge MA.  E. M. Clarke O. Grumberg and D. A. Peled. 2008. Model Checking. The MIT Press Cambridge MA."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/503209.503226"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2006.883060"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACSD.2010.13"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/1946284.1946307"},{"key":"e_1_3_2_1_13_1","volume-title":"APAC: A tool for reasoning about abstract probabilistic automata.","author":"Delahaye Beno\u00eet","year":"2011","unstructured":"Beno\u00eet Delahaye , Kim G Larsen , Axel Legay , Mikkel L Pedersen , 2011 . APAC: A tool for reasoning about abstract probabilistic automata. (2011). Beno\u00eet Delahaye, Kim G Larsen, Axel Legay, Mikkel L Pedersen, et al. 2011. APAC: A tool for reasoning about abstract probabilistic automata. (2011)."},{"volume-title":"Probability: theory and examples","author":"Durrett Rick","key":"e_1_3_2_1_14_1","unstructured":"Rick Durrett . 2010. Probability: theory and examples . Cambridge university press . Rick Durrett. 2010. Probability: theory and examples. Cambridge university press."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.sysconle.2004.08.009"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.23919\/ACC.2017.7963204"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-012-0162-4"},{"key":"e_1_3_2_1_18_1","volume-title":"Gurobi Optimization","author":"Inc.","year":"2015","unstructured":"Inc. Gurobi Optimization . 2015 . Gurobi Optimizer Reference Manual . (2015). http:\/\/www.gurobi.com Inc. Gurobi Optimization. 2015. Gurobi Optimizer Reference Manual. (2015). http:\/\/www.gurobi.com"},{"key":"e_1_3_2_1_19_1","volume-title":"A logic for reasoning about time and reliability. Formal aspects of computing 6, 5","author":"Hansson Hans","year":"1994","unstructured":"Hans Hansson and Bengt Jonsson . 1994. A logic for reasoning about time and reliability. Formal aspects of computing 6, 5 ( 1994 ), 512--535. Hans Hansson and Bengt Jonsson. 1994. A logic for reasoning about time and reliability. Formal aspects of computing 6, 5 (1994), 512--535."},{"key":"e_1_3_2_1_20_1","volume-title":"Wolpert","author":"Harris Christopher M.","year":"1998","unstructured":"Christopher M. Harris and Daniel M . Wolpert . 1998 . Signal-dependent noise determines motor planning. Nature 394, 6695 (1998), 780--784. Christopher M. Harris and Daniel M. Wolpert. 1998. Signal-dependent noise determines motor planning. Nature 394, 6695 (1998), 780--784."},{"key":"e_1_3_2_1_21_1","volume-title":"Communication and Software Systems: Performance Evaluation","volume":"4486","author":"Kwiatkowska M.","unstructured":"M. Kwiatkowska , G. Norman , and D. Parker . 2007. Stochastic Model Checking. In Formal Methods for the Design of Computer , Communication and Software Systems: Performance Evaluation , Vol. 4486 . Springer, 220--270. M. Kwiatkowska, G. Norman, and D. Parker. 2007. Stochastic Model Checking. In Formal Methods for the Design of Computer, Communication and Software Systems: Performance Evaluation, Vol. 4486. Springer, 220--270."},{"key":"e_1_3_2_1_22_1","volume-title":"Proc. Int. Conf. Comput.-Aided Verification (LNCS), G. Gopalakrishnan and S. Qadeer (Eds.)","volume":"6806","author":"Kwiatkowska M.","unstructured":"M. Kwiatkowska , G. Norman , and D. Parker . 2011. PRISM 4.0: Verification of Probabilistic Real-time Systems . In Proc. Int. Conf. Comput.-Aided Verification (LNCS), G. Gopalakrishnan and S. Qadeer (Eds.) , Vol. 6806 . Springer, 585--591. M. Kwiatkowska, G. Norman, and D. Parker. 2011. PRISM 4.0: Verification of Probabilistic Real-time Systems. In Proc. Int. Conf. Comput.-Aided Verification (LNCS), G. Gopalakrishnan and S. Qadeer (Eds.), Vol. 6806. Springer, 585--591."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12002-2_3"},{"key":"e_1_3_2_1_24_1","volume-title":"Stochastic Assume-Guarantee Contracts for Cyber-Physical System Design Under Probabilistic Requirements. arXiv preprint arXiv:1705.09316","author":"Li Jiwei","year":"2017","unstructured":"Jiwei Li , Pierluigi Nuzzo , Alberto Sangiovanni-Vincentelli , Yugeng Xi , and Dewei Li. 2017. Stochastic Assume-Guarantee Contracts for Cyber-Physical System Design Under Probabilistic Requirements. arXiv preprint arXiv:1705.09316 ( 2017 ). Jiwei Li, Pierluigi Nuzzo, Alberto Sangiovanni-Vincentelli, Yugeng Xi, and Dewei Li. 2017. Stochastic Assume-Guarantee Contracts for Cyber-Physical System Design Under Probabilistic Requirements. arXiv preprint arXiv:1705.09316 (2017)."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/CACSD.2004.1393890"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2013.6760330"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"crossref","unstructured":"Oded Maler and Dejan Nickovic. 2004. Monitoring Temporal Properties of Continuous Signals. In Formal Modeling and Analysis of Timed Systems. 152--166.  Oded Maler and Dejan Nickovic. 2004. Monitoring Temporal Properties of Continuous Signals. In Formal Modeling and Analysis of Timed Systems . 152--166.","DOI":"10.1007\/978-3-540-30206-3_12"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1137\/050622328"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2015.2453253"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2013.2295764"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.5555\/2032266.2032300"},{"volume-title":"Proc. Int. Conf. Decision and Control. IEEE, 81--87","author":"Raman Vasumathi","key":"e_1_3_2_1_32_1","unstructured":"Vasumathi Raman , Alexandre Donz\u00e9 , Mehdi Maasoumy , Richard M. Murray , Alberto Sangiovanni-Vincentelli , and Sanjit A. Seshia . 2014. Model predictive control with signal temporal logic specifications . In Proc. Int. Conf. Decision and Control. IEEE, 81--87 . Vasumathi Raman, Alexandre Donz\u00e9, Mehdi Maasoumy, Richard M. Murray, Alberto Sangiovanni-Vincentelli, and Sanjit A. Seshia. 2014. Model predictive control with signal temporal logic specifications. In Proc. Int. Conf. Decision and Control. IEEE, 81--87."},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.15607\/RSS.2016.XII.017"},{"key":"e_1_3_2_1_34_1","volume-title":"Taming Dr. Frankenstein: Contract-Based Design for Cyber-Physical Systems. European Journal of Control 18--3, 3","author":"Sangiovanni-Vincentelli Alberto","year":"2012","unstructured":"Alberto Sangiovanni-Vincentelli , Werner Damm , and Roberto Passerone . 2012. Taming Dr. Frankenstein: Contract-Based Design for Cyber-Physical Systems. European Journal of Control 18--3, 3 ( 2012 ), 217--238. Alberto Sangiovanni-Vincentelli, Werner Damm, and Roberto Passerone. 2012. Taming Dr. Frankenstein: Contract-Based Design for Cyber-Physical Systems. European Journal of Control 18--3, 3 (2012), 217--238."},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACC.2015.7171897"},{"key":"e_1_3_2_1_36_1","volume-title":"Operations Research: Applications & Algorithms","author":"Winston Wayne L.","year":"2008","unstructured":"Wayne L. Winston . 2008 . Operations Research: Applications & Algorithms . Thomson Business Press . Wayne L. Winston. 2008. Operations Research: Applications & Algorithms. Thomson Business Press."}],"event":{"name":"MEMOCODE '17: 15th ACM-IEEE International Conference on Formal Methods and Models for System Design","sponsor":["SIGBED ACM Special Interest Group on Embedded Systems","SIGDA ACM Special Interest Group on Design Automation","IEEE CAS","IEEE CEDA"],"location":"Vienna Austria","acronym":"MEMOCODE '17"},"container-title":["Proceedings of the 15th ACM-IEEE International Conference on Formal Methods and Models for System Design"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3127041.3127045","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3127041.3127045","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3127041.3127045","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:11:06Z","timestamp":1750212666000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3127041.3127045"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,9,29]]},"references-count":36,"alternative-id":["10.1145\/3127041.3127045","10.1145\/3127041"],"URL":"https:\/\/doi.org\/10.1145\/3127041.3127045","relation":{},"subject":[],"published":{"date-parts":[[2017,9,29]]},"assertion":[{"value":"2017-09-29","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}