{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,10]],"date-time":"2026-03-10T16:36:40Z","timestamp":1773160600548,"version":"3.50.1"},"reference-count":22,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2017,1,11]],"date-time":"2017-01-11T00:00:00Z","timestamp":1484092800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["1763"],"award-info":[{"award-number":["1763"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["GELO"],"award-info":[{"award-number":["GELO"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Theory Comput Syst"],"published-print":{"date-parts":[[2017,8]]},"DOI":"10.1007\/s00224-016-9724-y","type":"journal-article","created":{"date-parts":[[2017,1,10]],"date-time":"2017-01-10T23:27:06Z","timestamp":1484090826000},"page":"689-720","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Satisfiability of ECTL\u2217 with Local Tree Constraints"],"prefix":"10.1007","volume":"61","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5981-7515","authenticated-orcid":false,"given":"Claudia","family":"Carapelle","sequence":"first","affiliation":[]},{"given":"Shiguang","family":"Feng","sequence":"additional","affiliation":[]},{"given":"Alexander","family":"Kartzow","sequence":"additional","affiliation":[]},{"given":"Markus","family":"Lohrey","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,1,11]]},"reference":[{"key":"9724_CR1","unstructured":"Bojan\u0307czyk, M., Parys, P., Torun\u0307czyk, S.: The MSO+U theory of (N, < ) is undecidable. In: Proceedings of the 33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016), Leibniz International Proceedings in Informatics (LIPIcs), vol. 47, pp. 21:1\u201321:8. Schloss Dagstuhl\u2013Leibniz-Zentrum f\u00fcr Informatik (2016)"},{"key":"9724_CR2","unstructured":"Boja\u0144czyk, M., Toru\u0144czyk, S.: Weak MSO+U over infinite trees (long version). http:\/\/www.mimuw.edu.pl\/bojan\/papers\/wmsou-trees"},{"key":"9724_CR3","unstructured":"Boja\u0144czyk, M., Toru\u0144czyk, S.: Weak MSO+U over infinite trees. In: Proceedings of the 29th International Symposium on Theoretical Aspects of Computer Science (STACS 2012), Leibniz International Proceedings in Informatics (LIPIcs), vol. 14, pp. 648\u2013660. Schloss Dagstuhl\u2013Leibniz-Zentrum f\u00fcr Informatik (2012)"},{"key":"9724_CR4","doi-asserted-by":"crossref","unstructured":"Bozzelli, L., Gascon, R.: Branching-time temporal logic extended with qualitative presburger constraints. In: Proceedings of the 13th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2006), Lecture Notes in Computer Science, vol. 4246, pp. 197\u2013211. Springer (2006)","DOI":"10.1007\/11916277_14"},{"key":"9724_CR5","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/j.tcs.2013.12.002","volume":"523","author":"L Bozzelli","year":"2014","unstructured":"Bozzelli, L., Pinchinat, S.: Verification of gap-order constraint abstractions of counter systems. Theor. Comput. Sci. 523, 1\u201336 (2014)","journal-title":"Theor. Comput. Sci."},{"key":"9724_CR6","doi-asserted-by":"crossref","unstructured":"Carapelle, C., Feng, S., Kartzow, A., Lohrey, M.: Satisfiability of ECTL* with Tree Constraints. In: Proceedings of the 10th International Computer Science Symposium in Russia (CSR 2015), Lecture Notes in Computer Science, vol. 9139, pp. 94\u2013108. Springer (2015)","DOI":"10.1007\/978-3-319-20297-6_7"},{"key":"9724_CR7","doi-asserted-by":"crossref","unstructured":"Carapelle, C., Kartzow, A., Lohrey, M.: Satisfiability of CTL* with Constraints. In: Proceedings of the 24th International Conference on Concurrency Theory (CONCUR 2013), Lecture Notes in Computer Science, vol. 8052, pp. 455\u2013469. Springer (2013)","DOI":"10.1007\/978-3-642-40184-8_32"},{"issue":"5","key":"9724_CR8","doi-asserted-by":"crossref","first-page":"826","DOI":"10.1016\/j.jcss.2016.02.002","volume":"82","author":"C Carapelle","year":"2016","unstructured":"Carapelle, C., Kartzow, A., Lohrey, M.: Satisfiability of ECTL\u2217 with constraints. J. Comput. Syst. Sci. 82 (5), 826\u2013855 (2016). http:\/\/www.sciencedirect.com\/science\/article\/pii\/S002200001600012X","journal-title":"J. Comput. Syst. Sci."},{"issue":"3","key":"9724_CR9","doi-asserted-by":"publisher","first-page":"989","DOI":"10.1093\/logcom\/exv028","volume":"26","author":"S Demri","year":"2016","unstructured":"Demri, S., Deters, M.: Temporal logics on strings with prefix relation. J. Log. Comput. 26(3), 989\u20131017 (2016). doi: 10.1093\/logcom\/exv028 http:\/\/logcom.oxfordjournals.org\/content\/26\/3\/989","journal-title":"J. Log. Comput."},{"issue":"3","key":"9724_CR10","doi-asserted-by":"crossref","first-page":"380","DOI":"10.1016\/j.ic.2006.09.006","volume":"205","author":"S Demri","year":"2007","unstructured":"Demri, S., D\u2019Souza, D.: An automata-theoretic approach to constraint LTL. Inf. Comput. 205(3), 380\u2013415 (2007)","journal-title":"Inf. Comput."},{"issue":"1","key":"9724_CR11","doi-asserted-by":"crossref","first-page":"24","DOI":"10.1016\/j.tcs.2008.07.023","volume":"409","author":"S Demri","year":"2008","unstructured":"Demri, S., Gascon, R.: Verification of qualitative Z constraints. Theor. Comput. Sci. 409(1), 24\u201340 (2008)","journal-title":"Theor. Comput. Sci."},{"issue":"3","key":"9724_CR12","doi-asserted-by":"crossref","first-page":"16:1","DOI":"10.1145\/1507244.1507246","volume":"10","author":"S Demri","year":"2009","unstructured":"Demri, S., Lazi\u0107, R.: LTL with the freeze quantifier and register automata. ACM Trans. Comput. Log. 10(3), 16:1\u201316:30 (2009)","journal-title":"ACM Trans. Comput. Log."},{"issue":"3","key":"9724_CR13","doi-asserted-by":"crossref","first-page":"517","DOI":"10.1112\/plms\/s3-54.3.517","volume":"54","author":"M Droste","year":"1987","unstructured":"Droste, M.: Partially ordered sets with transitive automorphism groups. Proc. Lond. Math. Soc. 54(3), 517\u2013543 (1987)","journal-title":"Proc. Lond. Math. Soc."},{"key":"9724_CR14","unstructured":"Ebbinghaus, H., Flum, J.: Finite Model Theory. Springer Monographs in Mathematics. Springer Berlin Heidelberg (2005)"},{"key":"9724_CR15","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1016\/j.entcs.2009.05.040","volume":"239","author":"R Gascon","year":"2009","unstructured":"Gascon, R.: An automata-based approach for CTL* with constraints. Electron. Notes Theor. Comput. Sci. 239, 193\u2013211 (2009)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"9724_CR16","first-page":"172","volume":"2","author":"WH Gottschalk","year":"1951","unstructured":"Gottschalk, W.H.: Choice functions and Tychonoff\u2019s theorem. Proc. Am. Math. Soc. 2, 172 (1951)","journal-title":"Proc. Am. Math. Soc."},{"key":"9724_CR17","doi-asserted-by":"crossref","first-page":"337","DOI":"10.4153\/CJM-1949-031-1","volume":"1","author":"R Rado","year":"1949","unstructured":"Rado, R.: Axiomatic treatment of rank in infinite sets. Can. J. Math. 1, 337\u2013343 (1949)","journal-title":"Can. J. Math."},{"key":"9724_CR18","doi-asserted-by":"crossref","unstructured":"Thomas, W.: Computation tree logic and regular omega-languages. In: REX Workshop, pp. 690\u2013713 (1988)","DOI":"10.1007\/BFb0013041"},{"key":"9724_CR19","doi-asserted-by":"crossref","unstructured":"Thomas, W.: Languages, automata, and logic. In: Handbook of Formal Languages, pp. 389\u2013455. Springer (1996)","DOI":"10.1007\/978-3-642-59126-6_7"},{"key":"9724_CR20","doi-asserted-by":"crossref","unstructured":"Vardi, M.Y., Wolper, P.: Yet another process logic (preliminary version). In: Logic of Programs, pp. 501\u2013512 (1983)","DOI":"10.1007\/3-540-12896-4_383"},{"issue":"5","key":"9724_CR21","doi-asserted-by":"crossref","first-page":"789","DOI":"10.1090\/S0002-9939-1962-0172273-0","volume":"13","author":"ES Wolk","year":"1962","unstructured":"Wolk, E.S.: The comparability graph of a tree. Proc. Am. Math. Soc. 13(5), 789\u2013795 (1962)","journal-title":"Proc. Am. Math. Soc."},{"issue":"1","key":"9724_CR22","first-page":"17","volume":"16","author":"ES Wolk","year":"1965","unstructured":"Wolk, E.S.: A note on The comparability graph of a tree. Proc. Am. Math. Soc. 16(1), 17\u201320 (1965)","journal-title":"Proc. Am. Math. Soc."}],"container-title":["Theory of Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00224-016-9724-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00224-016-9724-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00224-016-9724-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,17]],"date-time":"2019-09-17T07:08:24Z","timestamp":1568704104000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00224-016-9724-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,1,11]]},"references-count":22,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2017,8]]}},"alternative-id":["9724"],"URL":"https:\/\/doi.org\/10.1007\/s00224-016-9724-y","relation":{},"ISSN":["1432-4350","1433-0490"],"issn-type":[{"value":"1432-4350","type":"print"},{"value":"1433-0490","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,1,11]]}}}