Universality Analysis for One-Clock Timed Automata

• Autorzy: Abdulla P.A. , Deneux J. , Ouaknine J. , Quaas K. , Worrell J.
• Języki publikacji: EN

Abstrakty

EN

This paper is concerned with the universality problem for timed automata: given a timed automaton A, does A accept all timed words? Alur and Dill have shown that the universality problem is undecidable if A has two clocks, but they left open the status of the problem when A has a single clock. In this paper we close this gap for timed automata over infinite words by showing that the one-clock universality problem is undecidable. For timed automata over finite words we show that the one-clock universality problem is decidable with non-primitive recursive complexity. This reveals a surprising divergence between the theory of timed automata over finite words and over infinite words. We also show that if ε-transitions or non-singular postconditions are allowed, then the one-clock universality problem is undecidable over both finite and infinite words. Furthermore, we present a zone-based algorithm for solving the universality problem for single-clock timed automata. We apply the theory of better quasi-orderings, a refinement of the theory of well quasi-orderings, to prove termination of the algorithm. We have implemented a prototype tool based on our method, and checked universality for a number of timed automata. Comparisons with a region-based prototype tool confirm that zones are a more succinct representation, and hence allow a much more efficient implementation of the universality algorithm.

Słowa kluczowe

EN

Timed Automata

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2008
• Tom: Vol. 89, nr 4
• Strony: 419--450
• Opis fizyczny: bibliogr. 38 poz., tab.

Twórcy

autor

Abdulla P.A.

autor

Deneux J.

autor

Ouaknine J.

autor

Quaas K.

autor

Worrell J.

• Uppsala University, Dag Hammarskjölds v. 10 B 75105 Uppsala, Sweden,

Bibliografia

