| Summary: | 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.
|
|---|
