PL EN


Preferencje help
Widoczny [Schowaj] Abstrakt
Liczba wyników
Tytuł artykułu

Checking MTL Properties of Discrete Timed Automata via Bounded Model Checking

Wybrane pełne teksty z tego czasopisma
Identyfikatory
Warianty tytułu
Języki publikacji
EN
Abstrakty
EN
We investigate a SAT-based bounded model checking (BMC) method for MTL (metric temporal logic) that is interpreted over linear discrete infinite time models generated by discrete timed automata. In particular, we translate the existential model checking problem for MTL to the existential model checking problem for a variant of linear temporal logic (called HLTL), and we provide a SAT-based BMC technique for HLTL. We show how to implement the BMC technique for HLTL and discrete timed automata, and as a case study we apply the technique in the analysis of GTPP, a Generic Timed Pipeline Paradigm modelled by a network of discrete timed automata.
Wydawca
Rocznik
Strony
553--568
Opis fizyczny
Bibliogr. 30 poz., rys.
Twórcy
  • IM&CS, Jan Długosz University, Al. Armii Krajowej 13/15, 42-200 Częstochowa, Poland
autor
  • IM&CS, Jan Długosz University, Al. Armii Krajowej 13/15, 42-200 Częstochowa, Poland
Bibliografia
  • [1] P. A. Abdulla, P. Bjesse, and N. Eén. Symbolic reachability analysis based on SAT-solvers. In Proceedings of TACAS’00, volume 1785 of LNCS, pages 411–425. Springer, 2000.
  • [2] R. Alur, R. Brayton, T. A. Henzinger, S. Qadeer, and S. Ramajani. Partial order reduction in symbolic state-space exploration. In Proceedings of CAV’97, volume 1254 of LNCS, pages 340–351. Springer, 1997.
  • [3] R. Alur and D. Dill. A theory of Timed Automata. Theoretical Computer Science, 126(2):183–235, 1994.
  • [4] R. Alur, T. Feder, and T. Henzinger. The benefits of relaxing punctuality. Journal of the ACM, 43(1):116–146, 1996.
  • [5] R. Alur and T. A. Henzinger. A really temporal logic. Journal of the ACM, 41(1):181–203, 1994.
  • [6] R. Alur and T. A. Henzinger. Real-time logics: complexity and expressiveness. Information and computation, 104: 390–401, 1993.
  • [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, pages 118–149. Academic Press, 2003.
  • [8] J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang. Symbolic model checking: 1020 states and beyond. Information and Computation, 98(2):142–170, 1992.
  • [9] S. Campos and E. Clarke. Real-time symbolic model checking for discrete time models. Theories and experiences for real-time system development, volume 2 of AMAST, pages 129–145. World Scientific, 1994.
  • [10] E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. The MIT Press, 1999.
  • [11] E. M. Clarke, D. E. Long, and K. L. McMillan. Compositional model checking. In Proceedings of LICS’89, pages 353–362. IEEE Computer Society, 1989.
  • [12] D. Dams, R. Gerth, B. Knaack, and R. Kuiper. Partial-order reduction techniques for real-time model checking. In Proceedings of the FMICS’98, pages 157–169, 1998.
  • [13] E. A. Emerson, A.K. Mok, A. P. Sistla, and J. Srinivasan. Quantitative temporal reasoning. Real-Time Systems, 4(4):331–352, December 1992.
  • [14] M. Felder, D. Mandrioli, and A. Morzenti. Proving Properties of Real-Time Systems Through Logical Specifications and Petri Net Models. IEEE Transaction on Software Engineering, 20(2):127–141, 1994.
  • [15] C. A. Furia and P. Spoletini. Tomorrow and all our yesterdays: MTL satisfiability over the integers. In Proceedings of ICTAC’2008, volume 5160 of LNCS, pages 253–264. Springer, 2008.
  • [16] G. J. Holzmann. SPIN Model Checker, The: Primer and Reference Manual. Addison Wesley Professional, 2003.
  • [17] R. Koymans. Specifying real-time properties with metric temporal logic. Real-Time Systems, 2(4):255–299, 1990.
  • [18] 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.
  • [19] 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 RTRTS’2010, volume 36 of EPTCS, pages 117–136, 2010.
  • [20] A. Lomuscio, W. Penczek, and B. Woźna. Bounded model checking for knowledge and real time. Artificial Intelligence, 171:1011–1038, 2007.
  • [21] O. Maler, D. Nickovic, and A. Pnueli. From MITL to timed automata. In Proceedings of FORMATS’2006, volume 4202 of LNCS, pages 274–289. Springer, 2006.
  • [22] D. Peled. All from one, one for all: on model checking using representatives. In Proceedings of CAV’93, volume 697 of LNCS, pages 409–423. Springer, 1993.
  • [23] W. Penczek, B. Woźna, and A. Zbrzezny. Bounded model checking for the universal fragment of CTL. Fundamenta Informaticae, 51(1-2):135–156, 2002.
  • [24] M. Pradella, A. Morzenti, and P. San Pietro. The symmetry of the past and of the future: bi-infinite time in the verification of temporal properties. In Proceedings of ESEC-FSE’2007, pages 312–320. ACM, 2007.
  • [25] M. Pradella, A. Morzenti, and P. San Pietro. A metric encoding for bounded model checking. In Proceedings of FM’2009, volume 5850 of LNCS, pages 741–756. Springer, 2009.
  • [26] M. R. and C. A. Furia. A Theory of Sampling for Continuous-time Metric Temporal Logic. ACM Transactions on Computational logic, 12(1):8:1–8:40, 2010.
  • [27] A. P. Sistla and E. M. Clarke. The complexity of propositional linear temporal logic. Journal of the ACM, 32(3):733–749, 1985.
  • [28] B. Woźna and A. Zbrzezny. Checking ACTL* properties of discrete timed automata via bounded model checking. In Proceedings of FORMATS’03, volume 2791 of LNCS, pages 18–33. Springer, 2004.
  • [29] B. Woźna-Szcześniak and A. Zbrzezny. A translation of the existential model checking problem from MITL to HLTL. Fundamenta Informaticae, 122(4):401–420, 2013.
  • [30] A. Zbrzezny. A new translation from ECTL* to SAT. Fundamenta Informaticae, 120(3–4):377–397, 2012.
Typ dokumentu
Bibliografia
Identyfikator YADDA
bwmeta1.element.baztech-d016c491-e2a2-4e49-a891-4f920ca62eb3
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.