A Translation of the Existential Model Checking Problem from MITL to HLTL

• Autorzy: Woźna-Szcześniak B. , Zbrzezny A.
• Języki publikacji: EN

Abstrakty

EN

In the paper we propose a translation of the existential model checking problemfor timed automata and properties expressible in MITL to the existential model checking problem for HLTL. Such a translation, for example, allows to adopt LTL bounded model checking method for verification of the MITL properties

Słowa kluczowe

EN

model checking; Timed Automata; Metric Interval Temporal Logic (MITL); MITL; translation from MITL to HLTL

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2013
• Tom: Vol. 122, nr 4
• Strony: 401--420
• Opis fizyczny: Bibliogr. 22 poz., rys.

Twórcy

autor

Woźna-Szcześniak B.

• IM&CS, Jan Długosz University Al. Armii Krajowej 13/15, 42-200 Cze¸stochowa, Poland

autor

Zbrzezny A.

• IM&CS, Jan Długosz University Al. Armii Krajowej 13/15, 42-200 Cze¸stochowa, Poland

Bibliografia

• [1] R. Alur, C. Courcoubetis, and D. Dill. Model checking in dense real-time. Information and Computation, 104(1):2–34, 1993.
• [2] R. Alur and D. Dill. Automata for modelling real-time systems. In Proceedings of the International Colloquium on Automata, Languages and Programming (ICALP’90), volume 443 of LNCS, pages 322–335. Springer-Verlag, 1990.
• [3] R. Alur, T. Feder, and T. Henzinger. The benefits of relaxing punctuality. Journal of the ACM, 43(1):116–146, 1996.
• [4] R. Alur and T. Henzinger. Logics and models of real time: A survey. In Proceedings of REX Workshop ‘Real Time: Theory and Practice’, volume 600 of LNCS, pages 74–106. Springer, 1992.
• [5] R. Alur and T. A. Henzinger. A really temporal logic. Journal of the ACM, 41(1):181–203, 1994.
• [6] J. C. M. Baeten and J. A. Bergstra. Real time process algebra. Formal Aspects of Computing, 3:142–188, 1991.
• [7] A. Biere, A. Cimatti, E. Clarke, O. Strichman, and Y. Zhu. Bounded model checking. In Highly Dependable Software, volume 58 of Advances in Computers. Academic Press, 2003. Pre-print.
• [8] P. Bouyer, N. Markey, J. Ouaknine, and J. Worrell. On expressiveness and complexity in real-time model checking. In Proceedings of the 35th International Colloquium on Automata, Languages and Programming, Part II (ICALP’08), volume 5126 of LNCS, pages 124–135. Springer, 2008.
• [9] E. M. Clarke and E. A. Emerson. Design and synthesis of synchronization skeletons using branching time temporal logic. In Proceedings of the Workshop on Logics of Programs, volume 131 of Lecture Notes in Computer Science, pages 52–71. Springer, 1981.
• [10] E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. The MIT Press, 1999.
• [11] C. Daws, A. Olivero, S. Tripakis, and S. Yovine. The tool KRONOS. In Hybrid Systems III, volume 1066 of LNCS, pages 208–219. Springer-Verlag, 1995.
• [12] P. Dembiński, A. Janowska, P. Janowski, W. Penczek, A. Pólrola, 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.
• [13] M. Felder, D. Mandrioli, and A. Morzenti. Proving properties of real-time systems through logical specifications and petri net models. IEEE Trans. Softw. Eng., 20(2):127–141, 1994.
• [14] R. Koymans. Specifying real-time properties with metric temporal logic. Real-Time Systems, 2(4):255–299, 1990.
• [15] O. Kupferman,M. Y. Vardi, and P. Wolper. An automata-theoretic approach to branching-time model checking. Journal of the ACM, 47(2):312–360, 2000.
• [16] K. G. Larsen, P. Pettersson, and W. Yi. UPPAAL: Status and developments. In Proceedings of the 9th International Conference on Computer Aided Verification (CAV’97), volume 1254 of LNCS, pages 456–459. Springer-Verlag, 1992.
• [17] D. Lepri, P. C. Őlveczky, and E. Ábrahám. Model Checking Classes of Metric LTL Properties of Object-Oriented Real-Time Maude Specifications. In Proceedings of the 1st International Workshop on Rewriting Techniques for Real-Time Systems, volume 36 of EPTCS, pages 117–136. Open Publishing Association, 2010.
• [18] O. Maler, D. Nickovic, and A. Pnueli. FromMITL to timed automata. In Proceedings of the 4th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS’06), volume 4202 of LNCS, pages 274–289. Springer, 2006.
• [19] J. Ouaknine and J. Worrell. On metric temporal logic and faulty turing machines. In Proceedings of the 9th International Conference on Foundations of Software Science and Computation Structures (FOSSACS’2006), volume 3921 of LNCS, pages 217–230. Springer-Verlag, 2006.
• [20] A. Pnueli. The Temporal Logic of Programs. In Proceedings of the 18th IEEE International Symposium on Foundations of Computer Science (FOCS’77), pages 46–57. IEEE Computer Society Presss, 1977.
• [21] A. P. Sistla and E. M. Clarke. The complexity of propositional linear temporal logic. Journal of the ACM, 32(3):733–749, 1985.
• [22] A. Zbrzezny. A new translation from ECTL* to SAT. In Proceedings of the International Workshop on Concurrency, Specification and Programming (CS&P’11), pages 589–600. Białystok University of Technology, 2011. http://csp2011.mimuw.edu.pl/proceedings/PDF/CSP2011589.pdf.