×

zbMATH — the first resource for mathematics

Theorem proving for pointwise metric temporal logic over the naturals via translations. (English) Zbl 1459.03012
Summary: 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 (i) a strict monotonic function and by (ii) a non-strict monotonic function (which allows multiple states to be mapped to the same time point). We use this logic to model examples from robotics, traffic management, and scheduling, discussing the effects of different modelling choices. 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. We also define a branching-time version of the logic and provide translations into computation tree logic.
MSC:
03B35 Mechanization of proofs and logical operations
03B44 Temporal logic
03B70 Logic in computer science
68T40 Artificial intelligence for robotics
68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
90B20 Traffic problems in operations research
90B35 Deterministic scheduling theory in operations research
Software:
GitHub; NuSMV; TRP++; TSPASS
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Aalta. http://lab205.org/aalta/
[2] Abbas, H.; Fainekos, G.; Sankaranarayanan, S.; Ivančić, F.; Gupta, A., Probabilistic temporal logic falsification of cyber-physical systems, ACM Trans. Embedded Comput. Syst. (TECS), 12, 2, 95:1-95:30 (2013)
[3] Alqahtani, S., Riley, I., Taylor, S., Gamble, R., Mailler, R.: MTL robustness for path planning with A*. In: André, E., Koenig, S., Dastani, M., Sukthankar, G. (eds.) International Foundation for Autonomous Agents and Multiagent Systems, AAMAS 2018, pp. 247-255 (2018)
[4] Alur, R.; Courcoubetis, C.; Dill, DL, Model-checking in dense real-time, Inf. Comput., 104, 1, 2-34 (1993) · Zbl 0783.68076
[5] Alur, R.; Feder, T.; Henzinger, TA, The benefits of relaxing punctuality, J. ACM, 43, 1, 116-146 (1996) · Zbl 0882.68021
[6] Alur, R.; Henzinger, TA, Real-time logics: complexity and expressiveness, Inf. Comput., 104, 1, 35-77 (1993) · Zbl 0791.68103
[7] Alur, R.; Henzinger, TA, A really temporal logic, J. ACM, 41, 1, 181-204 (1994) · Zbl 0807.68065
[8] Alur, R.; Henzinger, TA; Ho, P., Automatic symbolic verification of embedded systems, IEEE Trans. Softw. Eng., 22, 3, 181-201 (1996)
[9] Baader, F., Borgwardt, S., Koopmann, P., Ozaki, A., Thost, V.: Metric temporal description logics with interval-rigid names. In: Dixon, C., Finger, M. (eds.) FroCoS 2017, LNCS, vol. 10483, pp. 60-76 (2017). 10.1007/978-3-319-66167-4_4 · Zbl 06821627
[10] Bersani, MM; Rossi, M.; San Pietro, P., A tool for deciding the satisfiability of continuous-time metric temporal logic, Acta Inform., 53, 2, 171-206 (2016) · Zbl 1336.68230
[11] Bertello, M.; Gigante, N.; Montanari, A.; Reynolds, M.; Kambhampati, S., Leviathan: a new LTL satisfiability checking tool based on a one-pass tree-shaped tableau, IJCAI 2016, 950-956 (2016), Menlo Park: IJCAI/AAAI Press, Menlo Park
[12] Bouyer, P., Markey, N., Ouaknine, J., Worrell, J.: The cost of punctuality. In: LICS 2007, pp. 109-120. IEEE (2007). 10.1109/LICS.2007.49
[13] Brandt, S.; Kalaycı, EG; Kontchakov, R.; Ryzhikov, V.; Xiao, G.; Zakharyaschev, M.; Singh, S.; Markovitch, S., Ontology-based data access with a Horn fragment of metric temporal logic, AAAI 2017, 1070-1076 (2017), Menlo Park: AAAI Press, Menlo Park
[14] Brandt, S.; Kalaycı, EG; Ryzhikov, V.; Xiao, G.; Zakharyaschev, M., Querying log data with metric temporal logic, J. Artif. Intell. Res., 62, 829-877 (2018) · Zbl 1451.68087
[15] Cimatti, A.; Clarke, EM; Giunchiglia, E.; Giunchiglia, F.; Pistore, M.; Roveri, M.; Sebastiani, R.; Tacchella, A.; Brinksma, E.; Larsen, KG, NuSMV 2: An OpenSource tool for symbolic model checking, CAV 2002, LNCS, 359-364 (2002), Berlin: Springer, Berlin · Zbl 1010.68766
[16] 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) · Zbl 0890.90097
[17] Dixon, C.; Fisher, M.; Konev, B.; Konev, B.; Wolter, F., Temporal logic with capacity constraints, FroCoS 2007, LNCS, 163-177 (2007), Berlin: Springer, Berlin · Zbl 1148.03311
[18] Dixon, C.; Webster, M.; Saunders, J.; Fisher, M.; Dautenhahn, K.; Mistry, M.; Leonardis, A.; Witkowski, M.; Melhuish, C., “The Fridge Door is Open”-temporal verification of a robotic assistant’s behaviours, TAROS 2014, LNCS, 97-108 (2014), Berlin: Springer, Berlin
[19] Duque, I.; Dautenhahn, K.; Koay, KL; Willcock, L.; Christianson, B.; Miller, L., Knowledge-driven user activity recognition for a smart house - development and validation of a generic and low-cost, resource-efficient system, ACHI 2013, 141-146 (2013), Wilmington: IARIA XPS Press, Wilmington
[20] Emerson, E.; Mok, A.; Sistla, A.; Srinivasan, J., Quantitative temporal reasoning, Real-Time Syst., 4, 4, 331-352 (1992)
[21] Emerson, EA; Halpern, JY; Lewis, HR; Simons, BB; Burkhard, WA; Landweber, LH, Decision procedures and expressiveness in the temporal logic of branching time, STOC 1982, 169-180 (1982), New York: ACM, New York
[22] Fainekos, GE; Pappas, GJ, Robustness of temporal logic specifications for continuous-time signals, Theor. Comput. Sci., 410, 42, 4262-4291 (2009) · Zbl 1186.68287
[23] Fisher, M., A normal form for temporal logics and its applications in theorem-proving and execution, J. Logic Comput., 7, 4, 429-456 (1997) · Zbl 0893.03003
[24] Gabbay, D.; Pnueli, A.; Shelah, S.; Stavi, J.; Abrahams, PW; Lipton, RJ; Bourne, SR, On the temporal analysis of fairness, POPL 1980, 163-173 (1980), New York: ACM, New York
[25] 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) · Zbl 1191.68634
[26] Goré, R.; Demri, S.; Kapur, D.; Weidenbach, C., And-or tableaux for fixpoint logics with converse: LTL, CTL, PDL and CPDL, IJCAR 2014, LNCS, 26-45 (2014), Berlin: Springer, Berlin · Zbl 1423.68415
[27] Graham, RL, Bounds for certain multiprocessing anomalies, Bell Labs Tech. J., 45, 9, 1563-1581 (1966) · Zbl 0168.40703
[28] Gunadi, H.; Tiu, A.; Jones, C.; Pihlajasaari, P.; Sun, J., Efficient runtime monitoring with metric temporal logic: a case study in the Android operating system, FM 2014, LNCS, 296-311 (2014), Berlin: Springer, Berlin
[29] Gutiérrez-Basulto, V.; Jung, JC; Ozaki, A.; Kaminka, GA; Fox, M., On metric temporal description logics, ECAI 2016, Frontiers in Artificial Intelligence and Applications, 837-845 (2016), Amsterdam: IOS Press, Amsterdam · Zbl 1403.68265
[30] Hoxha, B., Mavridis, N., Fainekos, G.: VISPEC: A graphical tool for elicitation of MTL requirements. In: IROS 2015, vol. 2015-December, pp. 3486-3492. IEEE, New York (2015). 10.1109/IROS.2015.7353863
[31] Hustadt, U., Dixon, C., Ozaki, A.: Mtl: Tools and experiments. University of Liverpool, Liverpool http://cgi.csc.liv.ac.uk/ ullrich/MTL (2019)
[32] Hustadt, U., Konev, B.: \(TRP^{\mathtt{++}} 2.0\): a temporal resolution prover. In: Baader, F. (ed.) Proceedings of the CADE-19, LNCS, vol. 2741, pp. 274-278. Springer, Berlin (2003). 10.1007/978-3-540-45085-6_21
[33] Hustadt, U.; Ozaki, A.; Dixon, C.; de Moura, L., Theorem proving for metric temporal logic over the naturals, CADE-26, LNCS, 326-343 (2017), Berlin: Springer, Berlin · Zbl 06778412
[34] Janssen, G.: Logics for digital circuit verification: Theory, algorithms, and applications. Ph.D. thesis, Eindhoven University of Technology, Eindhoven (1999)
[35] Karaman, S., Frazzoli, E.: Vehicle routing problem with metric temporal logic specifications. In: CDC 2008, pp. 3953-3958. IEEE (2008). 10.1109/CDC.2008.4739366
[36] Leviathan. https://github.com/Corralx/leviathan
[37] Li, J.; Yao, Y.; Pu, G.; Zhang, L.; He, J.; Cheung, SC; Orso, A.; Storey, MAD, Aalta: an LTL satisfiability checker over infinite/finite traces, SIGSOFT FSE 2014, 731-734 (2014), New York: ACM, New York
[38] Liu, W.; Winfield, A., Modelling and optimisation of adaptive foraging in swarm robotic systems, Int. J. Robot. Res., 29, 14, 1743-1760 (2010)
[39] Logics Workbench. http://www.lwb.unibe.ch/index.html
[40] LS4. https://github.com/quickbeam123/ls4
[41] Ludwig, M.; Hustadt, U.; Lutz, C.; Raskin, J., Resolution-based model construction for PLTL, TIME 2009, 73-80 (2009), New York: IEEE, New York
[42] Ludwig, M.; Hustadt, U., Implementing a fair monodic temporal logic prover, AI Commun., 23, 2-3, 69-96 (2010) · Zbl 1206.68283
[43] Luo, R.; Valenzano, RA; Li, Y.; Beck, JC; McIlraith, SA; Baral, C.; Delgrande, JP; Wolter, F., Using metric temporal logic to specify scheduling problems, KR 2016, 581-584 (2016), Menlo Park: AAAI Press, Menlo Park
[44] Mohammed, A.; Furbach, U.; Dennis, L.; Boissier, O.; Bordini, RH, MAS: qualitative and quantitative reasoning, ProMAS 2011, LNCS, 114-132 (2011), Berlin: Springer, Berlin
[45] NuSMV. http://nusmv.fbk.eu/
[46] Ouaknine, J.; Worrell, J.; Cassez, F.; Jard, C., Some recent results in metric temporal logic, FORMATS 2008, LNCS, 1-13 (2008), Berlin: Springer, Berlin · Zbl 1171.68553
[47] pltl. http://users.cecs.anu.edu.au/ rpg/PLTLProvers/
[48] Pnueli, A.: The temporal logic of programs. In: Proceedings of the SFCS ’77, pp. 46-57. IEEE (1977). 10.1109/SFCS.1977.32
[49] Reynolds, M.: A new rule for LTL tableaux. In: D. Cantone, G. Delzanno (eds.) GandALF 2016, EPTCS, vol. 226, pp. 287-301 (2016). 10.4204/EPTCS.226.20
[50] Schwendimann, S.; de Swart, HCM, A new one-pass tableau calculus for PLTL, TABLEAUX 1998, LNCS, 277-292 (1998), Berlin: Springer, Berlin · Zbl 0903.03015
[51] Sistla, AP; Clarke, EM, The complexity of propositional linear temporal logics, J. ACM, 32, 3, 733-749 (1985) · Zbl 0632.68034
[52] Suda, M.; Weidenbach, C.; Gramlich, B.; Miller, D.; Sattler, U., A PLTL-prover based on labelled superposition with partial model guidance, IJCAR 2012, LNCS, 537-543 (2012), Berlin: Springer, Berlin · Zbl 1358.68266
[53] Thati, P.; Roşu, G., Monitoring algorithms for metric temporal logic specifications, Electron. Notes Theor. Comput. Sci., 113, 145-162 (2005)
[54] \(TRP^{\mathtt{++}} \). http://cgi.csc.liv.ac.uk/ konev/software/trp++/
[55] Tseitin, GS; Siekmann, JH; Wrightson, G., On the complexity of derivation in propositional calculus, Automation of Reasoning, vol 2: Classical Papers on Computational Logic 1967-1970, 466-483 (1983), Berlin: Springer, Berlin
[56] TSPASS. http://cgi.csc.liv.ac.uk/ michael/TLBook/TSPASS-System/
[57] Webster, M.; Dixon, C.; Fisher, M.; Salem, M.; Saunders, J.; Koay, KL; Dautenhahn, K.; Saez-Pons, J., Toward reliable autonomous robotic assistants through formal verification: a case study, IEEE Trans. Hum. Mach. Syst., 46, 2, 186-196 (2016)
[58] Zhang, L.; Hustadt, U.; Dixon, C., A resolution calculus for the branching-time temporal logic CTL, ACM Trans. Comput. Log, 15, 1, 10:1-10:38 (2014) · Zbl 1287.03033
[59] Zhou, Y., Maity, D., Baras, J.S.: Optimal mission planner with timed temporal logic constraints. In: ECC 2015, pp. 759-764. IEEE, New York (2015). 10.1109/ECC.2015.7330634
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.