Bounded Model Checking for the Existential Fragment of TCTL-G and Diagonal Timed Automata

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

Abstrakty

EN

Bounded Model Checking (BMC) is one of the well known SAT based symbolic model checking techniques. It consists in searching for a counterexample of a particular length, and generating a propositional formula that is satisfiable iff such a counterexample exists. The BMC method is feasible for the various classes of temporal logic; in particular it is feasible for TECTL (the existential fragment of Time Computation Tree Logic) and Diagonal-free Timed Automata. The main contribution of the paper is to show that the concept of Bounded Model Checking can be extended to deal with TECTL-G properties of Diagonal Timed Automata. We have implemented our new BMC algorithm, and we present preliminary experimental results, which demonstrate the efficiency of the method.

Słowa kluczowe

EN

bounded model checking; diagonal timed automata

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2007
• Tom: Vol. 79, nr 1-2
• Strony: 229--256
• Opis fizyczny: bibliogr. 37 poz., tab.

Twórcy

autor

Woźna B.

autor

Zbrzezny A.

• Institute of Mathematics and Computer Science, Jan Długosz University, Armii Krajowej 13/15, 42-200 Częstochowa, Poland,

Bibliografia

• [1] Alur, R., Courcoubetis, C., Dill, D.: Model Checking in Dense Real-Time, Information and Computation, 104(1), 1993, 2-34.
• [2] Alur, R., Dill, D.: A Theory of Timed Automata, Theoretical Computer Science, 126(2), 1994, 183-235.
• [3] Alur, R., Feder, T., Henzinger, T.: The Benefits of Relaxing Punctuality, Journal of the ACM, 43(1), 1996, 116-146.
• [4] Alur, R., Madhusudan, P.: Decision Problems for Timed Automata: A Survey, Formal Methods for the Design of Real-Time Systems, 3185, Springer Berlin / Heidelberg, 2004, ISBN 978-3-540-23068-7.
• [5] Biere, A., Cimatti, A., Clarke, E., Fujita, M., Zhu, Y.: Symbolic Model Checking Using SAT Procedures Instead of BDDs, Proceedings of the ACM/IEEE Design Automation Conference (DAC'99), 1999.
• [6] Bouajjani, A., Tripakis, S., Yovine, S.: On-the-Fly Symbolic Model Checking for Real-Time Systems, Proceedings of the 18th IEEE Real-Time Systems Symposium (RTSS'97), IEEE Computer Society, 1997.
• [7] Bryant, R.: Graph-Based Algorithms for Boolean Function Manipulation, IEEE Transaction on Computers, 35(8), 1986, 677-691.
• [8] Clarke, E. M., Grumberg, O., Peled, D. A.: Model Checking, The MIT Press, Cambridge, Massachusetts, 1999, ISBN 0-262-03270-8.
• [9] Dams, D., Gerth, R., Knaack, B., Kuiper, R.: Partial-Order Reduction Techniques for Real-Time Model Checking, Proceedings of the 3rd InternationalWorkshop on FormalMethods for Industrial Critical Systems, 1998.
• [10] Dams, D., Grumberg, O., Gerth, R.: Abstract Interpretation of Reactive Systems: Abstractions Preserving ACTL_, ECTL_ and CTL_, Proceedings of the IFIP Working Conference on Programming Concepts, Methods and Calculi (PROCOMET'94), Elsevier Science Publishers, 1994.
• [11] Daws, C., Tripakis, S.: Model Checking of Real-Time Reachability Properties Using Abstractions, Proceedings of the 4th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'98), 1384, Springer-Verlag, 1998.
• [12] Dembiński, P., Penczek, W., Pólrola, A.: Automated Verification of Infinite State Concurrent Systems: an Improvement in Model Generation, Proceedings of the 4th International Conference on Parallel Processing and Applied Mathematics (PPAM'01), 2328, Springer-Verlag, 2002.
• [13] Emerson, E. A.: Temporal and Modal Logic, in: Handbook of Theoretical Computer Science (J. van Leeuwen, Ed.), Elsevier Science Publishers, 1990, 996-1071.
• [14] Emerson, E. A., Sistla, A. P.: Symmetry and Model Checking, Formal Methods in System Design, 9, 1995, 105-131.
• [15] Fersman, E., Pettersson, P., Yi, W.: Timed automata with asynchronous processes: Schedulability and decidability, Proceedings of the 8th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'02), 2280, Springer-Verlag, 2002.
• [16] Kupferman, O., Henzinger, T. A., Vardi,M. Y.: A Space-EfficientOn-the-fly Algorithmfor Real-TimeModel Checking, Proceedings of the 7th International Conference on Concurrency Theory (CONCUR'96), 1119, Springer-Verlag, 1996.
• [17] Lilius, J.: Efficient State Space Search for Time Petri Nets, Proceedings ofMFCS Workshop on Concurrency, Brno'98, 18, Elsevier Science Publishers, 1999.
• [18] McMillan, K. L.: Symbolic Model Checking, Kluwer Academic Publishers, 1993, ISBN 0-7923-9380-5.
• [19] McMillan, K. L.: Applying SAT Methods in Unbounded Symbolic Model Checking, Proc. of the 14th Int. Conf. on Computer Aided Verification (CAV'02), 2404, Springer-Verlag, 2002.
• [20] Merlin, P., Farber, D. J.: Recoverability of Communication Protocols - Implication of a Theoretical Study, IEEE Trans. on Communications, 24(9), 1976, 1036-1043.
• [21] de Moura, L., Rueß, H., Sorea, M.: Lazy Theorem Proving for Bounded Model Checking over Infinite Domains, Proceedings of the 18th International Conference on Automated Deduction (CADE-18), 2392, Springer-Verlag, 2002.
• [22] Pagani, F.: Partial Orders and Verification of Real-Time Systems, Proceedings of the 4th International Symposium on Formal Techniques in Real Time and Fault Tolerant Systems (FTRTFT'96), 1135, Springer-Verlag, 1996.
• [23] Peled, D.: Partial Order Reduction: Linear and Branching Temporal Logics and Process Algebras, Proceedings of Partial Order Methods in Verification (POMIV'96), 29, Amer. Math. Soc., 1996.
• [24] Penczek, W., Pólrola, A.: Specification and Model Checking of Temporal Properties in Time Petri Nets and Timed Automata, Proceedings of the 25th International Conference on Applications and Theory of Petri Nets (ATPN'04), 3099, Springer-Verlag, 2004.
• [25] Penczek, W., Pólrola, A., Woźna, B., Zbrzezny, A.: Bounded Model Checking for Reachability Testing in Time Petri Nets, Proceedings of the InternationalWorkshop on Concurrency, Specification and Programming (CS&P'04), 170, Humboldt University, 2004.
• [26] Penczek, W., Woźna, B., Zbrzezny, A.: Bounded Model Checking for the Universal Fragment of CTL, Fundamenta Informaticae, 51(1-2), 2002, 135-156.
• [27] Penczek, W., Woźna, B., Zbrzezny, A.: Towards Bounded Model Checking for the Universal Fragment of TCTL, Proceedings of the 7th International Symposium on Formal Techniques in Real-Time and Fault Tolerant Systems (FTRTFT'02), 2469, Springer-Verlag, 2002.
• [28] R. Alur, T.A. Henzinger: Logics and Models of Real-Time: A Survey, Real Time: Theory in Practice, 600, Springer-Verlag, 1991.
• [29] Seshia, S., Bryant, R.: Unbounded, Fully Symbolic Model Checking of Timed Automata Using Boolean Methods, Proceedings of the 15th International Conference on Computer Aided Verification (CAV'03), 2725, Springer-Verlag, 2003.
• [30] Sorea, M.: Bounded Model Checking for Timed Automata, Proceedings of the 3rd Workshop on Models for Time-Critical Systems (MTCS'02), 68, Elsevier Science Publishers, 2002.
• [31] Tripakis, S., Yovine, S.: Analysis of Timed Systems Using Time-Abstracting Bisimulations, FormalMethods in System Design, 18(1), 2001, 25-68.
• [32] Wolper, P., Godefroid, P.: Partial Order Methods for Temporal Verification, Proceedings of the 4th International Conference on Concurrency Theory (CONCUR'93), 715, Springer-Verlag, 1993.
• [33] Woźna, B., Lomuscio, A., Penczek,W.: BoundedModel Checking for knowledge over real time, Proceedings of the 4st International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS'05), I, ACM Press, July 2005.
• [34] Woźna, B., Zbrzezny, A.: Checking ACTL_ Properties of Discrete Timed Automata via Bounded Model Checking, Proceedings of the 1st InternationalWorkshop on Formal Analysis and Modeling of Timed Systems (FORMATS'03), 2791, Springer-Verlag, 2004.
• [35] Woźna, B., Zbrzezny, A., Penczek, W.: Checking Reachability Properties for Timed Automata via SAT, Fundamenta Informaticae, 55(2), 2003, 223-241.
• [36] Zbrzezny, A.: Improvements in SAT-based Reachability Analysis for Timed Automata, Fundamenta Informaticae, 60(1-4), 2004, 417-434.
• [37] Zbrzezny, A.: SAT-based Reachability Checking for Timed Automata with Diagonal Constraints, Fundamenta Informaticae, 67(1-3), 2005, 303-322.