{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,28]],"date-time":"2026-07-28T13:39:02Z","timestamp":1785245942526,"version":"3.55.0"},"reference-count":43,"publisher":"MDPI AG","issue":"3","license":[{"start":{"date-parts":[[2021,6,25]],"date-time":"2021-06-25T00:00:00Z","timestamp":1624579200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/V026801"],"award-info":[{"award-number":["EP\/V026801"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["JSAN"],"abstract":"<jats:p>Usually, the design of an Autonomous Vehicle (AV) does not take into account traffic rules and so the adoption of these rules can bring some challenges, e.g., how to come up with a Digital Highway Code which captures the proper behaviour of an AV against the traffic rules and at the same time minimises changes to the existing Highway Code? Here, we formally model and implement three Road Junction rules (from the UK Highway Code). We use timed automata to model the system and the MCAPL (Model Checking Agent Programming Language) framework to implement an agent and its environment. We also assess the behaviour of our agent according to the Road Junction rules using a double-level Model Checking technique, i.e., UPPAAL at the design level and AJPF (Agent Java PathFinder) at the development level. We have formally verified 30 properties (18 with UPPAAL and 12 with AJPF), where these properties describe the agent\u2019s behaviour against the three Road Junction rules using a simulated traffic scenario, including artefacts like traffic signs and road users. In addition, our approach aims to extract the best from the double-level verification, i.e., using time constraints in UPPAAL timed automata to determine thresholds for the AVs actions and tracing the agent\u2019s behaviour by using MCAPL, in a way that one can tell when and how a given Road Junction rule was selected by the agent. This work provides a proof-of-concept for the formal verification of AV behaviour with respect to traffic rules.<\/jats:p>","DOI":"10.3390\/jsan10030041","type":"journal-article","created":{"date-parts":[[2021,6,27]],"date-time":"2021-06-27T23:57:22Z","timestamp":1624838242000},"page":"41","update-policy":"https:\/\/doi.org\/10.3390\/mdpi_crossmark_policy","source":"Crossref","is-referenced-by-count":19,"title":["A Double-Level Model Checking Approach for an Agent-Based Autonomous Vehicle and Road Junction Regulations"],"prefix":"10.3390","volume":"10","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5937-8193","authenticated-orcid":false,"given":"Gleifer Vaz","family":"Alves","sequence":"first","affiliation":[{"name":"Graduate Program in Computer Science (PPGCC), Federal University of Technology\u2014Parana (UTFPR), Ponta Grossa 84017-220, PR, Brazil"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1426-1896","authenticated-orcid":false,"given":"Louise","family":"Dennis","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Manchester, Manchester M13 9PL, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0875-3862","authenticated-orcid":false,"given":"Michael","family":"Fisher","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Manchester, Manchester M13 9PL, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"1968","published-online":{"date-parts":[[2021,6,25]]},"reference":[{"key":"ref_1","unstructured":"Avary, M., and Dawkins, T. (2020). Safe Drive Initiative: Creating Safe Autonomous Vehicle Policy, World Economic Forum."},{"key":"ref_2","doi-asserted-by":"crossref","first-page":"341","DOI":"10.1007\/s10506-017-9210-0","article-title":"On the problem of making autonomous vehicles conform to traffic law","volume":"25","author":"Prakken","year":"2017","journal-title":"Artif. Intell. Law"},{"key":"ref_3","unstructured":"Alves, G.V., Dennis, L., and Fisher, M. (2018, January 18\u201319). Formalisation of the Rules of the Road for embedding into an Autonomous Vehicle Agent. Proceedings of the International Workshop on Verification and Validation of Autonomous Systems, Oxford, UK."},{"key":"ref_4","unstructured":"Sekerinski, E., Moreira, N., Oliveira, J.N., Ratiu, D., Guidotti, R., Farrell, M., Luckcuck, M., Marmsoler, D., Campos, J., and Astarte, T. (2020). Formalisation and Implementation of Road Junction Rules on an Autonomous Vehicle Modelled as an Agent. International Symposium on Formal Methods, Springer International Publishing. Lecture Notes in Computer Science."},{"key":"ref_5","unstructured":"Philipp, R., Wittmann, D., Knobel, C., Weast, J., Garbacik, N., and Schnetter, P. (2019). Safety First for Automated Driving, Daimler AG."},{"key":"ref_6","unstructured":"Law Commission, U. (2020). Automated Vehicles: Summary of the Analysis of Responses to Consultation Paper 2 on Passenger Services and Public Transport, Law Commission."},{"key":"ref_7","unstructured":"The British Standards Institution (2020). PAS 1882 Data Collection and Management for Automated Vehicle Trials, The British Standards Institution."},{"key":"ref_8","unstructured":"Waymo (2020). Safety Report, Waymo LLC. Available online: https:\/\/waymo.com\/safety."},{"key":"ref_9","unstructured":"Department for Transport (2021, June 23). Using the Road (159 to 203)\u2014The Highway Code\u2014 Guidance\u2014GOV.UK, Available online: https:\/\/www.gov.uk\/guidance\/the-highway-code\/using-the-road-159-to-203."},{"key":"ref_10","doi-asserted-by":"crossref","unstructured":"Rizaldi, A., Keinholz, J., Huber, M., Feldle, J., Immler, F., Althoff, M., Hilgendorf, E., and Nipkow, T. (2017, January 20\u201322). Formalising and Monitoring Traffic Rules for Autonomous Vehicles in Isabelle\/HOL. Proceedings of the 13th International Conference on Integrated Formal Methods, Turin, Italy.","DOI":"10.1007\/978-3-319-66845-1_4"},{"key":"ref_11","doi-asserted-by":"crossref","unstructured":"Bhuiyan, H., Governatori, G., Rakotonirainy, A., Bond, A., Demmel, S., and Islam, M.B. (2020). Traffic Rules Encoding Using Defeasible Deontic Logic, IOS Press.","DOI":"10.3233\/FAIA200844"},{"key":"ref_12","doi-asserted-by":"crossref","first-page":"88","DOI":"10.1016\/j.scico.2017.05.006","article-title":"Formal Verification of Autonomous Vehicle Platooning","volume":"148","author":"Kamali","year":"2017","journal-title":"Sci. Comput. Program."},{"key":"ref_13","doi-asserted-by":"crossref","unstructured":"Al-Nuaimi, M., Qu, H., and Veres, S.M. (2018, January 21\u201324). Computational Framework for Verifiable Decisions of Self-Driving Vehicles. Proceedings of the 2018 IEEE Conference on Control Technology and Applications (CCTA), Copenhagen, Denmark.","DOI":"10.1109\/CCTA.2018.8511432"},{"key":"ref_14","doi-asserted-by":"crossref","first-page":"1251","DOI":"10.1007\/s10489-017-1112-z","article-title":"Agent systems verification: Systematic literature review and mapping","volume":"48","author":"Bakar","year":"2018","journal-title":"Appl. Intell."},{"key":"ref_15","unstructured":"Dennis, L.A. (2017). Gwendolen Semantics: 2017, Department of Computer Science, University of Liverpool. Technical Report ULCS-17-001."},{"key":"ref_16","doi-asserted-by":"crossref","unstructured":"Alur, R., Henzinger, T.A., and Sontag, E.D. (1996). UPPAAL\u2014A tool suite for automatic verification of real-time systems. Hybrid Systems III, Springer. Number 1066 in Lecture Notes in Computer Science.","DOI":"10.1007\/BFb0020931"},{"key":"ref_17","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1007\/s10515-011-0088-x","article-title":"Model Checking Agent Programming Languages","volume":"19","author":"Dennis","year":"2012","journal-title":"Autom. Softw. Eng."},{"key":"ref_18","doi-asserted-by":"crossref","first-page":"305","DOI":"10.1007\/s10515-014-0168-9","article-title":"Practical Verification of Decision-Making in Agent-Based Autonomous Systems","volume":"23","author":"Dennis","year":"2016","journal-title":"Autom. Softw. Eng."},{"key":"ref_19","doi-asserted-by":"crossref","first-page":"152","DOI":"10.1007\/978-3-030-51417-4_8","article-title":"The \u201cWhy Did You Do That?\u201d Button: Answering Why-Questions for End Users of Robotic Systems","volume":"12058","author":"Koeman","year":"2019","journal-title":"Lect. Notes Comput. Sci."},{"key":"ref_20","doi-asserted-by":"crossref","unstructured":"Leitner, A., Watzenig, D., and Ibanez-Guzman, J. (2020). Reliable Decision-Making in Autonomous Vehicles. Validation and Verification of Automated Systems: Results of the ENABLE-S3 Project, Springer International Publishing.","DOI":"10.1007\/978-3-030-14628-3"},{"key":"ref_21","doi-asserted-by":"crossref","first-page":"35","DOI":"10.4204\/EPTCS.257.5","article-title":"A Rational Agent Controlling an Autonomous Vehicle: Implementation and Formal Verification","volume":"257","author":"Fernandes","year":"2017","journal-title":"Electron. Proc. Theor. Comput. Sci."},{"key":"ref_22","doi-asserted-by":"crossref","first-page":"591","DOI":"10.1613\/jair.2502","article-title":"A Multiagent Approach to Autonomous Intersection Management","volume":"31","author":"Dresner","year":"2008","journal-title":"J. Artif. Intell. Res."},{"key":"ref_23","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1016\/j.tcs.2018.05.028","article-title":"An abstract model for proving safety of autonomous urban traffic","volume":"744","author":"Schwammberger","year":"2018","journal-title":"Theor. Comput. Sci."},{"key":"ref_24","doi-asserted-by":"crossref","unstructured":"Herrmann, A., Brenner, W., and Stadler, R. (2018). Autonomous Driving: How the Driverless Revolution Will Change the World, Emerald Publishing. [1st ed.].","DOI":"10.1108\/9781787148338"},{"key":"ref_25","unstructured":"Nigeria, H.C. (2021, June 23). Nigeria Highway Code\u2014III. ROAD JUNCTIONS. Available online: http:\/\/www.highwaycode.com.ng\/iii-road-junctions.html."},{"key":"ref_26","doi-asserted-by":"crossref","unstructured":"Fisher, M. (2011). An Introduction to Practical Formal Methods Using Temporal Logic, Wiley.","DOI":"10.1002\/9781119991472"},{"key":"ref_27","unstructured":"Baier, C., and Katoen, J.P. (2008). Principles of Model Checking (Representation and Mind Series), The MIT Press."},{"key":"ref_28","unstructured":"Bratman, M.E. (1987). Intentions, Plans, and Practical Reason, Harvard University Press."},{"key":"ref_29","doi-asserted-by":"crossref","unstructured":"El Fallah Seghrouchni, A., Dix, J., Dastani, M., and Bordini, R.H. (2009). Programming Rational Agents in GOAL. Multi-Agent Programming: Languages, Tools and Applications, Springer.","DOI":"10.1007\/978-0-387-89299-3"},{"key":"ref_30","doi-asserted-by":"crossref","unstructured":"Visser, W., Havelund, K., Brat, G., and Park, S. (2000, January 11\u201315). Model Checking Programs. Proceedings of the 15th IEEE International Conference Automated Software Engineering (ASE), Grenoble, France.","DOI":"10.1109\/ASE.2000.873645"},{"key":"ref_31","doi-asserted-by":"crossref","unstructured":"Bordini, R.H., H\u00fcbner, J.F., and Wooldridge, M. (2007). Programming Multi-Agent Systems in AgentSpeak Using Jason (Wiley Series in Agent Technology), John Wiley & Sons, Inc.","DOI":"10.1002\/9780470061848"},{"key":"ref_32","doi-asserted-by":"crossref","first-page":"499","DOI":"10.1093\/logcom\/exv002","article-title":"Two-Stage Agent Program Verification","volume":"28","author":"Dennis","year":"2018","journal-title":"J. Log. Comput."},{"key":"ref_33","first-page":"100:1","article-title":"Formal Specification and Verification of Autonomous Robotic Systems: A Survey","volume":"52","author":"Luckcuck","year":"2019","journal-title":"ACM Comput. Surv."},{"key":"ref_34","doi-asserted-by":"crossref","unstructured":"Althoff, M., Althoff, D., Wollherr, D., and Buss, M. (2010, January 21\u201324). Safety verification of autonomous vehicles for coordinated evasive maneuvers. Proceedings of the 2010 IEEE Intelligent Vehicles Symposium, San Diego, CA, USA.","DOI":"10.1109\/IVS.2010.5548121"},{"key":"ref_35","doi-asserted-by":"crossref","first-page":"1170","DOI":"10.1109\/TRO.2007.909810","article-title":"Decentralized Cooperative Policy for Conflict Resolution in Multivehicle Systems","volume":"23","author":"Pallottino","year":"2007","journal-title":"IEEE Trans. Robot."},{"key":"ref_36","doi-asserted-by":"crossref","unstructured":"He\u00df, D., Althoff, M., and Sattel, T. (2014, January 14\u201318). Formal verification of maneuver automata for parameterized motion primitives. Proceedings of the 2014 IEEE\/RSJ International Conference on Intelligent Robots and Systems, Chicago, IL, USA.","DOI":"10.1109\/IROS.2014.6942751"},{"key":"ref_37","doi-asserted-by":"crossref","first-page":"65","DOI":"10.1109\/MRA.2011.942116","article-title":"Correct, Reactive, High-Level Robot Control","volume":"18","author":"Wongpiromsarn","year":"2011","journal-title":"IEEE Robot. Autom. Mag."},{"key":"ref_38","doi-asserted-by":"crossref","unstructured":"Pek, C., Zahn, P., and Althoff, M. (2017, January 11\u201314). Verifying the safety of lane change maneuvers of self-driving vehicles based on formalized traffic rules. Proceedings of the 2017 IEEE Intelligent Vehicles Symposium (IV), Redondo Beach, CA, USA.","DOI":"10.1109\/IVS.2017.7995918"},{"key":"ref_39","unstructured":"Quigley, M., Conley, K., Gerkey, B.P., Faust, J., Foote, T., Leibs, J., Wheeler, R., and Ng, A.Y. (2009, January 12\u201317). ROS: An Open-source Robot Operating System. Proceedings of the ICRA Workshop on Open Source Software, Kobe, Japan."},{"key":"ref_40","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1016\/j.jpdc.2017.10.019","article-title":"Internet of agents framework for connected vehicles: A case study on distributed traffic control system","volume":"116","author":"Bui","year":"2018","journal-title":"J. Parallel Distrib. Comput."},{"key":"ref_41","doi-asserted-by":"crossref","unstructured":"Alouache, L., Nguyen, N., Aliouat, M., and Chelouah, R. (2018, January 23\u201326). Toward a hybrid SDN architecture for V2V communication in IoV environment. Proceedings of the 2018 Fifth International Conference on Software Defined Systems (SDS), Barcelona, Spain.","DOI":"10.1109\/SDS.2018.8370428"},{"key":"ref_42","doi-asserted-by":"crossref","first-page":"1038","DOI":"10.1016\/j.future.2019.09.016","article-title":"Agent-based Internet of Things: State-of-the-art and research challenges","volume":"102","author":"Savaglio","year":"2020","journal-title":"Future Gener. Comput. Syst."},{"key":"ref_43","unstructured":"Alves, G.V., Dennis, L., and Fisher, M. (2020, January 30). First Steps towards an Ethical Agent for Checking Decision and Behaviour for an Autonomous Vehicle on the Rules of the Road. Proceedings of the Second Workshop on Implementing Machine Ethics, Dublin, Ireland."}],"container-title":["Journal of Sensor and Actuator Networks"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.mdpi.com\/2224-2708\/10\/3\/41\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T06:24:19Z","timestamp":1760163859000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.mdpi.com\/2224-2708\/10\/3\/41"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,6,25]]},"references-count":43,"journal-issue":{"issue":"3","published-online":{"date-parts":[[2021,9]]}},"alternative-id":["jsan10030041"],"URL":"https:\/\/doi.org\/10.3390\/jsan10030041","relation":{},"ISSN":["2224-2708"],"issn-type":[{"value":"2224-2708","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,6,25]]}}}