| Summary: | Partial specifications al10w approximate models of systems such as Kripke structures, or labelled 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 specifkation abstracts a set of systems, whether Kripke, labelled transition systems, or systems with both atomic propositions and named transitions. This thesis deals in part with decision problems arising from desires to efficiently evaluate sentences of the modal J.t-calculus over a partial specification. Partial specifications also al10w a single system to be modeled by a number of pmtial specifications, which abstract away different parts of the system. Alternatively, a number of modal specifications may represent different requirements on a system. The thesis also addresses the question of whether a set of modal specifications is consistent, that is to say, whether a single system exists that is abstracted by each member of the set. This 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 modal specifications. The thesis also addresses the question of whether the systems a modal specification abstracts are all abstracted by a second modal specification, the problem of inclusion. The thesis demonstrates how commonly used 'specification patterns', interesting properties expressible in the modal fL-calculus, can be efficiently· evaluated over partial specifications, and gives upper and lower complexity bounds for the problems related to sets of partial specifications.
|
|---|
