Checking interval properties of computations. (English) Zbl 1350.68184
Summary: Model checking is a powerful method widely explored in formal verification. Given a model of a system, e.g., a Kripke structure, and a formula specifying its expected behaviour, one can verify whether the system meets the behaviour by checking the formula against the model. Classically, system behaviour is expressed by a formula of a temporal logic, such as LTL and the like. These logics are “point-wise” interpreted, as they describe how the system evolves state-by-state. However, there are relevant properties, such as those constraining the temporal relations between pairs of temporally extended events or involving temporal aggregations, which are inherently “interval-based”, and thus asking for an interval temporal logic. In this paper, we give a formalization of the model checking problem in an interval logic setting. First, we provide an interpretation of formulas of Halpern and Shoham’s interval temporal logic HS over finite Kripke structures, which allows one to check interval
properties of computations. Then, we prove that the model checking problem for HS against finite Kripke structures is decidable by a suitable small model theorem, and we provide a lower bound to its computational complexity.
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 03B25 | Decidability of theories and sets of sentences |
| 03B44 | Temporal logic |
| 68Q17 | Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) |
References:
| [1] | Allen, J.F.: Maintaining knowledge about temporal intervals. Commun. ACM 26(11), 832-843 (1983) · Zbl 0519.68079 · doi:10.1145/182.358434 |
| [2] | Bresolin, D., Della Monica, D., Goranko, V., Montanari, A., Sciavicco, G.: The dark side of interval temporal logic: marking the undecidability border. Ann. Math. Artif. Intell. 71(1-3), 41-83 (2014) · Zbl 1325.03014 · doi:10.1007/s10472-013-9376-4 |
| [3] | Bresolin, D., Goranko, V., Montanari, A., Sala, P.: Tableau-based decision procedures for the logics of subinterval structures over dense orderings. J. Log. Comput. 20(1), 133-166 (2010) · Zbl 1188.03009 · doi:10.1093/logcom/exn063 |
| [4] | Bresolin, D., Goranko, V., Montanari, A., Sciavicco, G.: Propositional interval neighborhood logics: expressiveness, decidability, and undecidable extensions. Ann. Pure Appl. Log. 161(3), 289-304 (2009) · Zbl 1221.03022 · doi:10.1016/j.apal.2009.07.003 |
| [5] | Bresolin, D., Montanari, A., Sala, P., Sciavicco, G.: What’s decidable about Halpern and Shoham’s interval logic? The maximal fragment \[{\sf AB}{\overline{\sf BL}}\] ABBL¯. In: Proceedings of the 26th LICS. IEEE Comp. Society Press, pp. 387-396 (2011) · Zbl 0441.68010 |
| [6] | Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Proceedings of the Workshop on Logic of Programs, LNCS, vol. 131. Springer, pp. 52-71 (1981) · Zbl 1181.03012 |
| [7] | Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (2002) |
| [8] | Della Monica, D., Goranko, V., Montanari, A., Sciavicco, G.: Interval temporal logics: a journey. Bull. EATCS 105, 73-99 (2011) · Zbl 1275.03087 |
| [9] | Gabbay, D.M.: The declarative past and imperative future: executable temporal logic for interactive systems. In: Proceedings of Temporal Logic in Specification, LNCS, vol. 398. Springer, pp. 409-448 (1987) |
| [10] | Goranko, V., Montanari, A., Sciavicco, G.: A road map of interval temporal logics and duration calculi. J. Appl. Non-Classical Log. 14(1-2), 9-54 (2004) · Zbl 1181.03012 · doi:10.3166/jancl.14.9-54 |
| [11] | Halpern, J.Y., Shoham, Y.: A propositional modal logic of time intervals. J. ACM 38(4), 935-962 (1991) · Zbl 0799.68175 · doi:10.1145/115234.115351 |
| [12] | Lange, M.: Model checking propositional dynamic logic with all extras. J. Appl. Log. 4(1), 39-49 (2006) · Zbl 1095.68053 · doi:10.1016/j.jal.2005.08.002 |
| [13] | Lodaya, K.: Sharpening the undecidability of interval temporal logic. In: Proceedings of the 6th ASIAN, LNCS, vol. 1961, pp. 290-298 (2000) · Zbl 0987.03015 |
| [14] | Lomuscio, A.R., Michaliszyn, J.: An epistemic Halpern-Shoham logic. In: Proceedings of the 23rd IJCAI. AAAI Press/International Joint Conferences on Artificial Intelligence (2013) · Zbl 0744.03022 |
| [15] | Lomuscio, A.R., Michaliszyn, J.: Decidability of model checking multi-agent systems against a class of EHS specifications. In: Proceedings of the 21st ECAI, pp. 543-548 (2014) · Zbl 1366.68179 |
| [16] | Marcinkowski, J., Michaliszyn, J.: The undecidability of the logic of subintervals. Fundam. Inf. 131(2), 217-240 (2014) · Zbl 1315.03027 |
| [17] | Montanari, A., Murano, A., Perelli, G., Peron, A.: Checking interval properties of computations. In: Proceedings of the 21st TIME, pp. 59-68 (2014) · Zbl 1350.68184 |
| [18] | Montanari, A., Puppis, G., Sala, P.: Maximal decidable fragments of Halpern and Shoham’s modal logic of intervals. In: Proceedings of the 37th ICALP, LNCS, vol. 6199, pp. 345-356 (2010) · Zbl 1288.03017 |
| [19] | Moszkowski, B.: Reasoning About Digital Circuits. PhD thesis, Department of Computer Science, Stanford University, Stanford, CA (1983) · Zbl 1275.03087 |
| [20] | Papadimitriou, C.H.: Computational Complexity. Addison-Wesley, Reading (1994) · Zbl 0833.68049 |
| [21] | Pnueli, A.: The temporal logic of programs. In: Proceedings of the 18th FOCS, pp. 46-57 (1977) · Zbl 1095.68053 |
| [22] | Pnueli, A.: The Temporal Semantics of Concurrent Programs. Theor. Comput. Sci. 13, 45-60 (1981) · Zbl 0441.68010 · doi:10.1016/0304-3975(81)90110-9 |
| [23] | Queille, J.P., Sifakis, J.:Specification and verification of concurrent programs in CESAR. In: Proceedings of the 6th SP, LNCS, vol. 137. Springer, pp. 337-351 (1981) · Zbl 1142.68440 |
| [24] | Roeper, P.: Intervals and tenses. J. Philos. Log. 9, 451-469 (1980) · Zbl 0451.03007 |
| [25] | Sipser, M.: Introduction to the Theory of Computation, 3rd edn. International Thomson Publishing, New York (2012) · Zbl 1169.68300 |
| [26] | Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logics. J. ACM 32(3), 733-749 (1985) · Zbl 0632.68034 · doi:10.1145/3828.3837 |
| [27] | Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Proceedings of the 1st LICS. IEEE Comp. Society Press, pp. 332-344 (1986) · Zbl 0632.68034 |
| [28] | Venema, Y.: A modal logic for chopping intervals. J. Log. Comput. 1(4), 453-476 (1991) · Zbl 0744.03022 · doi:10.1093/logcom/1.4.453 |
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.
