Towards more precise rewriting approximations

Abstract : To check a system, some verification techniques consider a set of terms I that represents the initial configurations of the system, and a rewrite system R that represents the system behavior. To check that no undesirable configuration is reached, they compute an over-approximation of the set of descendants (successors) issued from I by R, expressed by a tree language. Some techniques have been presented using regular tree languages, and more recently using non-regular languages to get better approximations: using context-free tree languages on the one hand, using synchronized tree languages on the other hand. In this paper, we merge these two approaches to get even better approximations: we compute an over-approximation of the descendants, using synchronized-context-free tree languages expressed by logic programs. We give several examples for which our procedure computes the descendants in an exact way, unlike former techniques.
Type de document :
Article dans une revue
Journal of Computer and System Sciences (JCSS), Elsevier, 2017, 〈http://www.sciencedirect.com/science/article/pii/S0022000017300065〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01521746
Contributeur : Pierre Réty <>
Soumis le : vendredi 12 mai 2017 - 11:31:37
Dernière modification le : mercredi 16 mai 2018 - 12:14:01

Identifiants

  • HAL Id : hal-01521746, version 1

Collections

Citation

Yohan Boichut, Jacques Chabin, Pierre Réty. Towards more precise rewriting approximations. Journal of Computer and System Sciences (JCSS), Elsevier, 2017, 〈http://www.sciencedirect.com/science/article/pii/S0022000017300065〉. 〈hal-01521746〉

Partager

Métriques

Consultations de la notice

329