Top

Published in:

2017 | OriginalPaper | Chapter

Theorem Proving for Metric Temporal Logic over the Naturals

Authors : Ullrich Hustadt, Ana Ozaki, Clare Dixon

Published in: Automated Deduction – CADE 26

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

We study translations from Metric Temporal Logic (MTL) over the natural numbers to Linear Temporal Logic (LTL). In particular, we present two approaches for translating from MTL to LTL which preserve the ExpSpace complexity of the satisfiability problem for MTL. In each of these approaches we consider the case where the mapping between states and time points is given by (1) a strict monotonic function and by (2) a non-strict monotonic function (which allows multiple states to be mapped to the same time point). Our translations allow us to utilise LTL solvers to solve satisfiability and we empirically compare the translations, showing in which cases one performs better than the other.

Dont have a licence yet? Then find out more about our products and how to get one now:

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!

inform now

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!

inform now

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!

inform now

previous chapter Detecting Inconsistencies in Large First-Order Knowledge Bases

next chapter Scavenger 0.1: A Theorem Prover Based on Conflict Resolution

We write \(\mathsf{min}(l+k,2\cdot C)\) for the minimum between \(l+k\) and \(2\cdot C\). If the minimum is \(2\cdot C\) then \( s^{j+1}_{2\cdot C} \) means that the sum of the last \(j+1\) variables is greater or equal to \(2\cdot C\).

Abbas, H., Fainekos, G., Sankaranarayanan, S., Ivančić, F., Gupta, A.: Probabilistic temporal logic falsification of cyber-physical systems. ACM Trans. Embed. Comput. Syst. (TECS) 12(2s), 95: 1–95: 30 (2013)

Alur, R., Feder, T., Henzinger, T.A.: The benefits of relaxing punctuality. J. ACM 43(1), 116–146 (1996)MathSciNetCrossRefMATH

Alur, R., Henzinger, T.A.: Real-time logics: complexity and expressiveness. Inf. Comput. 104(1), 35–77 (1993)MathSciNetCrossRefMATH

Alur, R., Henzinger, T.A.: A really temporal logic. J. ACM 41(1), 181–204 (1994)MathSciNetCrossRefMATH

Bersani, M.M., Rossi, M., Pietro, P.S.: A tool for deciding the satisfiability of continuous-time metric temporal logic. Acta Informatica 53(2), 171–206 (2016)MathSciNetCrossRefMATH

Bouyer, P., Markey, N., Ouaknine, J., Worrell, J.: The cost of punctuality. In: Proceedings of LICS 2007, pp. 109–120. IEEE (2007)

Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: an opensource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359–364. Springer, Heidelberg (2002). doi:10.1007/3-540-45657-0_29 CrossRef

Dauzère-Pérès, S., Paulli, J.: An integrated approach for modeling and solving the general multiprocessor job-shop scheduling problem using tabu search. Ann. Oper. Res. 70, 281–306 (1997)MathSciNetCrossRefMATH

Dixon, C., Fisher, M., Konev, B.: Temporal logic with capacity constraints. In: Konev, B., Wolter, F. (eds.) FroCoS 2007. LNCS, vol. 4720, pp. 163–177. Springer, Heidelberg (2007). doi:10.1007/978-3-540-74621-8_11 CrossRef

10.

Fisher, M.: A normal form for temporal logics and its applications in theorem-proving and execution. J. Logic Comput. 7(4), 429–456 (1997)MathSciNetCrossRefMATH

11.

Gabbay, D., Pnueli, A., Shelah, S., Stavi, J.: On the temporal analysis of fairness. In: Proceedings of POPL 1980, pp. 163–173. ACM (1980)

12.

Gerevini, A., Haslum, P., Long, D., Saetti, A., Dimopoulos, Y.: Deterministic planning in the fifth international planning competition: PDDL3 and experimental evaluation of the planners. Artif. Intell. 173(5—-6), 619–668 (2009)MathSciNetCrossRefMATH

13.

Goré, R.: And-or tableaux for fixpoint logics with converse: LTL, CTL, PDL and CPDL. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS, vol. 8562, pp. 26–45. Springer, Cham (2014). doi:10.1007/978-3-319-08587-6_3

14.

Graham, R.L.: Bounds for certain multiprocessing anomalies. Bell Labs Tech. J. 45(9), 1563–1581 (1966)CrossRefMATH

15.

Gunadi, H., Tiu, A.: Efficient runtime monitoring with metric temporal logic: a case study in the android operating system. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 296–311. Springer, Cham (2014). doi:10.1007/978-3-319-06410-9_21 CrossRef

16.

Hustadt, U., Konev, B.: TRP++ 2.0: a temporal resolution prover. In: Baader, F. (ed.) CADE 2003. LNCS, vol. 2741, pp. 274–278. Springer, Heidelberg (2003). doi:10.1007/978-3-540-45085-6_21 CrossRef

17.

Karaman, S., Frazzoli, E.: Vehicle routing problem with metric temporal logic specifications. In: Proceedings of CDC 2008, pp. 3953–3958. IEEE (2008)

18.

LS4. https://github.com/quickbeam123/ls4

19.

NuSMV. http://nusmv.fbk.eu/

20.

Ouaknine, J., Worrell, J.: Some recent results in metric temporal logic. In: Cassez, F., Jard, C. (eds.) FORMATS 2008. LNCS, vol. 5215, pp. 1–13. Springer, Heidelberg (2008). doi:10.1007/978-3-540-85778-5_1 CrossRef

21.

pltl. http://users.cecs.anu.edu.au/rpg/PLTLProvers/

22.

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

23.

Schuppan, V., Darmawan, L.: Evaluating LTL satisfiability solvers. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol. 6996, pp. 397–413. Springer, Heidelberg (2011). doi:10.1007/978-3-642-24372-1_28 CrossRef

24.

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

25.

Suda, M., Weidenbach, C.: A PLTL-prover based on labelled superposition with partial model guidance. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol. 7364, pp. 537–543. Springer, Heidelberg (2012). doi:10.1007/978-3-642-31365-3_42 CrossRef

26.

Thati, P., Roşu, G.: Monitoring algorithms for metric temporal logic specifications. Electronic Notes Theoret. Comput. Sci. 113, 145–162 (2005)CrossRef

27.

TRP++. http://cgi.csc.liv.ac.uk/konev/software/trp++/

28.

Tseitin, G.S.: On the complexity of derivation in propositional calculus. In: Siekmann, J.H., et al. (eds.) Automation of Reasoning, pp. 466–483. Springer, Heidelberg (1983)CrossRef

Title: Theorem Proving for Metric Temporal Logic over the Naturals
Authors: Ullrich Hustadt
Ana Ozaki
Clare Dixon
Publisher: Springer International Publishing
Book: Automated Deduction – CADE 26
Print ISBN: 978-3-319-63045-8

Electronic ISBN: 978-3-319-63046-5

Copyright Year: 2017
DOI: https://doi.org/10.1007/978-3-319-63046-5_20

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner