Jove
Visualize
Contact Us
JoVE
x logofacebook logolinkedin logoyoutube logo
ABOUT JoVE
OverviewLeadershipBlogJoVE Help Center
AUTHORS
Publishing ProcessEditorial BoardScope & PoliciesPeer ReviewFAQSubmit
LIBRARIANS
TestimonialsSubscriptionsAccessResourcesLibrary Advisory BoardFAQ
RESEARCH
JoVE JournalMethods CollectionsJoVE Encyclopedia of ExperimentsArchive
EDUCATION
JoVE CoreJoVE BusinessJoVE Science EducationJoVE Lab ManualFaculty Resource CenterFaculty Site
Terms & Conditions of Use
Privacy Policy
Policies

Related Experiment Video

Updated: Dec 11, 2025

Evaluation of an Exclusive Spur Dike U-Turn Design with Radar-Collected Data and Simulation
11:41

Evaluation of an Exclusive Spur Dike U-Turn Design with Radar-Collected Data and Simulation

Published on: February 1, 2020

20.7K

Formal Verification of Heuristic Autonomous Intersection Management Using Statistical Model Checking.

Aaditya Prakash Chouhan1, Gourinath Banda1

  • 1Discipline of Computer Science and Engineering, Indian Institute of Technology Indore, Madhya Pradesh 453552, India.

Sensors (Basel, Switzerland)
|August 19, 2020
PubMed
Summary
This summary is machine-generated.

Related Concept Videos

Mechanistic Models: Compartment Models in Algorithms for Numerical Problem Solving01:29

Mechanistic Models: Compartment Models in Algorithms for Numerical Problem Solving

206
Mechanistic models play a crucial role in algorithms for numerical problem-solving, particularly in nonlinear mixed effects modeling (NMEM). These models aim to minimize specific objective functions by evaluating various parameter estimates, leading to the development of systematic algorithms. In some cases, linearization techniques approximate the model using linear equations.
In individual population analyses, different algorithms are employed, such as Cauchy's method, which uses a...
206
Statically Indeterminate Problem Solving01:16

Statically Indeterminate Problem Solving

616
Statically indeterminate problems are those where statics alone can not determine the internal forces or reactions. Consider a structure comprising two cylindrical rods made of steel and brass. These rods are joined at point B and restrained by rigid supports at points A and C. Now, the reactions at points A and C and the deflection at point B are to be determined. This rod structure is classified as statically indeterminate as the structure has more supports than are necessary for maintaining...
616
Mathematical Modeling: Problem Solving01:29

Mathematical Modeling: Problem Solving

166
Mathematical modeling transforms real-world scenarios into mathematical expressions, allowing for structured problem-solving and analysis. This process involves defining the situation, assigning variables to measurable quantities, selecting an appropriate model, and solving the resulting equation. Such models are invaluable in finance, providing precise methods to evaluate investments, loans, and repayment structures.A widely used example is the calculation of fixed monthly payments on a loan,...
166
Woodward–Hoffmann Selection Rules and Microscopic Reversibility01:34

Woodward–Hoffmann Selection Rules and Microscopic Reversibility

3.6K
Electrocyclic reactions, cycloadditions, and sigmatropic rearrangements are concerted pericyclic reactions that proceed via a cyclic transition state. These reactions are stereospecific and regioselective. The stereochemistry of the products depends on the symmetry characteristics of the interacting orbitals and the reaction conditions. Accordingly, pericyclic reactions are classified as either symmetry-allowed or symmetry-forbidden. Woodward and Hoffmann presented the selection criteria for...
3.6K
Heuristics01:21

Heuristics

453
Heuristics are problem-solving strategies that use mental shortcuts to simplify decision-making. Unlike algorithms, which must be followed precisely to achieve a correct result, heuristics offer a general problem-solving framework. They save time and energy but can sometimes lead to less rational decisions.
People often rely on heuristics when faced with an overload of information, limited time, low importance of the decision, limited information, or when a heuristic readily comes to mind. For...
453
Constraints and Statical Determinacy01:26

