SearcharxivSearch

arXiv subjects

Wen-Long Jin

Publications and source records attributed to Wen-Long Jin.

At least 19 recordsLinked to original sources

FASTRIC: Prompt Specification Language for Verifiable LLM Interactions

Large Language Models (LLMs) execute complex multi-turn interaction protocols but lack formal specifications to verify execution against designer intent. We introduce FASTRIC, a Prompt Specification Language that makes implicit Finite State Machines (FSMs) explicit in natural language prompts, enabling conformance verification through execution trace analysis. The LLM serves as intelligent execution agent: interpreting designer-encoded FSMs to execute specified behavioral roles. Unlike symbolic specification languages requiring parsers and compilers, FASTRIC leverages LLMs as unified infrastructure-simultaneously parser, interpreter, runtime environment, and development assistant. FASTRIC guides designers to articulate seven FSM elements (Final States, Agents, States, Triggers, Roles, Initial State, Constraints) structuring multi-turn interactions. Specification formality-ranging from implicit descriptions that frontier models infer to explicit step-by-step instructions for weaker models-serves as a design parameter. We introduce procedural conformance as verification metric measuring execution adherence to FSM specifications. Testing a 3-state kindergarten tutoring FSM across four formality levels and three model scales (14.7B, 685B, 1T+ parameters) reveals optimal specification formality is a function of model capacity. DeepSeek-V3.2 (685B) achieves perfect conformance (1.00) at L2-L4; ChatGPT-5 (~1T) peaks at L3 (0.90) before collapsing at L4 (0.39); Phi4 (14.7B) shows no stable optimum with high variance (SD=0.16-0.36). These findings reveal model-specific formality ranges-"Goldilocks zones"-where specifications provide sufficient structure without over-constraint, establishing Prompt Specification Engineering for creating verifiable interaction protocols, transforming multi-turn interaction design from heuristic art to systematic engineering with measurable procedural guarantees.

cs.CL

Provably safe and human-like car-following behaviors: Part 1. Analysis of phases and dynamics in standard models

Trajectory planning is essential for ensuring safe driving in the face of uncertainties related to communication, sensing, and dynamic factors such as weather, road conditions, policies, and other road users. Existing car-following models often lack rigorous safety proofs and the ability to replicate human-like driving behaviors consistently. This article applies multi-phase dynamical systems analysis to well-known car-following models to highlight the characteristics and limitations of existing approaches. We begin by formulating fundamental principles for safe and human-like car-following behaviors, which include zeroth-order principles for comfort and minimum jam spacings, first-order principles for speeds and time gaps, and second-order principles for comfort acceleration/deceleration bounds as well as braking profiles. From a set of these zeroth- and first-order principles, we derive Newell's simplified car-following model. Subsequently, we analyze phases within the speed-spacing plane for the stationary lead-vehicle problem in Newell's model and its extensions, which incorporate both bounded acceleration and deceleration. We then analyze the performance of the Intelligent Driver Model and the Gipps model. Through this analysis, we highlight the limitations of these models with respect to some of the aforementioned principles. Numerical simulations and empirical observations validate the theoretical insights. Finally, we discuss future research directions to further integrate safety, human-like behaviors, and vehicular automation in car-following models, which are addressed in Part 2 of this study \citep{jin2025WA20-02_Part2}, where we develop a novel multi-phase projection-based car-following model that addresses the limitations identified here.

eess.SY

Provably safe and human-like car-following behaviors: Part 2. A parsimonious multi-phase model with projected braking

