On Communicating Automata with Bounded Channels

• Autorzy: Genest B. , Kuske D. , Muscholl A.
• Języki publikacji: EN

Abstrakty

EN

We review the characterization of communicating finite-state machines whose behaviors have universally or existentially bounded channels. These results rely on the theory of Mazurkiewicz traces. We investigate the question whether channel bound conditions are decidable for a given communicating finite-state machine.

Słowa kluczowe

EN

communicating automata; Mazurkiewicz traces

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2007
• Tom: Vol. 80, nr 1-3
• Strony: 147--167
• Opis fizyczny: bibliogr. 32 poz.

Twórcy

autor

Genest B.

autor

Kuske D.

autor

Muscholl A.

• LaBRI, Universite Bordeaux I, 351 cours de la Liberation, F-33405 Talence, France,

Bibliografia

• [1] ITU-TS recommendation Z.120, Message Sequence Charts, Geneva, 1999.
• [2] Abdulla, P., Jonsson, B.: Undecidable Verification Problems for Programs with Unreliable Channels, Information and Computation, 130(1), 1996, 71-90.
• [3] Abdulla, P., Jonsson, B.: Verifying programs with unreliable channels, Information and Computation, 127(2), 1996, 91-101.
• [4] Alur, R., Yannakakis,M.: Model checking of message sequence charts, Proc. CONCUR'99, number 1664 in LNCS, Springer, Berlin, 1999.
• [5] Baier, C., Bertrand, N., Schnoebelen, P.: Symbolic verification of communicating systems with probabilistic message losses: liveness and fairness, Proc. FORTE'06, number 4229 in LNCS, Springer, Berlin, 2006.
• [6] Boigelot, B., Godefroid, P.: Symbolic Verification of Communication Protocols with Infinite State Spaces using QDDs, Formal Methods in System Design, 14(3), 1999, 237-255.
• [7] Boigelot, B., Godefroid, P., Willems, B., Wolper, P.: The Power of QDDs, Proc. SAS'97, number 1302 in LNCS, Springer, Berlin, 1997.
• [8] Bollig, B., Leucker, M.: Message-Passing Automata are expressively equivalent to EMSO Logic, Theoretical Computer Science, 358(2-3), 2006, 150-172.
• [9] Bouajjani, A., Habermehl, P.: Symbolic Reachability Analysis of FIFO-Channel Systems with Nonregular Sets of Configurations, Theoretical Computer Science, 221(1-2), 1999, 211-250.
• [10] Brand, D., Zafiropulo, P.: On communicating finite-state machines, Journal of the Association for Computing Machinery, 30(2), 1983, 323-342.
• [11] Cécé, G., Finkel, A.: Programs with quasi-stable channels are effectively recognizable, Proc. CAV'97, number 1254 in LNCS, Springer, Berlin, 1997.
• [12] Diekert, V., Rozenberg, G.: The Book of Traces, World Scientific, Singapore, 1995.
• [13] Ebinger,W., Muscholl, A.: Logical definability on infinite traces, Theoretical Computer Science, 154(1), 1996, 67-84.
• [14] Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere!, Theoretical Computer Science, 256(1-2), 2001, 63-92.
• [15] Genest, B., Kuske, D., Muscholl, A.: A Kleene Theorem and Model Checking for a Class of Communicating Automata, Information and Computation, 204(6), 2006, 920-956.
• [16] Genest, B., Muscholl, A., Seidl, H., Zeitoun, M.: Infinite-state High-level MSCs: Model checking and realizability, Journal of Computer and System Sciences, 72(4), 2006, 617-647.
• [17] Gunter, E., Muscholl, A., Peled, D.: Compositional Message Sequence Charts, International Journal on Software Tools for Technology Transfer, 5(1), 2003, 78-89.
• [18] Henriksen, J. G., Mukund, M., Narayan Kumar, K., Sohoni, M., Thiagarajan, P.: A Theory of Regular MSC Languages, Information and Computation, 202(1), 2005, 1-38.
• [19] Kosaraju, S.: Decidability of reachability in vector addition systems, Proc. STOC'82, ACM, 1982.
• [20] Kuske, D.: Regular sets of infinite message sequence charts, Information and Computation, 187(1), 2003, 80-109.
• [21] Leue, S., Mayr, R., Wei, W.: A scalable incomplete test for the boundedness of UML RT models, Proc. TACAS'04, number 2988 in LNCS, Springer, Berlin, 2004.
• [22] Lohrey, M., Muscholl, A.: Bounded MSC communication, Information and Computation, 189(2), 2004, 160-181.
• [23] Madhusudan, P.: Reasoning about Sequential and Branching Behaviours of Message Sequence Graphs, Proc. ICALP'01, number 2076 in LNCS, Springer, Berlin, 2001.
• [24] Madhusudan, P., Meenakshi, B.: Beyond Message Sequence Graphs, Proc. FSTTCS'01, number 2245 in LNCS, Springer, Berlin, 2001.
• [25] Mayr, E.: An algorithm for the general Petri net reachability problem., SIAM Journal on Computing, 13, 1984, 441-459.
• [26] Mazurkiewicz, A.: Concurrent Program Schemes and their Interpretations, DAIMI Rep. PB 78, Aarhus University, Aarhus, 1977.
• [27] Morin, R.: Recognizable Sets of Message Sequence Charts, Proc. STACS'02, number 2285 in LNCS, Springer, Berlin, 2002.
• [28] Muscholl, A., Peled, D.: Message sequence graphs and decision problems on Mazurkiewicz traces, Proc. MFCS'99, number 1672 in LNCS, Springer, Berlin, 1999.
• [29] Schnoebelen, P.: Verifying lossy channel systems has nonprimitive recursive complexity, Information Processing Letters, 583, 2002, 251-261.
• [30] Schnoebelen, P.: The Verification of Probabilistic Lossy Channel Systems, Validation of Stochastic Systems: A Guide to Current Research, number 2925 in LNCS, Springer, Berlin, 2004.
• [31] Thomas,W.: On logical definability of trace languages, Proc. Workshop of ESPRIT BRA No 3166: Algebraic and Syntactic Methods in Computer Science (ASMICS), Report TUM-I9002, Technical University of Munich, 1990.
• [32] Zielonka, W.: Notes on finite asynchronous automata, R.A.I.R.O. - Informatique Théorique et Applications, 21, 1987, 99-135.