History-Preserving Bisimilarity for Higher-Dimensional Automata via Open Maps

Uli Fahrenberg 1 Axel Legay 1
1 ESTASYS - Efficient STAtistical methods in SYstems of systems
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : One of the popular notions of equivalence for non-interleaving concurrent systems is history-preserving bisimilarity (hp-bisimilarity). Higher-dimensional automata (HDA) is a non-interleaving formalism for reasoning about behavior of concurrent systems, which provides a generalization (up to hp-bisimilarity) to the main models of concurrency proposed in the literature. Using open maps, we can show that hp-bisimilarity for HDA has a characterization directly in terms of (higher-dimensional) transitions of the HDA, rather than in terms of runs as e.g. for Petri nets. Our results imply decidability of hp-bisimilarity for finite HDA. They also put hp-bisimilarity firmly into the open-maps framework and tighten the connections between bisimilarity and weak topological fibrations.
Type de document :
Communication dans un congrès
LICS 2013 - Twenty-Eighth Annual ACM/IEEE Symposium on Logic in Computer Science, Jun 2013, New Orleans, United States
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01087933
Contributeur : Uli Fahrenberg <>
Soumis le : jeudi 27 novembre 2014 - 10:04:07
Dernière modification le : mercredi 11 avril 2018 - 02:01:16
Document(s) archivé(s) le : lundi 2 mars 2015 - 09:18:59

Fichier

lics.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01087933, version 1

Citation

Uli Fahrenberg, Axel Legay. History-Preserving Bisimilarity for Higher-Dimensional Automata via Open Maps. LICS 2013 - Twenty-Eighth Annual ACM/IEEE Symposium on Logic in Computer Science, Jun 2013, New Orleans, United States. 〈hal-01087933〉

Partager

Métriques

Consultations de la notice

364

Téléchargements de fichiers

50