A high-level model checking language with compile-time pruning of local variables

Among Model Checking tools, the behaviour of a system is often formalized as a transition system with atomic propositions associated with states (Kripke structure). In current modelling languages, transitions are usually specified as updates of the system’s variables to be performed when certain conditions are satisfied. However, such a lowlevel representation makes the description of complex transformations difficult, in particular in the presence of structured data. We present a high-level language with imperative semantics for modelling finite-state systems. The language features are selected with the aim of enabling the translation of models into compact transition systems, amenable to efficient verification via Model Checking. To this end, we have developed a compiler of our high-level language into the modelling language of the PRISM probabilistic model checker. One of the main characteristics of the language is that it makes a very different treatment of global and local variables. It is assumed that global variables are actually the variables that describe the state of the modelled system, whereas local variables are only used to ease the specification of the systems internal mechanisms. In this paper we describe the procedure for the pruning of local variables that is executed at compile time.