Skip to main content
SpringerLink
Log in

On the Expressiveness of Metric Temporal Logic over Bounded Timed Words

  • Conference paper
Reachability Problems (RP 2014)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 8762))

Included in the following conference series:

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.

More extensive technical details as well as all proofs can be found in the full version of this paper [5].

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Alur, R., Dill, D.: A theory of timed automata. Theoretical Computer Science 126(2), 183–235 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  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. 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)

    Chapter  Google Scholar 

  4. Hirshfeld, Y., Rabinovich, A.: Expressiveness of metric modalities for continuous time. Logical Methods in Computer Science 3(1) (2007)

    Google Scholar 

  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. 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. 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. 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. Kamp, J.: Tense logic and the theory of linear order. Ph.D. thesis, University of California, Los Angeles (1968)

    Google Scholar 

  10. Koymans, R.: Specifying real-time properties with metric temporal logic. Real-Time Systems 2(4), 255–299 (1990)

    Article  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, University of Oxford, Wolfson Building,Parks Road, Oxford, OX1 3QD, UK

    Hsi-Ming Ho

Authors
  1. Hsi-Ming Ho
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, University of Oxford, Wolfson Building, Parks Road, OX1 3QD, Oxford, UK

    Joël Ouaknine

  2. Department of Computer Science, University of Liverpool, Liverpool, UK

    Igor Potapov

  3. Department of Computer Science, University of Oxford, UK

    James Worrell

Rights and permissions

Reprints and permissions

Copyright information

© 2014 Springer International Publishing Switzerland

About this paper

Cite this paper

Ho, HM. (2014). On the Expressiveness of Metric Temporal Logic over Bounded Timed Words. In: Ouaknine, J., Potapov, I., Worrell, J. (eds) Reachability Problems. RP 2014. Lecture Notes in Computer Science, vol 8762. Springer, Cham. https://doi.org/10.1007/978-3-319-11439-2_11

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-11439-2_11

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-11438-5

  • Online ISBN: 978-3-319-11439-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation