Guarded Variable Automata over Infinite Alphabets

Walid Belkhir 1 Yannick Chevalier 2 Michael Rusinowitch 1
1 CASSIS - Combination of approaches to the security of infinite states systems
FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies, Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : We define guarded variable automata (GVAs), a simple extension of finite automata over infinite alphabets. In this model the transitions are labelled by letters or variables ranging over an infinite alphabet and guarded by conjunction of equalities and disequalities. GVAs are well-suited for modeling component-based applications such as web services. They are closed under intersection, union, concatenation and Kleene operator, and their nonemptiness problem is PSPACE-complete. We show that the simulation preorder of GVAs is decidable. Our proof relies on the characterization of the simulation by means of games and strategies. This result can be applied to service composition synthesis.
Type de document :
Pré-publication, Document de travail
29 pages. arXiv admin note: text overlap with arXiv:1302.4205. 2013
Liste complète des métadonnées

https://hal.inria.fr/hal-00914779
Contributeur : Walid Belkhir <>
Soumis le : vendredi 6 décembre 2013 - 09:41:19
Dernière modification le : jeudi 11 janvier 2018 - 06:24:26

Identifiants

  • HAL Id : hal-00914779, version 1
  • ARXIV : 1304.6297

Citation

Walid Belkhir, Yannick Chevalier, Michael Rusinowitch. Guarded Variable Automata over Infinite Alphabets. 29 pages. arXiv admin note: text overlap with arXiv:1302.4205. 2013. 〈hal-00914779〉

Partager

Métriques

Consultations de la notice

307