nach oben

Erschienen in:

2016 | OriginalPaper | Buchkapitel

Interval Temporal Logic Model Checking: The Border Between Good and Bad HS Fragments

verfasst von : Laura Bozzelli, Alberto Molinari, Angelo Montanari, Adriano Peron, Pietro Sala

Erschienen in: Automated Reasoning

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

The model checking problem has thoroughly been explored in the context of standard point-based temporal logics, such as LTL, CTL, and CTL\(^{*}\), whereas model checking for interval temporal logics has been brought to the attention only very recently.

In this paper, we prove that the model checking problem for the logic of Allen’s relations started-by and finished-by is highly intractable, as it can be proved to be \({{\mathrm{\mathbf {EXPSPACE}}}}\)-hard. Such a lower bound immediately propagates to the full Halpern and Shoham’s modal logic of time intervals (HS). In contrast, we show that other noteworthy HS fragments, namely, Propositional Neighbourhood Logic extended with modalities for the Allen relation starts (resp., finishes) and its inverse started-by (resp., finished-by), turn out to have—maybe unexpectedly—the same complexity as LTL (i.e., they are \({{\mathrm{\mathbf {PSPACE}}}}\)-complete), thus joining the group of other already studied, well-behaved albeit less expressive, HS fragments.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Complexity Optimal Decision Procedure for a Propositional Dynamic Logic with Parallel Composition

Nächstes Kapitel : A Resolution-Based Prover for Multimodal K

All the results we prove in the paper hold for the strict semantics as well.

Note that such a \(\rho \)-position exists by definition of \(E(\varphi ,\rho )\).

Allen, J.F.: Maintaining knowledge about temporal intervals. Commun. ACM 26(11), 832–843 (1983)CrossRefMATH

Bozzelli, L., Molinari, A., Montanari, A., Peron, A., Sala, P.: Interval Temporal Logic Model Checking: the Border Between Good and Bad HS Fragments (2016). https://www.dimi.uniud.it/la-ricerca/pubblicazioni/preprints/1.2016

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)MathSciNetCrossRefMATH

Bresolin, D., Goranko, V., Montanari, A., Sala, P.: Tableau-based decision procedures for the logics of subinterval structures over dense orderings. J. Logic Comput. 20(1), 133–166 (2010)MathSciNetCrossRefMATH

Bresolin, D., Goranko, V., Montanari, A., Sciavicco, G.: Propositional interval neighborhood logics: expressiveness, decidability, and undecidable extensions. Ann. Pure Appl. Logic 161(3), 289–304 (2009)MathSciNetCrossRefMATH

Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (2002)

Emerson, E.A., Halpern, J.Y.: “Sometimes” and “not never” revisited: on branching versus linear time temporal logic. J. ACM 33(1), 151–178 (1986)MathSciNetCrossRefMATH

Giunchiglia, F., Traverso, P.: Planning as model checking. In: Biundo, S., Fox, M. (eds.) ECP 1999. LNCS, vol. 1809, pp. 1–20. Springer, Heidelberg (2000)CrossRef

Gottlob, G.: NP trees and Carnap’s modal logic. J. ACM 42(2), 421–457 (1995)MathSciNetCrossRefMATH

10.

Halpern, J.Y., Shoham, Y.: A propositional modal logic of time intervals. J. ACM 38(4), 935–962 (1991)MathSciNetCrossRefMATH

11.

Harel, D.: Algorithmics: The Spirit of Computing. Wesley, Reading (1992)MATH

12.

Lodaya, K.: Sharpening the undecidability of interval temporal logic. In: Kleinberg, R.D., Sato, M. (eds.) ASIAN 2000. LNCS, vol. 1961, pp. 290–298. Springer, Heidelberg (2000)CrossRef

13.

Lomuscio, A., Michaliszyn, J.: An epistemic Halpern-Shoham logic. In: IJCAI, pp. 1010–1016 (2013)

14.

Lomuscio, A., Michaliszyn, J.: Decidability of model checking multi-agent systems against a class of EHS specifications. In: ECAI, pp. 543–548 (2014)

15.

Lomuscio, A., Michaliszyn, J.: Model checking epistemic Halpern-Shoham logic extended with regular expressions. CoRR abs/1509.00608 (2015)

16.

Lomuscio, A., Raimondi, F.: mcmas: a model checker for multi-agent systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 450–454. Springer, Heidelberg (2006)CrossRef

17.

Marcinkowski, J., Michaliszyn, J.: The undecidability of the logic of subintervals. Fundamenta Informaticae 131(2), 217–240 (2014)MathSciNetMATH

18.

Molinari, A., Montanari, A., Murano, A., Perelli, G., Peron, A.: Checking interval properties of computations. Acta Informatica (2015, accepted for publication)

19.

Molinari, A., Montanari, A., Peron, A.: Complexity of ITL model checking: some well-behaved fragments of the interval logic HS. In: TIME, pp. 90–100 (2015)

20.

Molinari, A., Montanari, A., Peron, A.: A model checking procedure for interval temporal logics based on track representatives. In: CSL, pp. 193–210 (2015)

21.

Molinari, A., Montanari, A., Peron, A., Sala, P.: Model checking well-behaved fragments of HS: the (almost) final picture. In: KR (2016)

22.

Moszkowski, B.: Reasoning about digital circuits. Ph.D. thesis, Dept. of Computer Science, Stanford University, Stanford, CA (1983)

23.

Pnueli, A.: The temporal logic of programs. In: FOCS, pp. 46–57. IEEE (1977)

24.

Pratt-Hartmann, I.: Temporal prepositions and their logic. Artif. Intell. 166(1–2), 1–36 (2005)MathSciNetCrossRefMATH

25.

Roeper, P.: Intervals and tenses. J. Philos. Logic 9, 451–469 (1980)MathSciNetMATH

26.

Schnoebelen, P.: Oracle circuits for branching-time model checking. In: Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J. (eds.) ICALP 2003. LNCS, vol. 2719, pp. 790–801. Springer, Heidelberg (2003)CrossRef

27.

Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logics. J. ACM 32(3), 733–749 (1985)MathSciNetCrossRefMATH

28.

Venema, Y.: Expressiveness and completeness of an interval tense logic. Notre Dame J. Formal Logic 31(4), 529–547 (1990)MathSciNetCrossRefMATH

Titel: Interval Temporal Logic Model Checking: The Border Between Good and Bad HS Fragments
verfasst von: Laura Bozzelli
Alberto Molinari
Angelo Montanari
Adriano Peron
Pietro Sala
Verlag: Springer International Publishing
Buch: Automated Reasoning
Print ISBN: 978-3-319-40228-4

Electronic ISBN: 978-3-319-40229-1

Copyright-Jahr: 2016
DOI: https://doi.org/10.1007/978-3-319-40229-1_27

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner