Toward the Formalization of Macroscopic Models of Traffic Flow using Higher-order-logic Theorem Proving
IEEE Access, Vol. 8, pp. 27291–27307
Theorem Proving · HOL Light
A logical framework for the formal analysis of macroscopic traffic-flow models — capturing density, flow rate, and shockwave dynamics with the rigor of higher-order logic.
Abstract
Traditionally, traffic-flow analysis relies on data collection and simulation-based validation. As traffic infrastructure becomes more interconnected and automated, relying solely on simulation can miss anomalies that degrade mobility and safety. Higher-order-logic theorem proving overcomes the coverage limitations of simulation-based methods, and its soundness guarantees the correctness of results.
As a first step, we present a logical framework for the formal analysis of macroscopic traffic-flow models, formalizing foundational concepts — density, flow rate, mean speed, relative occupancy, and shockwave — using the HOL Light theorem prover. For illustration, we perform formal input-output and shockwave analysis of a German freeway.
Framework
People
Related Publications