Reachability Analysis for Timed Automata Using Partitioning Algorithms

• Autorzy: Półrola A. , Penczek W. , Szreter M.
• Języki publikacji: EN

Abstrakty

EN

The paper presents a new method for checking reachability properties of Timed Automata. The idea consists in on-the-fly verification of a property on a pseudo-bisimulating model generated by a modified partitioning algorithm. Pseudo-bisimulating models are often much smaller than forward-reachability graphs commonly used in reachability analysis. A theoretical description of the algorithm is supported by several experimental results.

Słowa kluczowe

EN

Timed Automata; pseudo-bisimulating models; pb-models

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2003
• Tom: Vol. 55, nr 2
• Strony: 203--221
• Opis fizyczny: bibliogr. 20 poz.

Twórcy

autor

Półrola A.

autor

Penczek W.

autor

Szreter M.

• Faculty of Mathematics, University of Lodz, Banacha 22, 90-238 Lodz, Poland,

Bibliografia

• [1] Alur, R., Courcoubetis, C., Dill, D., Halbwachs, N., Wong-Toi, H.: An Implementation of Three Algorithms for Timing Verification Based on Automata Emptiness, Proc. of the 13th IEEE Real-Time Systems Symposium (RTSS’92), IEEE Comp. Soc. Press, 1992, 157-166.
• [2] Alur, R., Courcoubetis, C., Dill, D., Halbwachs, N., Wong-Toi, H.: Minimization of Timed Transition Systems, Proc. of CONCUR’92, LNCS 630, Springer-Verlag, 1992, 340-354.
• [3] Audemard, G., Cimatti, A., Kornilowicz, A., Sebastiani, R.: Bounded Model Checking for Timed Systems, Technical Report 0201-05, ITC-IRST, Sommarive 16, 38050 Povo, Trento, Italy, January 2002.
• [4] Beyer, D.: Improvements in BDD-based Reachability Analysis of Timed Automata, Proc. of Int. Symp. of Formal Methods Europe (FME’01), LNCS 2021, Springer-Verlag, 2002, 318-343.
• [5] Bouajjani, A., Fernandez, J.-C., Halbwachs, N., Raymond, P., Ratel, C.: Minimal State Graph Generation, Science of Computer Programming, 18, 1992, 247-269.
• [6] Bouajjani, A., Tripakis, S., Yovine, S.: On-the-Fly Symbolic Model Checking for Real-Time Systems, Proc. of the 18th IEEE Real-Time Systems Symposium (RTSS’97), IEEE Comp. Soc. Press, 1997, 232-243.
• [7] Daws, C., Tripakis, S.: Model Checking of Real-Time Reachability Properties Using Abstractions, Proc. of the Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’98), LNCS 1384, Springer-Verlag, 1998, 313-329.
• [8] Dembiński, P., Janowska, A., Janowski, P., Penczek, W., Półrola, A., Szreter, M., Wźona, B., Zbrzezny, A.: VerICS: A Tool for Verifying Timed Automata and Estelle Specifications, Proc. of the 9th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’03), LNCS 2619, Springer-Verlag, 2003, 278-283.
• [9] Kang, I., Lee, I.: An Efficient State Space Generation for the Analysis of Real-Time Systems, Proc. of Int. Symposium on Software Testing and Analysis, 1996.
• [10] Larsen, K. G., Larsson, F., Pettersson, P., Yi, W.: Efficient Verification of Real-Time Systems: Compact Data Structures and State-Space Reduction, Proc. of the 18th IEEE Real-Time System Symposium (RTSS’97), IEEE Comp. Soc. Press, 1997, 14-24.
• [11] Niebert, P., Tripakis, S., Yovine, S.: Minimum-Time Reachability for Timed Automata, Proc. of the 8th IEEE Mediterranean Conf. on Control and Automation (MED’2000), IEEE Comp. Soc. Press, Patros, Greece, July 2000.
• [12] Penczek, W., Woźna, B., Zbrzezny, A.: Towards Bounded Model Checking for the Universal Fragment of TCTL, Proc. of the 7th Int. Symp. on Formal Techniques in Real-Time and Fault Tolerant Systems (FTRTFT’02), LNCS 2469, Springer-Verlag, 2002, 265-288.
• [13] Pnueli, A.: The Temporal Logic of Programs, Proc. of the 18th Int. Symp. Foundations of Computer Science (FOCS’77), 1977, 46-57.
• [14] Półrola, A., Penczek, W., Szreter, M.: Towards Refining Partitioning for Checking Reachability in Timed Automata, Proc. of the Int. Workshop on Concurrency, Specification and Programming (CS&P’02), 161(2), Humboldt University, 2002, 278-291.
• [15] Półrola, A., Penczek, W., Szreter, M.: Reachability Analysis for Timed Automata Based on Partitioning, Technical report, ICS PAS, Ordona 21, 01-237 Warsaw, 2003. To appear
• [16] Tripakis, S., Yovine, S.: Analysis of Timed Systems Based on Time-Abstracting Bisimulations, Proc. Of CAV’96, LNCS 1102, Springer-Verlag, 1996, 232-243.
• [17] Tripakis, S., Yovine, S.: Analysis of Timed Systems Using Time-Abstracting Bisimulations, Formal Methods in System Design, 18(1), 2001, 25-68.
• [18] Woźna, B., Penczek, W., Zbrzezny, A.: Checking Reachability Properties for Timed Automata via SAT, Technical Report 949, ICS PAS, Ordona 21, 01 - 237 Warsaw, October 2002.
• [19] Woźna, B., Penczek, W., Zbrzezny, A.: Reachability for Timed Systems Based on SAT-Solvers, Proc. of the Int. Workshop on Concurrency, Specification and Programming (CS&P’02), 161(2), Humboldt University, 2002, 380-395.
• [20] Yovine, S.: KRONOS: A Verification Tool for Real-Time Systems, Springer International Journal of Software Tools for Technology Transfer, 1(1/2), 1997, 123-133.