| |
Click here for full text:
Exploiting strong attractors to slaughter monsters - taming 101500 states and beyond.
Tofts, Chris
HPL-2006-121
Keyword(s): process algebra; approximation; graph building; model checking; BDD; probability
Abstract: The ‘holy grail’ of automated state based model checking is to build precisely the states needed to validate a property and no more. In this paper we present a natural filter on automata which exploits the nature of the design of concurrent systems to order the state construction. We demonstrate that this can provide a sequence of approximating models which permit us to both address infinite systems and large finite systems (a 500 component 101500 state system being effectively modelled). The models are optimal, in the number of states used, for the parameters (state occupancy probabilities and consequent rewards) they attempt to approximate. The filter on the states we deduce is an interesting variant on the near decomposable class of systems presented by Simon and Ando (1961), but one where the small value terms do not necessarily dominate the long run behaviour. The semantic nature of the decomposition avoids the need to instantiate any values, or introduce arbitrary numerical bounds during the automata construction, enabling us to derive bounds on permitted behaviour without an expensive rebuild of the automata. Whilst the main focus of the work is the evaluation of properties of probabilistic systems, probabilities are not required for the construction, consequently the approach can be exploited for qualitative arguments of system correctness. Seven examples of layering of various systems are presented. One of the most powerful properties of the approach is that it is reasonable to argue that either the approximation technique works, or the system is inherently badly designed.
22 Pages
Back to Index
|
Printable version
