{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,6]],"date-time":"2026-04-06T08:23:38Z","timestamp":1775463818825,"version":"3.50.1"},"reference-count":75,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[1990,3,1]],"date-time":"1990-03-01T00:00:00Z","timestamp":636249600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[1990,3]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>A brief overview is given of the temporal logics used in concurrent program verification and in database and systems specification. The properties of the underlying modal frame structures are analysed. The relative advantages of the linear and branching approaches are discussed. The state versus path formulas controversy is revisited. A meta-linear operator<jats:italic>L<\/jats:italic>is proposed and compared with the \u201cin all trajectories\u201d operator considered in the language CTL*. The usefulness of the new operator within the context of a layered methodology for database and information systems specification and verification is illustrated. The operator is seen as a \u201cframe change operator\u201d and other interesting operators of this class are referred. Finitary and infinitary axiomatisations are given for the operator<jats:italic>L<\/jats:italic>. The proof of the completeness of the infinitary axiomatisation is briefly outlined. This proof requires an appropriate extension of the usual Henkin methods.<\/jats:p>","DOI":"10.1007\/bf01888216","type":"journal-article","created":{"date-parts":[[2005,7,4]],"date-time":"2005-07-04T21:23:27Z","timestamp":1120512207000},"page":"24-59","source":"Crossref","is-referenced-by-count":7,"title":["Branching versus linear logics yet again"],"prefix":"10.1145","volume":"2","author":[{"given":"Jos\u00e9","family":"Carmo","sequence":"first","affiliation":[{"name":"Department of Mathematics, Section of Computer Science, IST, Av. Rovisco Pais, 1096, Lisboa Codex, Portugal"}]},{"given":"Am\u00edlcar","family":"Sernadas","sequence":"additional","affiliation":[{"name":"Department of Mathematics, Section of Computer Science, IST, Av. Rovisco Pais, 1096, Lisboa Codex, Portugal"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"publisher","DOI":"10.1145\/182.358434"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Ben-Ari M. Manna Z. and Pnueli A.: The Temporal Logic of Branching Time. Proc. 8th Annual Symposium on Principles of Programming Languages ACM pp. 164\u2013175 1981.","DOI":"10.1145\/567532.567551"},{"key":"e_1_2_1_2_3_2","volume-title":"The Logic of Time","author":"van Bentnern J. F. A. K.","year":"1982"},{"key":"e_1_2_1_2_4_2","unstructured":"Boolos G.: The Unprovability of Consistency. An Essay in Modal Logic Cambridge University Press 1979."},{"key":"e_1_2_1_2_5_2","unstructured":"Bubenko J.: The Temporal Dimension in Information Processing. In: Architecture and Models in Database Management G. Nijssen (ed.) North-Holland 1977."},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1111\/j.1755-2567.1978.tb00175.x","article-title":"The Unreal Future","author":"Burgess J. P.","year":"1978","journal-title":"Theoria"},{"key":"e_1_2_1_2_7_2","unstructured":"Carmo J.: The Infolog Branching Logic of Events. In: Theoretical and Formal Aspects of Information Systems 1985 A. Sernadas J. Bubenko and A. Oliv\u00e9 (eds) North-Holland pp. 159\u2013174 1985."},{"key":"e_1_2_1_2_8_2","unstructured":"Carmo J.: L\u00f3gicas Temporais para a Especifica\u00e7\u00e3o e Verifica\u00e7\u00e3o de Sistemas de Informa\u00e7\u00e3o Ph.D. thesis IST (the Lisbon Institute of Technology Technical University of Lisbon) 1988."},{"key":"e_1_2_1_2_9_2","unstructured":"Carmo J. and Sernadas A.: A Temporal Logic Framework for a Layered Approach to Systems Specification and Verification. In: Temporal Aspects in Information Systems C. Rolland F. Bodard and M. Leonard (eds) North-Holland pp. 31\u201346 1988."},{"key":"e_1_2_1_2_10_2","volume-title":"internal report","author":"Carmo J.","year":"1988"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"Carmo J. and Sernadas A.: Inevitability in Branching Time. In: Logic at Botik '89 A. R. Mayer and M. A. Taitslin (eds) LNCS 363 Springer-Verlag pp. 41\u201362 1989.","DOI":"10.1007\/3-540-51237-3_5"},{"key":"e_1_2_1_2_12_2","unstructured":"Carmo J. and Sernadas A.: A Completeness Result in a Mixed Branching-Linear Logic to appear in the proceedings of the Logic Colloquium in Memory of Hugo Ribeiro (Lisbon) 1989."},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"Casanova M. A. and Furtado A. L.: On the Description of Database Transition Constraints Using Temporal Languages. Proc. 2nd Workshop for Logical Basis for Data Bases pp. 211\u2013236 1982.","DOI":"10.1007\/978-1-4615-9385-0_8"},{"key":"e_1_2_1_2_14_2","unstructured":"Castilho J. M. V. Casanova M. A. and Furtado A. L.: A Temporal Framework for Information Systems Specification. Proc. 8th VLDB Conference pp. 280\u2013291 1982."},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Chellas B. F.: Modal Logic: An Introduction Cambridge University Press 1980.","DOI":"10.1017\/CBO9780511621192"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"Clarke E. M. and Emerson E. A.: Design and Synthesis of Synchronization Skeletons Using Branching Time Temporal Logic. Proc. Workshop on Logic of Programs LNCS 131 Springer-Verlag pp. 52\u201371 1981.","DOI":"10.1007\/BFb0025774"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"Clarke E. M. Grumberg O. and Kurshan R. P.: A Synthesis of Two Approaches for Verifying Finite State Concurrent Systems. In: Logic at Botik '89 A. R. Mayer and M. A. Taitslin (eds) LNCS 363 Springer-Verlag pp. 81\u201390 1989.","DOI":"10.1007\/3-540-51237-3_7"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"publisher","DOI":"10.1145\/360933.360975"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"crossref","unstructured":"Ehrich H.-D. Sernadas A. and Sernadas C.: Abstract Object Types for Databases. In: Advances in Object-Oriented Database Systems Dittrich (ed.) Springer-Verlag pp. 144\u2013149 1988.","DOI":"10.1007\/3-540-50345-5_10"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(83)90082-8"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","unstructured":"Emerson E.A. and Halpern J.Y.: Decision Procedures and Expressiveness in the Temporal Logic of Branching Time. Proc. 14th Annual ACM Symposium on Theory of Computing ACM pp. 169\u2013180 1982 (first version) and Journal of Comput. and Syst. Sciences 30 1\u201324 (1985) (second version).","DOI":"10.1145\/800070.802190"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"publisher","DOI":"10.1145\/4904.4999"},{"key":"e_1_2_1_2_23_2","unstructured":"Enderton B.: A Mathematical Introduction to Logic Academic Press 1972."},{"key":"e_1_2_1_2_24_2","unstructured":"Fiadeiro J.: C\u00e1lculo de Objectos e Eventas Ph.D. Thesis IST (the Lisbon Institute of Technology Technical University of Lisbon) 1989."},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"publisher","DOI":"10.1016\/0306-4379(86)90023-2"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00291052"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(79)90046-1"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"crossref","unstructured":"Furtado A. L. and Neuhold E. J.: Formal Technics for Data Base Design Springer-Verlag 1986.","DOI":"10.1007\/978-3-642-70592-2"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00649989"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"crossref","unstructured":"Gabbay D. M. Pnueli A. Shelah S. and Stavi J.: On the Temporal Analysis of Fairness. Proc. 7th Annual ACM Symposium on Principles of Programming Languages ACM pp. 163\u2013173 1980.","DOI":"10.1145\/567446.567462"},{"key":"e_1_2_1_2_31_2","unstructured":"Goldblatt R.: Axiomatizing the Logic of Computer Programming LNCS 137 Springer-Verlag 1982."},{"key":"e_1_2_1_2_32_2","unstructured":"Golshani F. Maibaum T. and Sadler M.: A Modal System of Algebras for Database Specification and Query\/Update Language Support. Proc. 9th VLDB Conference pp. 331\u2013339 1983."},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"crossref","unstructured":"Harel D.: First-Order Dynamic Logic LNCS 68 Springer-Verlag 1979.","DOI":"10.1007\/3-540-09237-4"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"crossref","unstructured":"Harel D. Kozen D. and Parikh R.: Process Logic: Expressiveness Decidability Completeness. Journal of Comput and Syst. Sciences 144\u2013170 (1982).","DOI":"10.1016\/0022-0000(82)90003-4"},{"key":"e_1_2_1_2_35_2","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_2_1_2_36_2","unstructured":"Hughes G. E. and Cresswell M. J.: An Introduction to Modal Logic Methuen and Co. 1968."},{"key":"e_1_2_1_2_37_2","unstructured":"Hughes G. E. and Cresswell M. J.: A Companion to Modal Logic Methuen and Co. 1984."},{"key":"e_1_2_1_2_38_2","volume-title":"Ph. D. thesis","author":"Kamp H.","year":"1968"},{"key":"e_1_2_1_2_39_2","unstructured":"Kung C.: A Temporal Framework for Information Systems Specification and Verification Ph. D. thesis Norwegian Institute of Technology 1984."},{"key":"e_1_2_1_2_40_2","unstructured":"Kung C.: A Tableaux Approach for Consistency Checking. In: Theoretical and Formal Aspects of Information Systems 1985 A. Sernadas J. Bubenko and A. Oliv\u00e9 (eds) North-Holland pp. 191\u2013207 1985."},{"key":"e_1_2_1_2_41_2","doi-asserted-by":"crossref","unstructured":"Lamport L.: \u201cSometime\u201d is Sometimes \u201cNot Never\u201d on the Temporal Logic of Programs. Proc. 7th Annual ACM Symposium on Principles of Programming Languages ACM pp. 174\u2013185 1980.","DOI":"10.1145\/567446.567463"},{"key":"e_1_2_1_2_42_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(82)91022-1"},{"key":"e_1_2_1_2_43_2","doi-asserted-by":"crossref","unstructured":"Lichtenstein O. Pnueli A. and Zuck L.: The Glory of the Past. In: Logics of Programs R. Parikh (ed.) LNCS 193 Springer-Verlag pp. 196\u2013218 1985.","DOI":"10.1007\/3-540-15648-8_16"},{"key":"e_1_2_1_2_44_2","unstructured":"Lipeck U. W.: Transformation of Dynamic Integrity Constraints into Transaction Specifications. Proc. Int. Conf. on Database Theory 1988 LNCS Springer-Verlag 1988."},{"key":"e_1_2_1_2_45_2","unstructured":"Lipeck U. W. Ehrich H. D. and Gogolla M.: Specifying Admissibility of Dynamic Database Behaviour Using Temporal Logic. In: Theoretical and Formal Aspects of Information Systems 1985 A. Sernadas J. Bubenko and A. Oliv\u00e9 (eds) North-Holland pp. 145\u2013157 1985."},{"key":"e_1_2_1_2_46_2","unstructured":"Maibaum T. S. E. Khosla S. and Jeremaes P.: A Modal (Action) Logic for Requirements Specification. In: IEE Computing Series 6 D. Barnes and P. Brown (eds) Peter Peregrinus 1986."},{"key":"e_1_2_1_2_47_2","doi-asserted-by":"crossref","unstructured":"Manna Z. and Pnueli A.: Verification of Concurrent Programs: the Temporal Framework. In: The Correctness Problem in Computer Science R. Boyer and J. Moore (eds) ILCS Academic Press pp. 215\u2013273 1981.","DOI":"10.21236\/ADA106750"},{"key":"e_1_2_1_2_48_2","doi-asserted-by":"crossref","unstructured":"Manna Z. and Pnueli A.: Proving Precedence Properties: the Temporal Way. Automata Languages and Programming 10th Colloquium LNCS 154 Springer-Verlag pp. 491\u2013512 1983.","DOI":"10.1007\/BFb0036932"},{"key":"e_1_2_1_2_49_2","doi-asserted-by":"crossref","unstructured":"McArthur R. P.: Tense Logic D. Reidel Publishing Company 1976.","DOI":"10.1007\/978-94-017-3219-2"},{"issue":"3","key":"e_1_2_1_2_50_2","first-page":"489","article-title":"The Strong Future Tense","author":"McCall S.","year":"1979","journal-title":"Notre Dame Journal of Formal Logic"},{"key":"e_1_2_1_2_51_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(81)90112-2"},{"key":"e_1_2_1_2_52_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00286492"},{"key":"e_1_2_1_2_53_2","doi-asserted-by":"publisher","DOI":"10.1145\/357172.357178"},{"key":"e_1_2_1_2_54_2","doi-asserted-by":"crossref","unstructured":"Pnueli A.: The Temporal Logic of Programs. Proc. 18th Annual ACM Symposium on Foundations of Computer Science IEEE pp. 45\u201357 1977.","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_2_1_2_55_2","doi-asserted-by":"crossref","unstructured":"Pnueli A.: The Temporal Semantics of Concurrent Programs. In: Semantics of Concurrent Computation G. Kahn (ed.) LNCS 70 Springer-Verlag pp. 1\u201320 1979.","DOI":"10.1007\/BFb0022460"},{"key":"e_1_2_1_2_56_2","unstructured":"Pnueli A.: Specification and Development of Reactive Systems. In: Information Processing 86 H. J. Kugler (ed.) pp. 845\u2013858 IFIP 1986."},{"key":"e_1_2_1_2_57_2","doi-asserted-by":"crossref","unstructured":"Pratt V. R.: Semantical Considerations on Floyd-Hoare Logic. Proc. 17th Annual IEEE Symposium on Foundations of Computer Science pp. 109\u2013121 1976.","DOI":"10.1109\/SFCS.1976.27"},{"issue":"1","key":"e_1_2_1_2_58_2","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1007\/BF01379149","article-title":"Modelling Concurrency with Partial Orders","volume":"15","author":"Pratt V. R.","year":"1987","journal-title":"Internationaljournal of Parallel Programming"},{"key":"e_1_2_1_2_59_2","doi-asserted-by":"crossref","unstructured":"Prior A.: Past Present and Future Oxford 1967.","DOI":"10.1093\/acprof:oso\/9780198243113.001.0001"},{"key":"e_1_2_1_2_60_2","first-page":"181","article-title":"Concurrency is More Fundamental than Interleaving","volume":"35","author":"Reisig W.","year":"1988","journal-title":"EATCS Bulletin"},{"key":"e_1_2_1_2_61_2","doi-asserted-by":"crossref","unstructured":"Rescher N. and Urquhart A.: Temporal Logic Springer-Verlag 1971.","DOI":"10.1007\/978-3-7091-7664-1"},{"key":"e_1_2_1_2_62_2","unstructured":"Rolland C. Leifert S. and Richard C: Tools for Information Systems Dynamics Management. Proc. 5th VLDB Conference 1979."},{"key":"e_1_2_1_2_63_2","unstructured":"Schiel U.: The Time Dimension in Information Systems. In: Theoretical and Formal Aspects of Information Systems A. Sernadas J. Bubenko and A. Oliv\u00e9 (eds) North-Holland pp. 67\u201375 1985."},{"issue":"2","key":"e_1_2_1_2_64_2","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1016\/0306-4379(80)90009-5","article-title":"Temporal Aspects of Logical Procedure Definition","volume":"5","author":"Sernadas A.","year":"1980","journal-title":"Information Systems"},{"key":"e_1_2_1_2_65_2","unstructured":"Sernadas A. and Sernadas C.: Infolog: an Integrated Model of Data and Processes INFOLOG RR05 IFIP WG 8.1 Meeting York 1983."},{"key":"e_1_2_1_2_66_2","unstructured":"Sernadas A. and Sernadas C.: Capturing Knowledge About the Organization Dynamics. In: Knowledge Representation for DDS L. B. Methlie and R. Sprague (eds) North-Holland 1985."},{"key":"e_1_2_1_2_67_2","unstructured":"Sernadas A. Carmo J. and Sernadas C.: Software Behavior Specification with Triggering Logic INFOLOG RR02 Faculty of Sciences Lisbon 1982."},{"key":"e_1_2_1_2_68_2","volume-title":"internal report","author":"Sernadas A.","year":"1989"},{"key":"e_1_2_1_2_69_2","unstructured":"Sernadas A. Sernadas C. and Ehrich H.-D.: Object-Oriented Specification of Databases: An Algebraic Approach. In: Proc. 13th Conference on Very Large Data Bases P. Hammersley (ed.) 1987."},{"key":"e_1_2_1_2_70_2","unstructured":"Sernadas A. Fiadeiro J. Sernadas C. and Ehrich H.-D.: Abstract Object Types: A Temporal Perspective. In: Colloquium on Temporal Logic and Specification A. Pnueli H. Barringer and B. Banieqbal (eds) Springer-Verlag (to be published)."},{"key":"e_1_2_1_2_71_2","unstructured":"Stirling C.: Comparing Linear and Branching Time Temporal Logics to appear in Proc. Alvey Colloquium on Temporal Logics Springer-Verlag 1987."},{"key":"e_1_2_1_2_72_2","doi-asserted-by":"publisher","DOI":"10.1111\/j.1755-2567.1970.tb00427.x"},{"key":"e_1_2_1_2_73_2","unstructured":"Veloso P. and Furtado A.L.: Towards Simpler and Yet Complete Formal Specifications. In: Theoretical and Formal Aspects of Information Systems 1985 A. Sernadas J. Bubenko and A. Oliv\u00e9 (eds) North-Holland pp. 175\u2013189 1985."},{"key":"e_1_2_1_2_74_2","unstructured":"Venema Y. de: Expressiveness and Completeness of an Interval Tense Logic ITLI Prepublication Series 88-02 Institute for Language Logic and Information University of Amsterdam 1988."},{"key":"e_1_2_1_2_75_2","unstructured":"Zanardo A.: A Complete Deductive System for Since-Until Branching-Time Logic internal report Dipartimento di Matematica Pura ed Applicata Universita' Degli Studi di Padova 1989."}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01888216.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01888216\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/BF01888216","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,2]],"date-time":"2025-01-02T09:33:23Z","timestamp":1735810403000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/BF01888216"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1990,3]]},"references-count":75,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1990,3]]}},"alternative-id":["10.1007\/BF01888216"],"URL":"https:\/\/doi.org\/10.1007\/bf01888216","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[1990,3]]}}}