Expressive and efficient model checking.

摘要

Model checking is an algorithmic proof technique for determining whether a reactive system satisfies a temporal logic specification describing the correct behavior of the system. Traditionally, temporal specifications have been qualitative in nature; for instance, specifying that an event would happen at some time in the future. With the advent of many hard real-time systems, such as onboard controllers, substantial need has arisen for quantitative temporal logics which can express, for example, deadlines on when in the future an event will occur.; Typically, model checkers evaluate specifications over representations of the given reactive system which may be exponentially larger than the textual description of the system. This state explosion problem is the single largest obstacle to the more wide spread application of model checking.; which can substantially ameliorate the state explosion problem, may be applied to model checking quantitative formulae. Furthermore, we describe several techniques for broadening the application of symmetry reduction. These techniques are capable of yielding the benefits of symmetry reduction for systems which are asymmetric.; We also describe two quantitative extensions to traditional temporal logics and give model checking algorithms for both these extensions. Firstly, we present Real-time Propositional Linear Temporal Logic, which combines extended regular expressions with Propositional Linear Temporal Logic. This combination caters to the expression of quantitative properties specifying the number of occurrences of independent events. Allowing quantification over events, permits the expression of deadlines given by the occurrence of atomic events. For instance, it is possible to write a specification saying that service requests for process one must be granted after no more than five service grants have been given to process two.; Secondly, we define Parameterized Real-Time Computation Tree Logic. The parameterized specifications definable in this logic allow designers to write the timing artifacts of a particular system design stage. In particular, it is possible to specificy that there is a finite bound on the length of time it takes before a given event occurs. Such specifications are parameterized over the natural numbers, yet we are able to show that the model checking problem for this logic is decidable and give efficient algorithms for large classes of formulae.