Ensuring safe and human-like trajectory planning for automated vehicles amidst real-world uncertainties remains a critical challenge. While existing car-following models often struggle to consistently provide rigorous safety proofs alongside human-like acceleration and deceleration patterns, we introduce a novel multi-phase projection-based car-following model. This model is designed to balance safety and performance by incorporating bounded acceleration and deceleration rates while emulating key human driving principles. Building upon a foundation of fundamental driving principles and a multi-phase dynamical systems analysis (detailed in Part 1 of this study \citep{jin2025WA20-02_Part1}), we first highlight the limitations of extending standard models like Newell's with simple bounded deceleration. Inspired by human drivers' anticipatory behavior, we mathematically define and analyze projected braking profiles for both leader and follower vehicles, establishing safety criteria and new phase definitions based on the projected braking lead-vehicle problem. The proposed parsimonious model combines an extended Newell's model for nominal driving with a new control law for scenarios requiring projected braking. Using speed-spacing phase plane analysis, we provide rigorous mathematical proofs of the model's adherence to defined safe and human-like driving principles, including collision-free operation, bounded deceleration, and acceptable safe stopping distance, under reasonable initial conditions. Numerical simulations validate the model's superior performance in achieving both safety and human-like braking profiles for the stationary lead-vehicle problem. Finally, we discuss the model's implications and future research directions.

eess.SY

Monotone three-dimensional surface and equivalent formulations of the generalized bathtub model

In the Lighthill-Whitham-Richards (LWR) model for single-lane traffic, vehicle trajectories follow the first-in-first-out (FIFO) principle and can be represented by a monotone three-dimensional surface of cumulative vehicle count. In contrast, the generalized bathtub model, which describes congestion dynamics in transportation networks using relative space, typically violates the FIFO principle, making its representation more challenging. Building on the characteristic distance ordering concept, we observe that trips in the generalized bathtub model can be ordered by their characteristic distances (remaining trip distance plus network travel distance). We define a new cumulative number of trips ahead of a trip with a given remaining distance at a time instant, showing it forms a monotone three-dimensional surface despite FIFO violations. Using the inverse function theorem, we derive equivalent formulations with different coordinates and dependent variables, including special cases for Vickrey's bathtub model and the basic bathtub model. We demonstrate numerical methods based on these formulations and discuss trip-based approaches for discrete demand patterns. This study enhances understanding of the generalized bathtub model's properties, facilitating its application in network traffic flow modeling, congestion pricing, and transportation planning.

physics.soc-ph

A Control Theoretic Approach to Simultaneously Estimate Average Value of Time and Determine Dynamic Price for High-occupancy Toll Lanes

The dynamic pricing problem of a freeway corridor with high-occupancy toll (HOT) lanes was formulated and solved based on a point queue abstraction of the traffic system [Yin and Lou, 2009]. However, existing pricing strategies cannot guarantee that the closed-loop system converges to the optimal state, in which the HOT lanes' capacity is fully utilized but there is no queue on the HOT lanes, and a well-behaved estimation and control method is quite challenging and still elusive. This paper attempts to fill the gap by making three fundamental contributions: (i) to present a simpler formulation of the point queue model based on the new concept of residual capacity, (ii) to propose a simple feedback control theoretic approach to estimate the average value of time and calculate the dynamic price, and (iii) to analytically and numerically prove that the closed-loop system is stable and guaranteed to converge to the optimal state, in either Gaussian or exponential manners.

eess.SY

Stable dynamic pricing scheme independent of lane-choice models for high-occupancy-toll lanes