• [1] Abdulla, P. A., Čerãns, K., Jonsson, B., Tsay, Y.-K.: Algorithmic Analysis of Programs with Well Quasi- Ordered Domains, Information and Computation, 160, 2000, 109-127.
• [2] Abdulla, P. A., Deneux, J., Ouaknine, J., Worrell, J.: Decidability and Complexity Results for Timed Automata via Channel Machines, Proc. ICALP '05, 32nd International Colloquium on Automata, Languages, and Programming, 3580, 2005.
• [3] Abdulla, P. A., Henda, N. B., Delzanno, G., Rezine, A.: Regular Model Checking without Transducers (On Efficient Verification of Parameterized Systems), Proc. TACAS '07, 13th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, 4424, Springer Verlag, 2007.
• [4] Abdulla, P. A., Jonsson, B.: Undecidable Verification Problems for Programs with Unreliable Channels, Information and Computation, 130(1), 1996, 71-90.
• [5] Abdulla, P. A., Jonsson, B.: Verifying Programs with Unreliable Channels, Information and Computation, 127(2), 1996, 91-101.
• [6] Abdulla, P. A., Jonsson, B.: Verifying Networks of Timed Processes, Proc. TACAS '98, 4th Int. Conf. On Tools and Algorithms for the Construction and Analysis of Systems (B. Steffen, Ed.), 1384, 1998.
• [7] Abdulla, P. A., Nylén, A.: Better is Better than Well: On Efficient Verification of Infinite-State Systems, Proc. LICS '00, 16th IEEE Int. Symp. on Logic in Computer Science, 2000.
• [8] Abdulla, P. A., Nylén, A.: Timed Petri Nets and BQOs, Proc. ICATPN'2001: 22nd Int. Conf. on application and theory of Petri nets, 2075, 2001.
• [9] Abdulla, P. A., Ouaknine, J., Quaas, K., Worrell, J.: Zone-Based Universality Analysis for Single-Clock Timed Automata, Proc. of FSEN 2007, IPM International Symposium on Fundamentals of Software Engineering, 4767, 2007.
• [10] Alur, R., Dill, D.: A Theory of Timed Automata, Theoretical Computer Science, 126, 1994, 183-235.
• [11] Alur, R., Feder, T., Henzinger, T.: The Benefits of Relaxing Punctually, Journal of the ACM, 43, 1996, 116-146.
• [12] Alur, R., Fix, L., Henzinger, T.: Event-clock automata: A determinizable class of timed automata, Theoretical Computer Science, 211, 1999, 253-273.
• [13] Alur, R., Henzinge, T.: Real-Time Logics: Complexity and Expressiveness, Information and Computation, 104(1), 1993, 35-77.
• [14] Alur, R., Madhusudan, P.: Decision problems for timed automata: A survey, 4th Intl. School on Formal Methods for Computer, Communication, and Software Systems: Real Time, 3185, 2004.
• [15] Alur, R., Torre, S. L., Madhusudan, P.: Perturbed Timed Automata, Proc. HSCC 05, 3414, 2005.
• [16] Bouyer, P.: Forward Analysis of Updatable Timed Automata, Formal Methods in System Design, 24(3), 2004, 281-320.
• [17] Bouyer, P., Dufourd, C., Fleury, E., Petit, A.: Updatable Timed Automata, Theoretical Computer Science, 321(2-3), 2004, 291-345.
• [18] Bouyer, P., Markey, N., Ouaknine, J., Worrell, J.: The Cost of Punctuality, Proceedings of the 22nd Annual IEEE Symposium on Logic in Computer Science (LICS'07), IEEE Computer Society Press, Wrocław, Poland, July 2007.
• [19] Cécé, G., Finkel, A., Iyer, S. P.: Unreliable Channels Are Easier to Verify Than Perfect Channels, Information and Computation, 124(1), 10 January 1996, 20-31.
• [20] Cormen, T., Leiserson, C., Rivest, R., Stein, C.: Introduction to Algorithms, MIT Press, McGraw-Hill, 2001.
• [21] Dill, D.: Timing Assumptions and Verification of Finite-State Concurrent Systems, Automatic Verification Methods for Finite-State Systems, 407, 1989.
• [22] Finkel, A., Schnoebelen, P.: Well-Structured Transition Systems Everywhere, Technical Report LSV-98-4, Ecole Normale Supérieure de Cachan, April 1998.
• [23] Henzinger, T., Manna, Z., Pnueli, A.: What Good are Digital Clocks?, Proc. ICALP '92, 623, 1992.
• [24] Henzinger, T. A., Kopke, P.W., Puri, A., Varaiya, P.: What's Decidable about Hybrid Automata?, J. Comput. Syst. Sci., 57(1), 1998, 94-124.
• [25] Laroussinie, F., Markey, N., Schnoebelen, P.: Model Checking Timed Automata with One or Two Clocks, Proc. CONCUR 2004, 15th Int. Conf. on Concurrency Theory, 3170, 2004.
• [26] Larsen, K., Pettersson, P., Yi, W.: UPPAAL in a Nutshell, Software Tools for Technology Transfer, 1(1-2), 1997.
• [27] Lasota, S., Walukiewicz, I.: Alternating Timed Automata, Proc. FOSSACS, 3441, 2005.
• [28] Lasota, S., Walukiewicz, I.: Alternating Timed Automata, ACM Trans. on Computational Logic, 2007, To appear.
• [29] Marcone, A.: Foundations of BQO Theory, Transactions of the American Mathematical Society, 345(2), 1994.
• [30] Mayr, R.: Undecidable Problems in Unreliable Computations, Theoretical Informatics (LATIN'2000), number 1776 in Lecture Notes in Computer Science, 2000.
• [31] Møller, J., Lichtenberg, J.: Difference Decision Diagrams, Master Thesis, Department of Information Technology, Technical University of Denmark, Building 344, DK-2800 Lyngby, Denmark, August 1998.
• [32] Niebert, P., Mahfoudh, M., Asarin, E., Bozga, M., Jain, N., Maler, O.: Verification of Timed Automata via Satisfiability Checking, FTRTFT'02, 7th Int. Symp. on Formal Techniques in Real-Time and Fault Tolerant Systems, 2469, 2002.
• [33] Ouaknine, J., Worrell, J.: Universality and Language Inclusion for Open and Closed Timed Automata, Proc. HSCC 03, 2623, 2003.
• [34] Ouaknine, J., Worrell, J.: On the Language Inclusion Problem for Timed Automata: Closing a Decidability Gap, Proc. LICS '04, 20th IEEE Int. Symp. on Logic in Computer Science, 2004.
• [35] Ouaknine, J., Worrell, J.: On the decidability of Metric Temporal Logic, Proc. 19th Annual Symp. on Logic in Computer Science (LICS'05), IEEE Comp. Soc. Press, 2005.
• [36] Schnoebelen, Ph.: Verifying Lossy Channel Systems has Nonprimitive Recursive Complexity, Information Processing Letters, 83(5), 2002, 251-261.
• [37] Thomson, B. S., Bruckner, J. B., Bruckner, A. M.: Elementary Real Analysis, Prentice Hall, 2001.
• [38] Yovine, S.: Kronos: A verification tool for real-time systems, Journal of Software Tools for Technology Transfer, 1(1-2), 1997.