{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,3]],"date-time":"2026-03-03T14:52:12Z","timestamp":1772549532709,"version":"3.50.1"},"reference-count":45,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2019,1,25]],"date-time":"2019-01-25T00:00:00Z","timestamp":1548374400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100004543","name":"China Scholarship Council","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100004543","id-type":"DOI","asserted-by":"crossref"}]},{"name":"TerraSwarm"},{"name":"one of six centers of STARnet"},{"name":"Semiconductor Research Corporation program"},{"name":"MARCO and DARPA"},{"DOI":"10.13039\/501100001809","name":"National Science Foundation of China","doi-asserted-by":"crossref","award":["61433002 and 61333009"],"award-info":[{"award-number":["61433002 and 61333009"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Embed. Comput. Syst."],"published-print":{"date-parts":[[2019,1,31]]},"abstract":"<jats:p>We present an assume-guarantee contract framework for cyber-physical system design under probabilistic requirements. Given a stochastic linear system and a set of requirements captured by bounded Stochastic Signal Temporal Logic (StSTL) contracts, we propose algorithms to check contract compatibility, consistency, and refinement, and generate a sequence of control inputs that satisfies a contract. We leverage encodings of the verification and control synthesis tasks into mixed integer optimization problems, and conservative approximations of probabilistic constraints that produce sound and tractable problem formulations. We illustrate the effectiveness of our approach on three case studies, including the design of controllers for aircraft power distribution networks.<\/jats:p>","DOI":"10.1145\/3243216","type":"journal-article","created":{"date-parts":[[2019,1,28]],"date-time":"2019-01-28T14:01:39Z","timestamp":1548684099000},"page":"1-26","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":23,"title":["Stochastic Assume-Guarantee Contracts for Cyber-Physical System Design"],"prefix":"10.1145","volume":"18","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2984-0364","authenticated-orcid":false,"given":"Pierluigi","family":"Nuzzo","sequence":"first","affiliation":[{"name":"University of Southern California, Los Angeles, CA"}]},{"given":"Jiwei","family":"Li","sequence":"additional","affiliation":[{"name":"Shanghai Jiao Tong University, Shanghai, P. R. China"}]},{"given":"Alberto L.","family":"Sangiovanni-Vincentelli","sequence":"additional","affiliation":[{"name":"University of California at Berkeley, Berkeley, CA"}]},{"given":"Yugeng","family":"Xi","sequence":"additional","affiliation":[{"name":"Shanghai Jiao Tong University, Shanghai, P. R. China"}]},{"given":"Dewei","family":"Li","sequence":"additional","affiliation":[{"name":"Shanghai Jiao Tong University, Shanghai, P. R. China"}]}],"member":"320","published-online":{"date-parts":[[2019,1,25]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"2018. Stochastic Contract-based Analysis and Synthesis. Retrieved from https:\/\/github.com\/nuzzo\/SCAnS.  2018. Stochastic Contract-based Analysis and Synthesis. Retrieved from https:\/\/github.com\/nuzzo\/SCAnS."},{"key":"e_1_2_1_2_1","volume-title":"Facets of Combinatorial Optimization","author":"Achterberg Tobias","unstructured":"Tobias Achterberg and Roland Wunderling . 2013. Mixed integer programming: Analyzing 12 years of progress . In Facets of Combinatorial Optimization . Springer , 449--481. Tobias Achterberg and Roland Wunderling. 2013. Mixed integer programming: Analyzing 12 years of progress. In Facets of Combinatorial Optimization. Springer, 449--481."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0005-1098(98)00178-2"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-92188-2_9"},{"key":"e_1_2_1_5_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."},{"key":"e_1_2_1_6_1","volume-title":"Applied Mathematical Programming","author":"Bradley Stephen","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_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2010.23"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2014.06.011"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/5397.5399"},{"key":"e_1_2_1_10_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_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/503209.503226"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2006.883060"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACSD.2010.13"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.5555\/1946284.1946307"},{"key":"e_1_2_1_15_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 , and Andrzej W\u0105sowski . 2011 . APAC: A tool for reasoning about abstract probabilistic automata. (2011). Beno\u00eet Delahaye, Kim G. Larsen, Axel Legay, Mikkel L. Pedersen, and Andrzej W\u0105sowski. 2011. APAC: A tool for reasoning about abstract probabilistic automata. (2011)."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.5555\/1869916"},{"key":"e_1_2_1_17_1","volume-title":"Remote stabilization over fading channels. Systems 8 Control Letters 54, 3","author":"Elia Nicola","year":"2005","unstructured":"Nicola Elia . 2005. Remote stabilization over fading channels. Systems 8 Control Letters 54, 3 ( 2005 ), 237--249. Nicola Elia. 2005. Remote stabilization over fading channels. Systems 8 Control Letters 54, 3 (2005), 237--249."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.23919\/ACC.2017.7963204"},{"key":"e_1_2_1_19_1","volume-title":"Seshia","author":"Ghosh Shromona","year":"2016","unstructured":"Shromona Ghosh , Dorsa Sadigh , Pierluigi Nuzzo , Vasumathi Raman , Alexandre Donze , Alberto Sangiovanni-Vincentelli , S. Shankar Sastry , and Sanjit A . Seshia . 2016 . Diagnosis and repair for synthesis from signal temporal logic specifications. Shromona Ghosh, Dorsa Sadigh, Pierluigi Nuzzo, Vasumathi Raman, Alexandre Donze, Alberto Sangiovanni-Vincentelli, S. Shankar Sastry, and Sanjit A. Seshia. 2016. Diagnosis and repair for synthesis from signal temporal logic specifications."},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-012-0162-4"},{"key":"e_1_2_1_21_1","volume-title":"Gurobi Optimization","author":"Inc.","year":"2015","unstructured":"Inc. Gurobi Optimization . 2015 . Gurobi Optimizer Reference Manual. Retrieved from http:\/\/www.gurobi.com. Inc. Gurobi Optimization. 2015. Gurobi Optimizer Reference Manual. Retrieved from http:\/\/www.gurobi.com."},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211866"},{"key":"e_1_2_1_23_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_2_1_24_1","volume-title":"Sangiovanni-Vincentelli","author":"Iannopollo Antonio","year":"2014","unstructured":"Antonio Iannopollo , Pierluigi Nuzzo , Stavros Tripakis , and Alberto L . Sangiovanni-Vincentelli . 2014 . Library-based scalable refinement checking for contract-based design. In Proc. Design, Automation and Test in Europe. 1--6. Antonio Iannopollo, Pierluigi Nuzzo, Stavros Tripakis, and Alberto L. Sangiovanni-Vincentelli. 2014. Library-based scalable refinement checking for contract-based design. In Proc. Design, Automation and Test in Europe. 1--6."},{"key":"e_1_2_1_25_1","volume-title":"Formal Methods for the Design of Computer, Communication and Software Systems: Performance Evaluation (SFM\u201907) (Lecture Notes in Computer Science)","author":"Kwiatkowska Marta","unstructured":"Marta Kwiatkowska , Gethin Norman , and David Parker . 2007. Stochastic model checking . In Formal Methods for the Design of Computer, Communication and Software Systems: Performance Evaluation (SFM\u201907) (Lecture Notes in Computer Science) , M. Bernardo and J. Hillston (Eds.), Vol. 4486 . Springer , 220--270. Marta Kwiatkowska, Gethin Norman, and David Parker. 2007. Stochastic model checking. In Formal Methods for the Design of Computer, Communication and Software Systems: Performance Evaluation (SFM\u201907) (Lecture Notes in Computer Science), M. Bernardo and J. Hillston (Eds.), Vol. 4486. Springer, 220--270."},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.5555\/2032305.2032352"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12002-2_3"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3127041.3127045"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/CACSD.2004.1393890"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2013.6760330"},{"key":"e_1_2_1_31_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_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/2.161279"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1137\/050622328"},{"key":"e_1_2_1_34_1","volume-title":"Proc. Design, Automation and Test in Europe","author":"Nuzzo Pierluigi","unstructured":"Pierluigi Nuzzo , Michele Lora , Yishai Feldman , and A. Sangiovanni-Vincentelli . 2018. CHASE: Contract-based requirement engineering for cyber-physical system design . In Proc. Design, Automation and Test in Europe . Dresden, Germany, 839--844. Pierluigi Nuzzo, Michele Lora, Yishai Feldman, and A. Sangiovanni-Vincentelli. 2018. CHASE: Contract-based requirement engineering for cyber-physical system design. In Proc. Design, Automation and Test in Europe. Dresden, Germany, 839--844."},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2015.2453253"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/JSEN.2012.2211098"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2013.2295764"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.5555\/2032266.2032300"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629335.1629348"},{"key":"e_1_2_1_40_1","volume-title":"Proc. Int. Conf. Decision and Control. IEEE, 81--87","author":"Raman Vasumathi","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_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1109\/TPWRS.2017.2745410"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.15607\/RSS.2016.XII.017"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.3166\/ejc.18.217-238"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACC.2015.7171897"},{"key":"e_1_2_1_45_1","volume-title":"Operations Research: Applications 8 Algorithms","author":"Winston Wayne L.","year":"2008","unstructured":"Wayne L. Winston . 2008 . Operations Research: Applications 8 Algorithms . Thomson Business Press . Wayne L. Winston. 2008. Operations Research: Applications 8 Algorithms. Thomson Business Press."}],"container-title":["ACM Transactions on Embedded Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3243216","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3243216","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T00:57:31Z","timestamp":1750208251000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3243216"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,1,25]]},"references-count":45,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2019,1,31]]}},"alternative-id":["10.1145\/3243216"],"URL":"https:\/\/doi.org\/10.1145\/3243216","relation":{},"ISSN":["1539-9087","1558-3465"],"issn-type":[{"value":"1539-9087","type":"print"},{"value":"1558-3465","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,1,25]]},"assertion":[{"value":"2017-12-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2018-07-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-01-25","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}