{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T07:00:02Z","timestamp":1779087602435,"version":"3.51.4"},"reference-count":73,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2012,8,13]],"date-time":"2012-08-13T00:00:00Z","timestamp":1344816000000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>Interval Temporal Logic (ITL) is an established temporal formalism for reasoning about time periods. For over 25 years, it has been applied in a number of ways and several ITL variants, axiom systems and tools have been investigated. We solve the longstanding open problem of finding a complete axiom system for basic quantifier-free propositional ITL (PITL) with infinite time for analysing nonterminating computational systems. Our completeness proof uses a reduction to completeness for PITL with finite time and conventional propositional linear-time temporal logic. Unlike completeness proofs of equally expressive logics with nonelementary computational complexity, our semantic approach does not use tableaux, subformula closures or explicit deductions involving encodings of omega automata and nontrivial techniques for complementing them. We believe that our result also provides evidence of the naturalness of interval-based reasoning.<\/jats:p>","DOI":"10.2168\/lmcs-8(3:10)2012","type":"journal-article","created":{"date-parts":[[2013,11,29]],"date-time":"2013-11-29T08:17:46Z","timestamp":1385713066000},"source":"Crossref","is-referenced-by-count":7,"title":["A Complete Axiom System for Propositional Interval Temporal Logic with Infinite Time"],"prefix":"10.46298","volume":"Volume 8, Issue 3","author":[{"given":"Ben","family":"Moszkowski","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"25203","published-online":{"date-parts":[[2012,8,13]]},"reference":[{"key":"10.2168\/LMCS-8(3:10)2012_BanieqbalBarringer86","unstructured":"Behnam Banieqbal and Howard Barringer. A study of an extended temporal logic and a temporal fixed point calculus. Technical Report UMCS-86-10-2, Dept. of Computer Science, University of Manchester, England, October 1986. revised June 1987."},{"key":"10.2168\/LMCS-8(3:10)2012_BanieqbalBarringer89a","doi-asserted-by":"crossref","unstructured":"Behnam Banieqbal and Howard Barringer. Temporal logic with fixed points. In Behnam Banieqbal, Howard Barringer, and Amir Pnueli, editors,Temporal Logic in Specification, Proceedings (Altrincham, UK, April, 1987), volume 398 ofLNCS, pages 62-74, Berlin, 1989. Springer-Verlag.","DOI":"10.1007\/3-540-51803-7_22"},{"key":"10.2168\/LMCS-8(3:10)2012_BalserBaeumler04","doi-asserted-by":"crossref","unstructured":"Michael Balser, Simon B\u00e4umler, Alexander Knapp, Wolfgang Reif, and Andreas Thums. Interactive verification of UML state machines. In Jim Davies, Wolfram Schulte, and Michael Barnett, editors,Proc. 6th International Conference on Formal Engineering Methods (ICFEM 2004), volume 3308 ofLNCS, pages 434-448. Springer-Verlag, 2004.","DOI":"10.1007\/978-3-540-30482-1_36"},{"issue":"2-3","key":"10.2168\/LMCS-8(3:10)2012_BaeumlerBalser10","doi-asserted-by":"crossref","first-page":"285","DOI":"10.3233\/AIC-2010-0458","volume":"23","author":"Simon B\u00e4umler, Michael Balser, Florian N","year":"2010","journal-title":"AI Communications"},{"key":"10.2168\/LMCS-8(3:10)2012_BarringerKuiper86","doi-asserted-by":"crossref","unstructured":"Howard Barringer, Ruurd Kuiper, and Amir Pnueli. A really abstract concurrent model and its temporal logic. InProc. 13th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL'86), pages 173-183. ACM, 1986.","DOI":"10.1145\/512644.512660"},{"key":"10.2168\/LMCS-8(3:10)2012_BradfieldStirling06","doi-asserted-by":"crossref","unstructured":"Julian Bradfield and Colin Stirling. Modal mu-calculi. InThe Handbook of Modal Logic, pages 721-756. Elsevier, 2006.","DOI":"10.1016\/S1570-2464(07)80015-2"},{"key":"10.2168\/LMCS-8(3:10)2012_BaeumlerSchellhorn09","doi-asserted-by":"crossref","first-page":"91","DOI":"10.1007\/s00165-009-0130-y","volume":"23","author":"Simon B\u00e4umler, Gerhard Schellhorn, Bogda","year":"2011","journal-title":"Formal Aspects of Computing"},{"issue":"2","key":"10.2168\/LMCS-8(3:10)2012_BowmanThompson03","doi-asserted-by":"crossref","first-page":"195","DOI":"10.1093\/logcom\/13.2.195","volume":"13","author":"Howard Bowman and Simon J. Thompson","year":"2003","journal-title":"Journal of Logic and Computation"},{"key":"10.2168\/LMCS-8(3:10)2012_Buechi62-lmcs-paper","unstructured":"J. R. B\u00fcchi. On a decision method in restricted second-order arithmetic. InProc. Int. Congress on Logic, Methodology, and Philosophy of Science 1960, pages 1-12. Stanford University Press, 1962."},{"key":"10.2168\/LMCS-8(3:10)2012_Chellas80","doi-asserted-by":"crossref","unstructured":"Brian F. Chellas.Modal Logic: An Introduction. Cambridge University Press, Cambridge, England, 1980.","DOI":"10.1017\/CBO9780511621192"},{"issue":"2","key":"10.2168\/LMCS-8(3:10)2012_Choueka74","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1016\/S0022-0000(74)80051-6","volume":"8","author":"Yaacov Choueka","year":"1974","journal-title":"Journal of Computer and System Sciences"},{"key":"10.2168\/LMCS-8(3:10)2012_ChouekaPeleg83","first-page":"21","volume":"21","author":"Yaacov Choueka and David Peleg","year":"1983","journal-title":"Bulletin of the European Association for Theoretical Computer Science"},{"key":"10.2168\/LMCS-8(3:10)2012_CauZedan97","doi-asserted-by":"crossref","unstructured":"A. Cau and H. Zedan. Refining Interval Temporal Logic specifications. In M. Bertran and T. Rus, editors,Transformation-Based Reactive Systems Development, volume 1231 ofLNCS, pages 79-94. AMAST, Springer-Verlag, 1997.","DOI":"10.1007\/3-540-63010-4_6"},{"key":"10.2168\/LMCS-8(3:10)2012_Dutertre95","doi-asserted-by":"crossref","unstructured":"Bruno Dutertre. Complete proof systems for first order Interval Temporal Logic. InProc. 10th Ann. IEEE Symp. on Logic in Computer Science (LICS '95), pages 36-43, Los Alamitos, Calif., USA, June 1995. IEEE Computer Society Press.","DOI":"10.1109\/LICS.1995.523242"},{"key":"10.2168\/LMCS-8(3:10)2012_DuanZhang08","doi-asserted-by":"crossref","unstructured":"Zhenhua Duan and Nan Zhang. A complete axiomatization of propositional projection temporal logic. In2nd IEEE\/IFIP Int'l Symp. on Theoretical Aspects of Software Eng. (TASE 2008), pages 271-278. IEEE Computer Society Press, 2008.","DOI":"10.1109\/TASE.2008.22"},{"key":"10.2168\/LMCS-8(3:10)2012_DuanZhang12","doi-asserted-by":"crossref","unstructured":"Zhenhua Duan, Nan Zhang, and Maciej Koutny. A complete axiomatization of propositional projection temporal logic.Theor. Comp. Sci., 2012..","DOI":"10.1016\/j.tcs.2012.01.026"},{"key":"10.2168\/LMCS-8(3:10)2012_Emerson90","doi-asserted-by":"crossref","unstructured":"E. Allen Emerson. Temporal and modal logic. In Jan van Leeuwen, editor,Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics, chapter 16, pages 995-1072. Elsevier\/MIT Press, Amsterdam, 1990.","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"key":"10.2168\/LMCS-8(3:10)2012_Fisher11","doi-asserted-by":"crossref","unstructured":"Michael Fisher.An Introduction to Practical Formal Methods Using Temporal Logic. John Wiley & Sons, 2011.","DOI":"10.1002\/9781119991472"},{"issue":"2","key":"10.2168\/LMCS-8(3:10)2012_FischerLadner79","first-page":"194","volume":"18","author":"Michael J. Fischer and Richard E. Ladner","year":"1979","journal-title":"Journal of Computer and System Sciences 1979"},{"key":"10.2168\/LMCS-8(3:10)2012_FrenchReynolds03","unstructured":"Tim French and Mark Reynolds. A sound and complete proof system for QPTL. In P. Balbiani, N-Y. Suzuki, F. Wolter, and M. Zakharyaschev, editors,Advances in Modal Logic, volume 4, pages 127-148. King's College Publications, London, 2003."},{"key":"10.2168\/LMCS-8(3:10)2012_GabbayPnueli80","doi-asserted-by":"crossref","unstructured":"D. Gabbay, A. Pnueli, S. Shelah, and J. Stavi. On the temporal analysis of fairness. InProc. 7th Ann. ACM Symp. on Principles of Programming Languages (POPL '80), pages 163-173. ACM, 1980.","DOI":"10.1145\/567446.567462"},{"key":"10.2168\/LMCS-8(3:10)2012_Guelev2007","doi-asserted-by":"crossref","unstructured":"Dimitar P. Guelev. Probabilistic interval temporal logic and duration calculus with infinite intervals: Complete proof systems.Logical Methods in Computer Science, 3(3), 2007.","DOI":"10.2168\/LMCS-3(3:3)2007"},{"key":"10.2168\/LMCS-8(3:10)2012_HughesCresswell96","doi-asserted-by":"crossref","unstructured":"George E. Hughes and Max J. Cresswell.A New Introduction to Modal Logic. Routledge, London, 1996.","DOI":"10.4324\/9780203290644"},{"key":"10.2168\/LMCS-8(3:10)2012_HarelKozen2000","doi-asserted-by":"crossref","unstructured":"David Harel, Dexter Kozen, and Jerzy Tiuryn.Dynamic Logic. MIT Press, Cambridge, Massachusetts, 2000.","DOI":"10.7551\/mitpress\/2516.001.0001"},{"key":"10.2168\/LMCS-8(3:10)2012_HalpernManna83","doi-asserted-by":"crossref","unstructured":"J. Halpern, Z. Manna, and B. Moszkowski. A hardware semantics based on temporal intervals. In J. Diaz, editor,Proc. 10th Int'l. Colloquium on Automata, Languages and Programming (ICALP '83), volume 154 ofLNCS, pages 278-291, Berlin, 1983. Springer-Verlag.","DOI":"10.1007\/BFb0036915"},{"issue":"1-3","key":"10.2168\/LMCS-8(3:10)2012_HenriksenThiagarajan99","doi-asserted-by":"crossref","first-page":"187","DOI":"10.1016\/S0168-0072(98)00039-6","volume":"96","author":"Jesper G. Henriksen and P. S. Thiagaraja","year":"1999","journal-title":"Annals of Pure and Applied Logic"},{"key":"10.2168\/LMCS-8(3:10)2012_IEEE1647-lmcs-paper","unstructured":"IEEE.Standard for the Functional Verification Languagee, Standard 1647-2008. ANSI\/IEEE, New York, 2008. Produced by theeFunctional Verification Language Working Group."},{"key":"10.2168\/LMCS-8(3:10)2012_ITLwebsite","doi-asserted-by":"crossref","unstructured":"Interval Temporal Logic webpages. http:\/\/www.tech.dmu.ac.uk\/STRL\/ITL\/, 2012. Roope Kaivola. Axiomatising linear time mu-calculus. In Insup Lee and Scott A. Smolka, editors,CONCUR '95, volume 962 ofLNCS, pages 423-437. Springer-Verlag, 1995.","DOI":"10.1007\/3-540-60218-6_32"},{"key":"10.2168\/LMCS-8(3:10)2012_Kamp68","unstructured":"Johan Anthony Willem Kamp.Tense Logic and the Theory of Linear Order. PhD thesis, University of California, Los Angeles, 1968."},{"key":"10.2168\/LMCS-8(3:10)2012_KroegerMerz08","unstructured":"Fred Kr\u00f6ger and Stephan Merz.Temporal Logic and State Systems. Texts in Theoretical Computer Science (An EATCS Series). Springer-Verlag, 2008."},{"key":"10.2168\/LMCS-8(3:10)2012_Kono95","doi-asserted-by":"crossref","unstructured":"Shinji Kono. A combination of clausal and non-clausal temporal logic programs. In Michael Fisher and Richard Owens, editors,Executable Modal and Temporal Logics, volume 897 ofLNCS, pages 40-57, Berlin, February 1995. Springer-Verlag.","DOI":"10.1007\/3-540-58976-7_3"},{"issue":"3","key":"10.2168\/LMCS-8(3:10)2012_Kozen83","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"Dexter Kozen","year":"1983","journal-title":"Theor. Comp. Sci."},{"key":"10.2168\/LMCS-8(3:10)2012_KozenParikh81","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1016\/0304-3975(81)90019-0","volume":"14","author":"Dexter Kozen and Rohit Parikh","year":"1981","journal-title":"Theor. Comp. Sci."},{"key":"10.2168\/LMCS-8(3:10)2012_KestenPnueli95","doi-asserted-by":"crossref","unstructured":"Y. Kesten and A. Pnueli. A complete proof system for QPTL. InProc. 10th IEEE Symp. on Logic in Computer Science (LICS'95), pages 2-12. IEEE Computer Society Press, 1995.","DOI":"10.1109\/LICS.1995.523239"},{"issue":"5","key":"10.2168\/LMCS-8(3:10)2012_KestenPnueli2002","first-page":"701","volume":"12","author":"Y. Kesten and A. Pnueli","year":"2002","journal-title":"Journal of Logic and Computation 2002"},{"key":"10.2168\/LMCS-8(3:10)2012_Lamport02","unstructured":"Leslie Lamport.Specifying Systems: The TLA+Language and Tools for Hardware and Software Engineers. Addison-Wesley Professional, 2002."},{"issue":"1","key":"10.2168\/LMCS-8(3:10)2012_LichtensteinPnueli00","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1093\/jigpal\/8.1.55","volume":"8","author":"Orna Lichtenstein and Amir Pnueli","year":"2000","journal-title":"Logic Journal of the IGPL"},{"key":"10.2168\/LMCS-8(3:10)2012_LichtensteinPnueli85","doi-asserted-by":"crossref","unstructured":"O. Lichtenstein, A. Pnueli, and L. Zuck. The glory of the past. In R. Parikh et al., editors,Logics of Programs, volume 193 ofLNCS, pages 196-218, Berlin, 1985. Springer-Verlag.","DOI":"10.1007\/3-540-15648-8_16"},{"issue":"5","key":"10.2168\/LMCS-8(3:10)2012_McNaughton66","doi-asserted-by":"crossref","first-page":"521","DOI":"10.1016\/S0019-9958(66)80013-X","volume":"9","author":"Robert McNaughton","year":"1966","journal-title":"Inf. and Control"},{"key":"10.2168\/LMCS-8(3:10)2012_Morley99","unstructured":"Matthew J. Morley. Semantics of temporal e. In T. F. Melham and F. G. Moller, editors,Banff'99Higher Order Workshop: Formal Methods in Computation,Ullapool, Scotland, 9-11 Sept. 1999, pages 138-142. University of Glasgow, Department of Computing Science Technical Report, 1999."},{"key":"10.2168\/LMCS-8(3:10)2012_Moszkowski83a","unstructured":"B. Moszkowski.Reasoning about Digital Circuits. PhD thesis, Department of Computer Science, Stanford University, June 1983. Technical report STAN-CS-83-970."},{"key":"10.2168\/LMCS-8(3:10)2012_Moszkowski83","doi-asserted-by":"crossref","unstructured":"B. Moszkowski. A temporal logic for multi-level reasoning about hardware. InProc. 6th Int'l. Symp. on Computer Hardware Description Languages, pages 79-90, Pittsburgh, Pennsylvania, 1983. North-Holland Pub. Co.","DOI":"10.21236\/ADA324174"},{"key":"10.2168\/LMCS-8(3:10)2012_Moszkowski85","doi-asserted-by":"crossref","first-page":"10","DOI":"10.1109\/MC.1985.1662795","volume":"18","author":"B. Moszkowski","year":"1985","journal-title":"Computer"},{"key":"10.2168\/LMCS-8(3:10)2012_Moszkowski86","doi-asserted-by":"crossref","unstructured":"B. Moszkowski.Executing Temporal Logic Programs. Cambridge University Press, Cambridge, England, 1986.","DOI":"10.1007\/3-540-15670-4_6"},{"key":"10.2168\/LMCS-8(3:10)2012_Moszkowski94","unstructured":"Ben Moszkowski. Some very compositional temporal properties. In E.-R. Olderog, editor,Programming Concepts, Methods and Calculi (PROCOMET'94), volume A-56 ofIFIP Transactions, pages 307-326. IFIP, Elsevier Science B.V. (North-Holland), 1994."},{"key":"10.2168\/LMCS-8(3:10)2012_Moszkowski95a","doi-asserted-by":"crossref","unstructured":"Ben Moszkowski. Compositional reasoning about projected and infinite time. InProc. 1st IEEE Int'l Conf. on Engineering of Complex Computer Systems (ICECCS'95), pages 238-245. IEEE Computer Society Press, 1995.","DOI":"10.1109\/ICECCS.1995.479336"},{"key":"10.2168\/LMCS-8(3:10)2012_Moszkowski96","doi-asserted-by":"crossref","unstructured":"Ben Moszkowski. Using temporal fixpoints to compositionally reason about liveness. In He Jifeng, John Cooke, and Peter Wallis, editors,BCS-FACS 7th Refinement Workshop, electronic Workshops in Computing, London, 1996. BCS-FACS, Springer-Verlag and British Computer Society.","DOI":"10.14236\/ewic\/RW1996.11"},{"key":"10.2168\/LMCS-8(3:10)2012_Moszkowski98","doi-asserted-by":"crossref","unstructured":"Ben Moszkowski. Compositional reasoning using Interval Temporal Logic and Tempura. In Willem-Paul de Roever, Hans Langmaack, and Amir Pnueli, editors,Compositionality: The Significant Difference, volume 1536 ofLNCS, pages 439-464, Berlin, 1998. Springer-Verlag.","DOI":"10.1007\/3-540-49213-5_17"},{"key":"10.2168\/LMCS-8(3:10)2012_Moszkowski00","unstructured":"Ben Moszkowski. A complete axiomatization of Interval Temporal Logic with infinite time (extended abstract). InProc. 15th Ann. IEEE Symp. on Logic in Computer Science (LICS 2000), pages 242-251. IEEE Computer Society Press, June 2000."},{"issue":"1-2","key":"10.2168\/LMCS-8(3:10)2012_Moszkowski04a","doi-asserted-by":"crossref","first-page":"55","DOI":"10.3166\/jancl.14.55-104","volume":"14","author":"Ben Moszkowski","year":"2004","journal-title":"Journal of Applied Non-Classical Logics"},{"issue":"2","key":"10.2168\/LMCS-8(3:10)2012_Moszkowski07-lmcs-paper","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1093\/logcom\/exm006","volume":"17","author":"Ben Moszkowski","year":"2007","journal-title":"Journal of Logic and Comp."},{"key":"10.2168\/LMCS-8(3:10)2012_Moszkowski11-TIME","doi-asserted-by":"crossref","unstructured":"Ben Moszkowski. Compositional reasoning using intervals and time reversal. In18th Int'l Symp. on Temporal Representation and Reasoning (TIME 2011), pages 107-114. IEEE Computer Society, 2011.","DOI":"10.1109\/TIME.2011.25"},{"key":"10.2168\/LMCS-8(3:10)2012_MoWang2011","doi-asserted-by":"crossref","unstructured":"Dapeng Mo, Xiaobing Wang, and Zhenhua Duan. Asynchronous communication in MSVL. In Shengchao Qin and Zongyan Qiu, editors,13th Int'l Conf. on Formal Engineering Methods (ICFEM 2011), volume 6991 ofLNCS, pages 82-97. Springer-Verlag, 2011.","DOI":"10.1007\/978-3-642-24559-6_8"},{"key":"10.2168\/LMCS-8(3:10)2012_OlderogDierks2008","doi-asserted-by":"crossref","unstructured":"Ernst-R\u00fcdiger Olderog and Henning Dierks.Real-Time Systems: Formal Specification and Automatic Verification. Cambridge University Press, Cambridge, England, 2008.","DOI":"10.1017\/CBO9780511619953"},{"key":"10.2168\/LMCS-8(3:10)2012_Paech88-techrep","unstructured":"Barbara Paech. Gentzen-systems for propositional temporal logics. Technical Report 88\/01, Institut f\u00fcr Informatik, Ludwig-Maximilians-Universit\u00e4t, Munich, Germany, February 1988."},{"key":"10.2168\/LMCS-8(3:10)2012_Paech89","doi-asserted-by":"crossref","unstructured":"Barbara Paech. Gentzen-systems for propositional temporal logics. In E. B\u00f6rger, H. Kleine B\u00fcning, and M. M. Richter, editors,Proceedings of the 2nd Workshop on Computer Science Logic (CSL'88), volume 385 ofLNCS, pages 240-253. Springer-Verlag, 1989.","DOI":"10.1007\/BFb0026305"},{"key":"10.2168\/LMCS-8(3:10)2012_Pnueli77","doi-asserted-by":"crossref","unstructured":"Amir Pnueli. The temporal logic of programs. InProc. 18th Ann. IEEE Symp. on the Foundation of Computer Science (FOCS), pages 46-57. IEEE Computer Society Press, 1977.","DOI":"10.1109\/SFCS.1977.32"},{"key":"10.2168\/LMCS-8(3:10)2012_RosnerPnueli86","unstructured":"R. Rosner and A. Pnueli. A choppy logic. InProc. 1st Ann. IEEE Symp. on Logic in Computer Science (LICS'86), pages 306-313. IEEE Computer Society Press, June 1986."},{"key":"10.2168\/LMCS-8(3:10)2012_ReifSchellhorn98","doi-asserted-by":"crossref","unstructured":"Wolfgang Reif, Gerhard Schellhorn, Kurt Stenzel, and Michael Balser. Structured specifications and interactive proofs with KIV. In Wolfgang Bibel and Peter H. Schmitt, editors,Automated Deduction - A Basis for Applications, Volume II: Systems and Implementation Techniques, pages 13-39. Kluwer Academic Publishers, Dordrecht, 1998.","DOI":"10.1007\/978-94-017-0435-9_1"},{"key":"10.2168\/LMCS-8(3:10)2012_Siefkes70","doi-asserted-by":"crossref","unstructured":"Dirk Siefkes.Decidable Theories I: B\u00fcchi's Monadic Second Order Successor Arithmetic, volume 120 ofLecture Notes in Mathematics. Springer-Verlag, Berlin, 1970.","DOI":"10.1007\/978-3-662-36678-3"},{"key":"10.2168\/LMCS-8(3:10)2012_Stirling01","doi-asserted-by":"crossref","unstructured":"Colin Stirling.Modal and Temporal Properties of Processes. Springer-Verlag, New York, 2001.","DOI":"10.1007\/978-1-4757-3550-5"},{"issue":"2","key":"10.2168\/LMCS-8(3:10)2012_Thomas79","doi-asserted-by":"crossref","first-page":"148","DOI":"10.1016\/S0019-9958(79)90629-6","volume":"42","author":"Wolfgang Thomas","year":"1979","journal-title":"Inf. and Control"},{"key":"10.2168\/LMCS-8(3:10)2012_Thomas90","doi-asserted-by":"crossref","unstructured":"W. Thomas. Automata on infinite objects. In Jan van Leeuwen, editor,Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics, chapter 4, pages 133-191. Elsevier\/MIT Press, Amsterdam, 1990.","DOI":"10.1016\/B978-0-444-88074-1.50009-3"},{"key":"10.2168\/LMCS-8(3:10)2012_Thomas97","doi-asserted-by":"crossref","unstructured":"W. Thomas. Languages, automata, and logic. In G. Rozenburg and A. Salomaa, editors,Handbook of Formal Languages, volume 3: Beyond words, chapter 7, pages 389-455. Springer-Verlag, Berlin, 1997.","DOI":"10.1007\/978-3-642-59126-6_7"},{"key":"10.2168\/LMCS-8(3:10)2012_ThumsSchellhorn04","doi-asserted-by":"crossref","unstructured":"Andreas Thums, Gerhard Schellhorn, Frank Ortmeier, and Wolfgang Reif. Interactive verification of Statecharts. In Hartmut Ehrig, Werner Damm, J\u00f6rg Desel, Martin Gro\u00dfe-Rhode, Wolfgang Reif, Eckehard Schnieder, and Engelbert Westk\u00e4mper, editors,SoftSpez Final Report, volume 3147 ofLNCS, pages 355-373. Springer-Verlag, 2004.","DOI":"10.1007\/978-3-540-27863-4_20"},{"key":"10.2168\/LMCS-8(3:10)2012_Walukiewicz95a","doi-asserted-by":"crossref","unstructured":"I. Walukiewicz. Completeness of Kozen's axiomatisation of the propositional \u00ce\u00bc-calculus. InProc. 10th Ann. Symp. on Logic in Computer Science (LICS'95), pages 14-24. IEEE Computer Society Press, 1995.","DOI":"10.1109\/LICS.1995.523240"},{"key":"10.2168\/LMCS-8(3:10)2012_Wolper82a","doi-asserted-by":"crossref","unstructured":"P. L. Wolper.Specification and Synthesis of Communicating Processes Using an Extended Temporal Logic. PhD thesis, Department of Computer Science, Stanford University, 1982.","DOI":"10.1145\/582153.582156"},{"issue":"1-2","key":"10.2168\/LMCS-8(3:10)2012_Wolper83","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1016\/S0019-9958(83)80051-5","volume":"56","author":"P. [L.] Wolper","year":"1983","journal-title":"Information and Control"},{"issue":"1","key":"10.2168\/LMCS-8(3:10)2012_WangXu2004","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1016\/S0166-218X(03)00201-4","volume":"136","author":"Hanpin Wang and Qiwen Xu","year":"2004","journal-title":"Discrete Applied Mathematics"},{"key":"10.2168\/LMCS-8(3:10)2012_ZhangDuan2012","doi-asserted-by":"crossref","unstructured":"Nan Zhang, Zhenhua Duan, and Cong Tian. A cylinder computation model for many-core parallel computing.Theor. Comp. Sci., 2012. doi:10.1016\/j.tcs.2012.02.011.","DOI":"10.1016\/j.tcs.2012.02.011"},{"key":"10.2168\/LMCS-8(3:10)2012_ZhouHansen2004","doi-asserted-by":"crossref","unstructured":"Zhou Chaochen and Michael R. Hansen.Duration Calculus: A Formal Approach to Real-Time Systems. Monographs in Theoretical Computer Science (An EATCS series). Springer-Verlag, 2004.","DOI":"10.1007\/978-3-662-06784-0"},{"issue":"5","key":"10.2168\/LMCS-8(3:10)2012_ZhouHoare91","doi-asserted-by":"crossref","first-page":"269","DOI":"10.1016\/0020-0190(91)90122-X","volume":"40","author":"Zhou Chaochen, C. A. R. Hoare, and A. P.","year":"1991","journal-title":"Information Processing Letters"},{"key":"10.2168\/LMCS-8(3:10)2012_ZhouZedan99","doi-asserted-by":"crossref","unstructured":"Shikun Zhou, Hussein Zedan, and Antonio Cau. A framework for analysing the effect of ``change'' in legacy code. In15th IEEE International Conference on Software Maintenance (ICSM'99), pages 411-420, 1999.","DOI":"10.1109\/ICSM.1999.792639"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/759\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/759\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T00:26:27Z","timestamp":1746059187000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/759"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,8,13]]},"references-count":73,"URL":"https:\/\/doi.org\/10.2168\/lmcs-8(3:10)2012","relation":{"is-same-as":[{"id-type":"arxiv","id":"1207.3816","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1207.3816","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"value":"1860-5974","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,8,13]]},"article-number":"759"}}