×

Diagnosis and opacity problems for infinite state systems modeled by recursive tile systems. (English) Zbl 1328.93166

Summary: 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.

MSC:

93C65 Discrete event control/observation systems
93B07 Observability

Software:

UMDES
PDFBibTeX XMLCite
Full Text: DOI HAL

References:

[1] Alur R, Etessami K, Yannakakis M (2001) Analysis of recursive state machines. In: CAV, vol 2102. LNCS, pp 207-220 · Zbl 0991.68535
[2] Alur R, Madhusudan P (2004) Visibly pushdown languages. In: STOC 04. ACM, pp 202-211 · Zbl 1192.68396
[3] Badouel E, Bednarczyk M, Borzyszkowski A, Caillaud B, Darondeau P (2007) Concurrent secrets. Discret Event Dyn Syst 17:425-446 · Zbl 1125.93320 · doi:10.1007/s10626-007-0020-5
[4] Baldan P, Chatain T, Haar S, König B (2010) Unfolding-based diagnosis of systems with an evolving topology. Inf Comput 208(10):1169-1192. doi:10.1016/j.ic.2009.11.009 · Zbl 1214.68242 · doi:10.1016/j.ic.2009.11.009
[5] Bouyer P, Chevalier F, D’Souza D (2005) Fault diagnosis using timed automata. In: FoSSaCS’05, vol 3441. LNCS, Edinburgh, pp 219-233 · Zbl 1118.68374
[6] Bryans J, Koutny M, Mazaré L, Ryan P Y A (2008) Opacity generalised to transition systems. Int J Inf Sec 7(6):421-435 · doi:10.1007/s10207-008-0058-x
[7] Cassandras CG, Lafortune S (1999) Introduction to discrete event systems. Springer · Zbl 0934.93001
[8] Cassez F (2009) The dark side of timed opacity. In: Proceedings of the 3rd international conference on information security and assurance (ISA’09), vol 5576. LNCS, Seoul, pp 21-30 · Zbl 1214.68242
[9] Cassez F, Dubreil J, Marchand H (2012) Synthesis of opaque systems with static and dynamic masks. Form 734Methods Syst Des 40(1):88-115 · Zbl 1247.68161
[10] Caucal D (2007) Deterministic graph grammars. In: Texts in logics and games 2, pp 169-250 · Zbl 1230.68121
[11] Caucal D, Hassen S (2008) Synchronization of grammars. In: Hirsch E, Razborov A, Semenov A, Slissenko A (eds) CSR, vol 5010. LNCS, Springer, pp 110-121 · Zbl 1142.68413
[12] Chédor S, Jéron T, Morvan C (2013) Test generation from recursive tile systems. Rapport de recherche RR-8206, INRIA. http://hal.inria.fr/hal-00778134 · Zbl 1354.68056
[13] Chédor S, Jéron T, Morvan C (2012) Test generation from recursive tiles systems. In: Brucker A, Julliand J (eds) 6th international conference on tests and proofs, vol 7305. LNCS, Prague, Czech Republic, pp 99-114. http://hal.inria.fr/hal-00743941, Prague, Czech Republic, p 99114 · Zbl 1354.68056
[14] Courcelle B (1990) Handbook of theoretical computer science, chap. Graph rewriting: an algebraic and logic approach. Elsevier · Zbl 1214.68242
[15] Dubreil J, Jéron T, Marchand H (2009) Monitoring confidentiality by diagnosis techniques. In: ECC. Budapest, Hungary, pp 2584-2590
[16] Hélouet L, Gazagnaire T, Genest B (2006) Diagnosis from scenarios. In: Proceedings of the 8th international workshop on discrete events systems, WODES’06, pp 307-312 · Zbl 1302.93147
[17] Hélouet L, Marchand H, Genest B, Gazagnaire T (2013) Diagnosis from scenarios, and applications. Discrete Event Dynamic Systems, Theory and Applications · Zbl 1302.93147
[18] Jéron T, Marchand H, Pinchinat S, Cordier M O (2006) Supervision patterns in discrete event systems diagnosis. In: WODES’06, pp 262-268
[19] Jiang S, Huang Z, Chandra V, Kumar R (2000) A polynomial algorithm for testing diagnosability of discrete event systems. IEEE Trans Autom Control 46: 1318-1321 · Zbl 1008.93053 · doi:10.1109/9.940942
[20] Kobayashi K, Hiraishi K (2013) Verification of opacity and diagnosability for pushdown systems. Journal of Applied Mathematics · Zbl 1266.93096
[21] Morvan C, Pinchinat S (2009) Diagnosability of pushdown systems. In: HVC2009, Haifa verification conference, vol 6405. LNCS, Haifa, pp 21-33 · Zbl 1272.93084
[22] Saboori A, Hadjicostis C (2008) Verification of initial-state opacity in security applications of des. In: 9th international workshop on discrete event systems, 2008. WODES 2008, pp 328-333
[23] Saboori A., Hadjicostis C.N. (2012) Verification of infinite-step opacity and complexity considerations. IEEE Trans Automat Contr 57(5):1265-1269 · Zbl 1369.93110 · doi:10.1109/TAC.2011.2173774
[24] Sampath M, Sengupta R, Lafortune S, Sinaamohideen K, Teneketzis D (1995) Diagnosability of discrete event systems. IEEE Trans Autom Control 40(9):1555-1575 · Zbl 0839.93072 · doi:10.1109/9.412626
[25] Sampath M, Sengupta R, Lafortune S, Sinaamohideen K, Teneketzis D (1996) Failure diagnosis using discrete event models. IEEE Trans Control Syst Technol 4 (2): 105-124 · doi:10.1109/87.486338
[26] Tripakis S (2002) Fault diagnosis for timed automata. In: Damm W, Olderog ER (eds) FTRTFT, vol 2469. LNCS, Springer, pp 205-224 · Zbl 1278.68140
[27] Ushio T, Onishi I, Okuda K (1998) Fault detection based on petri net models with faulty behaviors. IEEE Int Conf Syst Man Cybernet 1(1):113-118
[28] Wu YC, Lafortune S (2013) Comparative analysis of related notions of opacity in centralized and coordinated architectures. Discret Event Dyn Syst 23:307-339 · Zbl 1272.93084 · doi:10.1007/s10626-012-0145-z
[29] Yoo TS, Lafortune S (2002) Polynomial-time verification of diagnosability of partially-observed discrete event systems. IEEE Trans Autom Control 47(3):1491-1495 · Zbl 1364.93176
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.