{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:14:14Z","timestamp":1750220054783,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":27,"publisher":"ACM","license":[{"start":{"date-parts":[[2023,3,27]],"date-time":"2023-03-27T00:00:00Z","timestamp":1679875200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2023,3,27]]},"DOI":"10.1145\/3555776.3577720","type":"proceedings-article","created":{"date-parts":[[2023,6,7]],"date-time":"2023-06-07T17:16:29Z","timestamp":1686158189000},"page":"109-118","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Traffic Intersections as Agents: A model checking approach for analysing communicating agents"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1630-2153","authenticated-orcid":false,"given":"Thamilselvam","family":"B","sequence":"first","affiliation":[{"name":"IIT Hyderabad, Sangareddy, India"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8232-8269","authenticated-orcid":false,"given":"Yenda","family":"Ramesh","sequence":"additional","affiliation":[{"name":"IIT Hyderabad, Sangareddy, India"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9094-3368","authenticated-orcid":false,"given":"Subrahmanyam","family":"Kalyanasundaram","sequence":"additional","affiliation":[{"name":"IIT Hyderabad, Sangareddy, India"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3761-8501","authenticated-orcid":false,"given":"M V Panduranga","family":"Rao","sequence":"additional","affiliation":[{"name":"IIT Hyderabad, Sangareddy, India"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,6,7]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1016\/j.entcs.2005.10.040","article-title":"PMaude: Rewrite-based Specification Language for Probabilistic Object Systems","volume":"153","author":"Agha Gul A.","year":"2006","unstructured":"Gul A. Agha , Jos\u00e9 Meseguer , and Koushik Sen . 2006 . PMaude: Rewrite-based Specification Language for Probabilistic Object Systems . Electron. Notes Theor. Comput. Sci. 153 , 2 (2006), 213 -- 239 . Gul A. Agha, Jos\u00e9 Meseguer, and Koushik Sen. 2006. PMaude: Rewrite-based Specification Language for Probabilistic Object Systems. Electron. Notes Theor. Comput. Sci. 153, 2 (2006), 213--239.","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"crossref","first-page":"524","DOI":"10.1109\/TSE.2003.1205180","article-title":"Model-checking algorithms for continuous-time Markov chains","volume":"29","author":"Baier Christel","year":"2003","unstructured":"Christel Baier , Boudewijn Haverkort , Holger Hermanns , and J-P Katoen . 2003 . Model-checking algorithms for continuous-time Markov chains . IEEE Transactions on software engineering 29 , 6 (2003), 524 -- 541 . Christel Baier, Boudewijn Haverkort, Holger Hermanns, and J-P Katoen. 2003. Model-checking algorithms for continuous-time Markov chains. IEEE Transactions on software engineering 29, 6 (2003), 524--541.","journal-title":"IEEE Transactions on software engineering"},{"volume-title":"Principles of Model Checking (Representation and Mind Series)","author":"Baier Christel","key":"e_1_3_2_1_3_1","unstructured":"Christel Baier and Joost-Pieter Katoen . 2008. Principles of Model Checking (Representation and Mind Series) . The MIT Press . Christel Baier and Joost-Pieter Katoen. 2008. Principles of Model Checking (Representation and Mind Series). The MIT Press."},{"key":"e_1_3_2_1_4_1","unstructured":"Beno\u00eet Delahaye Axel Legay and Sean Sedwards. 2013. A Simple and Efficient Statistical Model Checking Algorithm to Evaluate Markov Decision Processes. (2013).  Beno\u00eet Delahaye Axel Legay and Sean Sedwards. 2013. A Simple and Efficient Statistical Model Checking Algorithm to Evaluate Markov Decision Processes. (2013)."},{"key":"e_1_3_2_1_5_1","volume-title":"German Conference on Multiagent System Technologies. Springer, 16--28","author":"Delgado Carla","year":"2009","unstructured":"Carla Delgado and Mario Benevides . 2009 . Verification of epistemic properties in probabilistic multi-agent systems . In German Conference on Multiagent System Technologies. Springer, 16--28 . Carla Delgado and Mario Benevides. 2009. Verification of epistemic properties in probabilistic multi-agent systems. In German Conference on Multiagent System Technologies. Springer, 16--28."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"crossref","first-page":"28573","DOI":"10.1109\/ACCESS.2018.2831228","article-title":"Multi-agent systems: A survey","volume":"6","author":"Dorri Ali","year":"2018","unstructured":"Ali Dorri , Salil S Kanhere , and Raja Jurdak . 2018 . Multi-agent systems: A survey . Ieee Access 6 (2018), 28573 -- 28593 . Ali Dorri, Salil S Kanhere, and Raja Jurdak. 2018. Multi-agent systems: A survey. Ieee Access 6 (2018), 28573--28593.","journal-title":"Ieee Access"},{"key":"e_1_3_2_1_7_1","volume-title":"12th ITS European Congress.","author":"Eriksen Andreas Berre","year":"2017","unstructured":"Andreas Berre Eriksen , Chao Huang , Jan Kildebogaard , Harry Lahrmann , Kim G Larsen , Marco Muniz , and Jakob Haahr Taankvist . 2017 . Uppaal stratego for intelligent traffic lights . In 12th ITS European Congress. Andreas Berre Eriksen, Chao Huang, Jan Kildebogaard, Harry Lahrmann, Kim G Larsen, Marco Muniz, and Jakob Haahr Taankvist. 2017. Uppaal stratego for intelligent traffic lights. In 12th ITS European Congress."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"crossref","first-page":"340","DOI":"10.1145\/174652.174658","article-title":"Reasoning about knowledge and probability","volume":"41","author":"Fagin Ronald","year":"1994","unstructured":"Ronald Fagin and Joseph Y Halpern . 1994 . Reasoning about knowledge and probability . Journal of the ACM (JACM) 41 , 2 (1994), 340 -- 367 . Ronald Fagin and Joseph Y Halpern. 1994. Reasoning about knowledge and probability. Journal of the ACM (JACM) 41, 2 (1994), 340--367.","journal-title":"Journal of the ACM (JACM)"},{"key":"e_1_3_2_1_9_1","volume-title":"2012 Ninth Int. Conf. on quantitative evaluation of systems. IEEE, 84--93","author":"Henriques David","year":"2012","unstructured":"David Henriques , Joao G Martins , Paolo Zuliani , Andr\u00e9 Platzer , and Edmund M Clarke . 2012 . Statistical model checking for Markov decision processes . In 2012 Ninth Int. Conf. on quantitative evaluation of systems. IEEE, 84--93 . David Henriques, Joao G Martins, Paolo Zuliani, Andr\u00e9 Platzer, and Edmund M Clarke. 2012. Statistical model checking for Markov decision processes. In 2012 Ninth Int. Conf. on quantitative evaluation of systems. IEEE, 84--93."},{"key":"e_1_3_2_1_10_1","volume-title":"International Workshop on Engineering Multi-Agent Systems. Springer, 109--130","author":"Herd Benjamin","year":"2015","unstructured":"Benjamin Herd , Simon Miles , Peter McBurney , and Michael Luck . 2015 . Quantitative analysis of multiagent systems through statistical model checking . In International Workshop on Engineering Multi-Agent Systems. Springer, 109--130 . Benjamin Herd, Simon Miles, Peter McBurney, and Michael Luck. 2015. Quantitative analysis of multiagent systems through statistical model checking. In International Workshop on Engineering Multi-Agent Systems. Springer, 109--130."},{"key":"e_1_3_2_1_11_1","volume-title":"International conference on runtime verification. Springer, 122--135","author":"Legay Axel","year":"2010","unstructured":"Axel Legay , Beno\u00eet Delahaye , and Saddek Bensalem . 2010 . Statistical model checking: An overview . In International conference on runtime verification. Springer, 122--135 . Axel Legay, Beno\u00eet Delahaye, and Saddek Bensalem. 2010. Statistical model checking: An overview. In International conference on runtime verification. Springer, 122--135."},{"key":"e_1_3_2_1_12_1","volume-title":"International Conference on Software Engineering and Formal Methods. Springer, 350--362","author":"Legay Axel","year":"2014","unstructured":"Axel Legay , Sean Sedwards , and Louis-Marie Traonouez . 2014 . Scalable verification of Markov decision processes . In International Conference on Software Engineering and Formal Methods. Springer, 350--362 . Axel Legay, Sean Sedwards, and Louis-Marie Traonouez. 2014. Scalable verification of Markov decision processes. In International Conference on Software Engineering and Formal Methods. Springer, 350--362."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"crossref","first-page":"9","DOI":"10.1007\/s10009-015-0378-x","article-title":"MCMAS: an open-source model checker for the verification of multi-agent systems","volume":"19","author":"Lomuscio Alessio","year":"2017","unstructured":"Alessio Lomuscio , Hongyang Qu , and Franco Raimondi . 2017 . MCMAS: an open-source model checker for the verification of multi-agent systems . Int. Jnl. on Software Tools for Tech. Transfer 19 , 1 (2017), 9 -- 30 . Alessio Lomuscio, Hongyang Qu, and Franco Raimondi. 2017. MCMAS: an open-source model checker for the verification of multi-agent systems. Int. Jnl. on Software Tools for Tech. Transfer 19, 1 (2017), 9--30.","journal-title":"Int. Jnl. on Software Tools for Tech. Transfer"},{"key":"e_1_3_2_1_14_1","volume-title":"2018 21st International Conference on Intelligent Transportation Systems (ITSC). 2575--2582","author":"Lopez Pablo Alvarez","year":"2018","unstructured":"Pablo Alvarez Lopez , Michael Behrisch , Laura Bieker-Walz , Jakob Erdmann , Yun-Pang Fl\u00f6tter\u00f6d , Robert Hilbrich , Leonhard L\u00fccken , Johannes Rummel , Peter Wagner , and Evamarie Wiessner . 2018 . Microscopic Traffic Simulation using SUMO . In 2018 21st International Conference on Intelligent Transportation Systems (ITSC). 2575--2582 . Pablo Alvarez Lopez, Michael Behrisch, Laura Bieker-Walz, Jakob Erdmann, Yun-Pang Fl\u00f6tter\u00f6d, Robert Hilbrich, Leonhard L\u00fccken, Johannes Rummel, Peter Wagner, and Evamarie Wiessner. 2018. Microscopic Traffic Simulation using SUMO. In 2018 21st International Conference on Intelligent Transportation Systems (ITSC). 2575--2582."},{"key":"e_1_3_2_1_15_1","first-page":"565","article-title":"Study on Static and Dynamic Traffic Control Systems","volume":"119","author":"Moganarangan N","year":"2018","unstructured":"N Moganarangan , N Balaji , RG Suresh Kumar , S Balaji , and N Palanivel . 2018 . Study on Static and Dynamic Traffic Control Systems . International Journal of Pure and Applied Mathematics 119 , 12 (2018), 565 -- 579 . N Moganarangan, N Balaji, RG Suresh Kumar, S Balaji, and N Palanivel. 2018. Study on Static and Dynamic Traffic Control Systems. International Journal of Pure and Applied Mathematics 119, 12 (2018), 565--579.","journal-title":"International Journal of Pure and Applied Mathematics"},{"key":"e_1_3_2_1_16_1","volume-title":"Sciammarella","author":"Nigro Libero","year":"2017","unstructured":"Libero Nigro and Paolo F . Sciammarella . 2017 . Statistical Model Checking Of Multi-Agent Systems. In European Conference on Modelling and Simulation, ECMS 2017, Budapest, Hungary, May 23-26, 2017, Proceedings. European Council for Modeling and Simulation , 11--17. Libero Nigro and Paolo F. Sciammarella. 2017. Statistical Model Checking Of Multi-Agent Systems. In European Conference on Modelling and Simulation, ECMS 2017, Budapest, Hungary, May 23-26, 2017, Proceedings. European Council for Modeling and Simulation, 11--17."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"crossref","first-page":"453","DOI":"10.1023\/A:1025007018583","article-title":"A knowledge based semantics of messages","volume":"12","author":"Parikh Rohit","year":"2003","unstructured":"Rohit Parikh and Ramaswamy Ramanujam . 2003 . A knowledge based semantics of messages . Journal of Logic, Language and Information 12 , 4 (2003), 453 -- 467 . Rohit Parikh and Ramaswamy Ramanujam. 2003. A knowledge based semantics of messages. Journal of Logic, Language and Information 12, 4 (2003), 453--467.","journal-title":"Journal of Logic, Language and Information"},{"key":"e_1_3_2_1_18_1","first-page":"167","article-title":"Verifying epistemic properties of multi-agent systems via bounded model checking","volume":"55","author":"Penczek Wojciech","year":"2003","unstructured":"Wojciech Penczek and Alessio Lomuscio . 2003 . Verifying epistemic properties of multi-agent systems via bounded model checking . Fundamenta Informaticae 55 , 2 (2003), 167 -- 185 . Wojciech Penczek and Alessio Lomuscio. 2003. Verifying epistemic properties of multi-agent systems via bounded model checking. Fundamenta Informaticae 55, 2 (2003), 167--185.","journal-title":"Fundamenta Informaticae"},{"key":"e_1_3_2_1_19_1","volume-title":"Proc. of the 14th Int. Conference on Agents and Artificial Intelligence, ICAART 2022","volume":"1","author":"Ramesh Yenda","year":"2022","unstructured":"Yenda Ramesh and M. V. Panduranga Rao . 2022. Statistical Model Checking for Probabilistic Temporal Epistemic Logics . In Proc. of the 14th Int. Conference on Agents and Artificial Intelligence, ICAART 2022 , Volume 1 , February 3-5, 2022 , Ana Paula Rocha, Luc Steels, and H. Jaap van den Herik (Eds.). SCITEPRESS, 53--63. Yenda Ramesh and M. V. Panduranga Rao. 2022. Statistical Model Checking for Probabilistic Temporal Epistemic Logics. In Proc. of the 14th Int. Conference on Agents and Artificial Intelligence, ICAART 2022, Volume 1, February 3-5, 2022, Ana Paula Rocha, Luc Steels, and H. Jaap van den Herik (Eds.). SCITEPRESS, 53--63."},{"key":"e_1_3_2_1_20_1","volume-title":"7th International Conference on Performance Evaluation Methodologies and Tools, ValueTools '13","author":"Sebastio Stefano","year":"2013","unstructured":"Stefano Sebastio and Andrea Vandin . 2013 . MultiVeStA: statistical model checking for discrete event simulators . In 7th International Conference on Performance Evaluation Methodologies and Tools, ValueTools '13 , Andr\u00e1s Horv\u00e1th, Peter Buchholz, Vittorio Cortellessa, Luca Muscariello, and Mark S. Squillante (Eds.). ICST\/ACM, 310--315. Stefano Sebastio and Andrea Vandin. 2013. MultiVeStA: statistical model checking for discrete event simulators. In 7th International Conference on Performance Evaluation Methodologies and Tools, ValueTools '13, Andr\u00e1s Horv\u00e1th, Peter Buchholz, Vittorio Cortellessa, Luca Muscariello, and Mark S. Squillante (Eds.). ICST\/ACM, 310--315."},{"key":"e_1_3_2_1_21_1","first-page":"1","article-title":"Bidirectionally Coupled Network and Road Traffic Simulation for Improved IVC Analysis","volume":"10","author":"Sommer Christoph","year":"2011","unstructured":"Christoph Sommer , Reinhard German , and Falko Dressler . 2011 . Bidirectionally Coupled Network and Road Traffic Simulation for Improved IVC Analysis . IEEE Transactions on Mobile Computing (TMC) 10 , 1 (January 2011), 3--15. Christoph Sommer, Reinhard German, and Falko Dressler. 2011. Bidirectionally Coupled Network and Road Traffic Simulation for Improved IVC Analysis. IEEE Transactions on Mobile Computing (TMC) 10, 1 (January 2011), 3--15.","journal-title":"IEEE Transactions on Mobile Computing (TMC)"},{"key":"e_1_3_2_1_22_1","volume-title":"2021 International Conference on COMmunication Systems & NETworkS (COMSNETS). IEEE, 404--412","author":"Thamilselvam B","year":"2021","unstructured":"B Thamilselvam , Subrahmanyam Kalyanasundaram , and MV Panduranga Rao . 2021 . Scalable coordinated intelligent traffic light controller for heterogeneous traffic scenarios using UPPAAL STRATEGO . In 2021 International Conference on COMmunication Systems & NETworkS (COMSNETS). IEEE, 404--412 . B Thamilselvam, Subrahmanyam Kalyanasundaram, and MV Panduranga Rao. 2021. Scalable coordinated intelligent traffic light controller for heterogeneous traffic scenarios using UPPAAL STRATEGO. In 2021 International Conference on COMmunication Systems & NETworkS (COMSNETS). IEEE, 404--412."},{"key":"e_1_3_2_1_23_1","volume-title":"Proceedings of the 1st international conference on Simulation tools and techniques for communications, networks and systems & workshops. 1--10","author":"Varga Andr\u00e1s","year":"2008","unstructured":"Andr\u00e1s Varga and Rudolf Hornig . 2008 . An overview of the OMNeT++ simulation environment . In Proceedings of the 1st international conference on Simulation tools and techniques for communications, networks and systems & workshops. 1--10 . Andr\u00e1s Varga and Rudolf Hornig. 2008. An overview of the OMNeT++ simulation environment. In Proceedings of the 1st international conference on Simulation tools and techniques for communications, networks and systems & workshops. 1--10."},{"key":"e_1_3_2_1_24_1","unstructured":"Georg Henrik Von Wright. 1951. An essay in modal logic. (1951).  Georg Henrik Von Wright. 1951. An essay in modal logic. (1951)."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1016\/j.knosys.2013.06.017","article-title":"Model checking epistemic-probabilistic logic using probabilistic interpreted systems","volume":"50","author":"Wan Wei","year":"2013","unstructured":"Wei Wan , Jamal Bentahar , and Abdessamad Ben Hamza . 2013 . Model checking epistemic-probabilistic logic using probabilistic interpreted systems . Knowledge-Based Systems 50 (2013), 279 -- 295 . Wei Wan, Jamal Bentahar, and Abdessamad Ben Hamza. 2013. Model checking epistemic-probabilistic logic using probabilistic interpreted systems. Knowledge-Based Systems 50 (2013), 279--295.","journal-title":"Knowledge-Based Systems"},{"key":"e_1_3_2_1_26_1","volume-title":"International Conference on Computer Aided Verification. Springer, 223--235","author":"Younes H\u00e5kan LS","year":"2002","unstructured":"H\u00e5kan LS Younes and Reid G Simmons . 2002 . Probabilistic verification of discrete event systems using acceptance sampling . In International Conference on Computer Aided Verification. Springer, 223--235 . H\u00e5kan LS Younes and Reid G Simmons. 2002. Probabilistic verification of discrete event systems using acceptance sampling. In International Conference on Computer Aided Verification. Springer, 223--235."},{"key":"e_1_3_2_1_27_1","volume-title":"10th Intl. Conf., TACAS","author":"Younes H\u00e5kan L. S.","year":"2004","unstructured":"H\u00e5kan L. S. Younes , Marta Z. Kwiatkowska , Gethin Norman , and David Parker . 2004. Numerical vs. Statistical Probabilistic Model Checking: An Empirical Study . In 10th Intl. Conf., TACAS 2004 , Joint European Conf.s on Theory and Practice of Software, ETAPS 2004, Barcelona, Spain, March 29 - April 2, 2004, Proc . 46--60. H\u00e5kan L. S. Younes, Marta Z. Kwiatkowska, Gethin Norman, and David Parker. 2004. Numerical vs. Statistical Probabilistic Model Checking: An Empirical Study. In 10th Intl. Conf., TACAS 2004, Joint European Conf.s on Theory and Practice of Software, ETAPS 2004, Barcelona, Spain, March 29 - April 2, 2004, Proc. 46--60."}],"event":{"name":"SAC '23: 38th ACM\/SIGAPP Symposium on Applied Computing","sponsor":["SIGAPP ACM Special Interest Group on Applied Computing"],"location":"Tallinn Estonia","acronym":"SAC '23"},"container-title":["Proceedings of the 38th ACM\/SIGAPP Symposium on Applied Computing"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3555776.3577720","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3555776.3577720","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T18:08:24Z","timestamp":1750183704000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3555776.3577720"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,3,27]]},"references-count":27,"alternative-id":["10.1145\/3555776.3577720","10.1145\/3555776"],"URL":"https:\/\/doi.org\/10.1145\/3555776.3577720","relation":{},"subject":[],"published":{"date-parts":[[2023,3,27]]},"assertion":[{"value":"2023-06-07","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}