Room 206 (2nd floor, badged access)
4 juillet 2019 - 14h00
Alternating Automata Modulo First Order Theories
par Radu IOSIF de VERIMAG
Abstract: We introduce first order alternating automata, a generalization of
boolean alternating automata, in which transition rules are described
by multisorted first order formulae, with states and internal
variables given by uninterpreted predicate terms. The model is closed
under union, intersection and complement, and its emptiness problem is
undecidable, even for the simplest data theory of equality. To cope
with the undecidability problem, we develop an abstraction refinement
semi-algorithm based on lazy annotation of the symbolic execution
paths with interpolants, obtained by applying (i) quantifier
elimination with witness term generation and (ii) Lyndon interpolation
in the quantifier-free theory of the data domain, with uninterpreted
predicate symbols. This provides a method for checking inclusion of
timed and finite-memory register automata, and emptiness of quantified
predicate automata, previously used in the verification of
parameterized concurrent programs, composed of replicated threads,
with shared memory. Joint work with Xiao Xu (VERIMAG).
