Constraints and Automata


Constraints are logical formulas interpreted in a fixed domain, together with decision procedures for basic questions such as satisfiability or entailment. A typical example is linear constraints over the integers.

Finite state automata as well as constraints both allow to define models, or (infinite) sets of data. The purpose of the seminar is to show how automata may be used in constraint solving and how constraint solving can be used for automata-based verification problems.

We will illustrate the relationships using two examples in each direction:

-> linear constraints over the integers

-> encompassment constraints on trees

<- (flat) finite state automata with counters

<- timed automata

©2002-2018 U.C. Regents