{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,3]],"date-time":"2026-03-03T02:41:54Z","timestamp":1772505714437,"version":"3.50.1"},"publisher-location":"Cham","reference-count":30,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031377051","type":"print"},{"value":"9783031377068","type":"electronic"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,7,17]],"date-time":"2023-07-17T00:00:00Z","timestamp":1689552000000},"content-version":"vor","delay-in-days":197,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We present a major new version of Scenic, a probabilistic programming language for writing formal models of the environments of cyber-physical systems. Scenic has been successfully used for the design and analysis of CPS in a variety of domains, but earlier versions are limited to environments that are essentially two-dimensional. In this paper, we extend Scenic with native support for 3D geometry, introducing new syntax that provides expressive ways to describe 3D configurations while preserving the simplicity and readability of the language. We replace Scenic\u2019s simplistic representation of objects as boxes with precise modeling of complex shapes, including a ray tracing-based visibility system that accounts for object occlusion. We also extend the language to support arbitrary temporal requirements expressed in LTL, and build an extensible Scenic parser generated from a formal grammar of the language. Finally, we illustrate the new application domains these features enable with case studies that would have been impossible to accurately model in Scenic 2.<\/jats:p>","DOI":"10.1007\/978-3-031-37706-8_13","type":"book-chapter","created":{"date-parts":[[2023,7,16]],"date-time":"2023-07-16T10:01:21Z","timestamp":1689501681000},"page":"253-265","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":13,"title":["3D Environment Modeling for\u00a0Falsification and\u00a0Beyond with\u00a0Scenic\u00a03.0"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3089-1129","authenticated-orcid":false,"given":"Eric","family":"Vin","sequence":"first","affiliation":[]},{"given":"Shun","family":"Kashiwa","sequence":"additional","affiliation":[]},{"given":"Matthew","family":"Rhea","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9992-9965","authenticated-orcid":false,"given":"Daniel J.","family":"Fremont","sequence":"additional","affiliation":[]},{"given":"Edward","family":"Kim","sequence":"additional","affiliation":[]},{"given":"Tommaso","family":"Dreossi","sequence":"additional","affiliation":[]},{"given":"Shromona","family":"Ghosh","sequence":"additional","affiliation":[]},{"given":"Xiangyu","family":"Yue","sequence":"additional","affiliation":[]},{"given":"Alberto L.","family":"Sangiovanni-Vincentelli","sequence":"additional","affiliation":[]},{"given":"Sanjit A.","family":"Seshia","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,7,17]]},"reference":[{"key":"13_CR1","first-page":"6028","volume":"36","author":"AS Azad","year":"2022","unstructured":"Azad, A.S., et al.: Programmatic modeling and generation of real-time strategic soccer environments for reinforcement learning. Proc. AAAI Conf. Artif. Intell. 36, 6028\u20136036 (2022)","journal-title":"Proc. AAAI Conf. Artif. Intell."},{"issue":"3","key":"13_CR2","doi-asserted-by":"publisher","first-page":"651","DOI":"10.1093\/logcom\/exn075","volume":"20","author":"A Bauer","year":"2010","unstructured":"Bauer, A., Leucker, M., Schallhart, C.: Comparing LTL semantics for runtime verification. J. Log. Comput. 20(3), 651\u2013674 (2010). https:\/\/doi.org\/10.1093\/logcom\/exn075","journal-title":"J. Log. Comput."},{"key":"13_CR3","doi-asserted-by":"publisher","unstructured":"Broy et al.: Model-based testing of reactive systems. Lecture Notes in Computer Science (2005). https:\/\/doi.org\/10.1007\/b137241","DOI":"10.1007\/b137241"},{"key":"13_CR4","unstructured":"Dawson-Haggerty, M., et al.: Trimesh. https:\/\/trimsh.org"},{"key":"13_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"432","DOI":"10.1007\/978-3-030-25540-4_25","volume-title":"Computer Aided Verification","author":"T Dreossi","year":"2019","unstructured":"Dreossi, T., et al.: VerifAI: a toolkit for the formal design and analysis of artificial intelligence-based systems. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11561, pp. 432\u2013442. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_25"},{"key":"13_CR6","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/11940197_12","volume-title":"Formal Approaches to Software Testing and Runtime Verification","author":"GE Fainekos","year":"2006","unstructured":"Fainekos, G.E., Pappas, G.J.: Robustness of temporal logic specifications. In: Havelund, K., N\u00fa\u00f1ez, M., Ro\u015fu, G., Wolff, B. (eds.) Formal Approaches to Software Testing and Runtime Verification, pp. 178\u2013192. Springer, Berlin Heidelberg, Berlin, Heidelberg (2006)"},{"issue":"6","key":"13_CR7","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2366145.2366154","volume":"31","author":"M Fisher","year":"2012","unstructured":"Fisher, M., Ritchie, D., Savva, M., Funkhouser, T., Hanrahan, P.: Example-based synthesis of 3d object arrangements. ACM Trans. Graph. 31(6), 1\u201311 (2012). https:\/\/doi.org\/10.1145\/2366145.2366154","journal-title":"ACM Trans. Graph."},{"key":"13_CR8","doi-asserted-by":"crossref","unstructured":"Ford, B.: Parsing expression grammars: a recognition-based syntactic foundation. In: Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 111\u2013122 (2004)","DOI":"10.1145\/964001.964011"},{"key":"13_CR9","doi-asserted-by":"crossref","unstructured":"Fremont, D.J., Chiu, J., Margineantu, D.D., Osipychev, D., Seshia, S.A.: Formal analysis and redesign of a neural network-based aircraft taxiing system with VerifAI. Computer Aided Verification, pp. 122\u2013134 (2020)","DOI":"10.1007\/978-3-030-53288-8_6"},{"key":"13_CR10","doi-asserted-by":"crossref","unstructured":"Fremont, D.J., Dreossi, T., Ghosh, S., Yue, X., Sangiovanni-Vincentelli, A.L., Seshia, S.A.: Scenic: A language for scenario specification and scene generation. In: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation (2019)","DOI":"10.1145\/3314221.3314633"},{"key":"13_CR11","unstructured":"Fremont, D.J., et al.: Scenic Repository. https:\/\/github.com\/BerkeleyLearnVerify\/Scenic"},{"key":"13_CR12","doi-asserted-by":"publisher","DOI":"10.1007\/s10994-021-06120-5","author":"DJ Fremont","year":"2022","unstructured":"Fremont, D.J., et al.: Scenic: a language for scenario specification and data generation. Mach. Learn. (2022). https:\/\/doi.org\/10.1007\/s10994-021-06120-5","journal-title":"Mach. Learn."},{"key":"13_CR13","doi-asserted-by":"crossref","unstructured":"Fremont, D.J., et al.: Formal scenario-based testing of autonomous vehicles: From simulation to the real world. In: 2020 IEEE Intelligent Transportation Systems Conference, ITSC 2020, pp. 913\u2013920. IEEE (2020). https:\/\/arxiv.org\/abs\/2003.07739","DOI":"10.1109\/ITSC45102.2020.9294368"},{"key":"13_CR14","doi-asserted-by":"publisher","unstructured":"Fu, R., Zhan, X., Chen, Y., Ritchie, D., Sridhar, S.: Shapecrafter: A recursive text-conditioned 3d shape generation model. CoRR abs\/2207.09446 (2022). https:\/\/doi.org\/10.48550\/arXiv.2207.09446","DOI":"10.48550\/arXiv.2207.09446"},{"key":"13_CR15","doi-asserted-by":"crossref","unstructured":"Goodman, N.D., Stuhlm\u00fcller, A.: The Design and Implementation of Probabilistic Programming Languages. http:\/\/dippl.org (2014) Accessed 28 Jan 2023","DOI":"10.1016\/j.cogsys.2013.07.003"},{"key":"13_CR16","unstructured":"iRobot: Create Educational Robot. https:\/\/edu.irobot.com\/what-we-offer\/create3"},{"issue":"9","key":"13_CR17","doi-asserted-by":"publisher","first-page":"920","DOI":"10.1007\/s11263-018-1103-5","volume":"126","author":"C Jiang","year":"2018","unstructured":"Jiang, C., et al.: Configurable 3D scene synthesis and 2D image rendering with per-pixel ground truth using stochastic grammars. Int. J. Comput. Vision 126(9), 920\u2013941 (2018). https:\/\/doi.org\/10.1007\/s11263-018-1103-5","journal-title":"Int. J. Comput. Vision"},{"key":"13_CR18","doi-asserted-by":"crossref","unstructured":"Maler, O., Nickovic, D.: Monitoring temporal properties of continuous signals. In: Proc. FORMATS (2004)","DOI":"10.1007\/978-3-540-30206-3_12"},{"key":"13_CR19","doi-asserted-by":"crossref","unstructured":"Michel, O.: Webots: Professional mobile robot simulation. J. Adv. Robot. Syst. 1(1), 39\u201342 (2004). http:\/\/www.ars-journal.com\/International-Journal-of-Advanced-Robotic-Systems\/Volume-1\/39-42.pdf","DOI":"10.5772\/5618"},{"key":"13_CR20","doi-asserted-by":"publisher","unstructured":"M\u00fcller, P., Wonka, P., Haegler, S., Ulmer, A., Van Gool, L.: Procedural modeling of buildings. ACM Trans. Graph. 25(3) (2006). https:\/\/doi.org\/10.1145\/1141911.1141931","DOI":"10.1145\/1141911.1141931"},{"key":"13_CR21","doi-asserted-by":"publisher","unstructured":"Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science (sfcs 1977), pp. 46\u201357 (1977). https:\/\/doi.org\/10.1109\/SFCS.1977.32","DOI":"10.1109\/SFCS.1977.32"},{"key":"13_CR22","unstructured":"Ritchie, D.: Quicksand: A Lightweight Implementation of Probabilistic Programming for Procedural Modeling and Design. In: 3rd NIPS Workshop on Probabilistic Programming (2014). https:\/\/dritchie.github.io\/pdf\/qs.pdf"},{"key":"13_CR23","unstructured":"Ritchie, D.: Probabilistic programming for procedural modeling and design. Ph.D. thesis, Stanford (2016). https:\/\/purl.stanford.edu\/vh730bw6700"},{"key":"13_CR24","unstructured":"Salgado, P.G., van Rossum, G., Nikolaou, L.: Pegen. https:\/\/we-like-parsers.github.io\/pegen\/"},{"key":"13_CR25","unstructured":"Seshia, S.A., Sadigh, D., Sastry, S.S.: Towards Verified Artificial Intelligence. ArXiv e-prints (July 2016)"},{"key":"13_CR26","unstructured":"Sutton, M., Greene, A., Amini, P.: Fuzzing: Brute force vulnerability discovery. Addison-Wesley (2007)"},{"key":"13_CR27","unstructured":"The Blender Community: Blender. http:\/\/www.blender.org"},{"key":"13_CR28","unstructured":"The OpenSCAD Community: OpenSCAD. https:\/\/openscad.org"},{"key":"13_CR29","doi-asserted-by":"crossref","unstructured":"Viswanadha, K., et al.: Addressing the IEEE AV test challenge with Scenic and VerifAI. In: 2021 IEEE International Conference on Artificial Intelligence Testing (AITest) (2021)","DOI":"10.1109\/AITEST52744.2021.00034"},{"key":"13_CR30","doi-asserted-by":"publisher","unstructured":"Wang, K., Savva, M., Chang, A.X., Ritchie, D.: Deep convolutional priors for indoor scene synthesis. ACM Trans. Graph. 37(4), 70 (2018). https:\/\/doi.org\/10.1145\/3197517.3201362","DOI":"10.1145\/3197517.3201362"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-37706-8_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,1,5]],"date-time":"2024-01-05T11:05:11Z","timestamp":1704452711000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-37706-8_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031377051","9783031377068"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-37706-8_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"17 July 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17 July 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 July 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"35","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.i-cav.org\/2023\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"hotcrp","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"261","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"67","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"26% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"11","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}