Complete and Efficient Checks for Branching-Time Abstractions

Computer programs, electronic control units in cars, model-driven development in software engineering, and non-linear feedback systems within biological cells are all examples of dynamical systems or processes that benefit greatly from their capture in formal models and subsequent analysis of such models. Model creation aids documentation, system comprehension and can facilitate change management. Model checking, an analysis of a model with respect to a fixed property, can gain important insights into subtleties of the dynamical systems these models represent, enabling system validation with predictive power.Automated or semi-automated model generation and analysis are necessary for any realistic technology transfer of model checking into industrial use contexts. Barriers to such technology transfer are foremost due to the lack of scalability (model checks are either undecidable or take too must time and space) and to the lack of full automation of existing model-checking methodology. Another barrier is that existing approaches cannot deal with more complex properties that mix path quantifiers but are needed in modern application contexts, e.g. A system can always reach a state from which a certain cyclic reaction is possible.'' This research creates a model-checking framework that addresses these barriers directly for this full range of complex properties: scalability through the ability to reduce all model checks to those with finite-state and small models; and automation through an extension of existing predicate-abstractiontechniques, notably the counter-example-guided abstraction refinement (CEGAR), to this setting of more complex properties.This research programme will also be carried out for quantitive systems in which the dynamics of a system is governed by probability distributions.To summarize, the main aim of this proposal is to develop a framework for efficient modelling, checking, and refining of abstractions that are complete (i.e. one can always discover compliance or non-compliance of a system with any property through some finite-state abstraction) and precise (i.e. the abstract model enjoys a maximum number of properties that are true in the system it abstracts) for properties that appeal to branching time and probabilities.