Checking Reachability Properties for Timed Automata via SAT

• Autorzy: Woźna, B. , Penczek, W. , Zbrzezny, A.
• 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 to the depth k Î N and encoded as a prepositional formula. Next the desired property is translated to a prepositional formula and the satisfiability of the conjunction of the two above defined formulas is checked. The unfolding of the transition 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. Keywords : Reachability problem, bounded model checking, translation to SAT, Timed Automata, Augmented Region Graphs, discretization.

PL

Testowanie osiągalności automatów czasowych z wykorzystaniem SAT. Praca opisuje nowe podejście do problemu osiągalności dla automatów czasowych. Główna idea polega na połączeniu znanego algorytmu przeszukującego przestrzeń stanów wszerz metodą BFS oraz metody ograniczonej weryfikacji modelowej. Aby sprawdzić, czy stan spełniający daną własność jest osiągalny w modelu dla rozważanego automatu czasowego postępujemy następująco. Rozwijamy stopniowo relację przejścia dla automatu, aż do głębokości k Î N i kodujemy ją jako formułę zdaniową. Następnie, za pomocą formuły zdaniowej kodowana jest rozważana własność i sprawdzana jest spełnialność koniunkcji obydwu zdefiniowanych formuł zdaniowych. Rozwijanie relacji przejścia może zostać zakończone jeśli poszukiwany stan został znaleziony lub wszystkie stany danego automatu czasowego zostały przeszukane.

Słowa kluczowe

PL

problem osiągalności; ograniczona weryfikacja modelowa; translacja do SAT; automat czasowy; wzbogacony graf regionów; dyskretyzacja

EN

reachability problem; bounded model checking; translation to SAT; Timed Automata; Augmented Region Graphs; discretization

• Czasopismo: Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk
• Rocznik: 2002
• Tom: Nr 949
• Strony: 1-19
• Opis fizyczny: Bibliogr. 30 poz., rys.

Twórcy

autor

Woźna, B.

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

autor

Penczek, W.

• Institute of Computer Science, PAS, Ordona 21, 01-237 Warsaw, Poland,

autor

Zbrzezny, A.

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

Bibliografia

