Previous: Generalized automata, Up: Definitions

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