Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Information Flow Tracking for Linux Handling Concurrent System Calls and Shared Memory Kapitel lesen Erstes Kapitel lesen

2017 | OriginalPaper | Buchkapitel

An In-Depth Investigation of Interval Temporal Logic Model Checking with Regular Expressions

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

Erschienen in: Software Engineering and Formal Methods

Verlag: Springer International Publishing

Einloggen

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

search-config
loading …

Abstract

In the last years, the model checking (MC) problem for interval temporal logic (ITL) has received an increasing attention as a viable alternative to the traditional (point-based) temporal logic MC, which can be recovered as a special case. Most results have been obtained by imposing suitable restrictions on interval labeling. In this paper, we overcome such limitations by using regular expressions to define the behavior of proposition letters over intervals in terms of the component states. We first prove that MC for Halpern and Shoham’s ITL (HS), extended with regular expressions, is decidable. Then, we show that formulas of a large class of HS fragments, namely, all fragments featuring (a subset of) HS modalities for Allen’s relations meets, met-by, starts, and started-by, can be model checked in polynomial working space (MC for all these fragments turns out to be PSPACE-complete).

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 Participatory Verification of Railway Infrastructure by Representing Regulations in RailCNL
Nächstes Kapitel PART: From Partial Analysis Results to a Proof Witness
Fußnoten
1
All the results we prove in the paper hold for the strict semantics as well.
 
2
As shown in [4], this is not the case in general: the computation-tree-based semantics of [10‐12] is subsumed by the state-based one of [14] and follow-up papers.
 
3
The factor 2 in front of \(|\psi '|\) is needed as the small-model requires a formula in NNF.
 
Literatur
1.
Allen, J.F.: Maintaining knowledge about temporal intervals. Commun. ACM 26(11), 832–843 (1983)CrossRef
2.
3.
Bozzelli, L., Molinari, A., Montanari, A., Peron, A., Sala, P.: Interval temporal logic model checking: the border between good and bad HS fragments. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS (LNAI), vol. 9706, pp. 389–405. Springer, Cham (2016). doi:10.​1007/​978-3-319-40229-1_​27CrossRef
4.
Bozzelli, L., Molinari, A., Montanari, A., Peron, A., Sala, P.: Interval vs. point temporal logic model checking: an expressiveness comparison. In: FSTTCS (2016)
5.
Bozzelli, L., Molinari, A., Montanari, A., Peron, A., Sala, P.: MC the logic of Allen’s relations meets and started-by is P\(^{\rm NP}\)-C. In: GandALF, pp. 76–90 (2016)
6.
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)MathSciNetCrossRef
7.
Esparza, J., Hansel, D., Rossmanith, P., Schwoon, S.: Efficient algorithms for model checking pushdown systems. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 232–247. Springer, Heidelberg (2000). doi:10.​1007/​10722167_​20CrossRef
8.
9.
Kupferman, O., Piterman, N., Vardi, M.Y.: From liveness to promptness. Formal Methods Syst. Des. 34(2), 83–103 (2009)CrossRef
10.
Lomuscio, A., Michaliszyn, J.: An epistemic HS logic. In: IJCAI, pp. 1010–1016 (2013)
11.
Lomuscio, A., Michaliszyn, J.: Decidability of model checking multi-agent systems against a class of EHS specifications. In: ECAI, pp. 543–548 (2014)
12.
Lomuscio, A., Michaliszyn, J.: Model checking multi-agent systems against epistemic HS specifications with regular expressions. In: KR, pp. 298–308 (2016)
13.
Marcinkowski, J., Michaliszyn, J.: The undecidability of the logic of subintervals. Fundamenta Informaticae 131(2), 217–240 (2014)MathSciNetMATH
14.
Molinari, A., Montanari, A., Murano, A., Perelli, G., Peron, A.: Checking interval properties of computations. Acta Informatica 53, 587–619 (2016)MathSciNetCrossRef
15.
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)
16.
Molinari, A., Montanari, A., Peron, A.: A model checking procedure for interval temporal logics based on track representatives. In: CSL, pp. 193–210 (2015)
17.
Molinari, A., Montanari, A., Peron, A., Sala, P.: Model checking well-behaved fragments of HS: the (Almost) final picture. In: KR, pp. 473–483 (2016)
18.
Montanari, A.: Interval temporal logics model checking. In: TIME, p. 2 (2016)
19.
Moszkowski, B.: Reasoning about digital circuits. Ph.D. thesis, Stanford (1983)
20.
21.
Venema, Y.: Expressiveness and completeness of an interval tense logic. Notre Dame J. Formal Log. 31(4), 529–547 (1990)MathSciNetCrossRef
Metadaten
Titel
An In-Depth Investigation of Interval Temporal Logic Model Checking with Regular Expressions
verfasst von
Laura Bozzelli
Alberto Molinari
Angelo Montanari
Adriano Peron
Copyright-Jahr
2017
Buch
Software Engineering and Formal Methods

Print ISBN: 978-3-319-66196-4

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

Copyright-Jahr: 2017

DOI
https://doi.org/10.1007/978-3-319-66197-1_7