Temporal Logic Model Checking

Illustrated with a toy example of traffic light

Published in

Towards NeSy

4 min readAug 22, 2023

Introduction

In light of recent advancements in deep neural networks, which have predominantly dominated fields like Natural Language Processing and Computer Vision, it’s important to recognize that these networks often fall short of being truly robust systems. A notable instance of this is highlighted in the paper titled “STLnet: Signal Temporal Logic Enforced Multivariate Recurrent Neural Networks.” In this paper, the authors strive to impose a series of constraints on sequentially generated data. To achieve this objective, the initial step involves verifying whether the generated sequential data adheres to these constraints or if violations occur. This brings us to the focal point of this blog: an exploration of the concept known as model checking. This involves adopting a temporal logic language for specification purposes. To illustrate this concept, a tangible example involving a malfunctioning traffic light is presented.

Code can be found at the end of this article.

Examples and descriptions are partially taken from slide 1&2 by Edmund M. Clarke, Jr. at CMU and Richard M. Murray etc, at CalTech.

Basics for Model Checking

System: a finite-state transition graph
Specification: system constraints written in temporal logic rules.
Model Checking: a search procedure to check if the system is a model for the specification. In other words, it is a process that traverses the transition graph thoroughly to see if any part of the graph violates the system constraints.

Linear Temporal Logic

A mathamatical language to specify system constraints.
Each moment in time has a well-defined successor moment in LTL.
LTL formulas:

This one-liner is usually seen in logic literature where researchers use one line to include all possible allowed formulas in the syntax. “|” stands for OR.

Operator precedence: Unary operators first, binary operators second. Among binary operators: \cup first, \land, \lor, \rightarrow second. Note that, although \lor, \rightarrow are not in the formulas one-liner, \lor, \rightarrow can be expressed using \land, \neg.

Path $\sigma$ is a sequence of states sampled from the transition graph. Given a system constraint expressed using LTL formula $\phi$, if path $\sigma$ does not violate the constraint, we say that:

Two important general temporal operators:

Diamond and Square operators are widely seen in temporal logic literature. Although these two operators are not specified in the one-liner syntax formula, they can be easily expressed using the allowed operators like shown in this figure.

Some common composite operators (from slides):

Traffic Light Toy Example

We have a malfunctioned traffic light defined by a probabilistic transition graph expressed as a dictionary. We have a set of constraints written in LTL formulas. Sample the transition graph for a predefined period of time and see if the system models the specification, if not, output the counter example.

Specifications in LTL formulas

Code

Can access github repo for more: https://github.com/jink1994/temporal_model_checking

The main logic in this code is:

Create a probabilistic transition graph that imitate a “malfunctioned” traffic light.
Have one decision function that judge whether a particular pair of states obeys all the LTL formulas.
Similate for a given time steps.

import random

# Define the states of the system
GREEN = 'green'
YELLOW = 'yellow'
RED = 'red'

# Define the decision function based on LTL formulas
# If any input 2-tuple violates the specification, the function output False
def hold_properties(current_state, next_state):
    if current_state == RED:
        return next_state == GREEN
    if current_state == GREEN:
        return next_state == YELLOW
    if current_state == YELLOW:
        return next_state == RED

# Define the probabilistic state transitions
transition_probabilities = {
  #Green light has a 20% chance of jumping directly into Red by definition
    GREEN: dict({YELLOW: 0.8, RED: 0.2}),
    YELLOW: dict({RED:1.0}),
    RED: dict({GREEN:1.0})
}

# Perform probabilistic state transition
def transition(current_state):
    next_state = random.choices(
        population=list(transition_probabilities[current_state].keys()),
        weights=list(transition_probabilities[current_state].values()),
        k=1
    )[0]
    return next_state

# Simulate state transitions
def simulate(num_steps):
    current_state = RED
    print("Starting in state:", current_state)

    for step in range(num_steps):
        next_state = transition(current_state)
        print("Step {}: Transition from {} to {}".format(step + 1, current_state, next_state))
        if not hold_properties(current_state, next_state):
            print("Temporal property violated.")
            print(f"Counterexample: {current_state} -> {next_state} (Violation)")
            break
        current_state = next_state

# Set the number of simulation steps
num_simulation_steps = 100

# Perform the simulation
simulate(num_simulation_steps)