A stable dynamic pricing scheme is essential to guarantee the desired performance of high-occupancy-toll (HOT) lanes, where single-occupancy vehicles (SOVs) can pay a price to use the HOT lanes. But existing methods apply to either only one type of lane-choice models with unknown parameters or different types of lane-choice models but with known parameters. In this study we present a new dynamic pricing scheme that is stable and applies to different types of lane-choice models with unknown parameters. There are two operational objectives for operating HOT lanes: (i) to maintain the free-flow condition to guarantee the travel time reliability; and (ii) to maximize the HOT lanes' throughput to minimize the system's total delay. The traffic dynamics on both HOT and general purpose (GP) lanes are described by point queue models, where the queueing times are determined by the demands and capacities. We consider three types of lane-choice models: the multinomial logit model when SOVs share the same value of time, the vehicle-based user equilibrium model when SOVs' values of time are heterogeneous and follow a distribution, and a general lane-choice model. We demonstrate that the second objective is approximately equivalent to the social welfare optimization principle for the logit model. Observing that the dynamic price and the excess queueing time on the GP lanes are linearly correlated in all the lane-choice models, we propose a feedback control method to determine the dynamic prices based on two integral controllers. We further present a method to estimate the parameters of a lane-choice model once its type is known. Analytically we prove that the equilibrium state of the closed-loop system with constant demand patterns is ideal, since the two objectives are achieved in it, and that it is asymptotically stable. With numerical examples we verify the effectiveness of the solution method.

eess.SY

Dynamic distance-based pricing scheme for high-occupancy-toll lanes along a freeway corridor

Single-occupancy vehicles (SOVs) are charged to use the highoccupancy-toll (HOT) lanes, while high-occupancy-vehicles (HOVs) can drive in them at no cost. The pricing scheme for HOT lanes has been extensively studied at local bottlenecks or at the network level through computationally expensive simulations. However, the HOT lane pricing study on a freeway corridor with multiple origins and destinations as well as multiple interacting bottlenecks is a challenging problem for which no analytical results are available. In this paper, we attempt to fill the gap by proposing to study the traffic dynamics in the corridor based on the relative space paradigm. In this new paradigm, the interaction of multiple bottlenecks and trips can be captured with Vickrey's bathtub model by a simple ordinary differential equation. We consider three types of lane choice behavior and analyze their properties. Then, we propose a distance-based dynamic pricing scheme based on a linear combination of I-controllers. This closed-loop controller is independent of the model and feeds back the travel time difference between HOT lanes and general-purpose lanes. Given the mathematical tractability of the system model, we analytically study the performance of the proposed closed-loop control under constant demand and show the existence and stability of the optimal equilibrium. Finally, we verify the results with numerical simulations considering a typical peak period demand pattern. In the future, we are interested in extending this work and testing the performance of the proposed linear combination of I-controllers for other traffic flow models.

eess.SY

Generalized bathtub model of network trip flows

In this study, we present a unified framework for modeling network trip flows with general distributions of trip distances, including negative exponential, constant, and regularly sorting trip distances studied in the literature. In addition to tracking the number of active trips as in Vickrey's model, this model also tracks the evolution of the distribution of active trips' remaining distances. We derive four equivalent differential formulations from the network fundamental diagram and the conservation law of trips for the number of active trips with remaining distances not smaller than any value. Then we define and discuss the properties of stationary and gridlock states, derive the integral form of the bathtub model with the characteristic method, obtain equivalent formulations by replacing the time coordinate with the cumulative travel distance, and present two numerical methods to solve the bathtub model based on the differential and integral forms respectively. We further study equivalent formulations and solutions for two special types of distributions of trip distances: time-independent negative exponential or deterministic. In particular, we present six equivalent conditions for Vickrey's bathtub model to be applicable. Finally we demonstrate that the fundamental diagram and the bathtub model can be extended for multi-commodity trip flows with trips served by mobility service vehicles.

math.DS

On the global stability of departure time user equilibrium: A Lyapunov approach

