Skip to main content
SpringerLink
Log in

An Application of Temporal Projection to Interleaving Concurrency

  • Conference paper
  • First Online:
Dependable Software Engineering: Theories, Tools, and Applications (SETTA 2015)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 9409))

Abstract

We revisit the earliest temporal projection operator \(\mathrm \Pi \) in discrete-time Propositional Interval Temporal Logic (PITL) and use it to formalise interleaving concurrency. The logical properties of \(\mathrm{\Pi }\) as a normal modality and a way to eliminate it in both PITL and conventional point-based Linear-Time Temporal Logic (LTL), which can be viewed as a PITL subset, are examined. We also formalise concurrency without \(\mathrm{\Pi }\), and relate the two approaches. Furthermore, \(\mathrm{\Pi }\) and another standard PITL projection operator are interdefinable and both suitable for reasoning about different time granularities. We mention other (mostly interval-based) temporal logics with similar forms of projection, as well as some related applications and international standards.

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. Baier, C., Katoen, J.: Principles of Model Checking. MIT Press (2008)

    Google Scholar 

  2. Bäumler, S., Balser, M., Nafz, F., Reif, W., Schellhorn, G.: Interactive verification of concurrent systems using symbolic execution. AI Commun. 23(2–3), 285–307 (2010)

    MathSciNet  MATH  Google Scholar 

  3. Bäumler, S., Schellhorn, G., Tofan, B., Reif, W.: Proving linearizability with temporal logic. Formal Aspects of Computing 23(1), 91–112 (2011)

    Article  MathSciNet  MATH  Google Scholar 

  4. Ben-Ari, M.: Principles of Concurrent and Distributed Programming. Addison-Wesley, second edn. (2006)

    Google Scholar 

  5. Cerny, E., Dudani, S., Havlicek, J., Korchemny, D.: SVA: The Power of Assertions in SystemVerilog, 2nd edn. Springer, Heidelberg (2015)

    Google Scholar 

  6. Chellas, B.F.: Modal Logic: An Introduction. Cambridge University Press, Cambridge (1980)

    Book  MATH  Google Scholar 

  7. Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)

    Google Scholar 

  8. Dang, V.H.: Projections: A technique for verifying real-time programs in DC. Tech. Rep. 178, UNU/IIST, Macau (1999). In: Proc. Conf. on Information Technology and Education, Ho Chi Minh City, Vietnam, January 2000

    Google Scholar 

  9. Duan, Z.: An Extended Interval Temporal Logic and a Framing Technique for Temporal Logic Programming. Ph.D. thesis, Dept. Comp. Sci., tech. rep. 556, Newcastle University, UK (1996). http://hdl.handle.net/10443/2075

  10. Duan, Z., Koutny, M., Holt, C.: Projection in temporal logic programming. In: Pfenning, F. (ed.) LPAR 1994. LNCS, vol. 822, pp. 333–344. Springer, Heidelberg (1994)

    Chapter  Google Scholar 

  11. Duan, Z., Yang, X., Koutny, M.: Framed temporal logic programming. Science of Computer Programming 70(1), 31–61 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  12. Eisner, C., Fisman, D.: A Practical Introduction to PSL. Springer, Heidelberg (2006)

    Google Scholar 

  13. Eisner, C., Fisman, D.: Temporal logic made practical. In: Clarke, E.M., Henzinger, T.A., Veith, H. (eds.) Handbook of Model Checking. Springer (Expected 2016). http://www.cis.upenn.edu/~fisman/documents/EF_HBMC14.pdf

  14. Eisner, C., Fisman, D., Havlicek, J., McIsaac, A., Van Campenhout, D.: The definition of a temporal clock operator. In: Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J. (eds.) ICALP 2003. LNCS, vol. 2719, pp. 857–870. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  15. Guelev, D.P.: A complete proof system for first-order interval temporal logic with projection. J. Log. Comput. 14(2), 215–249 (2004)

    Article  MathSciNet  MATH  Google Scholar 

  16. Guelev, D.P.: Logical interpolation and projection onto state in the Duration Calculus. J. Applied Non-Classical Logics 14(1–2), 181–208 (2004)

    Article  MathSciNet  MATH  Google Scholar 

  17. Guelev, D.P., Dang, V.H.: Prefix and projection onto state in duration calculus. Electr. Notes Theor. Comput. Sci. 65(6), 101–119 (2002)

    Article  MATH  Google Scholar 

  18. Guelev, D.P., Dang, V.H.: A relatively complete axiomatisation of projection onto state in the Duration Calculus. J. Applied Non-Classical Logics 14(1–2), 149–180 (2004)

    Article  MATH  Google Scholar 

  19. Halpern, J., Manna, Z., Moszkowski, B.: A hardware semantics based on temporal intervals. In: Diaz, J. (ed.) ICALP 1983. LNCS, vol. 154, pp. 278–291. Springer, Heidelberg (1983)

    Google Scholar 

  20. He, J.: A behavioral model for co-design. In: Wing, J.M., Woodcock, J., Davies, J. (eds.) FM 1999. LNCS, vol. 1709, pp. 1420–1438. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  21. Hollander, Y., Morley, M., Noy, A.: The e language: a fresh separation of concerns. In: Proc. TOOLS Europe 2001: 38th Int’l Conf. on Technology of Object-Oriented Languages and Systems, Components for Mobile Computing, pp. 41–50. IEEE Computer Society Press (2001)

    Google Scholar 

  22. Holzmann, G.: The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley Professional (2003)

    Google Scholar 

  23. Hughes, G.E., Cresswell, M.J.: A New Introduction to Modal Logic. Routledge, London (1996)

    Book  MATH  Google Scholar 

  24. IEEE: Standard for Property Specification Language (PSL), Standard 1850–2010. ANSI/IEEE, New York (2010)

    Google Scholar 

  25. IEEE: Standard for the Functional Verification Language e, Standard 1647–2011. ANSI/IEEE, New York (2011)

    Google Scholar 

  26. IEEE: Standard for SystemVerilog-Unified Hardware Design, Specification, and Verification Language, Standard 1800–2012. ANSI/IEEE, New York (2012)

    Google Scholar 

  27. ITL web pages. http://www.antonio-cau.co.uk/ITL/

  28. Jones, C.B.: Tentative steps toward a development method for interfering programs. ACM Trans. Program. Lang. Syst. 5(4), 596–619 (1983)

    Article  MATH  Google Scholar 

  29. Jones, C.B., Hayes, I.J., Colvin, R.J.: Balancing expressiveness in formal approaches to concurrency. Formal Asp. Comput. 27(3), 475–497 (2015)

    Article  MathSciNet  MATH  Google Scholar 

  30. Keller, R.M.: Formal verification of parallel programs. Commun. ACM 19(7), 371–384 (1976)

    Article  MathSciNet  MATH  Google Scholar 

  31. Kröger, F., Merz, S.: Temporal Logic and State Systems. Texts in Theoretical Computer Science (An EATCS Series). Springer, Heidelberg (2008)

    Google Scholar 

  32. Lamport, L.: Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley Professional (2002)

    Google Scholar 

  33. Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specifications. Springer, New York (1992)

    Book  MATH  Google Scholar 

  34. Morley, M.J.: Semantics of temporal e. In: Melham, T.F., Moller, F.G. (eds.) Banff’99 Higher Order Workshop: Formal Methods in Computation, Ullapool, Scotland, 9–11 Sept. 1999. pp. 138–142. Univ. Glasgow, Dept. Comp. Sci., tech. rep. (1999)

    Google Scholar 

  35. Moszkowski, B.: Reasoning about Digital Circuits. Ph.D. thesis, Department of Computer Science, Stanford University, tech. rep. STAN-CS-83-970 (June 1983)

    Google Scholar 

  36. Moszkowski, B.: Executing Temporal Logic Programs. Cambridge University Press, Cambridge (1986)

    MATH  Google Scholar 

  37. Moszkowski, B.: Compositional reasoning about projected and infinite time. In: Proc. 1st IEEE Int’l Conf. on Engineering of Complex Computer Systems (ICECCS’95), pp. 238–245. IEEE Computer Society Press (1995)

    Google Scholar 

  38. Moszkowski, B.: A hierarchical completeness proof for Propositional Interval Temporal Logic with finite time. J. Applied Non-Classical Logics 14(1–2), 55–104 (2004)

    Article  MATH  Google Scholar 

  39. Moszkowski, B.: A complete axiom system for propositional Interval Temporal Logic with infinite time. Log. Meth. Comp. Sci. 8(3:10), 1–56 (2012)

    MathSciNet  MATH  Google Scholar 

  40. Newcombe, C., Rath, T., Zhang, F., Munteanu, B., Brooker, M., Deardeuff, M.: How Amazon Web Services uses formal methods. Commun. ACM 58(4), 66–73 (2015)

    Article  Google Scholar 

  41. Olderog, E.R., Dierks, H.: Real-Time Systems: Formal Specification and Automatic Verification. Cambridge University Press, Cambridge (2008)

    Book  MATH  Google Scholar 

  42. Peterson, G.L.: Myths about the mutual exclusion problem. Inf. Process. Lett. 12(3), 115–116 (1981)

    Article  MATH  Google Scholar 

  43. de Roever, W.P., de Boer, F., Hanneman, U., Hooman, J., Lakhnech, Y., Poel, M., Zwiers, J.: Concurrency Verification: Introduction to Compositional and Noncompositional Methods. Cambridge University Press (2001)

    Google Scholar 

  44. Zhou, C., Hansen, M.R.: Duration Calculus: A Formal Approach to Real-Time Systems. Springer, Heidelberg (2004)

    MATH  Google Scholar 

  45. Zhou, C., Hoare, C.A.R., Ravn, A.P.: A calculus of durations. Inf. Process. Lett. 40(5), 269–276 (1991)

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. School of Computing Science, Newcastle University, Newcastle upon Tyne, UK

    Ben Moszkowski

  2. Department of Algebra and Logic, Institute of Mathematics and Informatics, Sofia, Bulgaria

    Dimitar P. Guelev

Authors
  1. Ben Moszkowski
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Dimitar P. Guelev
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Ben Moszkowski .

Editor information

Editors and Affiliations

  1. Nanjing University, Nanjing, Jiangsu, China

    Xuandong Li

  2. Birmingham City University, Birmingham, United Kingdom

    Zhiming Liu

  3. Uppsala University, Uppsala, Sweden

    Wang Yi

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this paper

Cite this paper

Moszkowski, B., Guelev, D.P. (2015). An Application of Temporal Projection to Interleaving Concurrency. In: Li, X., Liu, Z., Yi, W. (eds) Dependable Software Engineering: Theories, Tools, and Applications. SETTA 2015. Lecture Notes in Computer Science(), vol 9409. Springer, Cham. https://doi.org/10.1007/978-3-319-25942-0_10

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-25942-0_10

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-25941-3

  • Online ISBN: 978-3-319-25942-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation