Alternating Automata Modulo First Order Theories - IMAG Accéder directement au contenu
Communication Dans Un Congrès Année : 2019

Alternating Automata Modulo First Order Theories

Radu Iosif
  • Fonction : Auteur
  • PersonId : 840083
Xiao Xu
  • Fonction : Auteur
  • PersonId : 771451
  • IdRef : 187516375

Résumé

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 parameter-ized concurrent programs, composed of replicated threads, with shared memory.
Fichier principal
Vignette du fichier
final.pdf (178.37 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-02387992 , version 1 (02-12-2019)

Identifiants

Citer

Radu Iosif, Xiao Xu. Alternating Automata Modulo First Order Theories. Computer Aided Verification - 31st International Conference, Jul 2019, New York, United States. pp.43-63, ⟨10.1007/978-3-030-25543-5_3⟩. ⟨hal-02387992⟩
85 Consultations
104 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More