Previous: Generalized automata, Up: Definitions

`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.