Improvements in SAT-based Reachability Analysis for Timed Automata

• Autorzy: Zbrzezny A.
• Języki publikacji: EN

Abstrakty

EN

The paper deals with the problem of checking reachability for timed automata. In order to check reachability of a state satisfying some property, first the transition relation of a timed automaton is unfolded iteratively to some depth and encoded as a propositional formula. Next, the property is translated to a propositional formula and 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. In this paper we propose some improvements of the encoding of the transition relation for timed automata. The improvements are partially based on a new discretization scheme. The efficiency of the improved encoding is strongly supported by the experimental results. We also introduce a method for checking unreachability.

Słowa kluczowe

EN

machine theory; mathematical formulas; robotics; algorithms

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2004
• Tom: Vol. 60, nr 1-4
• Strony: 417--434
• Opis fizyczny: Bibliogr. 33 poz.

Twórcy

autor

Zbrzezny A.

• 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én. Symbolic reachability analysis based on SAT-solvers. In Proc. of TACAS '00. vol. 1785 of LNCS. pp. 411-425. 2000.
• [2] R. Alur. Timed automata. Proc. of CAV'99. vol. 1633 of LNCS, pp. 8-22
• [3] R. Alur and D. Dill. A theory of Timed Automata. Theoretical Computer Science, 126(2), pp. 183-235. 1994.
• [4] R. Alur, C. Courcoubetis, D. Dill, N. Halbwachs, and H. Wong-Toi. An Implementation of Three Algorithms for Timing Verification Based on Automata Emptiness. In Proc. of the 13th IEEE Real-Time Systems Symposium (RTSS'92), pp. 157-166, IEEE Comp. Soc. Press, 1992.
• [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. Cimatli, 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] D. Beyer. Improvements in BDD-based reachability analysis of Timed Automata. In Proc. of FME'01, vol. 2021 of LNCS. Springer-Verlag, 2002.
• [9] A. Biere. A. Cimatti, E. Clarke. M.Fujita, and Y. Zhu. Symbolic model checking using SAT procedures instead of BDDs. In Proc. of DAC'99. 1999.
• [10] 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.
• [11] A. Biere. A. Cimatti, E. M. Clarke, O. Strichman and Y. Zhu. Bounded Model Checking. In vol. 58 of Advances in Computers. Academic Press, 2003.
• [12] 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.
• [13] 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.
• [14] 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. ofTACAS’03, vol. 2619 of LNCS, Springer-Verlag, 2003.
• [15] P. Dembiński. W. Penczek, and A. Pół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.
• [16] C. Daws, A. Olivero, S. Tripakis, and S. Yovine. The Tool Kronos. "Hybrid Systems III", vol. 1066 of LNCS, pp. 208-219. Springer-Verlag. 2003.
• [17] E. Goldberg, Y. Novikov. BerkMin: a Fast and Robust Sat-Solver. presented at Design Automation & Test I Europe DATE 2002.2002.
• [18] A.Göllü and A. Puri and P. Varaiya. Discretization of timed automata. In Proc. of 33rd CDC, 1994.
• [19] K. Heljanko. Bounded reachability checking with process semantics. In Proc. of CONCUR'OI, vol. 2154 of LNCS. pp. 218-232. Springer-Verlag. 2001.
• [20] 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.
• [21] I. Kang, I. Lee, and Y. S. Kim. A state minimization technique for Timed Automata. In Proc. ofINF/NITY'96, August 1996.
• [22] 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.
• [23] 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.
• [24] P. Niebert. S. Tripakis, and S. Yovine. Minimum-time reachability for Timed Automata. In Proc. of MED ’00, July 2000. IEEE Comp. Soc. Press.
• [25] W. Penczek. B. Woźna, and A. Zbrzezny. Bounded model checking for the universal fragment of CTL. Fundamenta Informaticae, 51 (1-2): 135-156, June 2002.
• [26] W. Penczek, B. Woźna, 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.
• [27] M. Sheeran, S. Singh, and G. Stalmarck. Checking safety properties using induction and a SAT-solver. In Proc. of FMC AD'00, vol. 1954 of LNCS, pp. 108-125. Springer-Verlag, 2000.
• [28] Maria Sorea. Bounded model checking for timed automata. In Proc. of MTCS’02, vol. 68(5) of ENTCS. Elsevier Science Publishers, 2002.
• [29] S. Tripakis. Timed diagnostic for reachability properties. In Proc. of TACAS'99, vol. 1579 of LNCS, pp. 59-73. Springer-Verlag, 1999.
• [30] S. Tripakis and S. Yovine. Analysis of timed systems using time-abstracting bisimulations. Formal Methods in System Design, 18(1):25-68, 2001.
• [31] B. Woźna, A. Zbrzezny, and W. Penczek. Checking Reachability Properties for Timed Automata via SAT. Fundamenta Informaticae, 55(2):223-241, 2003.
• [32] S. Yovine. Model checking Timed Automata. In Embedded Systems, vol. 1494 of LNCS, pp. 1 14-152. Springer-Verlag, 1997.
• [33] A. Zbrzezny. Improvements in SAT-based Reachability Analysis for Timed Automata. In Proc. of the Int. Workshop on Concurrency, Specification and Programming (CS&P'03), 2003, 606-619.