A.3 State spaces

lbtt uses randomly generated state spaces in the model checking result cross-comparison test (see Model checking result cross-comparison test) and the model checking result consistency check (see Model checking result consistency check). Formally, the state spaces are (finite) Kripke structures with a total transition relation, i.e., directed graphs with a set of atomic propositions attached to each state, with each state having at least one immediate successor (which may be the state itself). The precise definition is as follows (as before, let AP be a finite set of atomic propositions).

A state space can be represented as a tuple <S, R, L>, where

• S is the finite set of states,
• R (a subset of S x S) is the transition relation, and
• L: S -> 2^AP is the labeling function which maps each state to a set of atomic propositions that hold in the state.