Constraints and Statical Determinacy

881
In structural engineering, the equilibrium of a system is not only determined by its equations of equilibrium but also with the help of constraints. Constraints refer to restrictions on the motion of a system. The proper combinations of constraints can minimize the total number of constraints needed to maintain a system in mechanical equilibrium. When this happens, the system is said to be statically determinate. For such systems, the unknown reaction supports can be estimated using equilibrium...
881

You might also read

Related Articles

Articles linked to this work by shared authors, journal, and citation graph.

Sort by
Same author

ElasticPay: Instant Peer-to-Peer Offline Extended Digital Payment System.

Sensors (Basel, Switzerland)·2025
Same author

A novel IoT-device management platform for on-the-fly generation of user interface <i>via</i> manifest-file addressing heterogeneity.

PeerJ. Computer science·2024
See all related articles

Statistical Model Checking (SMC) verifies autonomous vehicle safety. This study confirms the Heuristic Autonomous Intersection Management (HAIM) algorithm prevents collisions with high confidence.

Area of Science:

  • Robotics
  • Artificial Intelligence
  • Formal Methods

Background:

  • Autonomous vehicles (AVs) face consumer skepticism due to perceived safety concerns.
  • Formal verification techniques are crucial for establishing trust in AV technology but require further development.
  • Ensuring the safety and reliability of AV algorithms is paramount for widespread adoption.

Purpose of the Study:

  • To present Statistical Model Checking (SMC) as a viable method for verifying the safety of autonomous systems.
  • To apply SMC to the Heuristic Autonomous Intersection Management (HAIM) algorithm for safety verification.
  • To demonstrate a layered modeling and verification approach for autonomous intersection management algorithms.

Main Methods:

  • Formal modeling of the HAIM algorithm using a variant of Timed Automata.
Keywords:
autonomous vehiclescollision avoidanceheuristic algorithmintersection managementmodel checkinguppaal-SMC

More Related Videos

Evaluating the Effect of Roadside Parking on a Dual-Direction Urban Street
14:55

Evaluating the Effect of Roadside Parking on a Dual-Direction Urban Street

Published on: January 20, 2023

3.9K
Kinematic History of a Salient-recess Junction Explored through a Combined Approach of Field Data and Analog Sandbox Modeling
06:55

Kinematic History of a Salient-recess Junction Explored through a Combined Approach of Field Data and Analog Sandbox Modeling

Published on: August 5, 2016

8.4K

Related Experiment Videos

Last Updated: Dec 11, 2025

Evaluation of an Exclusive Spur Dike U-Turn Design with Radar-Collected Data and Simulation
11:41

Evaluation of an Exclusive Spur Dike U-Turn Design with Radar-Collected Data and Simulation

Published on: February 1, 2020

20.7K
Evaluating the Effect of Roadside Parking on a Dual-Direction Urban Street
14:55

Evaluating the Effect of Roadside Parking on a Dual-Direction Urban Street

Published on: January 20, 2023

3.9K
Kinematic History of a Salient-recess Junction Explored through a Combined Approach of Field Data and Analog Sandbox Modeling
06:55

Kinematic History of a Salient-recess Junction Explored through a Combined Approach of Field Data and Analog Sandbox Modeling

Published on: August 5, 2016

8.4K
  • Developing automata to represent vehicles, intersection managers (IM), and collision checkers.
  • Layered verification of the HAIM model, including implementation verification and error injection testing.

    • Main Results:

    • The study successfully applied SMC to verify the HAIM algorithm.
    • Layered verification confirmed the inherent behavior and correctness of the HAIM algorithm at each development stage.
    • Implementation verification and error injection testing ensured faithful system modeling.

    Conclusions:

    • Statistical Model Checking (SMC) provides a robust method for verifying the safety of autonomous intersection management algorithms.
    • The HAIM algorithm, when verified using SMC, demonstrates a high degree of confidence in collision-free operation.
    • The presented verification methodology is adaptable for other conflict-point-based autonomous intersection management systems.