Typical Paths of a Graph

• Autorzy: Cui C. , Dang Z. , Fischer T. R.
• Języki publikacji: EN

Abstrakty

EN

We introduce (finite and infinite) typical paths of a graph and prove that the typical paths carry all information with probability 1, asymptotically. An automata-theoretic characterization of the typical paths is shown: finite typical paths can be accepted by reversal-bounded multicounter automata and infinite typical paths can be accepted by counting B¨uchi automata (a generalization of reversal-bounded multicounter automata running on ů-words). We take a statechart example to show how to generate typical paths from a graph using SPIN model checker. The results are useful in automata theory since one can identify an information-concentrated-core of a regular language such that only words in the information-concentrated-core carry nontrivial information. When the graph is used to specify the system under test, the results are also useful in software testing by providing an information-theoretic approach to select test cases that carry nontrivial information of the system specification.

Słowa kluczowe

EN

graph; entropy; path

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2011
• Tom: Vol. 110, nr 1-4
• Strony: 95--109
• Opis fizyczny: Bibliogr. 18 poz.

Twórcy

autor

Cui C.

autor

Dang Z.

autor

Fischer T. R.

• School of Electrical Engineering and Computer Science, Washington State University, Pullman, WA 99164, USA,

Bibliografia

• [1] Ammann, P., Offutt, J.: Introduction to Software Testing, Cambridge University Press, 2008.
• [2] Beizer, B.: Software Testing Techniques, second edition, Van Nostrand Reinhold, 1990.
• [3] Chomsky, N., Miller, G. A.: Finite state languages, Information and Control, 1(2), 1958, 91-112.
• [4] Clarke, E. M., Grumberg, O., Peled, D. A.: Model Checking, MIT Press, 1999.
• [5] Cover, T. M., Thomas, J. A.: Elements of Information Theory, second edition,Wiley-Interscience, 2006.
• [6] Dang, Z., Ibarra, O. H.: On the existence of ω-chains for transitivemixed linear relations and its applications, International Journal of Foundations of Computer Science, 13(6), 2002, 911-936.
• [7] Dang, Z., Ibarra, O. H., Pietro, P. S.: Liveness verification of reversal-bounded multicounter machines with a free counter, FST TCS 2001: Foundations of Software Technology and Theoretical Computer Science (R. Hariharan, M. Mukund, V. Vinay, Eds.), LNCS 2245, Springer, Berlin, 2001.
• [8] Goodenough, J. B., Gerhart, S. L.: Toward a theory of test data selection, Proc. International Conference on Reliable Software, ACM, 1975.
• [9] Harel, D.: Statecharts: A visual formalism for complex systems, Sci. Comput. Program., 8(3), 1987, 231-274.
• [10] Holzmann, G. J.: The model checker SPIN, IEEE Transactions on Software Engineering, 23(5), 1997, 279-295.
• [11] Ibarra, O. H.: Reversal-bounded multicounter machines and their decision problems, J. ACM, 25(1), 1978, 116-133.
• [12] Ibarra, O. H., Dang, Z., Yang, L.: On counter machines, reachability problems, and Diophantine equations, Int. J. Found. Comput. Sci., 19(4), 2008, 919-934.
• [13] Pǎun, G.: Computing with membranes, J. Comput. Syst. Sci., 61(1), 2000, 108-143.
• [14] Thomas, W.: Automata on infinite objects, in: Handbook of Theoretical Computer Science: Formal Models and Semantics (J. Van Leeuwen, Ed.), MIT Press, 1990, 133-192.
• [15] Vardi, M. Y.: Probabilistic linear-time model checking: an overview of the automata-theoretic approach, Formal Methods for Real-Time and Probabilistic Systems (J. Katoen, Ed.), LNCS 1601, Springer, Berlin, 1999.
• [16] Yang, L., Dang, Z., Fischer, T. R.: Information gain of black-box testing, (To appear in Formal Aspects of Computing.).
• [17] Yang, L., Dang, Z., Fischer, T. R.: An information-theoretic complexity metric, Submitted, 2011.
• [18] Yeh, J.: Real Analysis: Theory of Measure and Integration, World Scientific,