SpringerLink
Log in

The Comparison of Expressiveness Between LTL and IGPoLTL

  • Conference paper
  • First Online:
Quantitative Logic and Soft Computing 2016

Part of the book series: Advances in Intelligent Systems and Computing ((AISC,volume 510))

  • 561 Accesses

Abstract

The expressiveness of linear temporal logic plays an important role in model checking. But the expressiveness of linear temporal logic based on generalized possibility measure has not been researched roundly. We compare the expressiveness of linear temporal logic (LTL) and interval generalized possibilistic linear temporal logic (IGPoLTL), and prove that LTL is a proper subclass of IGPoLTL. Besides, we define the \(\alpha \)-equivalence between LTL formulae and IGPoLTL formulae and get some corresponding properties.

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
EUR 32.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or Ebook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 169.00
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 219.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free ship** worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

References

  1. Baier, C., Katoen, J.P.: Principles of Model Checking. The MIT Press, Cambridge (2008)

    MATH  Google Scholar 

  2. Clark, E.M., Grumberg, O., Peled, D.: Model Checking. The MIT Press, Cambridge (1999)

    Google Scholar 

  3. Rozier, K.Y.: Linear temporal logic symbolic model checking. Comput. Sci. Rev. 5(2), 163–203 (2011)

    Article  MATH  Google Scholar 

  4. Li, Y.M., Li, L.J.: Model checking of linear-time properties based on possibility measure. IEEE Trans. Fuzzy Syst. 21(5), 842–854 (2013)

    Article  Google Scholar 

  5. Li, Y.M., Li, Y.L., Ma, Z.Y.: Computation tree logic model checking based on possibility measures. Fuzzy Sets Syst. 262, 44–59 (2015)

    Article  MathSciNet  Google Scholar 

  6. Chechik, M., Devereux, B., Gurfinkel, A., Easterbrook, S.: Multi-valued symbolic model-checking. ACM Trans. Softw. Eng. Methodol. 12(4), 371–408 (2003)

    Article  MATH  Google Scholar 

  7. Chechik, M., Easterbrook, S., Petrovykh, V.: Model-checking over multi-valued logics. In: Proceeding of Formal Methods Europe (FME01). Lecture Notes in Computer Science, vol. 2021, pp. 72–98. Springer, Berlin (2001)

    Google Scholar 

  8. Chechik, M., Gurfinkel, A., Devereux, B., Lai, A., Easterbrook, S.: Data structures for symbolic multi-valued model-checking. Formal Methods Syst. Design 29, 295–344 (2006)

    Article  MATH  Google Scholar 

  9. Frigeri, A., Pasquale, L., Spoletini, P.: Fuzzy time in linear temporal logic. ACM Trans. Comput. Logic (TOCL) 15(4), Article No. 30 (2014)

    Google Scholar 

  10. Mukherjee, S., Dasgupta, P.: A fuzzy real-time temporal logic. Int. J. Approx. Reason. 54(9), 1452–1470 (2013)

    Article  MathSciNet  MATH  Google Scholar 

  11. Pan, H.Y., Li, Y.M., Cao, Y.Z., Ma, Z.Y.: Model checking fuzzy computation tree logic. Fuzzy Sets Syst. 262, 60–77 (2015)

    Article  MathSciNet  Google Scholar 

  12. Li, Y.M.: Quantitative model checking of linear-time properties based on generalized possibility measures (2016). ar**v:1601.06504

  13. Li, Y.M., Ma, Z.Y.: Quantitative computation tree logic model checking based on generalized possibility measures. IEEE Trans. Fuzzy Syst. 23(6), 2034–2047 (2015)

    Article  Google Scholar 

Download references

Acknowledgments

This work is supported by the NSFC (Grants No. 11271237, No. 61228305).

Author information

Authors and Affiliations

  1. College of Computer Science, Shaanxi Normal University, **’an, 710119, China

    Jia-Qi Dang & Yong-Ming Li

Authors
  1. Jia-Qi Dang
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Yong-Ming Li
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Jia-Qi Dang .

Editor information

Editors and Affiliations

  1. Zhejiang, Zhejiang Sci-Tech University Zhejiang, Hangzhou, China

    Tai-He Fan

  2. Fujian, Jimei University Fujian, **amen, China

    Shui-Li Chen

  3. Zhejiang, Zhejiang Sci-Tech University Zhejiang, Hangzhou, China

    San-Min Wang

  4. Yanta, Shaanxi Normal University Yanta, **’an, China

    Yong-Ming Li

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing Switzerland

About this paper

Cite this paper

Dang, JQ., Li, YM. (2017). The Comparison of Expressiveness Between LTL and IGPoLTL. In: Fan, TH., Chen, SL., Wang, SM., Li, YM. (eds) Quantitative Logic and Soft Computing 2016. Advances in Intelligent Systems and Computing, vol 510. Springer, Cham. https://doi.org/10.1007/978-3-319-46206-6_16

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-46206-6_16

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-46205-9

  • Online ISBN: 978-3-319-46206-6

  • eBook Packages: EngineeringEngineering (R0)

Publish with us

Policies and ethics

Search

Navigation