On the Expressiveness of Metric Temporal Logic over Bounded Timed Words

  • Hsi-Ming Ho
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8762)

Abstract

It is known that Metric Temporal Logic (MTL) is strictly less expressive than the Monadic First-Order Logic of Order and Metric (FO[<, +1]) in the pointwise semantics over bounded time domains (i.e., timed words of bounded duration) [15]. In this paper, we present an extension of MTL which has the same expressive power as (FO[<, +1]) in both the pointwise and continuous semantics over bounded time domains.

Keywords

Temporal Logic Expressive Power Counting Modality Tense Logic Continuous Semantic 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Alur, R., Dill, D.: A theory of timed automata. Theoretical Computer Science 126(2), 183–235 (1994)MathSciNetCrossRefMATHGoogle Scholar
  2. 2.
    Bouyer, P., Chevalier, F., Markey, N.: On the expressiveness of TPTL and MTL. In: Sarukkai, S., Sen, S. (eds.) FSTTCS 2005. LNCS, vol. 3821, pp. 432–443. Springer, Heidelberg (2005)Google Scholar
  3. 3.
    Hirshfeld, Y., Rabinovich, A.: Expressiveness of metric modalities for continuous time. In: Grigoriev, D., Harrison, J., Hirsch, E.A. (eds.) CSR 2006. LNCS, vol. 3967, pp. 211–220. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  4. 4.
    Hirshfeld, Y., Rabinovich, A.: Expressiveness of metric modalities for continuous time. Logical Methods in Computer Science 3(1) (2007)Google Scholar
  5. 5.
    Ho, H.M., Ouaknine, J., Worrell, J.: On the expressiveness of metric temporal logic over bounded timed words (2014), http://www.cs.ox.ac.uk/people/hsi-ming.ho/exp-full.pdf, full version
  6. 6.
    Ho, H.M., Ouaknine, J., Worrell, J.: Online monitoring of metric temporal logic. In: Bonakdarpour, B., Smolka, S.A. (eds.) RV 2014. LNCS, vol. 8734, pp. 178–192. Springer, Heidelberg (2014), http://www.cs.ox.ac.uk/people/hsi-ming.ho/monitoring-rv.pdf Google Scholar
  7. 7.
    Hunter, P.: When is metric temporal logic expressively complete? In: Proceedings of CSL 2013. LIPIcs, vol. 23, pp. 380–394. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2013)Google Scholar
  8. 8.
    Hunter, P., Ouaknine, J., Worrell, J.: Expressive completeness of metric temporal logic. In: Proceedings of LICS 2013, pp. 349–357. IEEE Computer Society Press (2013)Google Scholar
  9. 9.
    Kamp, J.: Tense logic and the theory of linear order. Ph.D. thesis, University of California, Los Angeles (1968)Google Scholar
  10. 10.
    Koymans, R.: Specifying real-time properties with metric temporal logic. Real-Time Systems 2(4), 255–299 (1990)CrossRefGoogle Scholar
  11. 11.
    Ouaknine, J., Rabinovich, A., Worrell, J.: Time-bounded verification. In: Bravetti, M., Zavattaro, G. (eds.) CONCUR 2009. LNCS, vol. 5710, pp. 496–510. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  12. 12.
    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)CrossRefGoogle Scholar
  13. 13.
    Ouaknine, J., Worrell, J.: Towards a theory of time-bounded verification. In: Abramsky, S., Gavoille, C., Kirchner, C., Meyer auf der Heide, F., Spirakis, P.G. (eds.) ICALP 2010. LNCS, vol. 6199, pp. 22–37. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  14. 14.
    Pandya, P.K., Shah, S.S.: On expressive powers of timed logics: Comparing boundedness, non-punctuality, and deterministic freezing. In: Katoen, J.-P., König, B. (eds.) CONCUR 2011. LNCS, vol. 6901, pp. 60–75. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  15. 15.
    Prabhakar, P., D’Souza, D.: On the expressiveness of MTL with past operators. In: Asarin, E., Bouyer, P. (eds.) FORMATS 2006. LNCS, vol. 4202, pp. 322–336. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  16. 16.
    Wilke, T.: Specifying timed state sequences in powerful decidable logics and timed automata. In: Langmaack, H., de Roever, W.-P., Vytopil, J. (eds.) FTRTFT 1994 and ProCoS 1994. LNCS, vol. 863, pp. 694–715. Springer, Heidelberg (1994)CrossRefGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2014

Authors and Affiliations

  • Hsi-Ming Ho
    • 1
  1. 1.Department of Computer ScienceUniversity of OxfordOxfordUK

Personalised recommendations