Skip to Main content Skip to Navigation
Journal articles

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
IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL, Inria Rennes – Bretagne Atlantique
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.
Document type :
Journal articles
Complete list of metadata

Cited literature [28 references]  Display  Hide  Download

https://hal.inria.fr/hal-00994970
Contributor : Hervé Marchand <>
Submitted on : Thursday, May 22, 2014 - 2:20:30 PM
Last modification on : Tuesday, February 16, 2021 - 3:30:26 AM
Long-term archiving on: : Friday, August 22, 2014 - 12:30:37 PM

File

jdeds-rts14.pdf
Files produced by the author(s)

Identifiers

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, 2015, 25 ((1-2)), pp.271-294. ⟨10.1007/s10626-014-0197-3⟩. ⟨hal-00994970⟩

Share

Metrics

Record views

494

Files downloads

310