×

Timed modal logics for real-time systems. Specification, verification and control. (English) Zbl 1216.68158

Summary: In this paper, a timed modal logic \(L_{c}\) is presented for the specification and verification of real-time systems. Several important results for \(L_{c}\) are discussed. First we address the model checking problem and we show that it is an EXPTIME-complete problem. Secondly we consider expressiveness and we explain how to express strong timed bisimilarity and how to build characteristic formulas for timed automata. We also propose a compositional algorithm for \(L_{c}\) model checking. Finally we consider several control problems for which \(L_{c}\) can be used to check controllability.

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
03B45 Modal logic (including the logic of norms)
68Q45 Formal languages and automata

Software:

CMC; Kronos; Uppaal
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Aceto, L., Bouyer, P., Burgueño, A., & Larsen, K. G. (1998a). The power of reachability testing for timed automata. In V. Arvind, R. Ramanujam (Eds.), Proceedings of the 18th conference on fundations of software technology and theoretical computer science (FSTTCS’98) (Vol. 1530, pp. 245–256). Chennai, India: Lecture Notes in Computer Science. · Zbl 1023.68060
[2] Aceto, L., Burgueño, A., & Larsen, K. G. (1998b) Model checking via reachability testing for timed Automata. In Proceedings of the 4th international conference on tools and algorithms for the construction and analysis of systems (TACAS ’98) (Vol. 1384, pp. 263–280). Lisbon, Portugal, Mar. 1998, Lecture Notes in Computer Science.
[3] Aceto L., Ingólfsdóttir A., Pedersen M. L., Poulsen J. (2000) Characteristic formulae for timed automata. Theoretical Informatics and Applications 34(6): 565–584 · Zbl 0974.68121 · doi:10.1051/ita:2000131
[4] Aceto L., Laroussinie F. (2002) Is your model checker on time? On the complexity of model checking for timed modal logics. Journal of Logic and Algebraic Programming 52–53: 7–51 · Zbl 1008.68030 · doi:10.1016/S1567-8326(02)00022-X
[5] Alur R., Courcoubetis C., Dill D. L. (1993) Model-checking in dense real-time. Information and Computation 104(1): 2–34 · Zbl 0783.68076 · doi:10.1006/inco.1993.1024
[6] Alur, R., Courcoubetis, C., & Henzinger, T. A. (1994). The observational power of clocks. In Proceedings of the 5th international conference on theory of concurrency (CONCUR ’94) (Vol. 836, pp. 162–177). Uppsala, Sweden: Lecture Notes in Computer Science.
[7] Alur R., Dill D. L. (1994) A theory of timed automata. Theoretical Computer Science 126(2): 183–235 · Zbl 0803.68071 · doi:10.1016/0304-3975(94)90010-8
[8] Alur R., Feder T., Henzinger T. A. (1996) The benefits of relaxing punctuality. Journal of the ACM 43(1): 116–146 · Zbl 0882.68021 · doi:10.1145/227595.227602
[9] Alur, R., & Henzinger, T. A. (1992). Logics and models of real time: A survey. In Real-time: theory in practice, proceedings of REX workshop (Vol. 600, pp. 74–106). Mook, NL: Lecture Notes in Computer Science, June 1991.
[10] Alur R., Henzinger T. A. (1994) A really temporal logic. Journal of the ACM 41(1): 181–203 · Zbl 0807.68065 · doi:10.1145/174644.174651
[11] Andersen, H. R. (1995). Partial model checking (Extended Abstract). In Proceedings of the 10th IEEE Symposium (pp. 398–407). San Diego, CA, USA: Logic in Computer Science (LICS ’95), June 1995.
[12] Arnold A., Vincent A., Walukiewicz I. (2003) Games for synthesis of controllers with partial observation. Theoretical Computer Science 1(303): 7–34 · Zbl 1175.93148 · doi:10.1016/S0304-3975(02)00442-5
[13] Bouyer, P., Cassez, F., & Laroussinie, F. (2005). Modal logics for timed control. In M. Abadi, L. de Alfaro (Eds.), Proceedings of the 16th international conference on concurrency theory (CONCUR’05) (Vol. 3653, pp. 81–94). San Francisco, CA, USA: Lecture Notes in Computer Science. · Zbl 1134.68399
[14] Bouyer, P., Chevalier, F., & Markey, N. (2010). On the expressiveness of TPTL and MTL. Information and Computation. To appear. · Zbl 1209.03010
[15] Cassez, F., Henzinger, T. A., & Raskin, J.-F. (2002). A comparison of control problems for timed and hybrid systems. In Proceedings of 5th international workshop on hybrid systems: Computation and control (HSCC’02), LNCS (Vol. 2289, pp. 134–148). · Zbl 1044.93518
[16] Cassez, F., & Laroussinie, F. (2000). Model-checking for hybrid systems by quotienting and constraints solving. In E. A. Emerson, A. P. Sistla (Eds.), Proceedings of the 12th international conference on computer aided verification (CAV 2000) (Vol. 1855, pp. 373–388). Chicago, Illinois, USA: Lecture Notes in Computer Science. · Zbl 0974.68117
[17] Clarke E. M., Grumberg O., Peled D. A. (1999) Model checking. MIT Press, Cambridge
[18] Emerson E. A. (1990) Temporal and modal logic. In: Leeuwen J. v. Handbook of theoretical computer science, Vol. B (Chap. 16). Elsevier, Amsterdam, pp 995–1072 · Zbl 0900.03030
[19] Henzinger T. A., Nicollin X., Sifakis J., Yovine S. (1994) Symbolic model checking for real-time systems. Information and Computation 111(2): 193–244 · Zbl 0806.68080 · doi:10.1006/inco.1994.1045
[20] Janin, D., & Walukiewicz, I. (1995). Automata for the modal mu-calculus and related results. In Proceedings of the 20th international symposium on mathematical foundations of computer science (MFCS’95) (Vol. 969, pp. 552–562). Lecture Notes in Computer Science. · Zbl 1193.68163
[21] Laroussinie, F., & Larsen, K. G. (1995a). Compositional model-checking of real time systems. In I. Lee, S. A. Smolka (Eds.), Proceedings of the 6th international conference on concurrency theory (CONCUR’95) (Vol. 962, pp. 529–539). Philadelphia, Pennsylvania, USA: Lecture Notes in Computer Science.
[22] Laroussinie, F., & Larsen K. G. (1995b). Compositional model checking of real time systems. Technical Report RS-95-19, BRICS.
[23] Laroussinie, F., & Larsen, K. G. (1998). CMC: A tool for compositional model-checking of real-time systems. In: S. Budkowski, A. R. Cavalli, E. Najm (Eds.), Proceedings of IFIP TC6 WG6.1 joint international conference on formal description techniques for distributed systems and communication protocols (FORTE’XI) and protocol specification, testing and verification (PSTV’XVIII) (Vol. 135, pp. 439–456) Paris, France: IFIP Conference Proceedings.
[24] Laroussinie, F., Larsen, K. G., & Weise, C. (1995). From timed automata to logic–and Back. In J. Wiedermann, P. Hájek (Eds.), Proceedings of the 20th international symposium on mathematical fundations of computer science (MFCS’95) (Vol. 969, pp. 27–41) Prague, Czech Republic: Lecture Notes in Computer Science. · Zbl 1193.03069
[25] Larsen, K. G., Pettersson, P., & Yi, W. (1995). Model-checking for real-time systems. In Proceedings of the 10th international conference on fundamentals of computation theory (FCT ’95) (Vol. 965, pp. 62–88). Dresden, Germany: Lecture Notes in Computer Science, Aug. 1995.
[26] Larsen K. G., Pettersson P., Yi W. (1997) UPPAAL in a nutshell. Journal of Software Tools for Technology Transfer 1(1–2): 134–152 · Zbl 1060.68577 · doi:10.1007/s100090050010
[27] Maler, O., A. Pnueli, & Sifakis, J. (1995). On the synthesis of discrete controllers for timed systems. In Proceedings of the 12th annual symposium on theoretical aspects of computer science (STACS’95) (Vol. 900, pp. 229–242). Lecture Notes in Computer Science. · Zbl 1379.68227
[28] Manna Z., Pnueli A. (1992) The temporal logic of reactive and concurrent systems: Specification. Springer, New York · Zbl 0753.68003
[29] Milner R. (1989) A complete axiomatisation for observational congruence of finite-state behaviours. Information and Computation 81(2): 227–247 · Zbl 0688.68050 · doi:10.1016/0890-5401(89)90070-9
[30] Ouaknine, J., & Worrell, J. (2005). On the decidability of metric temporal logic. In Proceedings of the 20th IEEE Symposium. Chicago, IL, USA: Logic in Computer Science (LICS 2005), June 2005. · Zbl 1128.03008
[31] Park, D. (1981). Concurrency and automata on infinite sequences. In Proceedings of the 5th GI Conference on theoretical computer science, Karlsruhe, FRG, Mar. 1981 (Vol. 104, pp. 167–183). Lecture Notes in Computer Science.
[32] Yovine S. (1997) Kronos: A verification tool for real-time systems. Journal of Software Tools for Technology Transfer 1(1–2): 123–133 · Zbl 1060.68606 · doi:10.1007/s100090050009
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.