Checking Reachability Properties for Timed Automata via SAT

• Autorzy: Woźna, B. , Zbrzezny, A. , Penczek, W.
• Języki publikacji: EN

Abstrakty

EN

The paper deals with the problem of checking reachability for timed automata. The main idea consists in combining the well-know forward reachability algorithm and the Bounded Model Checking (BMC) method. In order to check reachability of a state satisfying some desired property, first the transition relation of a timed automaton is unfolded iteratively to some depth and encoded as a propositional formula. Next, the desired property is translated to a propositional formula and the satisfiability of the conjunction of the two defined above formulas is checked. The unfolding of the transition relation can be terminated when either a state satisfying the property has been found or all the states of the timed automaton have been searched. The efficiency of the method is strongly supported by the experimental results.

Słowa kluczowe

EN

Timed Automata; bounded model checking

• Czasopismo: Fundamenta Informaticae
• Rocznik: 2003
• Tom: Vol. 55, nr 2
• Strony: 223-241
• Opis fizyczny: bibliogr. 32 poz.

Twórcy

autor

Woźna, B.

autor

Zbrzezny, A.

autor

Penczek, W.

• Institute of mathematics and Computer Science, PU, Armii Krajowej 13/15, 42-200 Częstochowa, Poland,

Bibliografia

• [1] P. A. Abdulla, P. Bjesse, and N. E´en. Symbolic reachability analysis based on SAT-solvers. In Proc. of TACAS’00, vol. 1785 of LNCS, pp. 411-425. 2000.
• [2] R. Alur, C. Courcoubetis, and D. Dill. Model checking in dense real-time. Information and Computation, 104(1):2-34, 1993.
• [3] R. Alur and D. Dill. Automata for modelling real-time systems. In Proc. of ICALP’90, vol. 443 of LNCS, pp. 322-335. Springer-Verlag, 1990.
• [4] R. Alur and D. Dill. A theory of Timed Automata. Theoretical Computer Science, 126(2):183 - 235, 1994.
• [5] E. Asarin, M. Bozga, A. Kerbrat, O. Maler, A. Pnueli, and A. Rasse. Data-structures for the verification of Timed Automata. In Proc. of HART’97, vol. 1201 of LNCS, pp. 346-360. Springer-Verlag, 1997.
• [6] G. Audemard, P. Bertoli, A. Cimatti, A. Kornilowicz, and R. Sebastiani. A SAT based approach for solving formulas over boolean and linear mathematical propositions. In Proc. of CADE’02, vol. 2392 of LNCS. Springer-Verlag, 2002.
• [7] G. Audemard, A. Cimatti, A. Kornilowicz, and R. Sebastiani. Bounded model checking for timed systems. In Proc. of RT-TOOLS’02, 2002.
• [8] A. Biere, A. Cimatti, E. Clarke, and Y. Zhu. Symbolic model checking without BDDs. In Proc. of TACAS’99, vol. 1579 of LNCS, pp. 193-207. 1999.
• [9] A. Bouajjani, S. Tripakis, and S. Yovine. On-the-fly symbolic model checking for real-time systems. In Proc. of RTSS’97, pp. 232-243. IEEE Comp. Soc. Press, 1997.
• [10] Davis, M., Logemann, G., Loveland, D.: A machine program for theorem proving, Communications of the ACM, 5, 1962, 394-397.
• [11] C. Daws and S. Tripakis. Model checking of real-time reachability properties using abstractions. In Proc. of TACAS’98, vol. 1384 of LNCS, pp. 313-329. 1998.
• [12] L. de Moura, H. Rueß, and M. Sorea. Lazy theorem proving for bounded model checking over infinite domains. In Proc. of CADE’02, vol. 2392 of LNCS. 2002.
• [13] P. Dembi´nski, W. Penczek, and A. P´ołrola. Automated verification of infinite state concurrent systems: an improvement in model generation. In Proc. of PPAM’01, vol. 2328 of LNCS, pp. 247-255. Springer-Verlag, 2001.
• [14] K. Heljanko. Bounded reachability checking with process semantics. In Proc. of CONCUR’01, vol. 2154 of LNCS, pp. 218-232. Springer-Verlag, 2001.
• [15] I. Kang and I. Lee. An efficient state space generation for the analysis of real-time systems. In Proc. of Int. Symposium on Software Testing and Analysis, 1996.
• [16] I. Kang, I. Lee, and Y. S. Kim. A state minimization technique for Timed Automata. In Proc. of INFINITY’96, August 1996.
• [17] 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 RTSS’97, pp. 14-24. IEEE Comp. Soc. Press, 1997.
• [18] M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, and S. Malik. Chaff: Engineering an efficient SAT solver. In Proc. of DAC’01, pp. 530-535, June 2001.
• [19] P. Niebert, M. Mahfoudh, E. Asarin, M. Bozga, O. Maler, and N. Jain. Verification of Timed Automata via Satisfiability Checking. In Proc. of FTRTFT’02, vol. 2469 of LNCS, pp. 226-243. Springer-Verlag, 2002.
• [20] P. Niebert, S. Tripakis, and S. Yovine. Minimum-time reachability for Timed Automata. In Proc. of MED’00, July 2000. IEEE Comp. Soc. Press.
• [21] W. Penczek, B. Wo´zna, and A. Zbrzezny. Bounded model checking for the universal fragment of CTL. Fundamenta Informaticae, 51(1-2):135-156, June 2002.
• [22] W. Penczek, B. Wo´zna, and A. Zbrzezny. SAT-Based Bounded Model Checking for the Universal Fragment of TCTL. Report 947, ICS PAS, Warsaw, September 2002.
• [23] W. Penczek, B. Wo´zna, and A. Zbrzezny. Towards bounded model checking for the universal fragment of TCTL. In Proc. of FTRTFT’02, vol. 2469 of LNCS, pp. 265-288. Springer-Verlag, 2002.
• [24] R. Sebastiani. Integrating SAT solvers with math reasoners: Foundations and basic algorithms. Technical Report 0111-22, ITC-IRST, Trento, Italy, November 2001.
• [25] M. Sheeran, S. Singh, and G. Stalmarck. Checking safety properties using induction and a SAT-solver. In Proc. of FMCAD’00, vol. 1954 of LNCS, pp. 108-125. Springer-Verlag, 2000.
• [26] Maria Sorea. Bounded model checking for timed automata. In Proc. of MTCS’02, vol. 68(5) of ENTCS. Elsevier Science Publishers, 2002.
• [27] S. Tripakis. Minimization of timed systems. http://verimag.imag.fr/tripakis/dea.ps.gz, 1998.
• [28] S. Tripakis. Timed diagnostic for reachability properties. In Proc. of TACAS’99, vol. 1579 of LNCS, pp. 59-73. Springer-Verlag, 1999.
• [29] S. Tripakis and S. Yovine. Analysis of timed systems using time-abstracting bisimulations. Formal Methods in System Design, 18(1):25-68, 2001.
• [30] B. Woźna, W. Penczek, and A. Zbrzezny. Checking Reachability Properties for Timed Automata via SAT. Report 949 ICS PAS, Warsaw, October 2002.
• [31] S. Yovine. Model checking Timed Automata. In Embedded Systems, vol. 1494 of LNCS, pp. 114-152. Springer-Verlag, 1997.
• [32] Zhang, H.: SATO: An Efficient Propositional Prover, Proc. of the Int. Conf. on Automated Deduction (CADE’97), 1249, Springer-Verlag, 1997, pp. 272-275.