• [ABC+02] 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 the 18th Int. Conf. on Automated Deduction (CADE’02), volume 2392 of LNCS. Springer-Verlag, 2002.
• [ABE00] P. A. Abdulla, P. Bjesse, and N. Een. Symbolic reachability analysis based on SAT-solvers. In Proc. of TACAS’OO, volume 1785 of LNCS, pages 411-425. Springer-Verlag, 2000.
• [ABK 97] E. Asarin, M. Bozga, A. Kerbrat, O. Maler, A. Pnueli, and A. Rasse. Data-structures for the verification of Timed Automata. In Proc. of Int. Workshop on Hybrid and Real-Time Systems (HART’97), volume 1201 of LNCS, pages 346-360. Springer-Verlag, 1997.
• [ACD 92] R. Alur, C. Courcoubetis, D. Dill, N. Halbwaclis, 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), pages 157-166. IEEE Comp. Soc. Press, 1992.
• [ACD93] R. Alur, C. Courcoubetis, and D. Dill. Model checking in dense real-time. Information and Computation 104(l):2-34, 1993.
• [ACKS02] G. Audemard, A. Cimatti, A. Kornilowicz, and R. Sebastiani. Bounded model checking for timed systems. In Proc. of the 2nd Workshop on Real-Time Tools (RT-TOOLS’02), 2002. to appear.
• [AD90] R. Alur and D. Dill. Automata for modelling real-time systems. In Proc. of the International Colloquium on Automata, Languages and Programming (ICALP’90), volume 443 of LNCS, pages 322-335 Springer-Verlae 1990.
• [AD94] R. Alur and D. Dill. A theory of Timed Automata. Theoretical Computer Science, 126(2):183 - 235, 1994.
• [BCCZ99] A. Biere, A. Cimatti, E. Claxke, and Y. Zhu. Symbolic model checking without BDDs. In Proc. of TACAS’99, volume 1579 of LNCS, pages 193-207. Springer-Verlag, 1999.
• [BTY97] A. Bouajjani, S. Tripakis, and S. Yovine. On-the-fly symbolic model checking for real-time systems. In Proc. of the 18th IEEE Real-Time Systems Symposium (RTSS’97), pages 232 - 243. IEEE Comp. Soc. Press, 1997.
• [dMRS02] L. de Moura, H. Ruefl, and M. Sorea. Lazy theorem proving for bounded model checking over infinite domains. In Proc. of the 18th Int. Conf. on Automated Deduction (CADE’02), volume 2392 of LNCS. Springer-Verlag, 2002.
• [DPP01] P. Dembiński, W. Penczek, and A. Półrola. Automated verification of infinite state concurrent systems: an improvement in model generation. In Proc. of the Ąth Int. Conf. on Parallel Processing and Applied Mathematics (PPAM’01), volume 2328 of LNCS, pages 247-255. Springer-Verlag, 2001.
• [DT98] C. Daws and S. Tripakis. Model checking of real-time reachability properties using abstractions. In Proc. of TACAS’98, volume 1384 of LNCS, pages 313-329. Springer-Verlag, 1998.
• [HelOl] K. Heljanko. Bounded reachability checking with process semantics. In Proc. of CONCUR’Ol, volume 2154 of LNCS, pages 218-232. Springer-Verlag, 2001.
• [KL96] 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.
• [KLK96] I. Kang, I. Lee, and Y. S. Kim. A state minimization technique for Timed Automata. In Proc. of Int. Workshop on Verification of Infinite State Systems (INFINITY’96), August 1996.
• [LLPY97] 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 Comp. Soc. Press, 1997.
• [MMZ+01] M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, and S. Malik. Chaff: Engineering an efficient SAT solver. In Proc. of the 38th Design Automation Conference (DAC01), pages 530-535, June 2001.
• [NMA+02] P. Niebert, M. Mahfoudh, E. Asarin, M. Bozga, O. Maler, and N. Jain. Verification of Timed Automata via Satisfiability Checking. In Proc. of the 7th Int. Symp. on Formal Techniques in Real-Time and Fault Tolerant Systems (FTRTFT’02), volume 2469 of LNCS, pages 226-243. Springer-Verlag, 2002.
• [NTY00] P. Niebert, S. Tripakis, and S. Yovine. Minimum-time reachability for Timed Automata. In Proc. of the 8th IEEE Mediterranean Conf. on Control and Automation (MED’2000), Patros, Greece, July 2000. IEEE Comp. Soc. Press.
• [PWZ02a] 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.
• [PWZ02b] W. Penczek, B. Woźna, and A. Zbrzezny. SAT-Based Bounded Model Checking for the Universal Fragment of TCTL. Technical Report 947, ICS PAS, Ordona 21, 01 - 237 Warsaw, September 2002.
• [PWZ02c] W. Penczek, B. Woźna, and A. Zbrzezny. Towards bounded model checking for the universal fragment of TCTL. In Proc. of the 7th Int. Symp. on Formal Techniques in Real-Time and Fault Tolerant Systems (FTRTFT’02), volume 2469 of LNCS, pages 265-288. Springer-Verlag, 2002.
• [SebOl] R. Sebastiani. Integrating SAT solvers with math reasoners: Foundations and basic algorithms. Technical Report 0111-22, ITC-IRST, Sommarive 16, 38050 Povo, Trento, Italy, November 2001.
• [Sor02] Maria Sorea. Bounded modePchecking for timed automata. In Proc. of the Third Workshop on Models for Time-Critical Systems (MTCS’02); affiliated with CONCUR 2002., volume 68(5) of Electronic Notes in Theoretical Computer Science. Elsevier Science Publishers, 2002.
• [SSS00] M. Sheeran, S. Singh, and G. Stalmarck. Checking safety properties using induction and a SAT-solver. In Proc. of the Int. Conf. on Formal Methods in Computer-Aided Design (FMCAD’00), volume 1954 of LNCS, pages 108-125. Springer-Verlag, 2000.
• [Tri98] S. Tripakis. Minimization of timed systems, http://verimag.imag.fr/~tripakis/dea.ps.gz, 1998.
• [Tri99] S. Tripakis. Timed diagnostic for reachability properties. In Proc. of TACAS’99, volume 1579 of LNCS, pages 59-73. Springer-Verlag, 1999.
• [TY01] S. Tripakis and S. Yovine. Analysis of timed systems using time-abstracting bisimulations. Formal Methods in System Design, 18(1):25—68, 2001.
• [Yov97] S. Yovine. Model checking Timed Automata. In Embedded Systems, volume 1494 of LNCS, pages 114-152. Springer-Verlag, 1997.