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.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Ben-Ari M (2006) Principles of concurrent and distributed programming, 2nd edn. Addison-Wesley, Harlow
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
Baier C, Katoen J-P (2008) Principles of model checking. MIT Press, Cambridge, MA
Bäumler S, Schellhorn G, Tofan B, Reif W (2011) Proving linearizability with temporal logic.. Form Asp Comput 23(1): 91–112
Cerny E, Dudani S, Havlicek J, Korchemny D (2015) SVA: the power of assertions in systemVerilog, 2nd edn. Springer, Cham
Clarke EM, Grumberg O, Peled DA (1999) Model checking. MIT Press, Cambridge, MA
Chellas BF (1980) Modal logic: an introduction. Cambridge University Press, Cambridge, UK
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
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
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
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
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
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
Duan Z, Yang X, Koutny M (2008) Framed temporal logic programming.. Sci Comput Progr 70(1): 31–61
Eisner C, Fisman D (2006) A practical introduction to PSL. Springer, New York
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
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
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
Guelev DP, Van Hung D (2002) Prefix and projection onto state in duration calculus.. Electr Notes Theor Comput Sci 65(6): 101–119
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
Gelade W (2010) Succinctness of regular expressions with interleaving, intersection and counting.. Theor Comput Sci 411(31–33): 2987–2998
Gischer J (1981) Shuffle languages, Petri nets, and context-sensitive grammars.. Commun ACM 24(9): 597–605
Gischer J (1988) The equational theory of pomsets.. Theor Comput Sci 61: 199–224
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
Guelev DP (2004) A complete proof system for first-order interval temporal logic with projection.. J Log Comput 14(2): 215–249
Guelev DP (2004) Logical interpolation and projection onto state in the duration calculus.. J Appl Non Class Log 14(1–2): 181–208
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
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
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
Hughes GE, Cresswell MJ (1996) A new introduction to modal logic. Routledge, London
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
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
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
Holzmann G (2003) The SPIN model checker: primer and reference manual. Addison-Wesley Professional, Boston
IEEE (2010) Standard for property specification language (PSL), standard 1850–2010. ANSI/IEEE, New York
IEEE (2011) Standard for the functional verification language e, standard 1647–2011. ANSI/IEEE, New York
IEEE (2012) Standard for systemVerilog—unified hardware design, specification, and verification language, standard 1800–2012. ANSI/IEEE, New York
ISO (1986) Standard generalized markup language (SGML): ISO 8879:1986. International Organization for Standardization, Geneva, Switzerland
ITL web pages. http://www.antonio-cau.co.uk/ITL/. Accessed 8 June 2015
Jones CB, Hayes IJ, Colvin RJ (2015) Balancing expressiveness in formal approaches to concurrency.. Form Asp Comput 27(3): 475–497
Jones CB (October 1983) Tentative steps toward a development method for interfering programs. ACM Trans Program Lang Syst 5(4):596–619
Keller RM (1976) Formal verification of parallel programs.. Commun ACM 19(7): 371–384
Kröger F, Merz S (2008) Temporal logic and state systems. Texts in theoretical computer science (an EATCS series). Springer, Berlin
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
Katz S, Peled DA (1990) Interleaving set temporal logic.. Theor Comput Sci 75(3): 263–287
Katz S, Peled DA (1992) Verification of distributed programs using representative interleaving sequences.. Distrib Comput 6(2): 107–120
Lamport L (1983) What good is temporal logic? In: Mason REA (ed.) Information Processing 83, pp. 657–668. North-Holland,
Lamport L (2002) Specifying Systems: The TLA+ language and tools for hardware and software engineers. Addison-Wesley Professional, Boston, MA, USA
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
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
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
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
Moszkowski B (1983) Reasoning about digital circuits. PhD thesis, Department of Computer Science, Stanford University, June 1983. Technical report STAN–CS–83–970
Moszkowski B (1986) Executing temporal logic programs. Cambridge University Press, Cambridge
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
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
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
Moszkowski B (2012) A complete axiom system for propositional interval temporal logic, with infinite time.. Log Meth Comp Sci 8(3): 10–156
Moszkowski B (2013) Interconnections between classes of sequentially compositional temporal formulas.. Inf Process Lett 113(9): 350–353
Moszkowski B (2014) Compositional reasoning using intervals and time reversal.. Ann Math Artif Intell 71(1–3): 175–250
Manna Z, Pnueli A (1992) The temporal logic of reactive and concurrent systems: specifications. Springer, New York
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
Olderog E-R, Dierks H (2008) Real-time systems: formal specification and automatic verification. Cambridge University Press, Cambridge
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
Olderog E-R, Hoare CAR (1986) Specification-oriented semantics for communicating processes.. Acta Inf 23(1): 9–66
OWL-S (2004) Semantic markup for web services. http://www.w3.org/Submission/OWL-S/. Accessed 14 March 2016
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
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
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
Peled D (1996) Combining partial order reductions with on-the-fly model-checking.. Methods in System Design. 8(1): 39–64
Peterson GL (1981) Myths about the mutual exclusion problem.. Inf Process Lett 12(3): 115–116
Peled D, Wilke T (1997) Stutter-invariant temporal properties are expressible without the next-time operator.. Inf Process Lett 63(5): 243–246
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
Taubenfeld G (2006) Synchronization algorithms and concurrent programming. Pearson/Prentice Hall, Harlow
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
Valmari A (1992) A stubborn attack on state explosion.. Form Methods Syst Des 1(4): 297–322
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
Zhou C, Hansen MR (2004) Duration calculus: a formal approach to real-time systems. Springer, Berlin
Zhou C, Hoare CAR, Ravn AP (1991) A calculus of durations.. Inf Process Lett 40(5): 269–276
Author information
Authors and Affiliations
Corresponding author
Additional information
Cliff Jones, Xuandong Li, and Zhiming Liu
Rights and permissions
About this article
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
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s00165-017-0417-3