Path Compression in Timed Automata

• Autorzy: Janowska A. , Penczek W.
• Języki publikacji: EN

Abstrakty

EN

The paper presents a method of abstraction for timed systems. To extract an abstract model of a timed system we propose to use static analysis, namely a technique called path compression. The idea behind the path compression consists in identifying a path (or a set of paths) on which a process executes a sequence of transitions that do not influence a property being verified, and replacing this path with a single transition. The method is property driven since it depends on a formula in question. The abstraction is exact with respect to all the properties expressible in the temporal logic CTL*-X.

Słowa kluczowe

EN

path compression; Timed Automata

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2007
• Tom: Vol. 79, nr 3-4
• Strony: 379--399
• Opis fizyczny: bibliogr. 27 poz., tab.

Twórcy

autor

Janowska A.

autor

Penczek W.

• Institute of Informatics Warsaw University ul. Banacha 2 02-097 Warsaw, Poland,

Bibliografia

• [1] R Alur and D Dill. Automata for modelling real-time systems. In Proc. of the Int. Colloquium on Automata, Languages and Programming (ICALP'90), volume 443 of LNCS, pages 322-335. Springer-Verlag, 1990.
• [2] G. Behrmann, P. Bouyer, E. Fleury, and K. Larsen. Static guard analysis in timed automata verification. In Proc. of the 9th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'03), volume 2619 of LNCS, pages 254-277. Springer-Verlag, 2003.
• [3] G. Behrmann, A. David, and K. G. Larsen. A tutorial on Uppaal. In Formal Methods for the Design of Real-Time Systems (SFM-RT'04), volume 3185 of LNCS, pages 200-236. Springer-Verlag, 2004.
• [4] J. Bengtsson, B. Jonsson, J. Lilius, and W. Yi. Partial order reductions for timed systems. In Proc. of the 9th Int. Conf. on Concurrency Theory (CONCUR'98), volume 1466 of LNCS, pages 485-500. Springer-Verlag, 1998.
• [5] J. Bengtsson andW. Yi. Timed automata: Semantics, algorithms and tools. In Lecture Notes on Concurrency and Petri Nets, volume 3098 of LNCS. Springer-Verlag, 2004.
• [6] V. Braberman, D. Garbervetsky, and A. Olivero. Improving the verification of timed systems using influence information. In Proc. of Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'02), volume 2280 of LNCS, pages 21-36. Springer-Verlag, 2002.
• [7] M. C. Browne, E. Clarke, and O. Grumberg. Characterizing finite Kripke structures in propositional temporal logic. Theoretical Computer Science, 59(1/2):115-131, 1988.
• [8] T. H. Cormen, C. E. Leiserson, R. L. Rivest, and C. Stein. Introduction to Algorithms. MIT Press, 2001.
• [9] D. Dams, O. Grumberg, and R. Gerth. Abstract interpretation of reactive systems: Abstractions preserving ACTL_, ECTL_ and CTL_. In Proc. of the IFIP Working Conference on Programming Concepts, Methods and Calculi (PROCOMET'94). Elsevier, 1994.
• [10] C. Daws and S. Tripakis. Model checking of real-time reachability properties using abstractions. In Proc. Of the 4th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'98), volume 1384 of LNCS, pages 313-329. Springer-Verlag, 1998.
• [11] C. Daws and S. Yovine. Two examples of verification of multirate timed automata with kronos. In Proc. Of the 16th IEEE Real-Time Systems Symposium (RTSS'95), pages 66-75, 1995.
• [12] C. Daws and S. Yovine. Reducing the number of clock variables of timed automata. In Proc. of the IEEE Real-Time Systems Symposium (RTSS'96), pages 73-81. IEEE Computer Society, 1996.
• [13] P. Dembiński, A. Janowska, P. Janowski, W. Penczek, A. Półrola, M. Szreter, B. Woźna, and A. Zbrzezny. VerICS: A tool for verifying timed automata and Estelle specifications. In Proc. of the 9th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'03), volume 2619 of LNCS, pages 278-283. Springer-Verlag, 2003.
• [14] T. Henzinger, P.-H. Ho, and H. Wong-Toi. HYTECH: A model checker for hybrid systems. International Journal on Software Tools for Technology Transfer, 1(1-2):110-122, 1997.
• [15] T. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic model checking for real-time systems. Information and Computation, 111(2):193-244, 1994.
• [16] A. Janowska and P. Janowski. Slicing timed automata with discrete data. Fundamenta Informaticae, 72(1-3):181-195, 2006.
• [17] A. Janowska and W. Penczek. Static path compression in timed systems. In Proc. of the Int. Workshop on Concurrency, Specification and Programming (CS&P'06), volume 206(3) of Informatik-Berichte, pages 340-351. Humboldt University, 2006.
• [18] R. Jhala and R. Majumdar. Path slicing. In Proceedings of the ACM SIGPLAN conference on Programming language design and implementation (PLDI'05), pages 38-47, 2005.
• [19] J. Krákora and Z. Hanzálek. Timed automata approach for CAN verification. In 11th IFAC Symposium on Information Control Problems in Manufacturing. Elsevier, 2004.
• [20] K. G. Larsen, F. Larsson, P. Pettersson, and W. Yi. Efficient verification of real-time systems: Compact data structures and state-space reduction. In Proc. of the 18th IEEE Real-Time System Symposium (RTSS'97), pages 14-24. IEEE Computer Society, 1997.
• [21] K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.
• [22] P. Pettersson and K. G. Larsen. UPPAAL2k. Bulletin of the European Association for Theoretical Computer Science, 70:40-44, February 2000.
• [23] A. Półrola and A. Zbrzezny. Sat-based reachability checking for timed automata with discrete data. In Proc. of the Int. Workshop on Concurency, Specification and Programming (CSP'06), volume 206(2) of Informatik Berichte, pages 207-218. Humboldt University, 2006.
• [24] A. Valmari. The state explosion problem. In Lecture Notes on Petri Nets I: Basic Models. Advances in Petri Nets, volume 1491 of LNCS. Springer-Verlag, 1998.
• [25] M. Weiser. Program slicing. IEEE Trans. on Software Eng., 10(4), 1984.
• [26] K. Yorav and O. Grumberg. Static analysis for state-space reductions preserving temporal logics. Form. Methods Syst. Des., 25(1):67-96, 2004.
• [27] H. Zheng, E.Mercer, and C.Myers. Modular verification of timed circuits using automatic abstraction. IEEE Trans. on CAD of Integrated Circuits and Systems, 22(9):1138-1153, 2003.