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
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Bücher
Zeitschriften
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
MTZ-Fachkongress

Antriebe und Energiesysteme von morgen


Austausch von Automobil- und Energiewirtschaft

Am 14./15. Mai geht es in Chemnitz um die Mobilitätswende durch Elektro- und Wasserstofffahrzeuge.
Erweiterte Suche
Anmelden
nach oben
Acta Informatica
Erschienen in: Acta Informatica 2/2016

01.03.2016 | Original Article

A tool for deciding the satisfiability of continuous-time metric temporal logic

verfasst von: Marcello M. Bersani, Matteo Rossi, Pierluigi San Pietro

Erschienen in: Acta Informatica | Ausgabe 2/2016

Einloggen

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

search-config
loading …

Abstract

Constraint LTL over clocks is a variant of CLTL, an extension of linear-time temporal logic allowing atomic assertions in a concrete constraint system. Satisfiability of CLTL over clocks is here shown to be decidable by means of a reduction to a decidable Satisfiability Modulo Theories (SMT) problem. The result is a complete Bounded Satisfiability Checking procedure, which has been implemented by using standard SMT solvers. The importance of this technique derives from the possibility of translating various continuous-time metric temporal logics, such as MITL and QTL, into CLTL over clocks itself. Although standard decision procedures of these logics do exist, they have never been realized in practice. Suitable translations into CLTL over clocks have instead allowed us the development of the first prototype tool for deciding MITL and QTL. The paper also reports preliminary, but encouraging, experiments on some significant examples of MITL and QTL formulae.
Vorheriger Artikel Optimization in temporal qualitative constraint networks

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 "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

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
Fußnoten
1
Note that, in the formulae of this section, we write \(z_\delta \sim c\) as an abbreviation for \(\bigvee _{i \in \{ 0,1 \}} z^i_\delta \sim c\) (similarly for \(z_\psi \sim c\)).
 
2
With slight abuse, we use rational bound \(0.5\); as customary, a formula with only integer bounds can be obtained by doubling all constants appearing in the formula.
 
