{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,8]],"date-time":"2026-02-08T07:29:31Z","timestamp":1770535771474,"version":"3.49.0"},"reference-count":45,"publisher":"Association for Computing Machinery (ACM)","issue":"5s","license":[{"start":{"date-parts":[[2019,10,8]],"date-time":"2019-10-08T00:00:00Z","timestamp":1570492800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["CPS\/CNS-1453860"],"award-info":[{"award-number":["CPS\/CNS-1453860"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF-1837131"],"award-info":[{"award-number":["CCF-1837131"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000185","name":"DARPA","doi-asserted-by":"crossref","award":["N66001-17-1-4044"],"award-info":[{"award-number":["N66001-17-1-4044"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/100000183","name":"Army Research Office","doi-asserted-by":"publisher","award":["W911NF-17-1-0076"],"award-info":[{"award-number":["W911NF-17-1-0076"]}],"id":[{"id":"10.13039\/100000183","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Embed. Comput. Syst."],"published-print":{"date-parts":[[2019,10,31]]},"abstract":"<jats:p>In this paper, we propose Stochastic Temporal Logic (StTL) as a formalism for expressing probabilistic specifications on time-varying behaviors of controlled stochastic dynamical systems. To make StTL a more effective specification formalism, we introduce the quantitative semantics for StTL to reason about the robust satisfaction of an StTL specification by a given system. Additionally, we propose using the robustness value as the objective function to be maximized by a stochastic optimization algorithm for the purpose of controller design. Finally, we formulate an algorithm for parameter inference for Parameteric-StTL specifications, which allows specifications to be mined from output traces of the underlying system. We demonstrate and validate our framework on two case studies inspired by the automotive domain.<\/jats:p>","DOI":"10.1145\/3358231","type":"journal-article","created":{"date-parts":[[2019,10,10]],"date-time":"2019-10-10T13:13:05Z","timestamp":1570713185000},"page":"1-21","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":15,"title":["Specification Mining and Robust Design under Uncertainty"],"prefix":"10.1145","volume":"18","author":[{"given":"Panagiotis","family":"Kyriakis","sequence":"first","affiliation":[{"name":"University of Southern California"}]},{"given":"Jyotirmoy V.","family":"Deshmukh","sequence":"additional","affiliation":[{"name":"University of Southern California"}]},{"given":"Paul","family":"Bogdan","sequence":"additional","affiliation":[{"name":"University of Southern California"}]}],"member":"320","published-online":{"date-parts":[[2019,10,8]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2011.2160595"},{"key":"e_1_2_1_2_1","volume-title":"IEEE 55th Conference on Decision and Control (CDC). 6565--6570","author":"Aksaray D.","unstructured":"D. Aksaray , A. Jones , Z. Kong , M. Schwager , and C. Belta . 2016. Q-learning for robust satisfaction of signal temporal logic specifications . In IEEE 55th Conference on Decision and Control (CDC). 6565--6570 . D. Aksaray, A. Jones, Z. Kong, M. Schwager, and C. Belta. 2016. Q-learning for robust satisfaction of signal temporal logic specifications. In IEEE 55th Conference on Decision and Control (CDC). 6565--6570."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/TITS.2009.2018966"},{"key":"e_1_2_1_4_1","volume-title":"Proceedings of Runtime Verification. 147--160","author":"Asarin Eugene","year":"2011","unstructured":"Eugene Asarin , Alexandre Donz\u00e9 , Oded Maler , and Dejan Nickovic . 2011 . Parametric identification of temporal properties . In Proceedings of Runtime Verification. 147--160 . Eugene Asarin, Alexandre Donz\u00e9, Oded Maler, and Dejan Nickovic. 2011. Parametric identification of temporal properties. In Proceedings of Runtime Verification. 147--160."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1006\/jcss.1998.1601"},{"key":"e_1_2_1_6_1","volume-title":"Exploring New Frontiers of Theoretical Informatics","author":"Baier Christel","unstructured":"Christel Baier , Marcus Gr\u00f6\u00dfer , Martin Leucker , Benedikt Bollig , and Frank Ciesinski . 2004. Controller synthesis for probabilistic systems . In Exploring New Frontiers of Theoretical Informatics . Springer , 493--506. Christel Baier, Marcus Gr\u00f6\u00dfer, Martin Leucker, Benedikt Bollig, and Frank Ciesinski. 2004. Controller synthesis for probabilistic systems. In Exploring New Frontiers of Theoretical Informatics. Springer, 493--506."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3178126.3178132"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.125.1"},{"key":"e_1_2_1_9_1","volume-title":"Convex Optimization","author":"Boyd Stephen","unstructured":"Stephen Boyd and Lieven Vandenberghe . 2004. Convex Optimization . Cambridge University Press , New York, NY, USA . Stephen Boyd and Lieven Vandenberghe. 2004. Convex Optimization. Cambridge University Press, New York, NY, USA."},{"key":"e_1_2_1_10_1","doi-asserted-by":"crossref","unstructured":"Tom\u00e1\u0161 Br\u00e1zdil Krishnendu Chatterjee Martin Chmel\u00edk Vojt\u011bch Forejt Jan K\u0159et\u00ednsk\u00fd Marta Kwiatkowska David Parker and Mateusz Ujma. 2014. Verification of Markov decision processes using learning algorithms. In Automated Technology for Verification and Analysis. 98--114.  Tom\u00e1\u0161 Br\u00e1zdil Krishnendu Chatterjee Martin Chmel\u00edk Vojt\u011bch Forejt Jan K\u0159et\u00ednsk\u00fd Marta Kwiatkowska David Parker and Mateusz Ujma. 2014. Verification of Markov decision processes using learning algorithms. In Automated Technology for Verification and Analysis. 98--114.","DOI":"10.1007\/978-3-319-11936-6_8"},{"key":"e_1_2_1_11_1","volume-title":"The Analysis of Time Series: An Introduction","author":"Chatfield Chris","unstructured":"Chris Chatfield . 2016. The Analysis of Time Series: An Introduction . CRC press . Chris Chatfield. 2016. The Analysis of Time Series: An Introduction. CRC press."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2016.7798967"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.5555\/2050917.2050919"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-00151-3_1"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.automatica.2013.05.025"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_19"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_19"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2009.06.021"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2015.7403395"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/EMBC.2014.6944707"},{"key":"e_1_2_1_21_1","volume-title":"A logic for reasoning about time and reliability. Formal Aspects of Computing 6, 5 (1","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 (1 Sep 1994 ), 512--535. Hans Hansson and Bengt Jonsson. 1994. A logic for reasoning about time and reliability. Formal Aspects of Computing 6, 5 (1 Sep 1994), 512--535."},{"key":"e_1_2_1_22_1","volume-title":"1st and 2nd International Workshop on Applied veRification for Continuous and Hybrid Systems (EPiC Series in Computing), Goran Frehse and Matthias Althoff (Eds.)","volume":"34","author":"Hoxha Bardh","year":"2015","unstructured":"Bardh Hoxha , Houssam Abbas , and Georgios Fainekos . 2015 . Benchmarks for temporal logic requirements for automotive systems. In ARCH14-15 . 1st and 2nd International Workshop on Applied veRification for Continuous and Hybrid Systems (EPiC Series in Computing), Goran Frehse and Matthias Althoff (Eds.) , Vol. 34 . EasyChair, 25--30. Bardh Hoxha, Houssam Abbas, and Georgios Fainekos. 2015. Benchmarks for temporal logic requirements for automotive systems. In ARCH14-15. 1st and 2nd International Workshop on Applied veRification for Continuous and Hybrid Systems (EPiC Series in Computing), Goran Frehse and Matthias Althoff (Eds.), Vol. 34. EasyChair, 25--30."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-017-0447-4"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-017-9413-9"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2562059.2562140"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2015.2421907"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2014.7039487"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2009.2019791"},{"key":"e_1_2_1_29_1","volume-title":"2011 50th IEEE Conference on Decision and Control and European Control Conference. 6122--6127","author":"Kamgarpour M.","unstructured":"M. Kamgarpour , J. Ding , S. Summers , A. Abate , J. Lygeros , and C. Tomlin . 2011. Discrete time stochastic hybrid dynamical games: Verification 8 controller synthesis . In 2011 50th IEEE Conference on Decision and Control and European Control Conference. 6122--6127 . M. Kamgarpour, J. Ding, S. Summers, A. Abate, J. Lygeros, and C. Tomlin. 2011. Discrete time stochastic hybrid dynamical games: Verification 8 controller synthesis. In 2011 50th IEEE Conference on Decision and Control and European Control Conference. 6122--6127."},{"key":"e_1_2_1_30_1","doi-asserted-by":"crossref","unstructured":"J. Kapinski X. Jin J. Deshmukh A. Donz\u00e9 T. Yamaguchi H. Ito T. Kaga S. Kobuna and S. A. Seshia. 2016. ST-Lib: A library for specifying and classifying model behaviors. In SAE Technical Paper. SAE.  J. Kapinski X. Jin J. Deshmukh A. Donz\u00e9 T. Yamaguchi H. Ito T. Kaga S. Kobuna and S. A. Seshia. 2016. ST-Lib: A library for specifying and classifying model behaviors. In SAE Technical Paper. SAE.","DOI":"10.4271\/2016-01-0621"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2562059.2562146"},{"key":"e_1_2_1_32_1","volume-title":"Proceedings of the 2011 American Control Conference. 311--316","author":"Lahijanian M.","unstructured":"M. Lahijanian , S. B. Andersson , and C. Belta . 2011. Control of Markov decision processes from PCTL specifications . In Proceedings of the 2011 American Control Conference. 311--316 . M. Lahijanian, S. B. Andersson, and C. Belta. 2011. Control of Markov decision processes from PCTL specifications. In Proceedings of the 2011 American Control Conference. 311--316."},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.5555\/1939399.1939412"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12002-2_6"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3127041.3127045"},{"key":"e_1_2_1_36_1","volume-title":"Learning Monotone Partitions of Partially-Ordered Domains (Work in Progress). (July","author":"Maler Oded","year":"2017","unstructured":"Oded Maler . 2017. Learning Monotone Partitions of Partially-Ordered Domains (Work in Progress). (July 2017 ). https:\/\/hal.archives-ouvertes.fr\/hal-01556243 working paper or preprint. Oded Maler. 2017. Learning Monotone Partitions of Partially-Ordered Domains (Work in Progress). (July 2017). https:\/\/hal.archives-ouvertes.fr\/hal-01556243 working paper or preprint."},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30206-3_12"},{"key":"e_1_2_1_38_1","volume-title":"Computational Methods in Systems Biology, Monika Heiner and Adelinde M","author":"Rizk Aur\u00e9lien","unstructured":"Aur\u00e9lien Rizk , Gr\u00e9gory Batt , Fran\u00e7ois Fages , and Sylvain Soliman . 2008. On a continuous degree of satisfaction of temporal logic formulae with applications to systems biology . In Computational Methods in Systems Biology, Monika Heiner and Adelinde M . Uhrmacher (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg , 251--268. Aur\u00e9lien Rizk, Gr\u00e9gory Batt, Fran\u00e7ois Fages, and Sylvain Soliman. 2008. On a continuous degree of satisfaction of temporal logic formulae with applications to systems biology. In Computational Methods in Systems Biology, Monika Heiner and Adelinde M. Uhrmacher (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 251--268."},{"key":"e_1_2_1_39_1","volume-title":"Workshop on Applied veRification for Continuous and Hybrid Systems, ARCH@CPSWeek","author":"Roehm Hendrik","year":"2015","unstructured":"Hendrik Roehm , Rainer Gmehlich , Thomas Heinz , Jens Oehlerking , and Matthias Woehrle . 2015 . Industrial examples of formal specifications for test case generation . In Workshop on Applied veRification for Continuous and Hybrid Systems, ARCH@CPSWeek 2015. 80--88. Hendrik Roehm, Rainer Gmehlich, Thomas Heinz, Jens Oehlerking, and Matthias Woehrle. 2015. Industrial examples of formal specifications for test case generation. In Workshop on Applied veRification for Continuous and Hybrid Systems, ARCH@CPSWeek 2015. 80--88."},{"key":"e_1_2_1_40_1","unstructured":"Dorsa Sadigh and Ashish Kapoor. 2016. Safe control under uncertainty with probabilistic signal temporal logic. In Robotics Science and Systems.  Dorsa Sadigh and Ashish Kapoor. 2016. Safe control under uncertainty with probabilistic signal temporal logic. In Robotics Science and Systems."},{"key":"e_1_2_1_41_1","volume-title":"Eberhart","author":"Shi Yuhui","year":"1998","unstructured":"Yuhui Shi and Russell C . Eberhart . 1998 . Parameter selection in particle swarm optimization. In Evolutionary Programming VII, V. W. Porto, N. Saravanan, D. Waagen, and A. E. Eiben (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg, 591--600. Yuhui Shi and Russell C. Eberhart. 1998. Parameter selection in particle swarm optimization. In Evolutionary Programming VII, V. W. Porto, N. Saravanan, D. Waagen, and A. E. Eiben (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 591--600."},{"key":"e_1_2_1_42_1","volume-title":"Density Estimation for Statistics and Data Analysis","author":"Silverman Bernard W.","unstructured":"Bernard W. Silverman . 1986. Density Estimation for Statistics and Data Analysis . Vol. 26 . CRC press . Bernard W. Silverman. 1986. Density Estimation for Statistics and Data Analysis. Vol. 26. CRC press."},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1109\/TMECH.2008.915820"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3055004.3055017"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2015.7403399"}],"container-title":["ACM Transactions on Embedded Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3358231","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3358231","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3358231","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:23:07Z","timestamp":1750202587000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3358231"}},"subtitle":["A Stochastic Temporal Logic Approach"],"short-title":[],"issued":{"date-parts":[[2019,10,8]]},"references-count":45,"journal-issue":{"issue":"5s","published-print":{"date-parts":[[2019,10,31]]}},"alternative-id":["10.1145\/3358231"],"URL":"https:\/\/doi.org\/10.1145\/3358231","relation":{},"ISSN":["1539-9087","1558-3465"],"issn-type":[{"value":"1539-9087","type":"print"},{"value":"1558-3465","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,10,8]]},"assertion":[{"value":"2019-04-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-07-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-10-08","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}