{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,18]],"date-time":"2026-08-18T15:25:53Z","timestamp":1787066753745,"version":"build-2736575974"},"reference-count":51,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2022,5,23]],"date-time":"2022-05-23T00:00:00Z","timestamp":1653264000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,5,23]],"date-time":"2022-05-23T00:00:00Z","timestamp":1653264000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/100005156","name":"Alexander von Humboldt-Stiftung","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100005156","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100006764","name":"Technische Universit\u00e4t Berlin","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100006764","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Discrete Event Dyn Syst"],"published-print":{"date-parts":[[2022,9]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    In this paper, by developing appropriate methods, we for the first time obtain characterization of four fundamental notions of detectability for general labeled weighted automata over monoids (denoted by\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$\\mathcal {A}^{\\mathfrak {M}}$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:msup>\n                            <mml:mrow>\n                              <mml:mi>A<\/mml:mi>\n                            <\/mml:mrow>\n                            <mml:mrow>\n                              <mml:mi>M<\/mml:mi>\n                            <\/mml:mrow>\n                          <\/mml:msup>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    for short), where the four notions are strong (periodic) detectability (SD and SPD) and weak (periodic) detectability (WD and WPD). The contributions of the current paper are as follows. Firstly, we formulate the notions of concurrent composition, observer, and detector for\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$\\mathcal {A}^{\\mathfrak {M}}$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:msup>\n                            <mml:mrow>\n                              <mml:mi>A<\/mml:mi>\n                            <\/mml:mrow>\n                            <mml:mrow>\n                              <mml:mi>M<\/mml:mi>\n                            <\/mml:mrow>\n                          <\/mml:msup>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    . Secondly, we use the concurrent composition to give a necessary and sufficient condition for SD, use the detector to give a necessary and sufficient condition for SPD, and use the observer to give necessary and sufficient conditions for WD and WPD, all for general\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$\\mathcal {A}^{\\mathfrak {M}}$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:msup>\n                            <mml:mrow>\n                              <mml:mi>A<\/mml:mi>\n                            <\/mml:mrow>\n                            <mml:mrow>\n                              <mml:mi>M<\/mml:mi>\n                            <\/mml:mrow>\n                          <\/mml:msup>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    without any assumption. Thirdly, we prove that for a labeled weighted automaton over monoid\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$(\\mathbb {Q}^{k},+)$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:mo>(<\/mml:mo>\n                          <mml:msup>\n                            <mml:mrow>\n                              <mml:mi>\u211a<\/mml:mi>\n                            <\/mml:mrow>\n                            <mml:mrow>\n                              <mml:mi>k<\/mml:mi>\n                            <\/mml:mrow>\n                          <\/mml:msup>\n                          <mml:mo>,<\/mml:mo>\n                          <mml:mo>+<\/mml:mo>\n                          <mml:mo>)<\/mml:mo>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    (denoted by\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$\\mathcal {A}^{\\mathbb {Q}^{k}}$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:msup>\n                            <mml:mrow>\n                              <mml:mi>A<\/mml:mi>\n                            <\/mml:mrow>\n                            <mml:mrow>\n                              <mml:msup>\n                                <mml:mrow>\n                                  <mml:mi>\u211a<\/mml:mi>\n                                <\/mml:mrow>\n                                <mml:mrow>\n                                  <mml:mi>k<\/mml:mi>\n                                <\/mml:mrow>\n                              <\/mml:msup>\n                            <\/mml:mrow>\n                          <\/mml:msup>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    ), its concurrent composition, observer, and detector can be computed in\n                    <jats:italic>N<\/jats:italic>\n                    <jats:italic>P<\/jats:italic>\n                    , 2-\n                    <jats:italic>E<\/jats:italic>\n                    <jats:italic>X<\/jats:italic>\n                    <jats:italic>P<\/jats:italic>\n                    <jats:italic>T<\/jats:italic>\n                    <jats:italic>I<\/jats:italic>\n                    <jats:italic>M<\/jats:italic>\n                    <jats:italic>E<\/jats:italic>\n                    , and 2-\n                    <jats:italic>E<\/jats:italic>\n                    <jats:italic>X<\/jats:italic>\n                    <jats:italic>P<\/jats:italic>\n                    <jats:italic>T<\/jats:italic>\n                    <jats:italic>I<\/jats:italic>\n                    <jats:italic>M<\/jats:italic>\n                    <jats:italic>E<\/jats:italic>\n                    , respectively, by developing novel connections between\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$\\mathcal {A}^{\\mathbb {Q}^{k}}$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:msup>\n                            <mml:mrow>\n                              <mml:mi>A<\/mml:mi>\n                            <\/mml:mrow>\n                            <mml:mrow>\n                              <mml:msup>\n                                <mml:mrow>\n                                  <mml:mi>\u211a<\/mml:mi>\n                                <\/mml:mrow>\n                                <mml:mrow>\n                                  <mml:mi>k<\/mml:mi>\n                                <\/mml:mrow>\n                              <\/mml:msup>\n                            <\/mml:mrow>\n                          <\/mml:msup>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    and the\n                    <jats:italic>N<\/jats:italic>\n                    <jats:italic>P<\/jats:italic>\n                    -complete exact path length problem (proven by [Nyk\u00e4nen and Ukkonen, 2002]) and a subclass of Presburger arithmetic. As a result, we prove that for\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$\\mathcal {A}^{\\mathbb {Q}^{k}}$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:msup>\n                            <mml:mrow>\n                              <mml:mi>A<\/mml:mi>\n                            <\/mml:mrow>\n                            <mml:mrow>\n                              <mml:msup>\n                                <mml:mrow>\n                                  <mml:mi>\u211a<\/mml:mi>\n                                <\/mml:mrow>\n                                <mml:mrow>\n                                  <mml:mi>k<\/mml:mi>\n                                <\/mml:mrow>\n                              <\/mml:msup>\n                            <\/mml:mrow>\n                          <\/mml:msup>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    , SD can be verified in\n                    <jats:italic>c<\/jats:italic>\n                    <jats:italic>o<\/jats:italic>\n                    <jats:italic>N<\/jats:italic>\n                    <jats:italic>P<\/jats:italic>\n                    , while SPD, WD, and WPD can be verified in 2-\n                    <jats:italic>E<\/jats:italic>\n                    <jats:italic>X<\/jats:italic>\n                    <jats:italic>P<\/jats:italic>\n                    <jats:italic>T<\/jats:italic>\n                    <jats:italic>I<\/jats:italic>\n                    <jats:italic>M<\/jats:italic>\n                    <jats:italic>E<\/jats:italic>\n                    . Particularly, for\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$\\mathcal {A}^{\\mathbb {Q}^{k}}$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:msup>\n                            <mml:mrow>\n                              <mml:mi>A<\/mml:mi>\n                            <\/mml:mrow>\n                            <mml:mrow>\n                              <mml:msup>\n                                <mml:mrow>\n                                  <mml:mi>\u211a<\/mml:mi>\n                                <\/mml:mrow>\n                                <mml:mrow>\n                                  <mml:mi>k<\/mml:mi>\n                                <\/mml:mrow>\n                              <\/mml:msup>\n                            <\/mml:mrow>\n                          <\/mml:msup>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    in which from every state, a distinct state can be reached through some unobservable, instantaneous path, detector\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$\\mathcal {A}^{\\mathbb {Q}^{k}}_{det}$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:msubsup>\n                            <mml:mrow>\n                              <mml:mi>A<\/mml:mi>\n                            <\/mml:mrow>\n                            <mml:mrow>\n                              <mml:mi>d<\/mml:mi>\n                              <mml:mi>e<\/mml:mi>\n                              <mml:mi>t<\/mml:mi>\n                            <\/mml:mrow>\n                            <mml:mrow>\n                              <mml:msup>\n                                <mml:mrow>\n                                  <mml:mi>\u211a<\/mml:mi>\n                                <\/mml:mrow>\n                                <mml:mrow>\n                                  <mml:mi>k<\/mml:mi>\n                                <\/mml:mrow>\n                              <\/mml:msup>\n                            <\/mml:mrow>\n                          <\/mml:msubsup>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    can be computed in\n                    <jats:italic>N<\/jats:italic>\n                    <jats:italic>P<\/jats:italic>\n                    , and SPD can be verified in\n                    <jats:italic>c<\/jats:italic>\n                    <jats:italic>o<\/jats:italic>\n                    <jats:italic>N<\/jats:italic>\n                    <jats:italic>P<\/jats:italic>\n                    . Finally, we prove that the problems of verifying SD and SPD of deterministic, deadlock-free, and divergence-free\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$\\mathcal {A}^{\\mathbb {N}}$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:msup>\n                            <mml:mrow>\n                              <mml:mi>A<\/mml:mi>\n                            <\/mml:mrow>\n                            <mml:mrow>\n                              <mml:mi>\u2115<\/mml:mi>\n                            <\/mml:mrow>\n                          <\/mml:msup>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    over monoid\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$(\\mathbb {N},+)$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:mo>(<\/mml:mo>\n                          <mml:mi>\u2115<\/mml:mi>\n                          <mml:mo>,<\/mml:mo>\n                          <mml:mo>+<\/mml:mo>\n                          <mml:mo>)<\/mml:mo>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    are both\n                    <jats:italic>c<\/jats:italic>\n                    <jats:italic>o<\/jats:italic>\n                    <jats:italic>N<\/jats:italic>\n                    <jats:italic>P<\/jats:italic>\n                    -hard. The original methods developed in this paper will provide foundations for characterizing other fundamental properties (e.g., diagnosability and opacity) in labeled weighted automata over monoids. In addition, in order to differentiate labeled weighted automata over monoids from labeled timed automata, we also initially explore detectability in labeled timed automata, and prove that the SD verification problem is\n                    <jats:italic>P<\/jats:italic>\n                    <jats:italic>S<\/jats:italic>\n                    <jats:italic>P<\/jats:italic>\n                    <jats:italic>A<\/jats:italic>\n                    <jats:italic>C<\/jats:italic>\n                    <jats:italic>E<\/jats:italic>\n                    -complete, while WD and WPD are undecidable.\n                  <\/jats:p>","DOI":"10.1007\/s10626-022-00362-8","type":"journal-article","created":{"date-parts":[[2022,5,23]],"date-time":"2022-05-23T05:04:58Z","timestamp":1653282298000},"page":"435-494","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":14,"title":["Detectability of labeled weighted automata over monoids"],"prefix":"10.1007","volume":"32","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9547-103X","authenticated-orcid":false,"given":"Kuize","family":"Zhang","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2022,5,23]]},"reference":[{"key":"362_CR1","doi-asserted-by":"crossref","unstructured":"Adams S, Ouaknine J, Worrell J (2007) Undecidability of universality for timed automata with minimal resources. In: Raskin J-F, Thiagarajan PS (eds) Formal modeling and analysis of timed systems. Springer, Berlin, pp 25\u201337","DOI":"10.1007\/978-3-540-75454-1_4"},{"issue":"2","key":"362_CR2","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur R, Dill DL (1994) A theory of timed automata. Theor Comput Sci 126(2):183\u2013235","journal-title":"Theor Comput Sci"},{"key":"362_CR3","doi-asserted-by":"crossref","unstructured":"Atig MF, Habermehl P (2009) On Yen\u2019s path logic for Petri nets. In: Bournez O, Potapov I (eds) Reachability Problems. Springer, Berlin, pp 51\u201363","DOI":"10.1007\/978-3-642-04420-5_7"},{"issue":"1","key":"362_CR4","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1016\/S0304-3975(01)00271-7","volume":"289","author":"M-P B\u00e9al","year":"2002","unstructured":"B\u00e9al M-P, Carton O (2002) Determinization of transducers over finite and infinite words. Theor Comput Sci 289(1):225\u2013251","journal-title":"Theor Comput Sci"},{"key":"362_CR5","doi-asserted-by":"crossref","unstructured":"Bouyer P, Chevalier F, D\u2019Souza D (2005) Fault diagnosis using timed automata. In: Proceedings of the 8th international conference on foundations of software science and computation structures, FOSSACS\u201905. Springer, Berlin, pp 219\u2013233","DOI":"10.1007\/978-3-540-31982-5_14"},{"key":"362_CR6","first-page":"226","volume":"1","author":"PE Caines","year":"1988","unstructured":"Caines PE, Greiner R, Wang S (1988) Dynamical logic observers for finite automata. Inproceedings of the 27th IEEE conference on decision and control 1:226\u2013233","journal-title":"Inproceedings of the 27th IEEE conference on decision and control"},{"issue":"1","key":"362_CR7","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1093\/imamci\/8.1.45","volume":"8","author":"PE Caines","year":"1991","unstructured":"Caines PE, Greiner R, Wang S (1991) Classical and logic-based dynamic observers for finite automata. IMA J Math Control Inform 8(1):45\u201380, 03","journal-title":"IMA J Math Control Inform"},{"key":"362_CR8","volume-title":"Introduction to discrete event systems","author":"CG Cassandras","year":"2010","unstructured":"Cassandras CG, Lafortune S (2010) Introduction to discrete event systems, 2nd edn. Springer Publishing Company, Incorporated, Berlin","edition":"2nd edn."},{"issue":"4","key":"362_CR9","first-page":"497","volume":"88","author":"F Cassez","year":"2008","unstructured":"Cassez F, Tripakis S (2008) Fault diagnosis with static and dynamic observers. Fundamenta Informaticae 88(4):497\u2013540","journal-title":"Fundamenta Informaticae"},{"key":"362_CR10","doi-asserted-by":"crossref","unstructured":"Cassez F (2009) The dark side of timed opacity. In: Park JH, Chen H-H, Atiquzzaman M, Lee C., Kim T-H, Yeo S-S (eds) Advances in information security and assurance. Springer, Berlin, pp 21\u201330","DOI":"10.1007\/978-3-642-02617-1_3"},{"issue":"7","key":"362_CR11","doi-asserted-by":"publisher","first-page":"1752","DOI":"10.1109\/TAC.2012.2183169","volume":"57","author":"F Cassez","year":"2012","unstructured":"Cassez F (2012) The complexity of codiagnosability for discrete event and timed systems. IEEE Trans Autom Control 57(7):1752\u20131764","journal-title":"IEEE Trans Autom Control"},{"key":"362_CR12","doi-asserted-by":"crossref","unstructured":"Daviaud L, Jecker I, Reynier P-A, Villevalois D (2017) Degree of sequentiality of weighted automata. In: Esparza J, Murawski AS (eds) Foundations of software science and computation structures. Springer, Berlin, pp 215\u2013230","DOI":"10.1007\/978-3-662-54458-7_13"},{"key":"362_CR13","first-page":"3","volume":"6","author":"C Dima","year":"2001","unstructured":"Dima C (2001) Real-time automata. J Automata Languages Combinatorics 6:3\u201324, 01","journal-title":"J Automata Languages Combinatorics"},{"key":"362_CR14","volume-title":"Computers and intractability: A guide to the theory of NP-completeness","author":"MR Garey","year":"1990","unstructured":"Garey MR, Johnson DS (1990) Computers and intractability: A guide to the theory of NP-completeness. W. H. Freeman & Co, USA"},{"issue":"9","key":"362_CR15","doi-asserted-by":"publisher","first-page":"1424","DOI":"10.1109\/TAC.2002.802769","volume":"47","author":"A Giua","year":"2002","unstructured":"Giua A, Seatzu C (2002) Observability of place\/transition nets. IEEE Trans Autom Control 47(9):1424\u20131437","journal-title":"IEEE Trans Autom Control"},{"issue":"3","key":"362_CR16","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1016\/0304-3975(88)90136-3","volume":"56","author":"E Gr\u00e4del","year":"1988","unstructured":"Gr\u00e4del E (1988) Subclasses of Presburger arithmetic and the polynomial-time hierarchy. Theor Comput Sci 56(3):289\u2013301","journal-title":"Theor Comput Sci"},{"key":"362_CR17","unstructured":"Hack M (1975) Petri net languages. Technical report, Cambridge, MA, USA"},{"key":"362_CR18","volume-title":"Estimation and Inference in discrete event systems communications and control engineering","author":"CN Hadjicostis","year":"2020","unstructured":"Hadjicostis CN (2020) Estimation and Inference in discrete event systems communications and control engineering. Springer Nature, Switzerland"},{"issue":"12","key":"362_CR19","doi-asserted-by":"publisher","first-page":"152","DOI":"10.1137\/0301010","volume":"1","author":"RE Kalman","year":"1963","unstructured":"Kalman RE (1963) Mathematical description of linear dynamical systems. J Soc Industrial Appl Math Ser A Control 1(12):152\u2013192","journal-title":"J Soc Industrial Appl Math Ser A Control"},{"key":"362_CR20","doi-asserted-by":"publisher","first-page":"192","DOI":"10.1016\/j.automatica.2017.08.027","volume":"86","author":"C Keroglou","year":"2017","unstructured":"Keroglou C, Hadjicostis CN (2017) Verification of detectability in probabilistic finite automata. Automatica 86:192\u2013198","journal-title":"Automatica"},{"key":"362_CR21","doi-asserted-by":"publisher","first-page":"294","DOI":"10.1016\/j.ins.2020.04.024","volume":"528","author":"H Lan","year":"2020","unstructured":"Lan H, Tong Y, Guo J, Seatzu C (2020) Verification of C-detectability using Petri nets. Inf Sci 528:294\u2013310","journal-title":"Inf Sci"},{"key":"362_CR22","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1016\/j.automatica.2019.03.003","volume":"105","author":"A Lai","year":"2019","unstructured":"Lai A, Lahaye S, Giua A (2019) State estimation of max-plus automata with unobservable events. Automatica 105:36\u201342","journal-title":"Automatica"},{"issue":"3","key":"362_CR23","doi-asserted-by":"publisher","first-page":"1437","DOI":"10.1109\/TAC.2020.2995173","volume":"66","author":"A Lai","year":"2021","unstructured":"Lai A, Lahaye S, Giua A (2021a) Verification of detectability for unambiguous weighted automata. IEEE Trans Autom Control 66(3):1437\u20131444","journal-title":"IEEE Trans Autom Control"},{"key":"362_CR24","doi-asserted-by":"crossref","unstructured":"Lai A, Lahaye S, Komenda J (2021b) Observer construction for polynomially ambiguous max-plus automata. IEEE Transactions on Automatic Control page online","DOI":"10.1109\/TAC.2021.3069899"},{"key":"362_CR25","doi-asserted-by":"crossref","unstructured":"Li J, Lefebvre D, Hadjicostis CN, Li Z (2021), Observers for a class of timed automata based on elapsed time graphs. IEEE Transactions on Automatic Control, page online","DOI":"10.1109\/TAC.2021.3064542"},{"key":"362_CR26","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1016\/j.automatica.2018.03.077","volume":"93","author":"T Masopust","year":"2018","unstructured":"Masopust T (2018) Complexity of deciding detectability in discrete event systems. Automatica 93:257\u2013261","journal-title":"Automatica"},{"key":"362_CR27","doi-asserted-by":"publisher","first-page":"238","DOI":"10.1016\/j.automatica.2019.02.058","volume":"104","author":"T Masopust","year":"2019","unstructured":"Masopust T, Yin X (2019) Deciding detectability for labeled Petri nets. Automatica 104:238\u2013241","journal-title":"Automatica"},{"key":"362_CR28","unstructured":"Mazar\u00e9 L. (2004) Using unification for opacity properties. In: Proceedings of the workshop on issues in the theory of security (WITS\u201904), pp. 165\u2013176"},{"key":"362_CR29","first-page":"129","volume":"34","author":"EF Moore","year":"1956","unstructured":"Moore EF (1956) Gedanken-experiments on sequential machines. Automata Studies, Annals of Math. Studies 34:129\u2013153","journal-title":"Automata Studies, Annals of Math. Studies"},{"issue":"1","key":"362_CR30","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1006\/jagm.2001.1201","volume":"42","author":"M Nyk\u00e4nen","year":"2002","unstructured":"Nyk\u00e4nen M., Ukkonen E (2002) The exact path length problem. J Algo 42(1):41\u201353","journal-title":"J Algo"},{"key":"362_CR31","doi-asserted-by":"crossref","unstructured":"Ouaknine J, Worrell J (2003) Universality and language inclusion for open and closed timed automata. In: Maler O, Pnueli A (eds) Hybrid systems: Computation and control. Springer, Berlin, pp 375\u2013388","DOI":"10.1007\/3-540-36580-X_28"},{"issue":"4","key":"362_CR32","doi-asserted-by":"publisher","first-page":"765","DOI":"10.1145\/322276.322287","volume":"28","author":"CH Papadimitriou","year":"1981","unstructured":"Papadimitriou CH (1981) On the complexity of integer programming. J ACM 28(4):765\u2013768","journal-title":"J ACM"},{"key":"362_CR33","volume-title":"Theory of linear and integer programming","author":"A Schrijver","year":"1986","unstructured":"Schrijver A (1986) Theory of linear and integer programming. Wiley, USA"},{"issue":"9","key":"362_CR34","doi-asserted-by":"publisher","first-page":"1555","DOI":"10.1109\/9.412626","volume":"40","author":"M Sampath","year":"1995","unstructured":"Sampath M, Sengupta R, Lafortune S, Sinnamohideen K, Teneketzis D (1995) Diagnosability of discrete-event systems. IEEE Trans Autom Control 40(9):1555\u20131575","journal-title":"IEEE Trans Autom Control"},{"key":"362_CR35","first-page":"5","volume-title":"Homing and Synchronizing Sequences","author":"S Sandberg","year":"2005","unstructured":"Sandberg S (2005) Homing and Synchronizing Sequences. Springer, Berlin, pp 5\u201333"},{"issue":"12","key":"362_CR36","doi-asserted-by":"publisher","first-page":"2356","DOI":"10.1109\/TAC.2007.910713","volume":"52","author":"S Shu","year":"2007","unstructured":"Shu S, Lin F, Ying H (2007) Detectability of discrete event systems. IEEE Trans Autom Control 52(12):2356\u20132359","journal-title":"IEEE Trans Autom Control"},{"issue":"5","key":"362_CR37","doi-asserted-by":"publisher","first-page":"310","DOI":"10.1016\/j.sysconle.2011.02.001","volume":"60","author":"S Shu","year":"2011","unstructured":"Shu S, Lin F (2011) Generalized detectability for discrete event systems. Systems & Control Letters 60(5):310\u2013317","journal-title":"Systems & Control Letters"},{"key":"362_CR38","volume-title":"Introduction to the theory of computation","author":"M Sipser","year":"1996","unstructured":"Sipser M (1996) Introduction to the theory of computation, 1st edn. International Thomson Publishing, Canada","edition":"1st edn."},{"key":"362_CR39","doi-asserted-by":"crossref","unstructured":"Tripakis S (2002) Fault diagnosis for timed automata. In: Damm W, Olderog ER (eds) Formal techniques in real-time and fault-tolerant systems. Springer, Berlin, pp 205\u2013221","DOI":"10.1007\/3-540-45739-9_14"},{"key":"362_CR40","doi-asserted-by":"crossref","unstructured":"Turing A (1936) On computable numbers, with an application to the Entscheidungsproblem. In: Proceedings of the london mathematical society, pp 230\u2013265","DOI":"10.1112\/plms\/s2-42.1.230"},{"key":"362_CR41","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-77452-7","volume-title":"Supervisory control of Discrete-Event systems","author":"WM Wonham","year":"2019","unstructured":"Wonham WM, Cai K (2019) Supervisory control of Discrete-Event systems. Springer International Publishing, Berlin"},{"issue":"1","key":"362_CR42","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1016\/0890-5401(92)90059-O","volume":"96","author":"HC Yen","year":"1992","unstructured":"Yen HC (1992) A unified approach for deciding the existence of certain Petri net paths. Inf Comput 96(1):119\u2013137","journal-title":"Inf Comput"},{"key":"362_CR43","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1016\/j.automatica.2017.02.032","volume":"80","author":"X Yin","year":"2017","unstructured":"Yin X (2017) Initial-state detectability of stochastic discrete-event systems with probabilistic sensor failures. Automatica 80:127\u2013134","journal-title":"Automatica"},{"issue":"6","key":"362_CR44","doi-asserted-by":"publisher","first-page":"3040","DOI":"10.1137\/140991285","volume":"54","author":"K Zhang","year":"2016","unstructured":"Zhang K, Zhang L, Su R (2016) A weighted pair graph representation for reconstructibility of Boolean control networks. SIAM J Control Optim 54 (6):3040\u20133060","journal-title":"SIAM J Control Optim"},{"key":"362_CR45","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1016\/j.automatica.2017.03.023","volume":"81","author":"K Zhang","year":"2017","unstructured":"Zhang K (2017) The problem of determining the weak (periodic) detectability of discrete event systems is PSPACE-complete. Automatica 81:217\u2013220","journal-title":"Automatica"},{"issue":"7","key":"362_CR46","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1016\/j.ifacol.2018.06.296","volume":"51","author":"K Zhang","year":"2018","unstructured":"Zhang K, Giua A (2018) Weak (approximate) detectability of labeled Petri net systems with inhibitor arcs. IFAC-PapersOnLine 51(7):167\u2013171. 14th IFAC Workshop on Discrete Event Systems WODES 2018","journal-title":"IFAC-PapersOnLine"},{"key":"362_CR47","doi-asserted-by":"crossref","unstructured":"Zhang K, Giua A (2019) K-delayed strong detectability of discrete-event systems. In: Proceedings of the 58th IEEE conference on decision and control (CDC), pp 7647\u20137652","DOI":"10.1109\/CDC40024.2019.9028873"},{"issue":"3","key":"362_CR48","doi-asserted-by":"publisher","first-page":"465","DOI":"10.1007\/s10626-020-00311-3","volume":"30","author":"K Zhang","year":"2020","unstructured":"Zhang K, Giua A (2020) On detectability of labeled Petri nets and finite automata. Discrete Event Dynamic Systems 30(3):465\u2013497","journal-title":"Discrete Event Dynamic Systems"},{"key":"362_CR49","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25972-3","volume-title":"Discrete-Time And Discrete-Space dynamical systems. Communications and control engineering","author":"K Zhang","year":"2020","unstructured":"Zhang K, Zhang L, Xie L (2020) Discrete-Time And Discrete-Space dynamical systems. Communications and control engineering. Springer International Publishing, Berlin"},{"key":"362_CR50","doi-asserted-by":"publisher","first-page":"339","DOI":"10.3233\/FI-2021-2062","volume":"181","author":"K Zhang","year":"2021","unstructured":"Zhang K (2021) A unified method to decentralized state detection and fault diagnosis\/prediction of discrete-event systems. Fundamenta Informaticae 181:339\u2013371","journal-title":"Fundamenta Informaticae"},{"key":"362_CR51","unstructured":"Zhang K (2021) State-Based Opacity of Real-Time Automata. In: Castillo-Ramirez A, Guillon P, Perrot K (eds) 27th IFIP WG 1.5 International Workshop on Cellular Automata and Discrete Complex Systems (AUTOMATA 2021), volume 90 of Open Access Series in Informatics (OASIcs), pp 12:1\u201312:15, Dagstuhl, Germany. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik"}],"container-title":["Discrete Event Dynamic Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10626-022-00362-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10626-022-00362-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10626-022-00362-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,9,9]],"date-time":"2022-09-09T09:29:59Z","timestamp":1662715799000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10626-022-00362-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,5,23]]},"references-count":51,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2022,9]]}},"alternative-id":["362"],"URL":"https:\/\/doi.org\/10.1007\/s10626-022-00362-8","relation":{},"ISSN":["0924-6703","1573-7594"],"issn-type":[{"value":"0924-6703","type":"print"},{"value":"1573-7594","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,5,23]]},"assertion":[{"value":"26 June 2020","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"25 February 2022","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"23 May 2022","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}