Diagnosis and Opacity Problems for Infinite State Systems Modeled by Recursive Tile Systems

Sébastien Chédor 1 Christophe Morvan 1 Sophie Pinchinat 2 Hervé Marchand 1
1 SUMO - SUpervision of large MOdular and distributed systems
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
2 LogicA - Logic and Applications
ENS Cachan - École normale supérieure - Cachan, UR1 - Université de Rennes 1, IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : The analysis of discrete event systems under partial observation is an important topic, with major applications such as the detection of information flow and the diagnosis of faulty behaviors. These questions have, mostly, not been addressed for classical models of recursive systems, such as pushdown systems and recursive state machines. In this paper, we consider recursive tile systems, which are recursive infinite systems generated by a finite collection of finite tiles, a simplified variant of deterministic graph grammars (slightly more general than pushdown systems). Since these systems are infinite-state in general powerset constructions for monitoring do not always apply. We exhibit computable conditions on recursive tile systems and present non-trivial constructions that yield effective computation of the monitors.We apply these results to the classic problems of state-based opacity and diagnosability (off-line verification of opacity and diagnosability, and also run-time monitoring of these properties). For a decidable subclass of recursive tile systems, we also establish the decidability of the problems of state-based opacity and diagnosability.
Type de document :
Article dans une revue
Liste complète des métadonnées

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

https://hal.inria.fr/hal-00994970
Contributeur : Hervé Marchand <>
Soumis le : jeudi 22 mai 2014 - 14:20:30
Dernière modification le : mardi 16 janvier 2018 - 15:54:23
Document(s) archivé(s) le : vendredi 22 août 2014 - 12:30:37

Fichier

jdeds-rts14.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Citation

Sébastien Chédor, Christophe Morvan, Sophie Pinchinat, Hervé Marchand. Diagnosis and Opacity Problems for Infinite State Systems Modeled by Recursive Tile Systems. Discrete Event Dynamic Systems, Springer Verlag, 2014, 〈http://link.springer.com/article/10.1007/s10626-014-0197-3〉. 〈10.1007/s10626-014-0197-3〉. 〈hal-00994970〉

Partager

Métriques

Consultations de la notice

340

Téléchargements de fichiers

135