Model Checking: Programming a Simple Model Checker Together Part I
Although Model Checking can seem a very specific topic, understanding its concepts is a crucial point for many theoretical Formal Verification jobs, but also for many real-world applications. Our blog tries to combine what we have learned from the previous blogs with the coding.
Although Model Checking can seem a very specific topic, understanding its concepts is a crucial point for many theoretical Formal Verification jobs, but also for many real-world applications. Our blog tries to combine what we have learned from the previous blogs with the coding.
Introduction
The goal of this extension to the blog series about Model Checking is to apply the knowledge we used in the practical world. In this blog, we will define most of the building blocks of our Model Checker in Python. This includes most of the components we discussed in the previous blogs of this series. Furthermore, we introduced GitHub Classroom challenges for each section so that you can implement and test your implementation easily, as well as the proposed solutions in this blog. The solutions are not optimization-oriented, but rather explanation-oriented, and are kept as simple as possible.
Deterministic Finite Automata
As our first blog described Deterministic Finite Automata (DFA), we want to implement them as a Python class. You can implement this in the Github Classroom.
State Class
To achieve this, we defined a class State which represents a state of a DFA, and to which we can make a transition to another state with a given letter of some alphabet using the method make_transition. It creates a transition with the given letter if it did not already exist, or overwrites the end-state of the transition if it does. We can also read letters and words from a state using the methods read_letter and read_word, which return the state we arrive at after reading the letter or word.
class State:
def __init__(self, name: str, accepting: bool = False) -> None:
pass
def make_transition(self, letter: str, to: "State") -> None:
assert len(letter) == 1, "Only single-letter transitions are supported."
pass
def read_letter(self, letter: str) -> "State":
assert len(letter) == 1, "Only single-letter transitions are supported."
pass
def read_word(self, word: str) -> "State":
passDFA Class
A DFA object is defined only through an initial state of type State and an alphabet (a set of letters). The other states of the DFA can be reached through graph traversal from the initial state. This guarantees that our DFA does not contain any non-reachable state. The class has mainly three methods:
is_validchecks whether the current graph is a valid DFA. This includes the fact that every state has a transition with every letter of the alphabet. We do not worry about the case of multiple transitions of the same letter, as it is excluded by our definition of theStateclass:make_transitiondoes not add a new transition, but overwrites the existing one.acceptschecks whether the DFA accepts a given word.is_emptychecks whether the DFA accepts any word at all or if it accepts the empty language.
class DFA:
def __init__(self, initial_state: State, alphabet: set[str]) -> None:
assert all({len(letter) == 1 for letter in alphabet}), "Alphabet should only contain single-letters"
pass
def is_valid(self) -> bool:
pass
def accepts(self, word: str) -> bool:
if not self.is_valid(): # We exclude non-valid DFAs
raise ValueError("Cannot check acceptance on invalid DFAs")
pass
def is_empty(self) -> bool:
if not self.is_valid(): # We exclude non-valid DFAs
raise ValueError("Cannot check emptiness on invalid DFAs")
passSolution
Show / Hide Solution
class State:
def __init__(self, name: str, accepting: bool = False) -> None:
self.name = name
self.is_accepting = accepting
self.next_states = {}
def make_transition(self, letter: str, to: "State") -> None:
assert len(letter) == 1, "Only single-letter transitions are supported. "
self.next_states[letter] = to
def read_letter(self, letter: str) -> "State":
assert len(letter) == 1, "Only single-letter transitions are supported. "
if letter not in self.next_states:
raise KeyError(f"Can't find next state for the letter {letter}")
return self.next_states[letter]
def read_word(self, word: str) -> "State":
current_state = self
for letter in word:
current_state = current_state.read_letter(letter)
return current_state
class DFA:
def __init__(self, initial_state: State, alphabet: set[str]):
assert all({len(letter) == 1 for letter in alphabet}), "Alphabet should only contain single-letters. "
self.alphabet = alphabet
self.initial_state = initial_state
def is_valid(self) -> bool:
visited = set() # The names of the already visited states
ones_to_visit = {self.initial_state} # The states that are not visited yet
while ones_to_visit: # While there is still a state to visit
current_state = ones_to_visit.pop() # Take the state to visit
visited.add(current_state.name) # Mark that state as visited
current_letters = set() # The letters that this state has a mapping for
for letter, next_state in current_state.next_states.items(): # For each next state
current_letters.add(letter) # Add the letter to the letter set
# If the next state is not visited, mark as a state that needs to be visited as well
if next_state.name not in visited:
ones_to_visit.add(next_state)
# The mapping of the state must be exactly the same as the alphabet of the DFA
if current_letters != self.alphabet:
return False
return True
def accepts(self, word: str) -> bool:
if not self.is_valid(): # We exclude non-valid DFAs
raise ValueError("Cannot check acceptance on invalid DFAs")
current_state = self.initial_state # Start at the initial state
# Read letter by letter
for letter in word:
# If the word encounters some letter not in the alphabet, then we automatically reject
if letter not in self.alphabet:
return False
current_state = current_state.next_states[letter] # Go to the next state
return current_state.is_accepting
def is_empty(self) -> bool:
if not self.is_valid(): # We exclude non-valid DFAs
raise ValueError("Cannot check emptiness on invalid DFAs")
visited = set() # The names of the already visited states
ones_to_visit = [self.initial_state] # The states that are not visited yet
while ones_to_visit: # While there is still a state to visit
current_state = ones_to_visit.pop() # Take the state to visit
# If our visited state is accepting, we are done
if current_state.is_accepting:
return False
visited.add(current_state.name) # Mark that state as visited
# Add all next states which are not already visited
for next_state in current_state.next_states.values():
if next_state.name not in visited:
ones_to_visit.append(next_state)
return TrueKripke Structures
Our second blog concentrated on the modeling part. In particular, we introduced Kripke structures as one of the most widely used data structures to model a system. Our second task is to implement a Kripke Structure class with the ability to test for its validity. Similarly to how DFAs were defined, we define the states in Kripke structures as objects and connect them through transitions to create the LTS using only its initial states. The validity of Kripke structures is only determined by whether each state’s label contains only propositions from the set of propositions introduced during the initialization of the Kripke structure. The Proposition class is already implemented with the possibility to initialize multiple propositions at the same time by listing their names. Complete the implementation of the classes State and KripkeStructure to satisfy the validity check. You can use the given Github Classrom.
class Proposition:
def __init__(self, name: str) -> None:
self.name = name
@staticmethod
def propositions(*args) -> list["Proposition"]:
assert len(args) > 0 and all(isinstance(arg, str) for arg in args), "Only non-empty list of strings is allowed. "
return [Proposition(name) for name in args]
def __str__(self):
return self.name
def __repr__(self):
return self.name
class State:
def __init__(self, name: str, labels: set[Proposition]) -> None:
pass
def make_transition(self, state: "State") -> None:
pass
class KripkeStructure:
def __init__(self, initial_states: set[State], propositions: set[Proposition]) -> None:
pass
def is_valid(self) -> bool:
passSolution
Show / Hide Solution
class Proposition:
def __init__(self, name: str) -> None:
self.name = name
@staticmethod
def propositions(*args) -> list["Proposition"]:
assert len(args) > 0 and all(isinstance(arg, str) for arg in args), "Only non-empty list of strings is allowed. "
return [Proposition(name) for name in args]
def __str__(self):
return self.name
def __repr__(self):
return self.name
class State:
def __init__(self, name: str, labels: set[Proposition]) -> None:
self.name = name
self.next_states = set()
self.labels = labels
def make_transition(self, to: "State") -> None:
self.next_states.add(to)
class KripkeStructure:
def __init__(self, initial_states: set[State], propositions: set[Proposition]) -> None:
self.initial_states = initial_states
self.propositions = propositions
def is_valid(self) -> bool:
not_visited = self.initial_states.copy()
visited = set()
while not_visited:
state = not_visited.pop()
if not state.labels.issubset(self.propositions):
return False
visited.add(state)
for next_state in state.next_states:
if next_state not in visited:
not_visited.add(next_state)
return TrueLinear Temporal Logic
This task is probably the most challenging out of all. It is designed to create a simple Python API that allows the definition and verification of LTL formulae on simple infinite paths that are in the form x₀ x₁... xₙ (xₙ₊₁...xₘ)ω. In other words, the infinite path should be a prefix path concatenated to an infinitely repeated path. The exact implementation and design of most of LTL is left to the programmer, except for the PropositionLTLFormula class and InfinitePath class definition. However, the API should guarantee the following operations:
# A, B, C are objects of the class LTLFormula
negated_A = ~A
next_A = +A
A_or_B = A | B
A_until_B = A >> B
A_and_B = A & B
generally_A = G(A)
eventually_A = F(A)
true_formula = TRUE
some_random_combination = (A | +F(B >> (~C))) & G(B | (+B))You do not have to worry about the operations’ priorities, as you can assume that brackets will be used everywhere to avoid confusion. After defining the API, you need to check if an infinite path satisfies a given LTL formula. You can again use the Github Classroom. The code skeleton looks as follows:
from abc import ABC
class LTLFormula(ABC):
pass
class PropositionLTLFormula(LTLFormula):
def __init__(self, name: str) -> None:
self.name = name
@staticmethod
def propositions(*args) -> list["PropositionLTLFormula"]:
assert len(args) > 0 and all(isinstance(arg, str) for arg in args), "Only non-empty list of strings is allowed. "
return [PropositionLTLFormula(name) for name in args]
def __str__(self):
return self.name
def __repr__(self):
return self.name
class InfinitePath:
def __init__(self, linear_path: list[set[PropositionLTLFormula]], lasso_start_index: int):
assert 0 <= lasso_start_index < len(linear_path), "lasso must start at some point of the linear path."
pass
def satisfies(self, formula: LTLFormula):
passSolution
Show / Hide Solution
from abc import ABC
class LTLFormula(ABC):
def __pos__(self):
return NextLTLFormula(self)
def __invert__(self):
return NegationLTLFormula(self)
def __or__(self, other: LTLFormula):
return DisjunctionLTLFormula(self, other)
def __rshift__(self, other):
return UntilLTLFormula(self, other)
def __and__(self, other: LTLFormula):
return ~((~self) | (~other))
def F(self):
return TRUE >> self
def G(self):
return ~(~self).F()
def F(formula: LTLFormula):
return formula.F()
def G(formula: LTLFormula):
return formula.G()
class _TrueLTLFormula(LTLFormula):
def __init__(self):
pass
def __str__(self):
return "true"
def __repr__(self):
return "true"
TRUE = _TrueLTLFormula()
class PropositionLTLFormula(LTLFormula):
def __init__(self, name: str) -> None:
self.name = name
@staticmethod
def propositions(*args) -> list["PropositionLTLFormula"]:
assert len(args) > 0 and all(isinstance(arg, str) for arg in args), "Only non-empty list of strings is allowed. "
return [PropositionLTLFormula(name) for name in args]
def __str__(self):
return self.name
def __repr__(self):
return self.name
class NegationLTLFormula(LTLFormula):
def __init__(self, formula: LTLFormula):
self.formula = formula
def __str__(self):
return f"¬({self.formula})"
def __repr__(self):
return f"NOT({self.formula})"
class DisjunctionLTLFormula(LTLFormula):
def __init__(self, left: LTLFormula, right: LTLFormula):
self.left = left
self.right = right
def __str__(self):
return f"({self.left} ∨ {self.right})"
def __repr__(self):
return f"OR({self.left}, {self.right})"
class NextLTLFormula(LTLFormula):
def __init__(self, formula: LTLFormula):
self.formula = formula
def __str__(self):
return f"X{self.formula}"
def __repr__(self):
return f"Next({self.formula})"
class UntilLTLFormula(LTLFormula):
def __init__(self, left: LTLFormula, right: LTLFormula):
self.left = left
self.right = right
def __str__(self):
return f"({self.left} U {self.right})"
def __repr__(self):
return f"Until({self.left}, {self.right})"
class InfinitePath:
def __init__(self, linear_path: list[set[PropositionLTLFormula]], lasso_start_index: int):
assert 0 <= lasso_start_index < len(linear_path), "lasso must start at some point of the linear path."
self.linear_path = linear_path
self.lasso_start_index = lasso_start_index
def __satisfies_at_idx(self, formula: LTLFormula, at_idx: int = 0):
if formula == TRUE:
return True
if isinstance(formula, PropositionLTLFormula):
return formula in self.linear_path[at_idx]
if isinstance(formula, NegationLTLFormula):
return not self.__satisfies_at_idx(formula.formula, at_idx)
if isinstance(formula, DisjunctionLTLFormula):
return self.__satisfies_at_idx(formula.left, at_idx) or self.__satisfies_at_idx(formula.right, at_idx)
if isinstance(formula, NextLTLFormula):
next_idx = at_idx + 1
if next_idx >= len(self.linear_path):
next_idx = self.lasso_start_index
return self.__satisfies_at_idx(formula.formula, next_idx)
if isinstance(formula, UntilLTLFormula):
if at_idx < self.lasso_start_index:
while at_idx < len(self.linear_path):
if self.__satisfies_at_idx(formula.right, at_idx):
return True
if not self.__satisfies_at_idx(formula.left, at_idx):
return False
at_idx += 1
return False
if self.lasso_start_index == len(self.linear_path) - 1:
# Lasso starts at last index, so we only check that index for right
return self.__satisfies_at_idx(formula.right, self.lasso_start_index)
lasso_size = len(self.linear_path) - self.lasso_start_index
idx_from_lasso = at_idx - self.lasso_start_index
current_idx_from_lasso = (at_idx - self.lasso_start_index + 1) % lasso_size
while current_idx_from_lasso != idx_from_lasso:
current_idx = current_idx_from_lasso + self.lasso_start_index
if self.__satisfies_at_idx(formula.right, current_idx):
return True
if not self.__satisfies_at_idx(formula.left, current_idx):
return False
current_idx_from_lasso = (current_idx_from_lasso + 1) % lasso_size
return False
raise ValueError(f"Unknown formula type: {type(formula)}")
def satisfies(self, formula: LTLFormula):
return self.__satisfies_at_idx(formula)