Literatur
1.
2.
3.
Audemard, G., Cimatti, A., Kornilowicz, A., Sebastiani, R.: Bounded model checking for timed systems. In: Proceedings of FORTE, pp 243–259 (2002)
4.
Badban, B., Lange, M.: Exact incremental analysis of timed automata with an SMT-solver. In: FORMATS. volume 6919 of LNCS, pp. 177–192 (2011)
5.
Bengtsson, J., Yi, W.: Timed automata: semantics, algorithms and tools. In: Lecture Notes on Concurrency and Petri Nets. volume 3098 of LNCS, pp. 87–124 (2004)
6.
7.
Bersani, M.M., Frigeri, A., Morzenti, A., Pradella, M., Rossi, M., San Pietro, P.: Bounded reachability for temporal logic over constraint systems. In: TIME 2010, pp. 43–50. IEEE Computer Society, (2010)
8.
Bersani, M.M., Frigeri, A., Rossi, M., San Pietro, P.: Completeness of the bounded satisfiability problem for constraint LTL. In: Reachability Problems, volume 6945 of LNCS, pp. 58–71 (2011)
9.
Bersani, M.M., Rossi, M., San Pietro, P.: Deciding continuous-time metric temporal logic with counting modalities. In: Reachability Problems, volume 8169 of LNCS, pp. 70–82 (2013)
10.
Bersani, M.M., Rossi, M., San Pietro, P.: Deciding the satisfiability of MITL specifications. In: Proceedings of the International Symposium on Games, Automata, Logics and Formal Verification (GandALF), pp. 64–78 (2013)
11.
Bersani, M.M., Rossi, M., San Pietro, P.: On the satisfiability of metric temporal logics over the reals. In: Proceedings of the International Work on Automated Verification of Critical Systems (AVOCS), pp. 1–15 (2013)
12.
Bersani, M.M., Rossi, M., San Pietro, P.: A logical characterization of timed (non-)regular languages. In: Mathematical Foundations of Computer Science, volume 8634 of Lecture Notes in Computer Science, pp. 75–86 (2014)
13.
Bersani, M.M., Rossi, M., San Pietro, P.: An SMT-based approach to satisfiability checking of MITL. Inf. Comput. (2015, to appear)
14.
Biere, A., Heljanko, K., Junttila, T.A., Latvala, T., Schuppan, V.: Linear encodings of bounded LTL model checking. Log. Methods Comput. Sci. 2(5), 1–64 (2006)MathSciNetCrossRefMATH
15.
16.
Clarke, E.M., Kroening, D., Ouaknine, J., Strichman, O.: Completeness and complexity of bounded model checking. In: Verification Model Checking and Abstract Interpretation, volume 2937 of Lecture Notes in Computer Science, pp. 85–96. Springer, Berlin (2004)
17.
18.
D’Souza, D., Prabhakar, P.: On the expressiveness of mtl in the pointwise and continuous semantics. Int. J. Softw. Tools Technol. Transf. (STTT) 9(1), 1–4 (2007)CrossRef
19.
D’Souza, D., Tabareau, N.: On timed automata with input-determined guards. In: FORMATS/FTRTFT ’04, volume 3253 of Lecture Notes in Computer Science, pp. 68–83 (2004)
20.
Ferrante, J., Rackoff, C.: A decision procedure for the first order theory of real addition with order. SIAM J. Comput. 4(1), 69–76 (1975)MathSciNetCrossRefMATH
21.
Henzinger, T.A., Raskin, J.-F., Schobbens, P.-Y.: The regular real-time languages. In: In Proceedings of the 25th International Colloquium Automata, Languages, and Programming (ICALP’98), pp. 580–591. Springer, Berlin (1998)
22.
23.
Hirshfeld, Y., Rabinovich, A.M.: Logics for real time: decidability and complexity. Fundam. Inf. 62(1), 1–28 (2004)MathSciNetMATH
24.
25.
Maler, O., Nickovic, D., Pnueli, A.: From MITL to timed automata. In: Proceedings of FORMATS, volume 4202 of LNCS, pp. 274–289 (2006)
26.
27.
Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Trans. Program. Lang. Syst. 1(2), 245–257 (1979)CrossRefMATH
28.
Niebert, P., Mahfoudh, M., Asarin, E., Bozga, M., Maler, O., Jain, N.: Verification of timed automata via satisfiability checking. In: FTRTFT, volume 2469 of LNCS, pp. 225–243 (2002)
29.
30.
Ouaknine, J., Worrell, J.: On the decidability of metric temporal logic. In: LICS, pp. 188–197 (2005)
31.
Pradella, M., Morzenti, A., San Pietro, P.: Bounded satisfiability checking of metric temporal logic specifications. ACM Trans. Softw. Eng. Methodol. (TOSEM) 22(3), 20 (2013)CrossRef
32.
33.
Rabinovich, A.: Complexity of metric temporal logics with counting and the Pnueli modalities. Theor. Comput. Sci. 411, 2331–2342 (2010)MathSciNetCrossRefMATH
34.
Schobbens, P.-Y., Raskin, J.-F., Henzinger, T.A.: Axioms for real-time logics. Theor. Comput. Sci.274(1–2), 151–182 (2002)
35.
Tarski, A.: A decision method for elementary algebra and geometry, 2nd edn. University of California Press, Berkeley (1951)MATH
36.
Metadaten
Titel
A tool for deciding the satisfiability of continuous-time metric temporal logic
verfasst von
Marcello M. Bersani
Matteo Rossi
Pierluigi San Pietro
Publikationsdatum
01.03.2016
Verlag
Springer Berlin Heidelberg
Erschienen in
Acta Informatica / Ausgabe 2/2016
Print ISSN: 0001-5903
Elektronische ISSN: 1432-0525
DOI
https://doi.org/10.1007/s00236-015-0229-y

Premium Partner

    Bildnachweise