Partial specifications allow approximate models of systems such as Kripke structures, or labeled
transition systems to be created. Using the abstraction possible with these models, an avoidance
of the state-space explosion problem is possible, whilst still retaining a structure that can
have properties checked over it. A single partial specification abstracts a set of systems, whether
Kripke, labeled transition systems, or systems with both atomic propositions and named transitions.
This thesis deals in part with problems arising from a desire to efficiently evaluate
sentences of the modal μ-calculus over a partial specification.
Partial specifications also allow a single system to be modeled by a number of partial specifications,
which abstract away different parts of the system. Alternatively, a number of partial
specifications may represent different requirements on a system. The thesis also addresses the
question of whether a set of partial specifications is consistent, that is to say, whether a single
system exists that is abstracted by each member of the set. The effect of nominals, special
atomic propositions true on only one state in a system, is also considered on the problem of the
consistency of many partial specifications. The thesis also addresses the question of whether
the systems a partial specification abstracts are all abstracted by a second partial specification,
the problem of inclusion.
The thesis demonstrates how commonly used “specification patterns” – useful properties specified
in the modal μ-calculus, can be efficiently evaluated over partial specifications, and gives
upper and lower complexity bounds on the problems related to sets of partial specifications.