Model checking for data-based concurrent systems

This dissertation introduces predicate equation systems (PESs) as a uniform symbolic basis for model checking of data-based concurrent systems. In contrast with the finite-state concurrent systems that most model-checking research is directed toward, data-based concurrent systems use data variables that may draw values from infinite sets. PESs generalize first-order logic by adding capabilities for recursively-defined predicates, and may be seen as a first-order generalization of the well-studied boolean equation systems used in finite-state model checking. The dissertation also introduces a goal-directed, Gentzen-like proof system for proving PES formulas and shows how it may be used to define on-the-fly model checkers for data-based model-checking problems. Then the theory is used to develop model checkers for different data-based model-checking problems: real-time model checking, in both traditional and parametric forms; model-checking for Presburger systems, which feature the use of integer variables; and temporal-logic query checking for Presburger systems. In each case, implementations are presented, and extensive experimental data collected to compare these algorithms with existing approaches, when such exist. The general proof-search approach given here generally outperforms, in often startling fashion, the specialized routines found in the literature for these problems.