{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T03:38:27Z","timestamp":1740109107420,"version":"3.37.3"},"reference-count":82,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2017,7,1]],"date-time":"2017-07-01T00:00:00Z","timestamp":1498867200000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2017,7]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>\n            We revisit the earliest temporal projection operator\n            <jats:inline-formula>\n              <jats:alternatives>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi mathvariant=\"normal\">\u03a0<\/mml:mi>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula>\n            in discrete-time Propositional Interval Temporal Logic (PITL) and use it to formalise interleaving concurrency. The logical properties of\n            <jats:inline-formula>\n              <jats:alternatives>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi mathvariant=\"normal\">\u03a0<\/mml:mi>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula>\n            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\n            <jats:inline-formula>\n              <jats:alternatives>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi mathvariant=\"normal\">\u03a0<\/mml:mi>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula>\n            and the standard LTL operator\n            <jats:inline-formula>\n              <jats:alternatives>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi mathvariant=\"script\">U<\/mml:mi>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula>\n            (\u2018until\u2019) are briefly illustrated. We also formalise concurrent imperative programming constructs with and without\n            <jats:inline-formula>\n              <jats:alternatives>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi mathvariant=\"normal\">\u03a0<\/mml:mi>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula>\n            , and relate the two approaches. Peterson\u2019s mutual exclusion algorithm is used to illustrate reasoning with\n            <jats:inline-formula>\n              <jats:alternatives>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi mathvariant=\"normal\">\u03a0<\/mml:mi>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula>\n            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\n            <jats:inline-formula>\n              <jats:alternatives>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi mathvariant=\"normal\">\u03a0<\/mml:mi>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula>\n            help to reveal and analyse important differing viewpoints involving global time and the local projected time seen by each individual process. Links between\n            <jats:inline-formula>\n              <jats:alternatives>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi mathvariant=\"normal\">\u03a0<\/mml:mi>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula>\n            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.\n          <\/jats:p>","DOI":"10.1007\/s00165-017-0417-3","type":"journal-article","created":{"date-parts":[[2017,3,20]],"date-time":"2017-03-20T07:27:13Z","timestamp":1489994833000},"page":"705-750","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["An application of temporal projection to interleaving concurrency"],"prefix":"10.1145","volume":"29","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8965-9308","authenticated-orcid":false,"given":"Ben","family":"Moszkowski","sequence":"first","affiliation":[{"name":"School of Computing Science, Newcastle University, NE1 7RU, Newcastle upon Tyne, UK"}]},{"given":"Dimitar P.","family":"Guelev","sequence":"additional","affiliation":[{"name":"Department of Algebra and Logic, Institute of Mathematics and Informatics, Sofia, Bulgaria"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","volume-title":"Principles of concurrent and distributed programming,","author":"Ben-Ari M","year":"2006","edition":"2"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"publisher","DOI":"10.5555\/1735921.1735925"},{"key":"e_1_2_1_2_3_2","unstructured":"Baier C Katoen J-P (2008) Principles of model checking. MIT Press Cambridge MA"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-009-0130-y"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Cerny E Dudani S Havlicek J Korchemny D (2015) SVA: the power of assertions in systemVerilog 2nd edn. Springer Cham","DOI":"10.1007\/978-3-319-07139-8"},{"key":"e_1_2_1_2_6_2","unstructured":"Clarke EM Grumberg O Peled DA (1999) Model checking. MIT Press Cambridge MA"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Chellas BF (1980) Modal logic: an introduction. Cambridge University Press Cambridge UK","DOI":"10.1017\/CBO9780511621192"},{"key":"e_1_2_1_2_8_2","unstructured":"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"},{"key":"e_1_2_1_2_9_2","unstructured":"Volker D Gastin P (2008) First-order definable languages. In: Flum J Gr\u00e4del E Wilke T (eds) Logic and automata: history and perspectives volume 2 of texts in logic and games. Amsterdam University Press Amsterdam pp 261\u2013306"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"Duan Z Koutny M Holt C (1994) Projection in temporal logic programming. In: Pfennig F (ed) LPAR \u201994 volume 822 of LNCS. Springer Berlin pp 333\u2013344","DOI":"10.1007\/3-540-58216-9_48"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"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\u2013254","DOI":"10.1007\/978-3-642-04761-9_19"},{"volume-title":"Concurrency verification: introduction to compositional and noncompositional methods","year":"2001","author":"de Roever W-P","key":"e_1_2_1_2_12_2"},{"key":"e_1_2_1_2_13_2","unstructured":"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"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2007.09.001"},{"volume-title":"A practical introduction to PSL","year":"2006","author":"Eisner C","key":"e_1_2_1_2_15_2"},{"key":"e_1_2_1_2_16_2","unstructured":"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"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"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\u2013870","DOI":"10.1007\/3-540-45061-0_67"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","unstructured":"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\u20131072","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)80472-9"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"publisher","DOI":"10.3166\/jancl.14.149-180"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2010.04.036"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"publisher","DOI":"10.1145\/358746.358767"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(88)90124-7"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"crossref","unstructured":"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","DOI":"10.1007\/3-540-60761-7"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/14.2.215"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"publisher","DOI":"10.3166\/jancl.14.181-208"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","unstructured":"Godefroid P Wolper P (1991) A partial approach to model checking. In: 6th Annual symposium on logic in computer science (LICS \u201991). IEEE Computer Society Los Alamitos pp 406\u2013415","DOI":"10.1109\/LICS.1991.151664"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"crossref","unstructured":"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 \u201991) volume 575 of LNCS. Springer Berlin pp 332\u2013342","DOI":"10.1007\/3-540-55179-4_32"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01383879"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"crossref","DOI":"10.4324\/9780203290644","volume-title":"A new introduction to modal logic","author":"Hughes GE","year":"1996"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"crossref","unstructured":"He J (1999) A behavioral model for co-design. In: Wing JM Woodcock J Davies J (eds) FM\u201999 vol II volume 1709 of LNCS. Springer Berlin pp 1420\u20131438","DOI":"10.1007\/3-540-48118-4_25"},{"key":"#cr-split#-e_1_2_1_2_32_2.1","unstructured":"Halpern J Manna Z Moszkowski B (1983) A hardware semantics based on temporal intervals. In: Diaz J"},{"key":"#cr-split#-e_1_2_1_2_32_2.2","unstructured":"(ed) ICALP 1983 volume 154 of LNCS. Springer Berlin pp 278-291"},{"key":"e_1_2_1_2_33_2","unstructured":"Hollander Y Morley M Noy A (2001) The e language: a fresh separation of concerns. In: Proceedings of TOOLS Europe 2001: 38th internationa\u2019l conference on technology of object-oriented languages and systems components for mobile computing. IEEE Computer Society Los Alamitos pp 41\u201350"},{"volume-title":"The SPIN model checker: primer and reference manual","year":"2003","author":"Holzmann G","key":"e_1_2_1_2_34_2"},{"key":"e_1_2_1_2_35_2","unstructured":"IEEE (2010) Standard for property specification language (PSL) standard 1850\u20132010. ANSI\/IEEE New York"},{"key":"e_1_2_1_2_36_2","unstructured":"IEEE (2011) Standard for the functional verification language e standard 1647\u20132011. ANSI\/IEEE New York"},{"key":"e_1_2_1_2_37_2","unstructured":"IEEE (2012) Standard for systemVerilog\u2014unified hardware design specification and verification language standard 1800\u20132012. ANSI\/IEEE New York"},{"key":"e_1_2_1_2_38_2","unstructured":"ISO (1986) Standard generalized markup language (SGML): ISO 8879:1986. International Organization for Standardization Geneva Switzerland"},{"key":"e_1_2_1_2_39_2","unstructured":"ITL web pages.\nhttp:\/\/www.antonio-cau.co.uk\/ITL\/. Accessed 8 June 2015"},{"key":"e_1_2_1_2_40_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-014-0310-2"},{"key":"e_1_2_1_2_41_2","doi-asserted-by":"crossref","unstructured":"Jones CB (October 1983) Tentative steps toward a development method for interfering programs. ACM Trans Program Lang Syst 5(4):596\u2013619","DOI":"10.1145\/69575.69577"},{"key":"e_1_2_1_2_42_2","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360251"},{"key":"e_1_2_1_2_43_2","unstructured":"Kr\u00f6ger F Merz S (2008) Temporal logic and state systems. Texts in theoretical computer science (an EATCS series). Springer Berlin"},{"key":"e_1_2_1_2_44_2","doi-asserted-by":"crossref","unstructured":"Katz S Peled D (1987) Interleaving set temporal logic. In: 6th Annual ACM symposium on principles of distributed computing (PODC \u201987). ACM New York pp 178\u2013190","DOI":"10.1145\/41840.41855"},{"key":"e_1_2_1_2_45_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(90)90096-Z"},{"key":"e_1_2_1_2_46_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF02252682"},{"key":"e_1_2_1_2_47_2","unstructured":"Lamport L (1983) What good is temporal logic? In: Mason REA (ed.) Information Processing 83 pp. 657\u2013668. North-Holland"},{"key":"e_1_2_1_2_48_2","unstructured":"Lamport L (2002) Specifying Systems: The TLA+ language and tools for hardware and software engineers. Addison-Wesley Professional Boston MA USA"},{"key":"e_1_2_1_2_49_2","doi-asserted-by":"crossref","unstructured":"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\u2013218","DOI":"10.1007\/3-540-15648-8_16"},{"key":"e_1_2_1_2_50_2","doi-asserted-by":"crossref","unstructured":"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\u2014first international symposium (SETTA 2015) volume 9409 in LNCS. Springer Cham pp 153\u2013167","DOI":"10.1007\/978-3-319-25942-0_10"},{"key":"e_1_2_1_2_51_2","doi-asserted-by":"crossref","unstructured":"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\u2013382","DOI":"10.1007\/3-540-12896-4_374"},{"key":"e_1_2_1_2_52_2","unstructured":"Morley MJ (1999) Semantics of temporal e . In: Melham TF Moller FG (eds) Banff\u201999 higher order workshop: formal methods in computation Ullapool Scotland 9\u201311 Sept. 1999. Technical Report Department of Computing Science University of Glasgow Glasgow Scotland pp 138\u2013142"},{"key":"e_1_2_1_2_53_2","unstructured":"Moszkowski B (1983) Reasoning about digital circuits. PhD thesis Department of Computer Science Stanford University June 1983. Technical report STAN\u2013CS\u201383\u2013970"},{"key":"e_1_2_1_2_54_2","doi-asserted-by":"publisher","DOI":"10.5555\/6240"},{"key":"e_1_2_1_2_55_2","doi-asserted-by":"crossref","unstructured":"Moszkowski B (1995) Compositional reasoning about projected and infinite time. In: Proceedings of 1st IEEE internationa\u2019l conference on engineering of complex computer systems (ICECCS\u201995). IEEE Computer Society Los Alamitos pp 238\u2013245","DOI":"10.1109\/ICECCS.1995.479336"},{"key":"e_1_2_1_2_56_2","doi-asserted-by":"crossref","unstructured":"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\u2013234","DOI":"10.1007\/3-540-45022-X_19"},{"key":"e_1_2_1_2_57_2","doi-asserted-by":"crossref","unstructured":"Moszkowski B (2004) A hierarchical completeness proof for propositional interval temporal logic with finite time. J Appl Non Class Log 14(1\u20132):55\u2013104. Special issue on interval temporal logics and duration calculi. Goranko V Montanari A guest editors","DOI":"10.3166\/jancl.14.55-104"},{"issue":"3","key":"e_1_2_1_2_58_2","first-page":"10","article-title":"A complete axiom system for propositional interval temporal logic, with infinite time.","volume":"8","author":"Moszkowski B","year":"2012","journal-title":"Log Meth Comp Sci"},{"key":"e_1_2_1_2_59_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2013.02.005"},{"key":"e_1_2_1_2_60_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10472-013-9356-8"},{"key":"e_1_2_1_2_61_2","doi-asserted-by":"publisher","DOI":"10.5555\/128869"},{"key":"e_1_2_1_2_62_2","doi-asserted-by":"publisher","DOI":"10.1145\/2699417"},{"key":"e_1_2_1_2_63_2","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511619953","volume-title":"Real-time systems: formal specification and automatic verification","author":"Olderog E-R","year":"2008"},{"key":"#cr-split#-e_1_2_1_2_64_2.1","unstructured":"Olderog E-R Hoare CAR (1983) Specification-oriented semantics for communicating processes. In: D\u00edaz J"},{"key":"#cr-split#-e_1_2_1_2_64_2.2","unstructured":"(ed) Automata languages and programming 10th colloquium (ICALP 1983) volume 154 of LNCS. Springer Berlin pp 561-572"},{"key":"e_1_2_1_2_65_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00268075"},{"key":"e_1_2_1_2_66_2","unstructured":"OWL-S (2004) Semantic markup for web services. http:\/\/www.w3.org\/Submission\/OWL-S\/. Accessed 14 March 2016"},{"key":"e_1_2_1_2_67_2","doi-asserted-by":"crossref","unstructured":"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\u2013115","DOI":"10.1007\/978-3-319-25255-1_9"},{"key":"e_1_2_1_2_68_2","doi-asserted-by":"crossref","unstructured":"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\u2013220","DOI":"10.1007\/978-3-319-25150-9_13"},{"key":"e_1_2_1_2_69_2","doi-asserted-by":"crossref","unstructured":"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 \u201993) volume 697 of LNCS. Springer Berlin pp 409\u2013423","DOI":"10.1007\/3-540-56922-7_34"},{"key":"e_1_2_1_2_70_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00121262"},{"key":"e_1_2_1_2_71_2","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(81)90106-X"},{"key":"e_1_2_1_2_72_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0020-0190(97)00133-6"},{"key":"e_1_2_1_2_73_2","doi-asserted-by":"crossref","unstructured":"Schellhorn G Tofan B Ernst G Pf\u00e4hler J Reif W (2014) RGITL: a temporal logic framework for compositional reasoning about interleaved programs. Ann Math Artif Intell 71(1\u20133):131\u2013174","DOI":"10.1007\/s10472-013-9389-z"},{"key":"e_1_2_1_2_74_2","unstructured":"Taubenfeld G (2006) Synchronization algorithms and concurrent programming. Pearson\/Prentice Hall Harlow"},{"key":"#cr-split#-e_1_2_1_2_75_2.1","doi-asserted-by":"crossref","unstructured":"Valmari A (1991) Stubborn sets for reduced state space generation. In: Rozenberg G","DOI":"10.1007\/3-540-53863-1_36"},{"key":"#cr-split#-e_1_2_1_2_75_2.2","unstructured":"(ed) Advances in Petri nets 1990 volume 483 of LNCS. Springer Berlin pp 491-515"},{"key":"e_1_2_1_2_76_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00709154"},{"key":"e_1_2_1_2_77_2","unstructured":"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\u2014volume I ICCOMP\u201910. Stevens Point Wisconsin USA World Scientific and Engineering Academy and Society (WSEAS) pp 272\u2013280"},{"volume-title":"Duration calculus: a formal approach to real-time systems","year":"2004","author":"Zhou C","key":"e_1_2_1_2_78_2"},{"key":"e_1_2_1_2_79_2","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(91)90122-X"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-017-0417-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-017-0417-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-017-0417-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-017-0417-3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T16:14:21Z","timestamp":1641485661000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-017-0417-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,7]]},"references-count":82,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2017,7]]}},"alternative-id":["10.1007\/s00165-017-0417-3"],"URL":"https:\/\/doi.org\/10.1007\/s00165-017-0417-3","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"type":"print","value":"0934-5043"},{"type":"electronic","value":"1433-299X"}],"subject":[],"published":{"date-parts":[[2017,7]]}}}