{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,31]],"date-time":"2025-05-31T04:12:35Z","timestamp":1748664755021,"version":"3.41.0"},"publisher-location":"Cham","reference-count":45,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319259413"},{"type":"electronic","value":"9783319259420"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-25942-0_10","type":"book-chapter","created":{"date-parts":[[2015,10,16]],"date-time":"2015-10-16T09:32:14Z","timestamp":1444987934000},"page":"153-167","source":"Crossref","is-referenced-by-count":1,"title":["An Application of Temporal Projection to\u00a0Interleaving Concurrency"],"prefix":"10.1007","author":[{"given":"Ben","family":"Moszkowski","sequence":"first","affiliation":[]},{"given":"Dimitar P.","family":"Guelev","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,10,17]]},"reference":[{"key":"10_CR1","unstructured":"Baier, C., Katoen, J.: Principles of Model Checking. MIT Press (2008)"},{"issue":"2\u20133","key":"10_CR2","doi-asserted-by":"crossref","first-page":"285","DOI":"10.3233\/AIC-2010-0458","volume":"23","author":"S B\u00e4umler","year":"2010","unstructured":"B\u00e4umler, S., Balser, M., Nafz, F., Reif, W., Schellhorn, G.: Interactive verification of concurrent systems using symbolic execution. AI Commun. 23(2\u20133), 285\u2013307 (2010)","journal-title":"AI Commun."},{"issue":"1","key":"10_CR3","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/s00165-009-0130-y","volume":"23","author":"S B\u00e4umler","year":"2011","unstructured":"B\u00e4umler, S., Schellhorn, G., Tofan, B., Reif, W.: Proving linearizability with temporal logic. Formal Aspects of Computing 23(1), 91\u2013112 (2011)","journal-title":"Formal Aspects of Computing"},{"key":"10_CR4","unstructured":"Ben-Ari, M.: Principles of Concurrent and Distributed Programming. Addison-Wesley, second edn. (2006)"},{"key":"10_CR5","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-319-07139-8","volume-title":"SVA: The Power of Assertions in SystemVerilog","author":"E Cerny","year":"2015","unstructured":"Cerny, E., Dudani, S., Havlicek, J., Korchemny, D.: SVA: The Power of Assertions in SystemVerilog, 2nd edn. Springer, Heidelberg (2015)","edition":"2"},{"key":"10_CR6","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511621192","volume-title":"Modal Logic: An Introduction","author":"BF Chellas","year":"1980","unstructured":"Chellas, B.F.: Modal Logic: An Introduction. Cambridge University Press, Cambridge (1980)"},{"key":"10_CR7","volume-title":"Model Checking","author":"EM Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"10_CR8","unstructured":"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"},{"key":"10_CR9","unstructured":"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"},{"key":"10_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1007\/3-540-58216-9_48","volume-title":"Logic Programming and Automated Reasoning","author":"Z Duan","year":"1994","unstructured":"Duan, Z., Koutny, M., Holt, C.: Projection in temporal logic programming. In: Pfenning, F. (ed.) LPAR 1994. LNCS, vol. 822, pp. 333\u2013344. Springer, Heidelberg (1994)"},{"issue":"1","key":"10_CR11","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1016\/j.scico.2007.09.001","volume":"70","author":"Z Duan","year":"2008","unstructured":"Duan, Z., Yang, X., Koutny, M.: Framed temporal logic programming. Science of Computer Programming 70(1), 31\u201361 (2008)","journal-title":"Science of Computer Programming"},{"key":"10_CR12","volume-title":"A Practical Introduction to PSL","author":"C Eisner","year":"2006","unstructured":"Eisner, C., Fisman, D.: A Practical Introduction to PSL. Springer, Heidelberg (2006)"},{"key":"10_CR13","unstructured":"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"},{"key":"10_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"857","DOI":"10.1007\/3-540-45061-0_67","volume-title":"Automata, languages and programming","author":"C Eisner","year":"2003","unstructured":"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\u2013870. Springer, Heidelberg (2003)"},{"issue":"2","key":"10_CR15","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1093\/logcom\/14.2.215","volume":"14","author":"DP Guelev","year":"2004","unstructured":"Guelev, D.P.: A complete proof system for first-order interval temporal logic with projection. J. Log. Comput. 14(2), 215\u2013249 (2004)","journal-title":"J. Log. Comput."},{"issue":"1\u20132","key":"10_CR16","doi-asserted-by":"publisher","first-page":"181","DOI":"10.3166\/jancl.14.181-208","volume":"14","author":"DP Guelev","year":"2004","unstructured":"Guelev, D.P.: Logical interpolation and projection onto state in the Duration Calculus. J. Applied Non-Classical Logics 14(1\u20132), 181\u2013208 (2004)","journal-title":"J. Applied Non-Classical Logics"},{"issue":"6","key":"10_CR17","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/S1571-0661(04)80472-9","volume":"65","author":"DP Guelev","year":"2002","unstructured":"Guelev, D.P., Dang, V.H.: Prefix and projection onto state in duration calculus. Electr. Notes Theor. Comput. Sci. 65(6), 101\u2013119 (2002)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"issue":"1\u20132","key":"10_CR18","doi-asserted-by":"publisher","first-page":"149","DOI":"10.3166\/jancl.14.149-180","volume":"14","author":"DP Guelev","year":"2004","unstructured":"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\u20132), 149\u2013180 (2004)","journal-title":"J. Applied Non-Classical Logics"},{"key":"10_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"278","DOI":"10.1007\/BFb0036915","volume-title":"ICALP 1983","author":"J Halpern","year":"1983","unstructured":"Halpern, J., Manna, Z., Moszkowski, B.: A hardware semantics based on temporal intervals. In: Diaz, J. (ed.) ICALP 1983. LNCS, vol. 154, pp. 278\u2013291. Springer, Heidelberg (1983)"},{"key":"10_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1420","DOI":"10.1007\/3-540-48118-4_25","volume-title":"FM\u201999 - Formal Methods","author":"J He","year":"1999","unstructured":"He, J.: A behavioral model for co-design. In: Wing, J.M., Woodcock, J., Davies, J. (eds.) FM 1999. LNCS, vol. 1709, pp. 1420\u20131438. Springer, Heidelberg (1999)"},{"key":"10_CR21","doi-asserted-by":"crossref","unstructured":"Hollander, Y., Morley, M., Noy, A.: The e language: a fresh separation of concerns. In: Proc. TOOLS Europe 2001: 38th Int\u2019l Conf. on Technology of Object-Oriented Languages and Systems, Components for Mobile Computing, pp. 41\u201350. IEEE Computer Society Press (2001)","DOI":"10.1109\/TOOLS.2001.911754"},{"key":"10_CR22","unstructured":"Holzmann, G.: The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley Professional (2003)"},{"key":"10_CR23","doi-asserted-by":"publisher","DOI":"10.4324\/9780203290644","volume-title":"A New Introduction to Modal Logic","author":"GE Hughes","year":"1996","unstructured":"Hughes, G.E., Cresswell, M.J.: A New Introduction to Modal Logic. Routledge, London (1996)"},{"key":"10_CR24","unstructured":"IEEE: Standard for Property Specification Language (PSL), Standard 1850\u20132010. ANSI\/IEEE, New York (2010)"},{"key":"10_CR25","unstructured":"IEEE: Standard for the Functional Verification Language e, Standard 1647\u20132011. ANSI\/IEEE, New York (2011)"},{"key":"10_CR26","unstructured":"IEEE: Standard for SystemVerilog-Unified Hardware Design, Specification, and Verification Language, Standard 1800\u20132012. ANSI\/IEEE, New York (2012)"},{"key":"10_CR27","unstructured":"ITL web pages. http:\/\/www.antonio-cau.co.uk\/ITL\/"},{"issue":"4","key":"10_CR28","doi-asserted-by":"publisher","first-page":"596","DOI":"10.1145\/69575.69577","volume":"5","author":"CB Jones","year":"1983","unstructured":"Jones, C.B.: Tentative steps toward a development method for interfering programs. ACM Trans. Program. Lang. Syst. 5(4), 596\u2013619 (1983)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"3","key":"10_CR29","doi-asserted-by":"publisher","first-page":"475","DOI":"10.1007\/s00165-014-0310-2","volume":"27","author":"CB Jones","year":"2015","unstructured":"Jones, C.B., Hayes, I.J., Colvin, R.J.: Balancing expressiveness in formal approaches to concurrency. Formal Asp. Comput. 27(3), 475\u2013497 (2015)","journal-title":"Formal Asp. Comput."},{"issue":"7","key":"10_CR30","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1145\/360248.360251","volume":"19","author":"RM Keller","year":"1976","unstructured":"Keller, R.M.: Formal verification of parallel programs. Commun. ACM 19(7), 371\u2013384 (1976)","journal-title":"Commun. ACM"},{"key":"10_CR31","unstructured":"Kr\u00f6ger, F., Merz, S.: Temporal Logic and State Systems. Texts in Theoretical Computer Science (An EATCS Series). Springer, Heidelberg (2008)"},{"key":"10_CR32","unstructured":"Lamport, L.: Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley Professional (2002)"},{"key":"10_CR33","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0931-7","volume-title":"The Temporal Logic of Reactive and Concurrent Systems: Specifications","author":"Z Manna","year":"1992","unstructured":"Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specifications. Springer, New York (1992)"},{"key":"10_CR34","unstructured":"Morley, M.J.: Semantics of temporal e. In: Melham, T.F., Moller, F.G. (eds.) Banff\u201999 Higher Order Workshop: Formal Methods in Computation, Ullapool, Scotland, 9\u201311 Sept. 1999. pp. 138\u2013142. Univ. Glasgow, Dept. Comp. Sci., tech. rep. (1999)"},{"key":"10_CR35","unstructured":"Moszkowski, B.: Reasoning about Digital Circuits. Ph.D. thesis, Department of Computer Science, Stanford University, tech. rep. STAN-CS-83-970 (June 1983)"},{"key":"10_CR36","volume-title":"Executing Temporal Logic Programs","author":"B Moszkowski","year":"1986","unstructured":"Moszkowski, B.: Executing Temporal Logic Programs. Cambridge University Press, Cambridge (1986)"},{"key":"10_CR37","doi-asserted-by":"crossref","unstructured":"Moszkowski, B.: Compositional reasoning about projected and infinite time. In: Proc. 1st IEEE Int\u2019l Conf. on Engineering of Complex Computer Systems (ICECCS\u201995), pp. 238\u2013245. IEEE Computer Society Press (1995)","DOI":"10.1109\/ICECCS.1995.479336"},{"issue":"1\u20132","key":"10_CR38","doi-asserted-by":"publisher","first-page":"55","DOI":"10.3166\/jancl.14.55-104","volume":"14","author":"B Moszkowski","year":"2004","unstructured":"Moszkowski, B.: A hierarchical completeness proof for Propositional Interval Temporal Logic with finite time. J. Applied Non-Classical Logics 14(1\u20132), 55\u2013104 (2004)","journal-title":"J. Applied Non-Classical Logics"},{"issue":"3:10","key":"10_CR39","first-page":"1","volume":"8","author":"B Moszkowski","year":"2012","unstructured":"Moszkowski, B.: A complete axiom system for propositional Interval Temporal Logic with infinite time. Log. Meth. Comp. Sci. 8(3:10), 1\u201356 (2012)","journal-title":"Log. Meth. Comp. Sci."},{"issue":"4","key":"10_CR40","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1145\/2699417","volume":"58","author":"C Newcombe","year":"2015","unstructured":"Newcombe, C., Rath, T., Zhang, F., Munteanu, B., Brooker, M., Deardeuff, M.: How Amazon Web Services uses formal methods. Commun. ACM 58(4), 66\u201373 (2015)","journal-title":"Commun. ACM"},{"key":"10_CR41","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511619953","volume-title":"Real-Time Systems: Formal Specification and Automatic Verification","author":"ER Olderog","year":"2008","unstructured":"Olderog, E.R., Dierks, H.: Real-Time Systems: Formal Specification and Automatic Verification. Cambridge University Press, Cambridge (2008)"},{"issue":"3","key":"10_CR42","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1016\/0020-0190(81)90106-X","volume":"12","author":"GL Peterson","year":"1981","unstructured":"Peterson, G.L.: Myths about the mutual exclusion problem. Inf. Process. Lett. 12(3), 115\u2013116 (1981)","journal-title":"Inf. Process. Lett."},{"key":"10_CR43","unstructured":"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)"},{"key":"10_CR44","volume-title":"Duration Calculus: A Formal Approach to Real-Time Systems","author":"C Zhou","year":"2004","unstructured":"Zhou, C., Hansen, M.R.: Duration Calculus: A Formal Approach to Real-Time Systems. Springer, Heidelberg (2004)"},{"issue":"5","key":"10_CR45","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1016\/0020-0190(91)90122-X","volume":"40","author":"C Zhou","year":"1991","unstructured":"Zhou, C., Hoare, C.A.R., Ravn, A.P.: A calculus of durations. Inf. Process. Lett. 40(5), 269\u2013276 (1991)","journal-title":"Inf. Process. Lett."}],"container-title":["Lecture Notes in Computer Science","Dependable Software Engineering: Theories, Tools, and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-25942-0_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,31]],"date-time":"2025-05-31T01:50:07Z","timestamp":1748656207000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-25942-0_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319259413","9783319259420"],"references-count":45,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-25942-0_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}