Paper Info
Title
Alternating Automata Modulo First Order Theories
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.
Year
DOI
Venue
2019
10.1007/978-3-030-25543-5_3
COMPUTER AIDED VERIFICATION, CAV 2019, PT II
Field
DocType
Volume
Quantifier elimination,Parameterized complexity,Data domain,Shared memory,Computer science,Modulo,Automaton,Theoretical computer science,Predicate (grammar),Undecidable problem
Conference
11562
ISSN
Citations 
PageRank 
0302-9743
0
0.34
References 
Authors
0
2
Name
Order
Citations
PageRank
Radu Iosif148342.44
xiao xu2389.71