{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,7]],"date-time":"2025-12-07T16:01:17Z","timestamp":1765123277634,"version":"build-2065373602"},"reference-count":223,"publisher":"Elsevier","isbn-type":[{"type":"print","value":"9780444516909"}],"license":[{"start":{"date-parts":[[2007,1,1]],"date-time":"2007-01-01T00:00:00Z","timestamp":1167609600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2007,1,1]],"date-time":"2007-01-01T00:00:00Z","timestamp":1167609600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2007]]},"DOI":"10.1016\/s1570-2464(07)80014-0","type":"book-chapter","created":{"date-parts":[[2007,10,4]],"date-time":"2007-10-04T09:38:50Z","timestamp":1191490730000},"page":"655-720","source":"Crossref","is-referenced-by-count":18,"title":["11 Temporal logic"],"prefix":"10.1016","member":"78","reference":[{"key":"10.1016\/S1570-2464(07)80014-0_bib1","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/3-540-15648-8_1","article-title":"Nonclausal Temporal Deduction","volume":"193","author":"Abadi","year":"1985","journal-title":"Lecture Notes in Computer Science"},{"key":"10.1016\/S1570-2464(07)80014-0_bib2","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1145\/77600.77617","article-title":"Non-clausal deduction in first-order temporal logic","volume":"37","author":"Abadi","year":"1990","journal-title":"J. ACM"},{"key":"10.1016\/S1570-2464(07)80014-0_bib3","series-title":"Recent Advances in Temporal Databases","first-page":"43","article-title":"Temporal connectives versus explicit timestamps in temporal query languages","author":"Abiteboul","year":"1995"},{"key":"10.1016\/S1570-2464(07)80014-0_bib4","series-title":"ACM Symposium on Principles of Database Systems","first-page":"49","article-title":"Temporal versus first-order logic in query temporal databases","author":"Abiteboul","year":"1996"},{"key":"10.1016\/S1570-2464(07)80014-0_bib5","doi-asserted-by":"crossref","first-page":"296","DOI":"10.1145\/772062.772064","article-title":"An n! lower bound on formula size","volume":"4","author":"Adler","year":"2003","journal-title":"ACM Transactions on Computational Logic"},{"issue":"11","key":"10.1016\/S1570-2464(07)80014-0_bib6","doi-asserted-by":"crossref","first-page":"832","DOI":"10.1145\/182.358434","article-title":"Maintaining knowledge about temporal intervals","volume":"26","author":"Allen","year":"1983","journal-title":"Communications of the ACM"},{"issue":"2","key":"10.1016\/S1570-2464(07)80014-0_bib7","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1016\/0004-3702(84)90008-0","article-title":"Towards a general theory of action and time","volume":"23","author":"Allen","year":"1984","journal-title":"Artificial Intelligence"},{"key":"10.1016\/S1570-2464(07)80014-0_bib8","first-page":"35","article-title":"Real-time logics: Complexity and expressiveness","volume":"104","author":"Alur","year":"1993","journal-title":"Information and Control"},{"key":"10.1016\/S1570-2464(07)80014-0_bib9","doi-asserted-by":"crossref","first-page":"672","DOI":"10.1145\/585265.585270","article-title":"Alternating-time temporal logic","volume":"49","author":"Alur","year":"2002","journal-title":"Journal of the ACM"},{"issue":"1","key":"10.1016\/S1570-2464(07)80014-0_bib10","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1016\/0022-0000(87)90003-1","article-title":"Expressive completeness failure in branching time structures","volume":"34","author":"Amir","year":"1982","journal-title":"Journal of Computer and System Sciences"},{"year":"1982","author":"Amir","article-title":"Functional Completeness in Tense Logic","key":"10.1016\/S1570-2464(07)80014-0_bib11"},{"key":"10.1016\/S1570-2464(07)80014-0_bib12","doi-asserted-by":"crossref","first-page":"177","DOI":"10.1016\/S0019-9958(85)80059-0","article-title":"Separation in nonlinear time models","volume":"66","author":"Amir","year":"1985","journal-title":"Information and Control"},{"key":"10.1016\/S1570-2464(07)80014-0_bib13","doi-asserted-by":"crossref","first-page":"66","DOI":"10.1016\/0890-5401(87)90051-4","article-title":"Preservation of expressive completeness in temporal models","volume":"72","author":"Amir","year":"1987","journal-title":"Information and Computation"},{"key":"10.1016\/S1570-2464(07)80014-0_bib14","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1093\/logcom\/14.1.3","article-title":"On non-local propositional and weak monodic quantified CTL*","volume":"14","author":"Bauer","year":"2004","journal-title":"Journal of Logic and Computation"},{"year":"1993","author":"Ben-Ari","series-title":"Mathematical Logic for Computer Science","key":"10.1016\/S1570-2464(07)80014-0_bib15"},{"key":"10.1016\/S1570-2464(07)80014-0_bib16","first-page":"309","article-title":"Semantic entailment and formal derivability","volume":"18","author":"Beth","year":"1955","journal-title":"Mededelingen der Koninklijke Nederlandse Akad. van Wetensch"},{"year":"2000","author":"Bettini","series-title":"Time Granularities in Databases, Data Mining, and Temporal Reasoning","key":"10.1016\/S1570-2464(07)80014-0_bib17"},{"key":"10.1016\/S1570-2464(07)80014-0_bib18","doi-asserted-by":"crossref","first-page":"277","DOI":"10.1093\/logcom\/14.2.277","article-title":"Order independent temporal properties","volume":"14","author":"Bidoit","year":"2004","journal-title":"J. Logic Computat"},{"issue":"1","key":"10.1016\/S1570-2464(07)80014-0_bib19","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1093\/jigpal\/7.1.27","article-title":"Hybrid languages and temporal logic","volume":"7","author":"Blackburn","year":"1999","journal-title":"Logic Journal of the IGPL"},{"issue":"3","key":"10.1016\/S1570-2464(07)80014-0_bib20","doi-asserted-by":"crossref","first-page":"403","DOI":"10.1305\/ndjfl\/1093635505","article-title":"Concerted instant-interval temporal semantics I: Temporal ontologies","volume":"31","author":"Bochman","year":"1990","journal-title":"Notre Dame J. of Formal Logic"},{"year":"1995","series-title":"Time and Logic: A Computational Approach","key":"10.1016\/S1570-2464(07)80014-0_bib21"},{"key":"10.1016\/S1570-2464(07)80014-0_bib22","series-title":"Pro- ceedings of TIME-97 the Fourth International Workshop on Temporal Representation and Reasoning","first-page":"20","article-title":"A Resolution Method for CTL Branching-Time Temporal Logic","author":"Bolotov","year":"1997"},{"key":"10.1016\/S1570-2464(07)80014-0_bib23","series-title":"Proc. FSTTCS 2005","first-page":"432","article-title":"On the expressiveness of TPTL and MTL","volume":"3821","author":"Bouyer","year":"2005"},{"key":"10.1016\/S1570-2464(07)80014-0_bib24","series-title":"Advances in Temporal Logic","first-page":"435","article-title":"Specification and prototyping of structured multimedia documents using interval temporal logic","author":"Bowman","year":"2000"},{"key":"10.1016\/S1570-2464(07)80014-0_bib25","series-title":"Logic, Methodology, and Philosophy of Science: Proc. 1960 Intern. Congress","first-page":"1","article-title":"On a decision method in restricted second order arithmetic","author":"B\u00fcchi","year":"1962"},{"key":"10.1016\/S1570-2464(07)80014-0_bib26","doi-asserted-by":"crossref","first-page":"282","DOI":"10.1111\/j.1755-2567.1970.tb00428.x","article-title":"An approach to tense logic","volume":"36","author":"Bull","year":"1970","journal-title":"Theoria"},{"key":"10.1016\/S1570-2464(07)80014-0_bib27","series-title":"Handbook of Philosophical Logic II","first-page":"1","article-title":"Basic modal logic","author":"Bull","year":"1984"},{"key":"10.1016\/S1570-2464(07)80014-0_bib28","doi-asserted-by":"crossref","first-page":"566","DOI":"10.2307\/2273296","article-title":"Logic and time","volume":"44","author":"Burgess","year":"1979","journal-title":"J. Symbolic Logic"},{"key":"10.1016\/S1570-2464(07)80014-0_bib29","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1007\/BF00370320","article-title":"Decidability for branching time","volume":"39","author":"Burgess","year":"1980","journal-title":"Studia Logica"},{"issue":"2","key":"10.1016\/S1570-2464(07)80014-0_bib30","first-page":"367","article-title":"Axioms for tense logic I: \u2018Since\u2019 and \u2018Until\u2019","volume":"23","author":"Burgess","year":"1982","journal-title":"Notre Dame J. Formal Logic"},{"issue":"4","key":"10.1016\/S1570-2464(07)80014-0_bib31","doi-asserted-by":"crossref","first-page":"375","DOI":"10.1305\/ndjfl\/1093870150","article-title":"Axioms for tense logic II. Time periods","volume":"23","author":"Burgess","year":"1982","journal-title":"Notre Dame Journal of Formal Logic"},{"key":"10.1016\/S1570-2464(07)80014-0_bib32","series-title":"Handbook of Philo- sophical Logic, vol II: Extensions of Classical Logic","first-page":"89","article-title":"Basic tense logic","author":"Burgess","year":"1984"},{"issue":"2","key":"10.1016\/S1570-2464(07)80014-0_bib33","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1305\/ndjfl\/1093870820","article-title":"The decision problem for linear temporal logic","volume":"26","author":"Burgess","year":"1985","journal-title":"Notre Dame J. Formal Logic"},{"key":"10.1016\/S1570-2464(07)80014-0_bib34","series-title":"Proceedings of the 1th International Conference on Automated Deduction, volume 170 of Lecture Notes in Computer Science","first-page":"113","article-title":"A Decision Method for Linear Temporal Logic","author":"Cavalli","year":"1984"},{"key":"10.1016\/S1570-2464(07)80014-0_bib35","series-title":"Proc. IBM Workshop on Logic of Programs, Yorktown Heights, NY","first-page":"52","article-title":"Synthesis of synchronization skeletons for branching time temporal logic","author":"Clarke","year":"1981"},{"key":"10.1016\/S1570-2464(07)80014-0_bib36","first-page":"1635","article-title":"Model checking","volume":"volume II","author":"Clarke","year":"2001"},{"key":"10.1016\/S1570-2464(07)80014-0_bib37","series-title":"Proceedings of Conference on Automated Deduction (CADE)","first-page":"397","article-title":"Monodic Temporal Resolution","author":"Degtyarev","year":"2003"},{"key":"10.1016\/S1570-2464(07)80014-0_bib38","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1023\/A:1021352309671","article-title":"Equality and monodic first-order temporal logic","volume":"72","author":"Degtyarev","year":"2002","journal-title":"Studia Logica"},{"key":"10.1016\/S1570-2464(07)80014-0_bib39","series-title":"Handbook of Theoretical Computer Science","first-page":"995","article-title":"Temporal and modal logics","author":"Emerson","year":"1990"},{"key":"10.1016\/S1570-2464(07)80014-0_bib40","series-title":"Logics for Concurrency","first-page":"41","article-title":"Automated temporal reasoning for reactive systems","author":"Emerson","year":"1996"},{"key":"10.1016\/S1570-2464(07)80014-0_bib41","doi-asserted-by":"crossref","first-page":"241","DOI":"10.1016\/0167-6423(83)90017-5","article-title":"Using branching time temporal logic to synthesise synchronisation skeletons","volume":"2","author":"Emerson","year":"1982","journal-title":"Sci. of Computer Programming"},{"issue":"1","key":"10.1016\/S1570-2464(07)80014-0_bib42","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0022-0000(85)90001-7","article-title":"Decision procedures and expressiveness in the temporal logic of branching time","volume":"30","author":"Emerson","year":"1985","journal-title":"J. Comp and Sys. Sci"},{"key":"10.1016\/S1570-2464(07)80014-0_bib43","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1145\/4904.4999","article-title":"\u2018Sometimes\u2019 and \u2018not never\u2019 revisited: on branching versus linear time","volume":"33","author":"Emerson","year":"1986","journal-title":"J. ACM"},{"key":"10.1016\/S1570-2464(07)80014-0_bib44","series-title":"29th IEEE Foundations of Computer Science, Proceedings","first-page":"328","article-title":"Complexity of tree automata and modal logics of programs","author":"Emerson","year":"1988"},{"key":"10.1016\/S1570-2464(07)80014-0_bib45","series-title":"Proc. 12th ACM Symp. Princ. Prog. Lang.","first-page":"84","article-title":"Modalities for model checking: branching time strikes back","author":"Emerson","year":"1985"},{"key":"10.1016\/S1570-2464(07)80014-0_bib46","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1016\/S0019-9958(84)80047-9","article-title":"Deciding full branching time logic","volume":"61","author":"Emerson","year":"1984","journal-title":"Information and Control"},{"key":"10.1016\/S1570-2464(07)80014-0_bib47","doi-asserted-by":"crossref","first-page":"88","DOI":"10.1006\/inco.1999.2846","article-title":"An until hierarchy and other applications of an Ehrenfeucht-Fra\u00efss\u00e9 game for temporal logic","volume":"160","author":"Etessami","year":"2000","journal-title":"Information and Computation"},{"year":"1995","author":"Fagin","series-title":"Reasoning about Knowledge","key":"10.1016\/S1570-2464(07)80014-0_bib48"},{"key":"10.1016\/S1570-2464(07)80014-0_bib49","series-title":"Logic, Language and Reasoning: Essays in Honour of Dov Gabbay","first-page":"81","article-title":"Imperative history: two-dimensional executable temporal logic","author":"Finger","year":"1999"},{"key":"10.1016\/S1570-2464(07)80014-0_bib50","series-title":"Proceedings of the 12th International Joint Conference on Artificial Intelligence (IJCAI)","first-page":"99","article-title":"A resolution method for temporal logic","author":"Fisher","year":"1991"},{"key":"10.1016\/S1570-2464(07)80014-0_bib51","series-title":"Handbook of Knowledge Representation, volume 2 of Foundations of Artificial Intelligence","article-title":"Temporal Representation and Reasoning","author":"Fisher","year":"2006"},{"issue":"1","key":"10.1016\/S1570-2464(07)80014-0_bib52","doi-asserted-by":"crossref","first-page":"12","DOI":"10.1145\/371282.371311","article-title":"Clausal Temporal Resolution","volume":"2","author":"Fisher","year":"2001","journal-title":"ACM Transactions on Computa- tional Logic"},{"year":"1952","series-title":"Fredric Brenton Fitch Symbolic Logic","key":"10.1016\/S1570-2464(07)80014-0_bib53"},{"year":"1983","author":"Fitting","series-title":"Proof methods for modal and intuitionistic logics","key":"10.1016\/S1570-2464(07)80014-0_bib54"},{"key":"10.1016\/S1570-2464(07)80014-0_bib55","doi-asserted-by":"crossref","first-page":"229","DOI":"10.1023\/A:1024643624349","article-title":"Branching within time: an expressively complete and elementarily decidable temporal logic for time granularity","volume":"1","author":"Franceschet","year":"2003","journal-title":"Research on Language and Computation"},{"year":"1972","author":"Frege","series-title":"Conceptual Notation (Begriffschrift), and related articles","key":"10.1016\/S1570-2464(07)80014-0_bib56"},{"key":"10.1016\/S1570-2464(07)80014-0_bib57","first-page":"229","article-title":"A sound and complete proof system for QPTL","volume":"volume 4","author":"French","year":"2003"},{"year":"1976","author":"Gabbay","series-title":"Investigations in Modal and Tense Logics with Applications to Problems in Philosophy and Linguistics, volume 92 of Synthese","key":"10.1016\/S1570-2464(07)80014-0_bib58"},{"key":"10.1016\/S1570-2464(07)80014-0_bib59","series-title":"Aspects of Philosophical Logic","first-page":"91","article-title":"Expressive functional completeness in tense logic (preliminary report)","author":"Gabbay","year":"1981"},{"key":"10.1016\/S1570-2464(07)80014-0_bib60","series-title":"Aspects of Philosophical Logic","first-page":"67","article-title":"An irreflexivity lemma with applications to axiomatizations of conditions on tense frames","author":"Gabbay","year":"1981"},{"key":"10.1016\/S1570-2464(07)80014-0_bib61","series-title":"Proceedings of Colloquium on Temporal Logic in Specification, Altrincham, 1987, volume 398 of Lecture Notes in Computer Science","first-page":"67","article-title":"Declarative past and imperative future: Executable temporal logic for interactive sys- tems","author":"Gabbay","year":"1989"},{"issue":"2","key":"10.1016\/S1570-2464(07)80014-0_bib62","doi-asserted-by":"crossref","first-page":"229","DOI":"10.1093\/logcom\/1.2.229","article-title":"An axiomatisation of the temporal logic with until and since over the real numbers","volume":"1","author":"Gabbay","year":"1990","journal-title":"Journal of Logic and Computation"},{"key":"10.1016\/S1570-2464(07)80014-0_bib63","series-title":"Logic Colloquium '90, volume 2 of Lecture Notes in Logic","first-page":"89","article-title":"Temporal expressive completeness in the presence of gaps","author":"Gabbay","year":"1993"},{"volume":"Vol. 1","year":"1994","author":"Gabbay","key":"10.1016\/S1570-2464(07)80014-0_bib64"},{"key":"10.1016\/S1570-2464(07)80014-0_bib65","series-title":"Volume 148 of Studies in Logic and the Foundations of Mathematics","article-title":"M any-Dimensional Modal Logics: Theory and Applications","author":"Gabbay","year":"2003"},{"key":"10.1016\/S1570-2464(07)80014-0_bib66","series-title":"Proceedings of the Seventh ACM Symposium on the Principles of Programming Languages","first-page":"163","article-title":"On the Temporal Analysis of Fairness","author":"Gabbay","year":"1980"},{"year":"1987","author":"Galton","series-title":"Temporal logics and their applications","key":"10.1016\/S1570-2464(07)80014-0_bib67"},{"key":"10.1016\/S1570-2464(07)80014-0_bib68","series-title":"Handbook of Philosophical Logic","first-page":"249","article-title":"Quantification in modal logic","author":"Garson","year":"1984"},{"key":"10.1016\/S1570-2464(07)80014-0_bib69_1","doi-asserted-by":"crossref","first-page":"176","DOI":"10.1007\/BF01201353","article-title":"Untersuchungen \u00fcber das logische Schliessen","volume":"39","author":"Gentzen","year":"1934","journal-title":"Math. Zeitschrift"},{"key":"10.1016\/S1570-2464(07)80014-0_bib69_2","doi-asserted-by":"crossref","first-page":"405","DOI":"10.1007\/BF01201363","article-title":"Untersuchungen \u00fcber das logische Schliessen","volume":"39","author":"Gentzen","year":"1934","journal-title":"Math. Zeitschrift"},{"key":"10.1016\/S1570-2464(07)80014-0_bib70","series-title":"Albert Einstein: Philosopher-Scientist","first-page":"555","article-title":"A remark about the relationship between relativity theory and idealistic philosophy","author":"G\u00f6del","year":"1970"},{"key":"10.1016\/S1570-2464(07)80014-0_bib71","doi-asserted-by":"crossref","first-page":"219","DOI":"10.1007\/BF00370321","article-title":"Diodorean modality in Minkowski space-time","volume":"39","author":"Goldblatt","year":"1980","journal-title":"Studia Logica"},{"key":"10.1016\/S1570-2464(07)80014-0_bib72","series-title":"Center for the Study of Language and Information","article-title":"Logics of Time and Computation, volume 7 of CSLI Lecture Notes","author":"Goldblatt","year":"1992"},{"key":"10.1016\/S1570-2464(07)80014-0_bib73","series-title":"Center for the Study of Language and Information","article-title":"Mathematics of Modality, volume 43 of CSLI Lecture Notes","author":"Goldblatt","year":"1993"},{"issue":"3","key":"10.1016\/S1570-2464(07)80014-0_bib74","doi-asserted-by":"crossref","first-page":"221","DOI":"10.1080\/11663081.2000.10510998","article-title":"Computation tree logics and temporal logics with reference pointers","volume":"10","author":"Goranko","year":"2000","journal-title":"Journal of Applied Non-classical Logics"},{"key":"10.1016\/S1570-2464(07)80014-0_bib75","series-title":"Proc. Internat. Conference on Automated Reasoning with Analytic Tableaux and Related Methods (Tableaux 2003)","first-page":"102","article-title":"A general tableau method for propositional interval temporal logics","author":"Goranko","year":"2003"},{"issue":"9","key":"10.1016\/S1570-2464(07)80014-0_bib76","first-page":"1137","article-title":"Propositional interval neighborhood logics","volume":"9","author":"Goranko","year":"2003","journal-title":"Journal of Universal Computer Science"},{"issue":"1","key":"10.1016\/S1570-2464(07)80014-0_bib77","first-page":"11","article-title":"A road map of propositional interval temporal logics and duration calculi","volume":"14","author":"Goranko","year":"2004","journal-title":"Journal of Applied Non-classical Logics"},{"key":"10.1016\/S1570-2464(07)80014-0_bib78","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1016\/j.tcs.2005.07.043","article-title":"Complete axiomatization and decidability of alternating-time temporal logic","volume":"353","author":"Goranko","year":"2006","journal-title":"Theoretical Computer Science"},{"issue":"3","key":"10.1016\/S1570-2464(07)80014-0_bib79","doi-asserted-by":"crossref","first-page":"433","DOI":"10.1007\/BF01057938","article-title":"Cut-free sequent and tableau systems for propositional diodorean modal logics","volume":"53","author":"Gor\u00e9","year":"1994","journal-title":"Studia Logica"},{"key":"10.1016\/S1570-2464(07)80014-0_bib80","series-title":"Handbook of Tableau Methods","first-page":"297","article-title":"Tableau methods for modal and temporal logics","author":"Gor\u00e9","year":"1999"},{"year":"1984","author":"Gough","article-title":"Decision Procedures for Temporal Logic","key":"10.1016\/S1570-2464(07)80014-0_bib81"},{"issue":"1\u20136","key":"10.1016\/S1570-2464(07)80014-0_bib82","first-page":"1","article-title":"The succinctness of first-order logic on linear orders","volume":"1","author":"Grohe","year":"2005","journal-title":"Logical Methods in Computer Science"},{"key":"10.1016\/S1570-2464(07)80014-0_bib83_1","first-page":"5","article-title":"Elementary properties of ordered abelian groups","volume":"3","author":"Gurevich","year":"1964","journal-title":"Algebra and Logic"},{"issue":"46","key":"10.1016\/S1570-2464(07)80014-0_bib83_2","first-page":"165","year":"1965","journal-title":"Amer. Math. Soc."},{"key":"10.1016\/S1570-2464(07)80014-0_bib84","doi-asserted-by":"crossref","first-page":"179","DOI":"10.1016\/0003-4843(82)90004-3","article-title":"Monadic theory of order and topology in ZFC","volume":"23","author":"Gurevich","year":"1982","journal-title":"Annals of Math. Logic"},{"key":"10.1016\/S1570-2464(07)80014-0_bib85","doi-asserted-by":"crossref","first-page":"668","DOI":"10.2307\/2274321","article-title":"The decision problem for branching time logic","volume":"50","author":"Gurevich","year":"1985","journal-title":"J. of Symbolic Logic"},{"key":"10.1016\/S1570-2464(07)80014-0_bib86","series-title":"Proceedings of International Colloquium on Automata, Languages and Programming, volume 267 of Lecture Notes in Computer Science","first-page":"269","article-title":"Computation tree logic CTL* and path quantifiers in the monadic the- ory of the binary tree","author":"Hafer","year":"1987"},{"key":"10.1016\/S1570-2464(07)80014-0_bib87","series-title":"Proceedings, Symposium on Logic in Computer Science","first-page":"279","article-title":"A propositional modal logic of time intervals","author":"Halpern","year":"1986"},{"key":"10.1016\/S1570-2464(07)80014-0_bib88","first-page":"195","article-title":"The complexity of reasoning about knowledge and time","volume":"38","author":"Halpern","year":"1989","journal-title":"JCSS"},{"key":"10.1016\/S1570-2464(07)80014-0_bib89","first-page":"7","article-title":"Form and content in quantification theory","volume":"8","author":"Hintikka","year":"1955","journal-title":"Acta Philosophica Fennica"},{"key":"10.1016\/S1570-2464(07)80014-0_bib90","series-title":"Logic at Work, volume 24 of Studies in Fuzziness and Soft Computing","first-page":"158","article-title":"Mosaics and step-by-step (Remarks on 'A modal logic of relations')","author":"Hirsch","year":"1998"},{"issue":"62","key":"10.1016\/S1570-2464(07)80014-0_bib91","first-page":"1","article-title":"Logics for real time: Decidability and complexity","author":"Hirschfield","year":"2004","journal-title":"Fundamenta Informaticae"},{"key":"10.1016\/S1570-2464(07)80014-0_bib92","series-title":"Handbook of Philosophical Logic","first-page":"1","article-title":"Elementary predicate logic","author":"Hodges","year":"1983"},{"key":"10.1016\/S1570-2464(07)80014-0_bib93","doi-asserted-by":"crossref","first-page":"535","DOI":"10.1007\/BF01049409","article-title":"Finite H-dimension does not imply expressive completeness","volume":"23","author":"Hodkinson","year":"1994","journal-title":"J. Philosophical Logic"},{"key":"10.1016\/S1570-2464(07)80014-0_bib94","series-title":"Modal logic and process algebra, volume 53 of Lecture notes","first-page":"171","article-title":"Expressive completeness of Until and Since over Dedekind complete linear time","author":"Hodkinson","year":"1995"},{"key":"10.1016\/S1570-2464(07)80014-0_bib95","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(94)00084-V","article-title":"On Gabbay's temporal fixed point operator","volume":"139","author":"Hodkinson","year":"1995","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1570-2464(07)80014-0_bib96","doi-asserted-by":"crossref","first-page":"185","DOI":"10.1023\/A:1021356410579","article-title":"Monodic packed fragment with equality is decidable","volume":"72","author":"Hodkinson","year":"2002","journal-title":"Studia Logica"},{"key":"10.1016\/S1570-2464(07)80014-0_bib97","doi-asserted-by":"crossref","first-page":"94","DOI":"10.1016\/j.apal.2005.06.007","article-title":"Complexity of monodic packed fragment over linear and real time","volume":"138","author":"Hodkinson","year":"2006","journal-title":"Annals of Pure and Applied Logic"},{"doi-asserted-by":"crossref","unstructured":"I. Hodkinson, R. Kontchakov, A. Kurucz, F. Wolter, and M. Zakharyaschev. On the computational complexity of decidable fragments of first-order linear temporal logics. In Reynolds and Sattar [169], pages 91-98.","key":"10.1016\/S1570-2464(07)80014-0_bib98","DOI":"10.1109\/TIME.2003.1214884"},{"issue":"1","key":"10.1016\/S1570-2464(07)80014-0_bib99","doi-asserted-by":"crossref","first-page":"81","DOI":"10.1023\/A:1017951631048","article-title":"The k-variable property is stronger than k-dimension k","volume":"26","author":"Hodkinson","year":"1997","journal-title":"J. Philosophical Logic"},{"key":"10.1016\/S1570-2464(07)80014-0_bib100","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1016\/S0168-0072(00)00018-X","article-title":"Decidable fragments of first-order temporal logics","volume":"106","author":"Hodkinson","year":"2000","journal-title":"Ann. Pure Appl. Logic"},{"key":"10.1016\/S1570-2464(07)80014-0_bib101","series-title":"Logic for Programming, Artificial Intelligence and Reasoning, volume 2250 of LNAI","first-page":"1","article-title":"Monodic fragments of first-order temporal logics: 2000-2001 A.D","author":"Hodkinson","year":"2001"},{"key":"10.1016\/S1570-2464(07)80014-0_bib102","series-title":"Proc. 17th IEEE Symposium on Logic in Computer Science (LICS)","first-page":"393","article-title":"M on odic fragments of first-order branching temporal logics","author":"Hodkinson","year":"2002"},{"year":"1968","author":"Hughes","series-title":"An Introduction to Modal Logic","key":"10.1016\/S1570-2464(07)80014-0_bib103"},{"key":"10.1016\/S1570-2464(07)80014-0_bib104","doi-asserted-by":"crossref","first-page":"257","DOI":"10.1090\/S0002-9947-1924-1501278-0","article-title":"A new set of postulates for betweenness, with proof of complete independence","volume":"26","author":"Huntington","year":"1924","journal-title":"Transactions of the American Mathematical Society"},{"key":"10.1016\/S1570-2464(07)80014-0_bib105","series-title":"Proceedings of 19th Interna- tional Conference on Automated Deduction (CADE)","first-page":"274","article-title":"TRP++2.0: A temporal resolution prover","author":"Hustadt","year":"2003"},{"key":"10.1016\/S1570-2464(07)80014-0_bib106","series-title":"LICS87, Proceedings of the Symposium on Logic in Computer Science, Ithaca, New York","first-page":"236","article-title":"Definability with bounded number of bound variables","author":"Immerman","year":"1987"},{"issue":"4","key":"10.1016\/S1570-2464(07)80014-0_bib107","first-page":"173","article-title":"Natural deduction system for tense logics","volume":"23","author":"Indrzejczak","year":"1994","journal-title":"Bulletin of the Section of Logic"},{"key":"10.1016\/S1570-2464(07)80014-0_bib108","series-title":"ICTL 2000, Proceedings","first-page":"93","article-title":"Multiple sequent calculus for tense logics","author":"Indrzejczak","year":"2000"},{"key":"10.1016\/S1570-2464(07)80014-0_bib109","doi-asserted-by":"crossref","first-page":"345","DOI":"10.1023\/B:STUD.0000009565.98020.9b","article-title":"A labelled natural deduction system for linear temporal logic","volume":"75","author":"Indrzejczak","year":"2003","journal-title":"Studia Logica"},{"unstructured":"G. Jaeger, A. Heuerding, S. Schwendimann, F. Achermann, P. Balsiger, P. Brambilla, H. Zimmer- mann, M. Bianchi, K. Guggisberg, and W. Heinle. LWB-The Logics Workbench 1.0. www. lwb.unibe. ch, University of Berne, Switzerland.","key":"10.1016\/S1570-2464(07)80014-0_bib110"},{"year":"2001","author":"Kaiman","series-title":"Automated Reasoning with Otter","key":"10.1016\/S1570-2464(07)80014-0_bib111"},{"year":"1968","author":"Kamp","article-title":"Tense logic and the theory of linear order","key":"10.1016\/S1570-2464(07)80014-0_bib112"},{"key":"10.1016\/S1570-2464(07)80014-0_bib113","first-page":"237","article-title":"Formal properties of \u201cnow\u201d","volume":"37","author":"Kamp","year":"1971","journal-title":"Theoria"},{"key":"10.1016\/S1570-2464(07)80014-0_bib114","doi-asserted-by":"crossref","first-page":"119","DOI":"10.1007\/BF01053026","article-title":"Cut-free sequent calculi for some tense logics","volume":"53","author":"Kashima","year":"1994","journal-title":"Studia Logica"},{"key":"10.1016\/S1570-2464(07)80014-0_bib115","series-title":"The Proceedings of Computer Aided Verification (CAV), volume 697 of Lecture Notes in Computer Science","first-page":"97","article-title":"A decision algorithm for full propositional temporal logic","author":"Kesten","year":"1997"},{"key":"10.1016\/S1570-2464(07)80014-0_bib116","series-title":"Logic for Programming and Automated Reasoning (LPAR 2003), volume 2850 of Lecture Notes in Artificial Intelligence","first-page":"214","article-title":"Handling equality in monodic temporal resolution","author":"Konev","year":"2003"},{"key":"10.1016\/S1570-2464(07)80014-0_bib117","doi-asserted-by":"crossref","first-page":"91","DOI":"10.1023\/B:STUD.0000027468.28935.6d","article-title":"Temporalizing tableaux","volume":"76","author":"Kontchakov","year":"2004","journal-title":"Studia Logica"},{"key":"10.1016\/S1570-2464(07)80014-0_bib118","doi-asserted-by":"crossref","first-page":"403","DOI":"10.1023\/A:1008223921944","article-title":"Bisimulations for temporal logic","volume":"6","author":"Kurtonina","year":"1997","journal-title":"Journal of Logic, Language and Information"},{"year":"1987","author":"Ladkin","article-title":"The Logic of Time Representation","key":"10.1016\/S1570-2464(07)80014-0_bib119"},{"key":"10.1016\/S1570-2464(07)80014-0_bib120","series-title":"Theoretical Aspects of Reasoning about Knowledge (Proc. 1986 Conference)","first-page":"207","article-title":"The logic of distributed protocols","author":"Ladner","year":"1986"},{"year":"1991","author":"Lamport","article-title":"The temporal logic of actions","key":"10.1016\/S1570-2464(07)80014-0_bib121"},{"key":"10.1016\/S1570-2464(07)80014-0_bib122","series-title":"Proc. 17th Annual IEEE Symposium on Logic in Computer Science (LICS'02)","first-page":"383","article-title":"Temporal logic with forgettable past","author":"Laroussinie","year":"2002"},{"key":"10.1016\/S1570-2464(07)80014-0_bib123","doi-asserted-by":"crossref","first-page":"236","DOI":"10.1006\/inco.1999.2817","article-title":"Specification in CTL+past for verification in CTL","volume":"156","author":"Laroussinie","year":"2000","journal-title":"Information and Computation"},{"key":"10.1016\/S1570-2464(07)80014-0_bib124","series-title":"Logics of Programs (Proc. Conf. Brooklyn USA 1985), volume 193 of Lecture Notes in Computer Science","first-page":"196","article-title":"The glory of the past","author":"Lichtenstein","year":"1985"},{"key":"10.1016\/S1570-2464(07)80014-0_bib125","series-title":"12th Internat. Symp. on Temporal Representation and Reasoning (TIME 2005)","first-page":"138","article-title":"Quantitative temporal logics: PSPACE and below","author":"Lutz","year":"2005"},{"year":"1992","author":"Manna","series-title":"The Temporal Logic of Reactive and Concurrent Systems, Vol. 1: Specifications","key":"10.1016\/S1570-2464(07)80014-0_bib126"},{"year":"1995","author":"Manna","series-title":"The Temporal Logic of Reactive and Concurrent Systems, Vol. 2: Safety","key":"10.1016\/S1570-2464(07)80014-0_bib127"},{"key":"10.1016\/S1570-2464(07)80014-0_bib128","series-title":"Proc. 23rd ACM Symposium on Principles of Database Systems","first-page":"13","article-title":"Conditional XPath, the first order complete XPath dialect","author":"Marx","year":"2004"},{"key":"10.1016\/S1570-2464(07)80014-0_bib129","series-title":"Automated Reasoning with Analytic Tableaux and Related Methods, Proceedings of Interna- tional Conference, TABLEAUX 2000, St. Andrews, Scotland, July 2000","first-page":"324","article-title":"The mosaic method for temporal logics","author":"Marx","year":"2000"},{"issue":"6","key":"10.1016\/S1570-2464(07)80014-0_bib130","doi-asserted-by":"crossref","first-page":"897","DOI":"10.1093\/logcom\/9.6.897","article-title":"Undecidability of compass logic","volume":"9","author":"Marx","year":"1999","journal-title":"J. Logic and Computation"},{"year":"1997","author":"Marx","series-title":"Multi-Dimensional Modal Logic","key":"10.1016\/S1570-2464(07)80014-0_bib131"},{"year":"1995","author":"McGuire","article-title":"Two Methods for Checking Formulas of Temporal Logic","key":"10.1016\/S1570-2464(07)80014-0_bib132"},{"key":"10.1016\/S1570-2464(07)80014-0_bib133","doi-asserted-by":"crossref","first-page":"521","DOI":"10.1016\/S0019-9958(66)80013-X","article-title":"Testing and generating infinite sequences by finite automata","volume":"9","author":"McNaughton","year":"1966","journal-title":"Information and Control"},{"key":"10.1016\/S1570-2464(07)80014-0_bib134","series-title":"Proc. International Cong, of Mathematicians (vol. 2)","first-page":"477","article-title":"The inherent computational complexity of theories of ordered sets","author":"Meyer","year":"1974"},{"issue":"2","key":"10.1016\/S1570-2464(07)80014-0_bib135","doi-asserted-by":"crossref","first-page":"305","DOI":"10.1093\/jigpal\/6.2.305","article-title":"Taming first-order logic","volume":"6","author":"Mikul\u00e1s","year":"1998","journal-title":"Journal of the IGPL"},{"key":"10.1016\/S1570-2464(07)80014-0_bib136","first-page":"360","article-title":"On the expressive power of C'TL*","author":"M\u00f6ller","year":"1999"},{"issue":"4","key":"10.1016\/S1570-2464(07)80014-0_bib137","doi-asserted-by":"crossref","first-page":"641","DOI":"10.1093\/logcom\/12.4.641","article-title":"Extending Kamp's theorem to model time granularity","volume":"12","author":"Montanari","year":"2002","journal-title":"Journal of Logic and Computation"},{"year":"1986","author":"Moszkowski","series-title":"Executing Temporal Logic Programs","key":"10.1016\/S1570-2464(07)80014-0_bib138"},{"key":"10.1016\/S1570-2464(07)80014-0_bib139","series-title":"3rd IEEE Symposium on Logic in Computer Science, Proceedings","first-page":"422","article-title":"Weak alternating automata give a simple explanation of why most temporal and dynamic logics are decidable in exponential time","author":"M\u00fcller","year":"1988"},{"year":"1986","author":"N\u00e9meti","article-title":"Free Algebras and Decidability in Algebraic Logic","key":"10.1016\/S1570-2464(07)80014-0_bib140"},{"key":"10.1016\/S1570-2464(07)80014-0_bib141","series-title":"Logic Colloquium '92","first-page":"171","article-title":"Decidable versions of first order logic and cylindric-relativized set algebras","author":"N\u00e9meti","year":"1995"},{"year":"1996","author":"0hstrom","series-title":"Temporal Logic: From Ancient Ideas to Artificial Intelligence, volume 57 of Studies in Linguistic and Philosophy","key":"10.1016\/S1570-2464(07)80014-0_bib142"},{"issue":"39","key":"10.1016\/S1570-2464(07)80014-0_bib143","doi-asserted-by":"crossref","first-page":"325","DOI":"10.1007\/BF00713542","article-title":"On the size of refutation Kripke models for some linear modal and tense logics","author":"Ono","year":"1980","journal-title":"Studia Logica"},{"year":"1998","author":"Ostroff","article-title":"Composition and refinement of discrete real-time systems","key":"10.1016\/S1570-2464(07)80014-0_bib144"},{"key":"10.1016\/S1570-2464(07)80014-0_bib145","series-title":"Computer Science Logic '88, Proceedings, volume 385 of LNCS","first-page":"240","article-title":"Gentzen-systems for propositional temporal logics","author":"Paech","year":"1988"},{"key":"10.1016\/S1570-2464(07)80014-0_bib146","series-title":"Proceedings of the First International Joint Conference on Automated Reasoning (IJCAR), volume 2083 of Lecture Notes in Artificial Intelligence","first-page":"107","article-title":"Deduction-Based Decision Procedure for a Clausal Miniscoped Fragment of FTL","author":"Pliuskevicius","year":"2001"},{"key":"10.1016\/S1570-2464(07)80014-0_bib147","series-title":"Proceedings of the Eighteenth Symposium on Founda- tions of Computer Science","first-page":"46","article-title":"The temporal logic of programs","author":"Pnueli","year":"1977"},{"issue":"47","key":"10.1016\/S1570-2464(07)80014-0_bib148","doi-asserted-by":"crossref","first-page":"641","DOI":"10.2307\/2273594","article-title":"Deux ou trois choses que je sais de Ln","author":"Poizat","year":"1982","journal-title":"Journal of Symbolic Logic"},{"year":"1957","author":"Prior","series-title":"Time and Modality","key":"10.1016\/S1570-2464(07)80014-0_bib149"},{"year":"1967","author":"Prior","series-title":"Past, Present and Future","key":"10.1016\/S1570-2464(07)80014-0_bib150"},{"year":"1968","author":"Prior","series-title":"Papers on Time and Tense","key":"10.1016\/S1570-2464(07)80014-0_bib151"},{"key":"10.1016\/S1570-2464(07)80014-0_bib152","first-page":"1","article-title":"Decidability of second order theories and automata on infinite trees","volume":"141","author":"Rabin","year":"1969","journal-title":"Trans. Amer. Math. Soc"},{"key":"10.1016\/S1570-2464(07)80014-0_bib153","series-title":"Handbook of Mathematical Logic","first-page":"595","article-title":"Decidable theories","author":"Rabin","year":"1977"},{"key":"10.1016\/S1570-2464(07)80014-0_bib154","doi-asserted-by":"crossref","first-page":"669","DOI":"10.1093\/logcom\/8.5.669","article-title":"On the decidability of continuous time specification formalisms","volume":"8","author":"Rabinovich","year":"1998","journal-title":"Journal of Logic and Computation"},{"year":"1947","author":"Reichenbach","series-title":"Elements of Symbolic logic","key":"10.1016\/S1570-2464(07)80014-0_bib155"},{"year":"1971","author":"Rescher","series-title":"Temporal Logic","key":"10.1016\/S1570-2464(07)80014-0_bib156"},{"key":"10.1016\/S1570-2464(07)80014-0_bib157","doi-asserted-by":"crossref","first-page":"165","DOI":"10.1007\/BF00370112","article-title":"An axiomatization for Until and Since over the reals without the IRR rule","volume":"51","author":"Reynolds","year":"1992","journal-title":"Studia Logica"},{"key":"10.1016\/S1570-2464(07)80014-0_bib158","doi-asserted-by":"crossref","first-page":"197","DOI":"10.1007\/BF01050343","article-title":"Axiomatisation and decidability of Fand Pin cyclical time","volume":"23","author":"Reynolds","year":"1994","journal-title":"Journal of Philosophical Logic"},{"key":"10.1016\/S1570-2464(07)80014-0_bib159","series-title":"Temporal Logic, volume 827 of Lecture Notes in Artificial Intelligence","first-page":"117","article-title":"Axiomatizing U and S over integer time","author":"Reynolds","year":"1994"},{"key":"10.1016\/S1570-2464(07)80014-0_bib160","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1007\/BF00370836","article-title":"Axiomatising first-order temporal logic: Until and since over linear time","volume":"57","author":"Reynolds","year":"1996","journal-title":"Studia Logica"},{"key":"10.1016\/S1570-2464(07)80014-0_bib161","doi-asserted-by":"crossref","first-page":"419","DOI":"10.1305\/ndjfl\/1039700748","article-title":"A decidable logic of parallelism","volume":"38","author":"Reynolds","year":"1997","journal-title":"Notre Dame Journal of Formal Logic"},{"key":"10.1016\/S1570-2464(07)80014-0_bib162","series-title":"Fifteenth Annual IEEE Symposium on Logic in Computer Science (LICS'2000), Santa Barbara, California, USA, June 26-28, 2000","first-page":"229","article-title":"More past glories","author":"Reynolds","year":"2000"},{"issue":"3","key":"10.1016\/S1570-2464(07)80014-0_bib163","doi-asserted-by":"crossref","first-page":"1011","DOI":"10.2307\/2695091","article-title":"An axiomatization of full computation tree logic","volume":"66","author":"Reynolds","year":"2001","journal-title":"J. Symbolic Logic"},{"key":"10.1016\/S1570-2464(07)80014-0_bib164","series-title":"Australian Artificial Intelligence Conference, AI'01, Adelaide, Australia, December 11-14, 2001, Proceedings, volume 2256 of Lecture Notes in A.I.","first-page":"414","article-title":"Continuous temporal models","author":"Reynolds","year":"2001"},{"key":"10.1016\/S1570-2464(07)80014-0_bib165","doi-asserted-by":"crossref","first-page":"679","DOI":"10.1093\/logcom\/12.4.679","article-title":"Axioms for branching time","volume":"12","author":"Reynolds","year":"2002","journal-title":"Journal of Logic and Computation"},{"key":"10.1016\/S1570-2464(07)80014-0_bib166","doi-asserted-by":"crossref","first-page":"393","DOI":"10.1016\/S0022-0000(03)00005-9","article-title":"The complexity of the temporal logic with until over general linear time","volume":"66","author":"Reynolds","year":"2003","journal-title":"Journal of Computer and System Sciences"},{"key":"10.1016\/S1570-2464(07)80014-0_bib167","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1016\/j.ic.2005.03.005","article-title":"An axiomatization of PCTL*","volume":"201","author":"Reynolds","year":"2005","journal-title":"Information and Computation"},{"unstructured":"[168] M. Reynolds. The complexity of the temporal logic over the reals, submitted. Version available at http:\/\/www.csse.uwa.edu.au\/~mark\/research\/Online\/CORT.","key":"10.1016\/S1570-2464(07)80014-0_bib168"},{"year":"2003","series-title":"Proc. TIME-ICTL.","key":"10.1016\/S1570-2464(07)80014-0_bib169"},{"issue":"1","key":"10.1016\/S1570-2464(07)80014-0_bib170","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1145\/321250.321253","article-title":"A Machine-Oriented Logic Based on the Resolution Principle","volume":"12","author":"Robinson","year":"1965","journal-title":"Journal of the ACM"},{"year":"1982","author":"Rosenstein","series-title":"Linear orderings","key":"10.1016\/S1570-2464(07)80014-0_bib171"},{"key":"10.1016\/S1570-2464(07)80014-0_bib172","series-title":"First Annual IEEE Symposium on Logic in Computer Science LICS'86","first-page":"306","article-title":"A choppy logic","author":"Rosner","year":"1986"},{"key":"10.1016\/S1570-2464(07)80014-0_bib173","series-title":"Proceedings of the Third Scandinavian Logic Symposium, Uppsala, 1973","first-page":"110","article-title":"Completeness and correspondence in the first and second order semantics for modal logic","author":"Sahlqvist","year":"1975"},{"key":"10.1016\/S1570-2464(07)80014-0_bib174","doi-asserted-by":"crossref","first-page":"992","DOI":"10.2307\/2274758","article-title":"A new proof of Sahlqvist's theorem on modal definability and complete-ness","volume":"54","author":"Sambin","year":"1989","journal-title":"J. Symbolic Logic"},{"key":"10.1016\/S1570-2464(07)80014-0_bib175","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1080\/11663081.1992.10510780","article-title":"Expressive completeness of temporal logic over trees","volume":"2","author":"Schlingloff","year":"1992","journal-title":"Journal of Applied Non-classical Logics"},{"key":"10.1016\/S1570-2464(07)80014-0_bib176","series-title":"Pro- ceedings of Tableaux 98, volume 1397 of Lecture Notes in Artificial Intelligence","first-page":"277","article-title":"A New One-Pass Tableau Calculus for PLTL","author":"Schwendimann","year":"1998"},{"key":"10.1016\/S1570-2464(07)80014-0_bib177","doi-asserted-by":"crossref","first-page":"301","DOI":"10.1111\/j.1755-2567.1970.tb00429.x","article-title":"Modal logics with linear alternative relations","volume":"36","author":"Segerberg","year":"1970","journal-title":"Theoria"},{"key":"10.1016\/S1570-2464(07)80014-0_bib178","article-title":"An essay in classical modal logic","volume":"13","author":"Segerberg","year":"1971"},{"key":"10.1016\/S1570-2464(07)80014-0_bib179","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1007\/BF01418760","article-title":"Modal logics of domains on the real plane","volume":"42","author":"Shehtman","year":"1983","journal-title":"Studia Logica"},{"key":"10.1016\/S1570-2464(07)80014-0_bib180","doi-asserted-by":"crossref","first-page":"379","DOI":"10.2307\/1971037","article-title":"The monadic theory of order","volume":"102","author":"Shelah","year":"1975","journal-title":"Annals of Mathematics"},{"key":"10.1016\/S1570-2464(07)80014-0_bib181","doi-asserted-by":"crossref","first-page":"825","DOI":"10.1137\/0213051","article-title":"Is the interesting part of process logic uninteresting: a trans-lation from PL to PDL","volume":"13","author":"Sherman","year":"1984","journal-title":"SIAM J. on Computing"},{"key":"10.1016\/S1570-2464(07)80014-0_bib182","first-page":"57","article-title":"Cut-free systems for the modal logic S4.3 S4.3 GRZ","volume":"25","author":"Shimura","year":"1991","journal-title":"Reports on Mathematical Logic"},{"key":"10.1016\/S1570-2464(07)80014-0_bib183","doi-asserted-by":"crossref","first-page":"733","DOI":"10.1145\/3828.3837","article-title":"The complexity of propositional linear temporal logics","volume":"32","author":"Sistla","year":"1985","journal-title":"J. ACM"},{"key":"10.1016\/S1570-2464(07)80014-0_bib184","series-title":"Handbook of Logic in Computer Science, volume 2 (Background: Computational Structures)","first-page":"477","article-title":"Modal and temporal logics","author":"Stirling","year":"1992"},{"key":"10.1016\/S1570-2464(07)80014-0_bib185","series-title":"Project MAC Tech. Report 133","article-title":"The complexity of decision problems in automata theory and logic","author":"Stockmeyer","year":"1974"},{"key":"10.1016\/S1570-2464(07)80014-0_bib186","series-title":"Handbook of Philosophical Logic, volume 1","first-page":"133","article-title":"Systems of deduction","author":"Sundholm","year":"1983"},{"year":"1993","series-title":"Temporal Databases: Theory, Design and Implementation","key":"10.1016\/S1570-2464(07)80014-0_bib187"},{"key":"10.1016\/S1570-2464(07)80014-0_bib188","series-title":"Handbook of Philosophical Logic, Vol II: Extensions of Classical Logic","first-page":"135","article-title":"Combinations of tense and modality","author":"Thomason","year":"1984"},{"doi-asserted-by":"crossref","unstructured":"D. Toman. On incompleteness of multi-dimensional first-order temporal logics. In Reynolds and Sattar [169], pages 99-106.","key":"10.1016\/S1570-2464(07)80014-0_bib189","DOI":"10.1109\/TIME.2003.1214885"},{"key":"10.1016\/S1570-2464(07)80014-0_bib190","series-title":"Advances in Database Technology EDBT'96, volume 1057 of Lecture Notes in Computer Science","first-page":"307","article-title":"First-order queries over temporal databases inexpressible in first-order logic","author":"Toman","year":"1996"},{"year":"1983","author":"van Benthem","series-title":"The Logic of Time","key":"10.1016\/S1570-2464(07)80014-0_bib191"},{"key":"10.1016\/S1570-2464(07)80014-0_bib192","series-title":"Hand- book of Logic in Artificial Intelligence and Logic Programming: Epistemic and Temporal Reasoning, volume 4","first-page":"241","article-title":"Temporal logic","author":"van Benthem","year":"1995"},{"key":"10.1016\/S1570-2464(07)80014-0_bib193","series-title":"Logics of Programs, volume 164 of LNCS","first-page":"501","article-title":"Yet another process logic","author":"Vardi","year":"1984"},{"key":"10.1016\/S1570-2464(07)80014-0_bib194","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1006\/inco.1994.1092","article-title":"Reasoning about infinite computations","volume":"115","author":"Vardi","year":"1994","journal-title":"Information and Computation"},{"key":"10.1016\/S1570-2464(07)80014-0_bib195","doi-asserted-by":"crossref","first-page":"529","DOI":"10.1305\/ndjfl\/1093635589","article-title":"Expressiveness and completeness of an interval tense logic","volume":"31","author":"Venema","year":"1990","journal-title":"Notre Dame J. Formal Logic"},{"issue":"4","key":"10.1016\/S1570-2464(07)80014-0_bib196","doi-asserted-by":"crossref","first-page":"453","DOI":"10.1093\/logcom\/1.4.453","article-title":"A modal logic for chopping intervals","volume":"1","author":"Venema","year":"1991","journal-title":"Journal of Logic and Computation"},{"key":"10.1016\/S1570-2464(07)80014-0_bib197","series-title":"Algebraic logic, volume 54 of Colloq. Math. Soc. J. Bolyai","first-page":"695","article-title":"Relational games","author":"Venema","year":"1991"},{"key":"10.1016\/S1570-2464(07)80014-0_bib198","series-title":"Diamonds and Defaults","first-page":"349","article-title":"Completeness by completeness: Since and Until","author":"Venema","year":"1993"},{"key":"10.1016\/S1570-2464(07)80014-0_bib199","series-title":"The Blackwell Guide to Philosophical Logic","first-page":"203","article-title":"Temporal logic","author":"Venema","year":"2001"},{"key":"10.1016\/S1570-2464(07)80014-0_bib200","series-title":"Logic at Work: Essays Dedicated to the Memory of Helena Rasiowa","first-page":"124","article-title":"A modal logic of relations","author":"Venema","year":"1999"},{"key":"10.1016\/S1570-2464(07)80014-0_bib201","series-title":"Proceedings 5th Foundations of Software Technologies and Theoretical Computer Science Conference 1985, volume 206 of Lecture Notes in Computer Science","first-page":"272","article-title":"A Decision Method for Temporal Logic based on Resolution","author":"Venkatesh","year":"1986"},{"year":"1999","author":"Wansing","series-title":"Displaying Modal Logics","key":"10.1016\/S1570-2464(07)80014-0_bib202"},{"key":"10.1016\/S1570-2464(07)80014-0_bib203","series-title":"Ninth Symp on Principles of Programming Languages","first-page":"20","article-title":"Specification and synthesis of communicating processes using an extended temporal logic","author":"Wolper","year":"1982"},{"year":"1982","author":"Wolper","article-title":"Synthesis of communicating processes from temporal logic specifications","key":"10.1016\/S1570-2464(07)80014-0_bib204"},{"issue":"1\u20132","key":"10.1016\/S1570-2464(07)80014-0_bib205","first-page":"72","article-title":"Temporal logic can be more expressive","volume":"56","author":"Wolper","year":"1983","journal-title":"Information and Computation"},{"key":"10.1016\/S1570-2464(07)80014-0_bib206","first-page":"110","article-title":"The tableau method for temporal logic: an overview","volume":"28","author":"Wolper","year":"1985","journal-title":"Logique et Analyse"},{"key":"10.1016\/S1570-2464(07)80014-0_bib207","series-title":"Proc. 24th ACM Symp. on Foundations of Comp. Sci.","first-page":"185","article-title":"Reasoning about infinite computation paths","author":"Wolper","year":"1983"},{"key":"10.1016\/S1570-2464(07)80014-0_bib208","doi-asserted-by":"crossref","first-page":"757","DOI":"10.2307\/2275755","article-title":"The finite model property in tense logic","volume":"60","author":"Wolter","year":"1995","journal-title":"Journal of Symbolic Logic"},{"key":"10.1016\/S1570-2464(07)80014-0_bib209","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1305\/ndjfl\/1040046085","article-title":"A counterexample in tense logic","volume":"37","author":"Wolter","year":"1996","journal-title":"Notre Dame Journal of Formal Logic"},{"key":"10.1016\/S1570-2464(07)80014-0_bib210","doi-asserted-by":"crossref","first-page":"481","DOI":"10.1002\/malq.19960420140","article-title":"Properties of tense logics","volume":"42","author":"Wolter","year":"1996","journal-title":"Mathematical Logic Quarterly"},{"key":"10.1016\/S1570-2464(07)80014-0_bib211","doi-asserted-by":"crossref","first-page":"145","DOI":"10.1002\/malq.19960420113","article-title":"Tense logic without tense operators","volume":"42","author":"Wolter","year":"1996","journal-title":"Mathematical Logic Quarterly"},{"key":"10.1016\/S1570-2464(07)80014-0_bib212","doi-asserted-by":"crossref","first-page":"131","DOI":"10.2307\/2275736","article-title":"Completeness and decidability of tense logics closely related to logics above","volume":"62","author":"Wolter","year":"1997","journal-title":"K4. Journal of Symbolic Logic"},{"key":"10.1016\/S1570-2464(07)80014-0_bib213","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1016\/S0168-0072(01)00124-5","article-title":"Axiomatizing the monodic fragment of first-order temporal logic","volume":"118","author":"Wolter","year":"2002","journal-title":"Ann. Pure. Appl. Logic"},{"key":"10.1016\/S1570-2464(07)80014-0_bib214","first-page":"181","article-title":"On some U, S-tenselogics","volume":"17","author":"Ming","year":"1988","journal-title":"J. of Philosophical Logic"},{"key":"10.1016\/S1570-2464(07)80014-0_bib215","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1007\/BF00935598","article-title":"Axiomatization of'Peircean' branching-time logic","volume":"49","author":"Zanardo","year":"1990","journal-title":"Studia Logica"},{"key":"10.1016\/S1570-2464(07)80014-0_bib216","doi-asserted-by":"crossref","DOI":"10.1007\/BF00284972","article-title":"A complete deductive system for Since-Until branching time logic","author":"Zanardo","year":"1991","journal-title":"J. Philosophical Logic"},{"key":"10.1016\/S1570-2464(07)80014-0_bib217","doi-asserted-by":"crossref","first-page":"1","DOI":"10.2307\/2275595","article-title":"Branching-time logic with quantification over branches: the point of view of modal logic","volume":"61","author":"Zanardo","year":"1996","journal-title":"J. Symbolic Logic"},{"year":"2003","author":"Zanardo","article-title":"First-order and second-order aspects of branching-time semantics","key":"10.1016\/S1570-2464(07)80014-0_bib218_1"},{"year":"2002","article-title":"Dipartimento di Matematica Universita di Padova, 2003","series-title":"HPLMC (2nd Internat. Workshop on the History and Philosophy of Logic, Mathematics and Computation, Donostia \u2014 San Sebastian (Spain), 7-9 November 2002)","key":"10.1016\/S1570-2464(07)80014-0_bib218_2"},{"year":"2004","author":"Zhou","article-title":"A Formal Approach to Real-Time Systems","key":"10.1016\/S1570-2464(07)80014-0_bib219"},{"issue":"5","key":"10.1016\/S1570-2464(07)80014-0_bib220","doi-asserted-by":"crossref","first-page":"269","DOI":"10.1016\/0020-0190(91)90122-X","article-title":"A calculus of durations","volume":"40","author":"Zhou","year":"1991","journal-title":"Information Processing Letters"}],"container-title":["Studies in Logic and Practical Reasoning","Handbook of Modal Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1570246407800140?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1570246407800140?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T23:17:42Z","timestamp":1761607062000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1570246407800140"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007]]},"ISBN":["9780444516909"],"references-count":223,"URL":"https:\/\/doi.org\/10.1016\/s1570-2464(07)80014-0","relation":{},"ISSN":["1570-2464"],"issn-type":[{"type":"print","value":"1570-2464"}],"subject":[],"published":{"date-parts":[[2007]]}}}