 Axiomatic systems and state transition systems used for correctness evaluation can be understood as theories of the represented artifacts, in that they are used to predict and explain their future behaviors. Methodologically state transition systems in model checking can be compared with scientific models in empirical sciences (Angius and Tamburrini 2011). For instance, Kripke Structures (see Clarke et al. 1999 ch. 2) are in compliance with Suppes’ (1960) definition of scientific models as set-theoretic structures establishing proper mapping relations with models of data collected by means of experiments on the target empirical system (see also the entry on  models in science).  Kripke Structures and other state transition systems utilized in formal verification methods are often called system specifications. They are distinguished from common specifications, also called property specifications. The latter specify some required behavioral properties the program to be encoded must instantiate, while the former specify (in principle) all potential executions of an already encoded program, thus allowing for algorithmic checks on its traces (Clarke et al. 1999). In order to achieve this goal, system specifications are considered as abductive structures, hypothesizing the set of potential executions of a target computational system on the basis of the program’s code and the allowed state transitions (Angius 2013b). Indeed, once it has been checked whether some temporal logic formula holds of the modeled Kripke Structure, the represented program is empirically tested against the behavioral property corresponding to the checked formula, in order to evaluate whether the model-hypothesis is an adequate representation of the target computational system. Accordingly, property specifications and system specifications differ also in their intentional stance (Turner 2011): the former are requirements on the program to be encoded, the latter are (hypothetical) descriptions of the encoded program. The descriptive and abductive character of state transition systems in model checking is an additional and essential feature putting state transition systems on a par with scientific models.