ACTL* properties and Bounded Model Checking

• Autorzy: Woźna B.
• Języki publikacji: EN

Abstrakty

EN

The main contribution of the paper consists in showing that the bounded model checking (BMC) method is feasible for ACTL* (the universal fragment of CTLS) which subsumes both ACTL and LTL. The extension to ACTL* is obtained by redefining the function returning the sufficient number of executions over which an ACTL* formula is checked, and then combining the two known translations to SAT for ACTL and LTL formulas. The proposed translation of ACTL* formulas is essentially different from the existing translations of both ACTL and LTL formulas. Moreover, the formal treatment is the basis for the implementation of the technique in the symbolic model checker Verics.

Słowa kluczowe

EN

bounded model checking; logic ACTL; ECTL; bounded semantics; translation to SAT

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2004
• Tom: Vol. 63, nr 1
• Strony: 65--87
• Opis fizyczny: Bibliogr. 33 poz.

Twórcy

autor

Woźna B.

• Department of Computer Science, King's College London Strand. London WC2R 2LS, UK
• Institute of Mathematics and Computer Science. PU, Armii Krajowej 13/15, 42-200 Częstochowa, Poland

Bibliografia

• [1] Audemard. G., Cimatti. A., Kornilowicz, A.. Sebastiani. R.; Bounded Model Cheeking tor Timed Systems. Proc: of the 22nd Int. Conf. on Formal Techniques for Networked and Disiributed Systems {FORTE'02), LNCS 2529. Springer-Verlag. 2002.243-259.
• [2] Benedetti. M., Cimatti. A.: Bounded Model Checking for Past LTL. Proc. of the 9th Int. Conf on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'03), LNCS 2619. Springer-Verlag. 2(K)3. 18-33.
• [3] Bengtsson. J., Jonsson. B., Lilius. J., Yi, W.: Partial Order Reductions for Timed Systems. Proc. of the 9th Int. Conf on Concurrency Theory (C0NCUR'98). LNCS 1466, Springer-Verlag. 1998,485-500.
• [4] Biere. A., Cimatli. A., Clarke, E., M. Fujita., Zhu. Y.: Symbolic Model Checking Using SAT Procedures Instead of BDDs. Proc. of the ACM/IEEE Design Automation Conference (DAC 99 i, 1999.317-320.
• [5] Biere, A., Cimatti. A., Clarke. E., Zhu. Y.: Symbolic Model Checking without BDDs, Proc. of the 5th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'99), LNCS 1579, Springer-Verlag. 1999. 193-207.
• [6] Clarke. E., Biere, A., Raimi, R., Zhu, Y.: Bounded Model Checking Using Satisfiability Solving. Formal Methods in System Design, 19(1). 2001. 7-34.
• [7] Clarke, E. M., Grumberg. O., Peled, D.: Model Checking, MIT Press, 1999.
• [8] Dams, D., Grumberg. O., Gertb, R.: Abstract Interpretation of Reactive Systems: Abstractions Preserving ACTL*, ECTL' and CTL'. Proc. of the IFIP Working Conference on Programming Concepts, Methods and Calculi (PROCOMET’94)Esevier Science Publishers. 1994.
• [9] Daws, C., Tripakis, S.: Model Checking of Real-Time Reachability Properties Using Abstractions. Proc. of the 4th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'98) LNCSI 1384, Springer-Verlag. 1998. 313-329.
• [10] Dembiński, P., Janowska, A., Janowski, P., Penczek, W., Półrola, A., Szreter, M., Woźna, B., Zbrzezny, A.: VerlCS: A Tool for Verifying Timed Automata and Estelle Specifications. Proc. of the 9th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'O3}. LNCS 2619. Springer-Verlag. 2(M)3.278-283.
• [11] Emerson, E. A., Lei, C. L.: Modalities for Model Checking: Branching Time Logic Strikes Back. Proc. of the 12th ACM Symp. on Principles of Programming Languages, 1985, 84-96.
• [12] Emerso,. E. A., Sistia, A.P.: Symmetry and Model Checking, Formal Methods in System Design, 9, 1995. 105-131.
• [13] Gastin. P., Oddoux. D.: Fast LTL to Büchi Automata Translation, Proc. of the I3th Int. Conf. on Computer Aided Verification (CAVOI). LNCS 2102, Springer-Verlag. 2001, 53-65.
• [14] Grumberg, O., Long, D. E.: Model Checking and Modular Verification. Proc. of the 2nd Int. Conf. on Concurrency Theory (CONCUR’91), LNCS 527. Springer-Verlag. 1991. 250-265.
• [15] Heljanko, K.: Bounded Reachability Checking with Process Semantics, Proc. of the Int. Conf. on Concurrency Theory (CONCU’01l), LNCS 2154, Springer-Verlag. 2001.218-232.
• [16] Heljanko, K., Niemelii, I.: Bounded LTL Model Checking with Stable Models. Proc. of the 6th Int. Conf on Logic Programming and Nonmonotonic Reasoning (LPNMR’2001), LNCS 2173. Springer-Verlag. 2001, 200-212.
• [17] McMillan, K.L.: Symbolic Model Checking, Kluwer Academic Publishers, 1993.
• [18] de Moura, L.. Rueβ, H., Sorea, M.: Lazy Theorem Proving for Bounded Model Checking over Infinite Domains, Proc. of the 18th Inf. Conf. on Automated Deduction (CADE-18), LNCS 2392, Springer-Verlag. 2002,438-455.
• [19] Nieben. P., Mahfoudh, M., Asarin, E., Bozga, M., Maler. O., Jain, N.: Verification of Timed Automata via Satisfiability Checking. Proc. of the 7th Int. Symp. on Formal Techniques in Real-Time and Fault Tolerant Systems (FTRTFT'02), LNCS 2469, Springer-Verlag, 2002,226-243.
• [20] Pagani, F.: Partial Orders and Verification of Real-Time Systems, Proc. of the 4th Int. Symp. on Formal Techniques in Real Time and Fault Tolerant Systems (FTRTFT'96), LNCS I 135. Springer-Verlag, 1996, 327-346.
• [21] Peled, D.: Partial Order Reduction: Linear and Branching Temporal Logics and Process Algebras, Proc. of Partial Order Methods in Verification (POMIV'96), 29, Amen Math, Soc, 1996, 79-88.
• [22] Penczek, W., Półrola, A.: Abstractions and Partial Order Reductions for Checking Branching Properties of Time Petri Nets. Proc. of the 22nd Int. Conf. on Applications and Theory of Petri Nets (ICATPN'OI). LNCS 2075, Springer-Verlag, 2001, 323-342.
• [23] Penczek, W., Szreter, M., Gerth, R., Kuiper, R.: Improving Partial Order Reductions for Universal Branching Time Properties, Fundamenta Informaticae, 43, 2000, 245-267.
• [24] Penczek, W., Woźna. B., Zbrzezny, A.: Bounded Model Checking for the Universal Fragment of CTL, Fundamenta Informaticae, 51(1-2), 2002. 135-156.
• [25] Penczek, W., Woźna, B., Zbrzezny, A.: Towards Bounded Model Checking for the Universal Fragment of TCTL. Proc. of the 7th Int. Symp. on Formal Techniques in Real-Time and Fault Tolerant Systems (FTRTFT’02), LNCS 2469, Springer-Verlag, 2002. 265-288.
• [26] Sorea. M.: Bounded Model Checking for Timed Automata, Proc. of the 3rd Workshop on Models for Time-Critical Systems (MTCS'O2), 68{5). Elsevier Science Publishers, 2002.
• [27] Tripakis. S., Yovine, S.: Analysis of Timed Systems Using Time-Abstracting Bisimulations, Formal Methods in System Design. 18(1), 2001, 25-68.
• [28] Wolper, P., Godefroid. P.: Partial Order Methods for Temporal Verification, Proc. of the 4th Int. Conf on Concurrency Theory (CONCUR’93), LNCS 715, Springer-Verlag, 1993, 233-246.
• [29] Woźna, B., Penczek, W., Zbrzezny, A.: Reachability for Timed Systems Based on SAT-Solvers, Proc. of the Int. Workshop on Concurrency, Specification and Programming (CS&P'O2), 161(2). Humboldt University, 2002, 380-395.
• [30] Woźna, B., Zbrzezny. A.: Reaching the Limits for Bounded Model Checking, Technical Report 958, ICS PAS, Ordona 21. 01 - 237 Warsaw, May 2003.
• [31] Woźna. B., Zbrzezny, A.: Checking ACTL* Properties of Discrete Timed Automata via Bounded Model Checking, Proc. of the 1st Int. Workshop on Formal Analysis and Modeling of Timed Systems (FORMATS '03), LNCS 2791, Springer-Verlag. 2004. 18 - 33.
• [32] Woźna, B., Zbrzezny, A.: Checking ACTL' Properties of Discrete Timed Automata via Bounded Model Checking (Revi.sed version of the paper published in Proceedings of the 1st International Workshop on Formal Analysis and Modeling of Timed Systems (FORMATS'03)). Technical Report TR-04-04, Department of Computer Science. King's College London, April 2004.
• [33] Woźna, B., Zbrzezny, A., Penczek, W.: Checking Reachability Properties for Timed Automata via SAT. Fundamenta Informaticae. 55(2). 2003, 223-241.