Petri Net Reachability Graphs: Decidability Status of First Order Properties

Résumé : Dans ce papier, nous examinons les propriétés de décision et de complexité pour des problèmes de model-checking sur les graphes d'accessibilité des réseaux de Petri, pour des langages modaux et du premier ordre. Nous modulons différents paramètres de façon à proposer une frontière aussi précise que possible entre décidable et indécidable. En dernier lieu nous mettons en évidence la robustesse de nos techniques de preuve.
Type de document :
Article dans une revue
Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2012, 8 (4:9), pp.1-28. 〈http://arxiv.org/abs/1210.2972〉. 〈10.2168/LMCS-8(4:9)2012〉
Liste complète des métadonnées

Littérature citée [39 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00743935
Contributeur : Christophe Morvan <>
Soumis le : lundi 22 octobre 2012 - 10:20:31
Dernière modification le : jeudi 11 janvier 2018 - 06:20:13
Document(s) archivé(s) le : mercredi 23 janvier 2013 - 03:35:45

Fichier

1210.2972.pdf
Fichiers éditeurs autorisés sur une archive ouverte

Identifiants

Citation

Philippe Darondeau, Stephane Demri, Roland Meyer, Christophe Morvan. Petri Net Reachability Graphs: Decidability Status of First Order Properties. Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2012, 8 (4:9), pp.1-28. 〈http://arxiv.org/abs/1210.2972〉. 〈10.2168/LMCS-8(4:9)2012〉. 〈hal-00743935〉

Partager

Métriques

Consultations de la notice

288

Téléchargements de fichiers

518