In (Jin, 2018), a new day-to-day dynamical system was proposed for drivers' departure time choice at a single bottleneck. Based on three behavioral principles, the nonlocal departure and arrival times choice problems were converted to the local scheduling payoff choice problem, whose day-to-day dynamics are described by the Lighthill-Whitham-Richards (LWR) model on an imaginary road of increasing scheduling payoff. Thus the departure time user equilibrium (DTUE), the arrival time user equilibrium (ATUE), and the scheduling payoff user equilibrium (SPUE) are uniquely determined by the stationary state of the LWR model, which was shown to be locally, asymptotically stable with analysis of the discrete approximation of the LWR model and through a numerical example. In this study attempt to analytically prove the global stability of the SPUE, ATUE, and DTUE. We first generalize the conceptual models for arrival time and scheduling payoff choices developed in (Jin, 2018) for a single bottleneck with a generalized scheduling cost function, which includes the cost of the free-flow travel time. Then we present the LWR model for the day-to-day dynamics for the scheduling payoff choice as well as the SPUE. We further formulate a new optimization problem for the SPUE and demonstrate its equivalent to the optimization problem for the ATUE in (Iryo and Yoshii, 2007). Finally we show that the objective functions in the two optimization formulations are equal and can be used as the potential function for the LWR model and prove that the stationary state of the LWR model, and therefore, the SPUE, DTUE, and ATUE, are globally, asymptotically stable, by using Lyapunov's second method. Such a globally stable behavioral model can provide more efficient departure time and route choice guidance for human drivers and connected and autonomous vehicles in more complicated networks.

math.OC

Stable day-to-day dynamics for departure time choice

In this paper we present a stable day-to-day dynamical system for drivers' departure time choice at a single bottleneck. We first define within-day traffic dynamics with the point queue model, costs, the departure time user equilibrium (DTUE), and the arrival time user equilibrium (ATUE). We then identify three behavioral principles: (i) Drivers choose their departure and arrival times in a backward fashion (backward choice principle); (ii) After choosing the arrival times, they update their departure times to balance the total costs (cost balancing principle); (iii) They choose their arrival times to reduce their scheduling costs or gain their scheduling payoffs (scheduling cost reducing or scheduling payoff gaining principle). In this sense, drivers' departure and arrival time choices are driven by their scheduling payoff choice. With a single tube or imaginary road model, we convert the nonlocal day-to-day arrival time shifting problem to a local scheduling payoff shifting problem. After introducing a new variable for the imaginary density, we apply the Lighthill-Whitham-Richards (LWR) model to describe the day-to-day dynamics of scheduling payoff choice and present splitting and cost balancing schemes to determine arrival and departure flow-rates accordingly. We also develop the corresponding discrete models for numerical solutions. We theoretically prove that the day-to-day stationary state of the LWR model leads to the scheduling payoff user equilibrium (SPUE), which is equivalent to both DTUE and ATUE and stable. We use one numerical example to demonstrate the effectiveness and stability of the new day-to-day dynamical model.

math.OC

Nonstandard second-order formulation of the LWR model

We present a second-order formulation of the LWR model based on Phillips' model (Phillips, 1979); but the model is nonstandard with a hyperreal infinitesimal relaxation time. Since the original Phillips model is unstable with three different definitions of stability in both Eulerian and Lagrangian coordinates, we cannot use traditional methods to prove the equivalence between the second-order model, which can be considered the zero-relaxation limit of Phillips' model, and the LWR model, which is the equilibrium counterpart of Phillips' model. Instead, we resort to a nonstandard method based on the equivalence relationship between second-order continuum and car-following models established in (Jin, 2016) and prove that the nonstandard model and the LWR model are equivalent, since they have the same anisotropic car-following model and stability property. We further derive conditions for the nonstandard model to be forward-traveling and collision-free, prove that the collision-free condition is consistent with but more general than the CFL condition (Courant et al., 1928), and demonstrate that only anisotropic and symplectic Euler discretization methods lead to physically meaningful solutions. We numerically solve the lead-vehicle problem and show that the nonstandard second-order model has the same shock and rarefaction wave solutions as the LWR model for both Greenshields and triangular fundamental diagrams; for a non-concave fundamental diagram we show that the collision-free condition, but not the CFL condition, yields physically meaningful results. Finally we present a correction method to eliminate negative speeds and collisions in general second-order models, and verify the method with a numerical example.

math.AP

Performance analysis and signal design for a stationary signalized ring road

Existing methods for traffic signal design are either too simplistic to capture realistic traffic characteristics or too complicated to be mathematically tractable. In this study, we attempts to fill the gap by presenting a new method based on the LWR model for performance analysis and signal design in a stationary signalized ring road. We first solve the link transmission model to obtain an equation for the boundary flow in stationary states, which are defined to be time-periodic solutions in both flow-rate and density with a period of the cycle length. We then derive an explicit macroscopic fundamental diagram (MFD), in which the average flow-rate in stationary states is a function of both traffic density and signal settings. Finally we present simple formulas for optimal cycle lengths under five levels of congestion with a start-up lost time. With numerical examples we verify our analytical results and discuss the existence of near-optimal cycle lengths. This study lays the foundation for future studies on performance analysis and signal design for more general urban networks based on the kinematic wave theory.

math.DS

Analysis of traffic statics and dynamics in a signalized double-ring network: A Poincaré map approach

Understanding traffic statics and dynamics in urban networks is critical to develop effective control and management strategies. In this paper, we provide a novel approach to study the traffic statics and dynamics in a signalized double-ring network, which can provide insights into the operation of more general signalized traffic networks. Under the framework of the link queue model (LQM) and the assumption of a triangular traffic flow fundamental diagram, the signalized double-ring network is studied as a switched affine system. Due to periodic signal regulations, periodic density evolution orbits are formed and defined as stationary states. A Poincaré map approach is introduced to analyze the properties of such stationary states. With short cycle lengths, closed-form Poincaré maps are derived. Stationary states and their stability properties are obtained by finding and analyzing the fixed points on the Poincaré maps. It is found that a stationary state can be asymptotically stable, Lyapunov stable, or unstable. The impacts of retaining ratios and initial densities on the macroscopic fundamental diagrams (MFDs) and the gridlock times are analyzed. Multivaluedness and gridlock phenomena as well as the unstable branch with non-zero average network flow-rates are observed on the MFDs. With long cycle lengths, fixed points on the Poincaré maps are solved numerically, and the obtained stationary states and the MFDs are very similar to those with short cycle lengths. Compared with earlier studies, this paper provides an analytical framework that can be used to provide complete and closed-form solutions to the statics and dynamics of double-ring networks. This can lead to a better understanding of how the combination of signalized intersections and turning maneuvers is expected to impact network properties, like the MFD.

math.DS

On the equivalence between continuum and car-following models of traffic flow

Recently different formulations of the first-order Lighthill-Whitham-Richards (LWR) model have been identified in different coordinates and state variables. However, there exists no systematic method to convert higher-order continuum models into car-following models and vice versa. In this study we propose a simple method to enable systematic conversions between higher-order continuum and car-following models in two steps: equivalent transformations of variables between Eulerian and Lagrangian coordinates, and finite difference approximations of first-order derivatives in Lagrangian coordinates. With the method, we derive higher-order continuum models from a number of well-known car-following models. We also derive car-following models from higher-order continuum models. For general second-order models, we demonstrate that the car-following and continuum formulations share the same fundamental diagram, but the string stability condition of a car-following model is different from the linear stability condition of a continuum model. This study reveals relationships between many existing models and also leads to a number of new models.

math.AP

Point queue models: a unified approach

In transportation and other types of facilities, various queues arise when the demands of service are higher than the supplies, and many point and fluid queue models have been proposed to study such queueing systems. However, there has been no unified approach to deriving such models, analyzing their relationships and properties, and extending them for networks. In this paper, we derive point queue models as limits of two link-based queueing model: the link transmission model and a link queue model. With two definitions for demand and supply of a point queue, we present four point queue models, four approximate models, and their discrete versions. We discuss the properties of these models, including equivalence, well-definedness, smoothness, and queue spillback, both analytically and with numerical examples. We then analytically solve Vickrey's point queue model and stationary states in various models. We demonstrate that all existing point and fluid queue models in the literature are special cases of those derived from the link-based queueing models. Such a unified approach leads to systematic methods for studying the queueing process at a point facility and will also be helpful for studies on stochastic queues as well as networks of queues.

