SpringerLink
Log in

An application of temporal projection to interleaving concurrency

  • Original Article
  • Published:
Formal Aspects of Computing

Abstract

We revisit the earliest temporal projection operator \({\Pi}\) in discrete-time Propositional Interval Temporal Logic (PITL) and use it to formalise interleaving concurrency. The logical properties of \({\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, as are stutter-invariant formulas. Striking similarities between the expressiveness of \({\Pi}\) and the standard LTL operator \({\mathcal{U}}\) (‘until’) are briefly illustrated. We also formalise concurrent imperative programming constructs with and without \({\Pi}\), and relate the two approaches. Peterson’s mutual exclusion algorithm is used to illustrate reasoning with \({\Pi}\) about a concrete programming example. Projection with fairness and non-fairness assumptions are both discussed. This all illustrates an approach to the analysis of such concurrent interleaving finite-state systems using temporal logic formulas with projection constructs to reason about correctness properties. Unlike conventional LTL formulas about concurrency which normally largely focus on global time, properties expressed in LTL combined with \({\Pi}\) help to reveal and analyse important differing viewpoints involving global time and the local projected time seen by each individual process. Links between \({\Pi}\) and another standard PITL projection operator, both suitable for reasoning about different time granularities, are demonstrated by showing the two operators to be interdefinable. We briefly look at other (mostly interval-based) temporal logics with similar forms of projection, as well as some related applications and industrial standards.

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

Access this article

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

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Ben-Ari M (2006) Principles of concurrent and distributed programming, 2nd edn. Addison-Wesley, Harlow

    MATH  Google Scholar 

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

    MathSciNet  MATH  Google Scholar 

  3. Baier C, Katoen J-P (2008) Principles of model checking. MIT Press, Cambridge, MA

  4. Bäumler S, Schellhorn G, Tofan B, Reif W (2011) Proving linearizability with temporal logic.. Form Asp Comput 23(1): 91–112

    Article  MathSciNet  MATH  Google Scholar 

  5. Cerny E, Dudani S, Havlicek J, Korchemny D (2015) SVA: the power of assertions in systemVerilog, 2nd edn. Springer, Cham

  6. Clarke EM, Grumberg O, Peled DA (1999) Model checking. MIT Press, Cambridge, MA

  7. Chellas BF (1980) Modal logic: an introduction. Cambridge University Press, Cambridge, UK

  8. Van Hung D (January 2000) Projections: A technique for verifying real-time programs in DC. Technical report 178, UNU/IIST, Macau, 1999. Also in proceedings of conference on information technology and education, Ho Chi Minh city, Vietnam

  9. Volker D, Gastin P (2008) First-order definable languages. In: Flum J, Grädel E, Wilke T (eds) Logic and automata: history and perspectives, volume 2 of texts in logic and games. Amsterdam University Press, Amsterdam, pp 261–306

  10. Duan Z, Koutny M, Holt C (1994) Projection in temporal logic programming. In: Pfennig F (ed) LPAR ’94, volume 822 of LNCS. Springer, Berlin, pp 333–344

  11. Dax C, Klaedtke F, Leue S (2009) Specification languages for stutter-invariant regular properties. In: Liu Z, Ravn AP (eds) 7th International symposium on automated technology for verification and analysis (ATVA 2009), volume 5799 of LNCS. Springer, Berlin, pp 244–254

  12. de Roever W-P, de Boer F, Hanneman U, Hooman J, Lakhnech Y, Poel M, Zwiers J (2001) Concurrency verification: introduction to compositional and noncompositional methods. Cambridge University Press, Cambridge

    MATH  Google Scholar 

  13. Duan Z (1996) An extended interval temporal logic and a framing technique for temporal logic programming. PhD thesis, Department of Computing Science, Newcastle University, Newcastle upon Tyne, England, Tech. rep. 556

  14. Duan Z, Yang X, Koutny M (2008) Framed temporal logic programming.. Sci Comput Progr 70(1): 31–61

    Article  MathSciNet  MATH  Google Scholar 

  15. Eisner C, Fisman D (2006) A practical introduction to PSL. Springer, New York

    Google Scholar 

  16. Eisner C, Fisman D (2015) Temporal logic made practical. http://www.cis.upenn.edu/~fisman/documents/EF_HBMC14.pdf, 2014. Accessed 4 June 2015. In: Clarke EM, Henzinger TA, Veith H (eds) Expected to appear in 2018 in Handbook of model checking. Springer, Cham

  17. Eisner C, Fisman D, Havlicek J, McIsaac A, Van Campenhout D (2003) The definition of a temporal clock operator. In: Baeten JCM, Lenstra JK, Parrow J, Woeginger GJ (eds) ICALP 2003, volume 2719 of LNCS. Springer, Berlin, pp 857–870

  18. Allen EE (1990) Temporal and modal logic. In: van Leeuwen J (ed) Handbook of theoretical computer science, volume B: formal models and semantics, chapter 16. Elsevier/MIT Press, Amsterdam, pp 995–1072

  19. Guelev DP, Van Hung D (2002) Prefix and projection onto state in duration calculus.. Electr Notes Theor Comput Sci 65(6): 101–119

    Article  MATH  Google Scholar 

  20. Guelev DP, Van Hung D (2004) A relatively complete axiomatisation of projection onto state in the duration calculus.. J Appl Non Class Log 14(1-2): 149–180

    Article  MATH  Google Scholar 

  21. Gelade W (2010) Succinctness of regular expressions with interleaving, intersection and counting.. Theor Comput Sci 411(31–33): 2987–2998

    Article  MathSciNet  MATH  Google Scholar 

  22. Gischer J (1981) Shuffle languages, Petri nets, and context-sensitive grammars.. Commun ACM 24(9): 597–605

    Article  MathSciNet  MATH  Google Scholar 

  23. Gischer J (1988) The equational theory of pomsets.. Theor Comput Sci 61: 199–224

    Article  MathSciNet  MATH  Google Scholar 

  24. Godefroid P (1996) Partial-order methods for the verification of concurrent systems: an approach to the state-explosion problem, volume 1032 of LNCS. Springer, Berlin

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

    Article  MathSciNet  MATH  Google Scholar 

  26. Guelev DP (2004) Logical interpolation and projection onto state in the duration calculus.. J Appl Non Class Log 14(1–2): 181–208

    Article  MathSciNet  MATH  Google Scholar 

  27. Godefroid P, Wolper P (1991) A partial approach to model checking. In: 6th Annual symposium on logic in computer science (LICS ’91). IEEE Computer Society, Los Alamitos, pp 406–415

  28. Godefroid P, Wolper P (1991) Using partial orders for the efficient verification of deadlock freedom and safety properties. In: Larsen KG, Skou A (eds) 3rd International workshop on computer aided verification (CAV ’91), volume 575 of LNCS. Springer, Berlin, pp 332–342

  29. Godefroid P, Wolper P (1993) Using partial orders for the efficient verification of deadlock freedom and safety properties.. Form Methods Syst Des 2(2): 149–164

    Article  MATH  Google Scholar 

  30. Hughes GE, Cresswell MJ (1996) A new introduction to modal logic. Routledge, London

    Book  MATH  Google Scholar 

  31. He J (1999) A behavioral model for co-design. In: Wing JM, Woodcock J, Davies J (eds) FM’99, vol II, volume 1709 of LNCS. Springer, Berlin, pp 1420–1438

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

  33. Hollander Y, Morley M, Noy A (2001) The e language: a fresh separation of concerns. In: Proceedings of TOOLS Europe 2001: 38th internationa’l conference on technology of object-oriented languages and systems, components for mobile computing. IEEE Computer Society, Los Alamitos, pp 41–50

  34. Holzmann G (2003) The SPIN model checker: primer and reference manual. Addison-Wesley Professional, Boston

    Google Scholar 

  35. IEEE (2010) Standard for property specification language (PSL), standard 1850–2010. ANSI/IEEE, New York

  36. IEEE (2011) Standard for the functional verification language e, standard 1647–2011. ANSI/IEEE, New York

  37. IEEE (2012) Standard for systemVerilog—unified hardware design, specification, and verification language, standard 1800–2012. ANSI/IEEE, New York

  38. ISO (1986) Standard generalized markup language (SGML): ISO 8879:1986. International Organization for Standardization, Geneva, Switzerland

  39. ITL web pages. http://www.antonio-cau.co.uk/ITL/. Accessed 8 June 2015

  40. Jones CB, Hayes IJ, Colvin RJ (2015) Balancing expressiveness in formal approaches to concurrency.. Form Asp Comput 27(3): 475–497

    Article  MathSciNet  MATH  Google Scholar 

  41. Jones CB (October 1983) Tentative steps toward a development method for interfering programs. ACM Trans Program Lang Syst 5(4):596–619

  42. Keller RM (1976) Formal verification of parallel programs.. Commun ACM 19(7): 371–384

    Article  MathSciNet  MATH  Google Scholar 

  43. Kröger F, Merz S (2008) Temporal logic and state systems. Texts in theoretical computer science (an EATCS series). Springer, Berlin

  44. Katz S, Peled D (1987) Interleaving set temporal logic. In: 6th Annual ACM symposium on principles of distributed computing (PODC ’87). ACM, New York, pp 178–190

  45. Katz S, Peled DA (1990) Interleaving set temporal logic.. Theor Comput Sci 75(3): 263–287

    Article  MathSciNet  MATH  Google Scholar 

  46. Katz S, Peled DA (1992) Verification of distributed programs using representative interleaving sequences.. Distrib Comput 6(2): 107–120

    Article  MathSciNet  MATH  Google Scholar 

  47. Lamport L (1983) What good is temporal logic? In: Mason REA (ed.) Information Processing 83, pp. 657–668. North-Holland,

  48. Lamport L (2002) Specifying Systems: The TLA+ language and tools for hardware and software engineers. Addison-Wesley Professional, Boston, MA, USA

  49. Lichtenstein O, Pnueli A, Zuck L (1985) The glory of the past. In: Parikh R (ed) Logics of Programs, volume 193 of LNCS. Springer, Berlin, pp 196–218

  50. Moszkowski B, Guelev DP (2015) An application of temporal projection to interleaving concurrency. In: Li X, Liu Z, Yi W (eds) Dependable software engineering: theories, tools, and applications—first international symposium (SETTA 2015), volume 9409 in LNCS. Springer, Cham, pp 153–167

  51. Moszkowski B, Manna Z (1984) Reasoning in interval temporal logic. In: Clarke EM, Kozen D (eds) Proceedings of workshop on logics of programs, Pittsburgh, PA, June, 1983, volume 164 of LNCS. Springer, Berlin, pp 371–382

  52. Morley MJ (1999) Semantics of temporal e. In: Melham TF, Moller FG (eds) Banff’99 higher order workshop: formal methods in computation, Ullapool, Scotland, 9–11 Sept. 1999. Technical Report, Department of Computing Science, University of Glasgow, Glasgow, Scotland, pp 138–142

  53. Moszkowski B (1983) Reasoning about digital circuits. PhD thesis, Department of Computer Science, Stanford University, June 1983. Technical report STAN–CS–83–970

  54. Moszkowski B (1986) Executing temporal logic programs. Cambridge University Press, Cambridge

    MATH  Google Scholar 

  55. Moszkowski B (1995) Compositional reasoning about projected and infinite time. In: Proceedings of 1st IEEE internationa’l conference on engineering of complex computer systems (ICECCS’95). IEEE Computer Society, Los Alamitos, pp 238–245

  56. Moszkowski B (2000) An automata-theoretic completeness proof for interval temporal logic (extended abstract). In: Montanari U, Rolim J, Welzl E (eds) Proceedings of 27th international colloquium on automata, languages and programming (ICALP 2000), volume 1853 of LNCS. Springer, Berlin, pp 223–234

  57. Moszkowski B (2004) A hierarchical completeness proof for propositional interval temporal logic with finite time. J Appl Non Class Log 14(1–2):55–104. Special issue on interval temporal logics and duration calculi. Goranko V, Montanari A, guest editors

  58. Moszkowski B (2012) A complete axiom system for propositional interval temporal logic, with infinite time.. Log Meth Comp Sci 8(3): 10–156

    MathSciNet  MATH  Google Scholar 

  59. Moszkowski B (2013) Interconnections between classes of sequentially compositional temporal formulas.. Inf Process Lett 113(9): 350–353

    Article  MathSciNet  MATH  Google Scholar 

  60. Moszkowski B (2014) Compositional reasoning using intervals and time reversal.. Ann Math Artif Intell 71(1–3): 175–250

    Article  MathSciNet  MATH  Google Scholar 

  61. Manna Z, Pnueli A (1992) The temporal logic of reactive and concurrent systems: specifications. Springer, New York

    Book  MATH  Google Scholar 

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

    Article  Google Scholar 

  63. Olderog E-R, Dierks H (2008) Real-time systems: formal specification and automatic verification. Cambridge University Press, Cambridge

    Book  MATH  Google Scholar 

  64. Olderog E-R, Hoare CAR (1983) Specification-oriented semantics for communicating processes. In: Díaz J (ed) Automata, languages and programming, 10th colloquium (ICALP 1983), volume 154 of LNCS. Springer, Berlin, pp 561–572

  65. Olderog E-R, Hoare CAR (1986) Specification-oriented semantics for communicating processes.. Acta Inf 23(1): 9–66

    Article  MathSciNet  MATH  Google Scholar 

  66. OWL-S (2004) Semantic markup for web services. http://www.w3.org/Submission/OWL-S/. Accessed 14 March 2016

  67. Peng F, Chen H (2015) Discovering restricted regular expressions with interleaving. In: Reynold C, Bin C, Zhenjie Z, Ruichu C, Jia X (eds) 17th Asia-Pacific Web conference on web technologies and applications (APWeb 2015), volume 9313 of LNCS. Springer, Cham, pp 104–115

  68. Peng F, Chen H, Mou X (2015) Deterministic regular expressions with interleaving. In: Leucker M, Rueda C, Valencia FD (eds) 12th International colloquium on theoretical aspects of computing (ICTAC 2015), volume 9399 of LNCS. Springer, Cham, pp 203–220

  69. Peled D (1993) All from one, one for all: on model checking using representatives. In: Costas Courcoubetis, (ed), 5th International conference on computer aided verification (CAV ’93), volume 697 of LNCS. Springer, Berlin, pp 409–423

  70. Peled D (1996) Combining partial order reductions with on-the-fly model-checking.. Methods in System Design. 8(1): 39–64

    Article  Google Scholar 

  71. Peterson GL (1981) Myths about the mutual exclusion problem.. Inf Process Lett 12(3): 115–116

    Article  MATH  Google Scholar 

  72. Peled D, Wilke T (1997) Stutter-invariant temporal properties are expressible without the next-time operator.. Inf Process Lett 63(5): 243–246

    Article  MathSciNet  MATH  Google Scholar 

  73. Schellhorn G, Tofan B, Ernst G, Pfähler J, Reif W (2014) RGITL: a temporal logic framework for compositional reasoning about interleaved programs. Ann Math Artif Intell 71(1–3):131–174

  74. Taubenfeld G (2006) Synchronization algorithms and concurrent programming. Pearson/Prentice Hall, Harlow

  75. Valmari A (1991) Stubborn sets for reduced state space generation. In: Rozenberg G (ed) Advances in Petri nets 1990, volume 483 of LNCS. Springer, Berlin, pp 491–515

  76. Valmari A (1992) A stubborn attack on state explosion.. Form Methods Syst Des 1(4): 297–322

    Article  MATH  Google Scholar 

  77. Yang C, Duan Z (2010) Compositional verification with stutter-invariant propositional projection temporal logic. In: Proceedings of the 14th WSEAS international conference on computers: part of the 14th WSEAS CSCC multiconference—volume I, ICCOMP’10. Stevens Point, Wisconsin, USA, World Scientific and Engineering Academy and Society (WSEAS), pp 272–280

  78. Zhou C, Hansen MR (2004) Duration calculus: a formal approach to real-time systems. Springer, Berlin

    MATH  Google Scholar 

  79. Zhou C, Hoare CAR, Ravn AP (1991) A calculus of durations.. Inf Process Lett 40(5): 269–276

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. School of Computing Science, Newcastle University, Newcastle upon Tyne, NE1 7RU, 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.

Additional information

Cliff Jones, Xuandong Li, and Zhiming Liu

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Moszkowski, B., Guelev, D.P. An application of temporal projection to interleaving concurrency. Form Asp Comp 29, 705–750 (2017). https://doi.org/10.1007/s00165-017-0417-3

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s00165-017-0417-3

Keywords

Search

Navigation