1.2.2: Formal model#
In a nutshell
A conceptual model written in natural language is unavoidably ambiguous: two people reading the same description can implement it differently and get different results. This page answers how we remove that ambiguity, by turning the narrative into precise rules that fix exactly what each entity does, when it acts, and how the entities interact.
The formal model is the conceptual model written in precise, unambiguous terms. It specifies what each entity does, when it acts, and how the entities interact, in a form that can be translated directly into code. Nikolic, van Dam and Lukszo describe this as the stage at which the narrative of the system is turned into a set of rules that fix the order of events, the entities’ behaviours, and the changes in their state [1].
1.2.2.1: What formalisation does#
Formalisation removes the ambiguity of natural language by transforming each part of the conceptual model into something precise. Precision means more than replacing words with symbols. A formal description fixes the type, unit, permitted range, and initial value of each variable; states which rules may change it; and identifies constraints that must never be violated. It also forces the modeller to decide what happens at boundaries and in exceptional cases. For example, it must state whether speed may become negative and how a vehicle behaves when no gap is available. The result is a contract that can be implemented, tested, and compared with the original conceptual account.
Consider each part of the transformation in turn:
Each concept becomes a variable with a defined meaning, type, unit, range, and initial value. In the traffic model, speed is no longer an informal idea: it is a non-negative number measured per time step, bounded by a vehicle’s preferred maximum, and assigned a value when the vehicle is created. These definitions prevent two implementations from storing or interpreting the same concept differently [1].
Each relationship becomes a rule, function, equation, or logical condition that determines a future value from the current state. Saying that a driver “slows when too close” is not yet sufficient: the formal model must define how the gap is measured, the condition that counts as too close, and how much speed changes when that condition is met. The rule can then be evaluated in exactly the same way for every vehicle [1][2].
Every assumption that was implicit in the conceptual model is written down, together with its reasoning or source. For example, the traffic model assumes one lane, no overtaking, identical reaction intervals, and perfect observation of the next vehicle’s position. Stating these choices makes clear which real-world processes the model deliberately ignores and therefore where its conclusions may or may not apply [1].
1.2.2.2: Choices the formal model must fix#
Turning relationships into rules is not a single decision. The formal stage forces three separate choices, each of which can change the behaviour the model produces.
Before taking each choice in turn, preview all three below: each names one choice the formal model must settle, and pinning that choice down removes an ambiguity that would otherwise let two modellers build different models.
Each of the three choices is examined in turn below.
1.2.2.2.1: Numerical or logical form#
Rules can be written in more than one form, and a model often mixes them. A numerical rule calculates a quantity, such as increasing a vehicle’s speed by one unit while keeping it below its maximum. A logical rule tests a condition, such as whether the gap ahead is smaller than the distance needed to move safely, and selects what happens next. The distinction is about the form of the rule, not the kind of model: one agent step commonly uses a logical condition to decide which numerical update to apply [2].
Choosing the form also determines what must be verified. A numerical rule needs defined units, bounds, and behaviour at extreme values; a logical rule needs conditions that are complete and do not leave important cases undefined. Writing both explicitly lets the modeller test boundary cases before the rule is translated into code, such as a vehicle already at maximum speed or a gap exactly equal to the safety threshold.
1.2.2.2.2: Order of updating#
The order of updating must be stated, whether the entities act one after another or all at once from a snapshot of the previous step, since the two can give different behaviour [2].
Whether that choice actually changes the behaviour depends on the rule; decide, for each rule below, whether switching between the two orders would change the outcome.
The order matters precisely when entities read one another within a step, which is exactly when the formal model must state it.
1.2.2.2.3: Time step#
The time step should be chosen to match the fastest process the model needs to capture, so that nothing important happens “between” steps [2]. If one step represents a second, every rate and movement rule must be expressed per second; if it represents a day, processes that occur within a day are necessarily compressed or omitted. A step that is too large can skip important interactions, while an unnecessarily small step increases computation and may suggest more temporal precision than the evidence provides.
The formal model must also state when agents observe and update within that interval. For the traffic model, vehicles first read the positions relevant to the current step, then adjust speed and position according to the stated update scheme. That convention ensures that the time unit, the rule, and the order of updating describe one consistent transition from one model state to the next.
Fixing these choices is not busywork: it is what turns a readable description into a runnable one. Formalising the rules also tends to expose gaps the conceptual model glossed over, and catching them here is far cheaper than discovering them later during implementation [1]. With the transformation and its choices in hand, the traffic model makes all of this concrete.
1.2.2.3: The traffic example#
Fig. 6 Figure 1.6 The car-following rule made precise: each vehicle measures the gap to the vehicle ahead, accelerates by a fixed amount if the gap is safe (up to its maximum speed) or decelerates if it is not, then advances by its new speed.#
The conceptual model says each vehicle adjusts its speed based on the gap to the vehicle ahead. The formal model has to say exactly how. A simple and widely used car-following rule describes each vehicle with three steps applied once per simulation step: if the gap to the next vehicle is large enough to be safe, the vehicle accelerates a little, up to its maximum speed; if the gap is too small, it decelerates; and after updating its speed, it moves forward by that new speed [3].
Written as pseudocode, one update step is:
for each vehicle in the simulation:
gap = distance to next vehicle ahead
if gap > safe_distance:
speed = min(speed + acceleration, max_speed)
else:
speed = speed * deceleration_factor
position = position + speed
This rule mixes the numerical and logical forms from Section 1.2.2.2.1: the test gap > safe_distance is a logical condition, while the speed and position updates are numerical. Writing it down forces decisions the conceptual stage left open. The vehicles update one after another, the order-of-updating choice made concrete. The safe distance, the acceleration, and the deceleration factor are all parameters. The maximum speed may be the same for every vehicle or differ between them, which is where heterogeneity enters. Each of these is an assumption worth recording, because each one can change the behaviour the model produces [1]. Once the rules are in this form, the model is precise enough to implement, and two people working from the same description should produce code that behaves in compatible ways [1][2].
Read the rule part by part before moving on, considering the job each fragment does in the formal model.
Each fragment plays exactly one role, and together they show that a formal rule is a weave of logical tests, numerical updates, chosen parameters, and points of heterogeneity.
As written, this rule is fully deterministic: given the same starting positions, every run unfolds identically. The activity below keeps the same car-following rule but adds one extra ingredient, a small chance that a distracted driver taps the brakes for no reason, so you can see how a single random term changes the collective behaviour.
1.2.2.4: Rule lab#
Now try the rule yourself. Each car follows the same rule: speed up when the road ahead is clear, brake for the car in front, and, in this version, occasionally a distracted driver taps the brakes for no reason.
The jams appeared from nothing but the same rule applied to every car, and the exact values you gave the rule decided whether traffic flowed or seized up. That is the point of writing the rule down precisely: small changes to the parameters, not the road, are what change the behaviour the model produces.
With the rules now precise enough to translate directly into code, the next stage, Section 1.2.3, turns the formal model into a working implementation.
Key takeaways#
Key takeaways
The formal model turns the conceptual description into precise rules: concepts become variables, relationships become equations or if-then rules, and assumptions are stated explicitly.
It also fixes the order of updating and the size of the time step, both of which can change the model’s behaviour.
Pseudocode or equations remove the ambiguity of natural language, so two people building from the same formal model get compatible results.