math.DS

Continuous formulations and analytical properties of the link transmission model

The link transmission model (LTM) has great potential for simulating traffic flow in large-scale networks since it is much more efficient and accurate than the Cell Transmission Model (CTM). However, there lack general continuous formulations of LTM, and there has been no systematic study on its analytical properties such as stationary states and stability of network traffic flow. In this study we attempt to fill the gaps. First we apply the Hopf-Lax formula to derive Newell's simplified kinematic wave model with given boundary cumulative flows and the triangular fundamental diagram. We then apply the Hopf-Lax formula to define link demand and supply functions, as well as link queue and vacancy functions, and present two continuous formulations of LTM, by incorporating boundary demands and supplies as well as invariant macroscopic junction models. With continuous LTM, we define and solve the stationary states in a road network. We also apply LTM to directly derive a Poincaré map to analyze the stability of stationary states in a diverge-merge network. Finally we present an example to show that LTM is not well-defined with non-invariant junction models. We can see that Newell's model and LTM complement each other and provide an alternative formulation of the network kinematic wave model. This study paves the way for further extensions, analyses, and applications of LTM in the future.

math.DS

Control of a lane-drop bottleneck through variable speed limits

In this study, we formulate the VSL control problem for the traffic system in a zone upstream to a lane-drop bottleneck based on two traffic flow models: the Lighthill-Whitham-Richards (LWR) model, which is an infinite-dimensional partial differential equation, and the link queue model, which is a finite-dimensional ordinary differential equation. In both models, the discharging flow-rate is determined by a recently developed model of capacity drop, and the upstream in-flux is regulated by the speed limit in the VSL zone. Since the link queue model approximates the LWR model and is much simpler, we first analyze the control problem and develop effective VSL strategies based on the former. First for an open-loop control system with a constant speed limit, we prove that a constant speed limit can introduce an uncongested equilibrium state, in addition to a congested one with capacity drop, but the congested equilibrium state is always exponentially stable. Then we apply a feedback proportional-integral (PI) controller to form a closed-loop control system, in which the congested equilibrium state and, therefore, capacity drop can be removed by the I-controller. Both analytical and numerical results show that, with appropriately chosen controller parameters, the closed-loop control system is stable, effect, and robust. Finally, we show that the VSL strategies based on I- and PI-controllers are also stable, effective, and robust for the LWR model. Since the properties of the control system are transferable between the two models, we establish a dual approach for studying the control problems of nonlinear traffic flow systems. We also confirm that the VSL strategy is effective only if capacity drop occurs. The obtained method and insights can be useful for future studies on other traffic control methods and implementations of VSL strategies.

math.OC

A kinematic wave theory of capacity drop

Capacity drop at active bottlenecks is one of the most puzzling traffic phenomena, but a thorough understanding is practically important for designing variable speed limit and ramp metering strategies. In this study, we attempt to develop a simple model of capacity drop within the framework of kinematic wave theory based on the observation that capacity drop occurs when an upstream queue forms at an active bottleneck. In addition, we assume that the fundamental diagrams are continuous in steady states. This assumption is consistent with observations and can avoid unrealistic infinite characteristic wave speeds in discontinuous fundamental diagrams. A core component of the new model is an entropy condition defined by a discontinuous boundary flux function. For a lane-drop area, we demonstrate that the model is well-defined, and its Riemann problem can be uniquely solved. We theoretically discuss traffic stability with this model subject to perturbations in density, upstream demand, and downstream supply. We clarify that discontinuous flow-density relations, or so-called "discontinuous" fundamental diagrams, are caused by incomplete observations of traffic states. Theoretical results are consistent with observations in the literature and are verified by numerical simulations and empirical observations. We finally discuss potential applications and future studies.

math-ph