{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T21:15:48Z","timestamp":1742937348877,"version":"3.40.3"},"publisher-location":"Cham","reference-count":46,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031635007"},{"type":"electronic","value":"9783031635014"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,7,2]],"date-time":"2024-07-02T00:00:00Z","timestamp":1719878400000},"content-version":"vor","delay-in-days":183,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Our main result is a doubly exponential decision procedure for the first-order equality theory of streams with addition, convolution, and control-oriented stream operations. This stream logic is shown to be expressive for solving basic problems in stream calculus.<\/jats:p>","DOI":"10.1007\/978-3-031-63501-4_8","type":"book-chapter","created":{"date-parts":[[2024,7,1]],"date-time":"2024-07-01T09:02:00Z","timestamp":1719824520000},"page":"137-156","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["A Decision Method for\u00a0First-Order Stream Logic"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1405-2990","authenticated-orcid":false,"given":"Harald","family":"Ruess","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,7,2]]},"reference":[{"key":"8_CR1","volume-title":"Foundations of Analysis Over Surreal Number Fields","author":"NL Alling","year":"1987","unstructured":"Alling, N.L.: Foundations of Analysis Over Surreal Number Fields. Elsevier, Amsterdam (1987)"},{"key":"8_CR2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511546563","volume-title":"Automatic Sequences: Theory, Applications, Generalizations","author":"JP Allouche","year":"2003","unstructured":"Allouche, J.P., Shallit, J.: Automatic Sequences: Theory, Applications, Generalizations. Cambridge University Press, Cambridge (2003)"},{"issue":"4","key":"8_CR3","doi-asserted-by":"publisher","first-page":"1336","DOI":"10.1017\/jsl.2014.27","volume":"79","author":"W Anscombe","year":"2014","unstructured":"Anscombe, W., Koenigsmann, J.: An existential $$\\emptyset $$-definition of $${F}_{q}[[t]]$$ in $${F}_{q}((t))$$. J. Symb. Log. 79(4), 1336\u20131343 (2014)","journal-title":"J. Symb. Log."},{"key":"8_CR4","doi-asserted-by":"crossref","unstructured":"Ax, J.: On the undecidability of power series fields. In: Proceedings of the American Mathematical Society, vol. 16, no. 846, p. 4 (1965)","DOI":"10.2307\/2033940"},{"issue":"6","key":"8_CR5","doi-asserted-by":"publisher","first-page":"1002","DOI":"10.1145\/235809.235813","volume":"43","author":"S Basu","year":"1996","unstructured":"Basu, S., Pollack, R., Roy, M.F.: On the combinatorial and algebraic complexity of quantifier elimination. J. ACM (JACM) 43(6), 1002\u20131045 (1996)","journal-title":"J. ACM (JACM)"},{"key":"8_CR6","unstructured":"Bourbaki, N.: El\u00e9ments de Math\u00e9matiques, vol. Livre II, Alg\u00e8bre, chap. 6, Groupes et corps ordonn\u00e9s. Hermann, Paris (1964)"},{"issue":"114106","key":"8_CR7","first-page":"1","volume":"974","author":"M Broy","year":"2023","unstructured":"Broy, M.: Specification and verification of concurrent systems by causality and realizability. Theoret. Comput. Sci. 974(114106), 1\u201361 (2023)","journal-title":"Theoret. Comput. Sci."},{"key":"8_CR8","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4613-0091-5","volume-title":"Specification and Development of Interactive Systems: Focus on Streams, Interfaces, and Refinement","author":"M Broy","year":"2012","unstructured":"Broy, M., St\u00f8len, K.: Specification and Development of Interactive Systems: Focus on Streams, Interfaces, and Refinement. Springer, New York (2012). https:\/\/doi.org\/10.1007\/978-1-4613-0091-5"},{"issue":"2","key":"8_CR9","doi-asserted-by":"publisher","first-page":"166","DOI":"10.2307\/2271090","volume":"34","author":"JR Buchi","year":"1969","unstructured":"Buchi, J.R., Landweber, L.H.: Definability in the monadic second-order theory of successor. J. Symb. Log. 34(2), 166\u2013170 (1969)","journal-title":"J. Symb. Log."},{"issue":"1","key":"8_CR10","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1147\/rd.191.0012","volume":"19","author":"WH Burge","year":"1975","unstructured":"Burge, W.H.: Stream processing functions. IBM J. Res. Dev. 19(1), 12\u201325 (1975)","journal-title":"IBM J. Res. Dev."},{"key":"8_CR11","doi-asserted-by":"publisher","DOI":"10.1201\/9781315273112","volume-title":"Enumerative Combinatorics","author":"CA Charalambides","year":"2018","unstructured":"Charalambides, C.A.: Enumerative Combinatorics. Chapman and Hall\/CRC, Boca Raton (2018)"},{"key":"8_CR12","doi-asserted-by":"crossref","unstructured":"Cherlin, G., Dickmann, M.A.: Real closed rings II. Model theory. Ann. Pure Appl. Logic 25(3), 213\u2013231 (1983)","DOI":"10.1016\/0168-0072(83)90019-2"},{"key":"8_CR13","doi-asserted-by":"publisher","first-page":"401","DOI":"10.24033\/bsmf.1926","volume":"108","author":"G Christol","year":"1980","unstructured":"Christol, G., Kamae, T., Mend\u00e8s France, M., Rauzy, G.: Suites alg\u00e9briques, automates et substitutions. Bull. Soc. Math. France 108, 401\u2013419 (1980)","journal-title":"Bull. Soc. Math. France"},{"issue":"6","key":"8_CR14","doi-asserted-by":"publisher","first-page":"1157","DOI":"10.3233\/JCS-2009-0393","volume":"18","author":"MR Clarkson","year":"2010","unstructured":"Clarkson, M.R., Schneider, F.B.: Hyperproperties. J. Comput. Secur. 18(6), 1157\u20131210 (2010)","journal-title":"J. Comput. Secur."},{"issue":"12","key":"8_CR15","doi-asserted-by":"publisher","first-page":"1236","DOI":"10.1016\/j.apal.2013.06.010","volume":"164","author":"R Cluckers","year":"2013","unstructured":"Cluckers, R., Derakhshan, J., Leenknegt, E., Macintyre, A.: Uniformly defining valuation rings in henselian valued fields with finite or pseudo-finite residue fields. Ann. Pure Appl. Logic 164(12), 1236\u20131246 (2013)","journal-title":"Ann. Pure Appl. Logic"},{"issue":"2","key":"8_CR16","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1002\/cpa.3160220202","volume":"22","author":"PJ Cohen","year":"1969","unstructured":"Cohen, P.J.: Decision procedures for real and p-adic fields. Commun. Pure Appl. Math. 22(2), 131\u2013151 (1969)","journal-title":"Commun. Pure Appl. Math."},{"key":"8_CR17","doi-asserted-by":"crossref","unstructured":"Cola\u00e7o, J.L., Pagano, B., Pouzet, M.: Scade 6: a formal language for embedded critical software development. In: 2017 International Symposium on Theoretical Aspects of Software Engineering (TASE), pp. 1\u201311. IEEE (2017)","DOI":"10.1109\/TASE.2017.8285623"},{"key":"8_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/3-540-07407-4_17","volume-title":"Automata Theory and Formal Languages","author":"GE Collins","year":"1975","unstructured":"Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decompostion. In: Brakhage, H. (ed.) GI-Fachtagung 1975. LNCS, vol. 33, pp. 134\u2013183. Springer, Heidelberg (1975). https:\/\/doi.org\/10.1007\/3-540-07407-4_17"},{"key":"8_CR19","doi-asserted-by":"crossref","unstructured":"Courcelle, B., Engelfriet, J.: Graph Structure and Monadic Second-order Logic: A Language-Theoretic Approach, vol.\u00a0138. Cambridge University Press, Cambridge (2012)","DOI":"10.1017\/CBO9780511977619"},{"issue":"1\u20132","key":"8_CR20","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1016\/S0747-7171(88)80004-X","volume":"5","author":"JH Davenport","year":"1988","unstructured":"Davenport, J.H., Heintz, J.: Real quantifier elimination is doubly exponential. J. Symb. Comput. 5(1\u20132), 29\u201335 (1988)","journal-title":"J. Symb. Comput."},{"issue":"1","key":"8_CR21","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1017\/jsl.2014.13","volume":"80","author":"A Fehm","year":"2015","unstructured":"Fehm, A.: Existential $$\\emptyset $$-definability of henselian valuation rings. J. Symb. Log. 80(1), 301\u2013307 (2015)","journal-title":"J. Symb. Log."},{"key":"8_CR22","doi-asserted-by":"crossref","unstructured":"Goguen, J.A., Meseguer, J.: Security policies and security models. In: 1982 IEEE Symposium on Security and Privacy, p. 11. IEEE (1982)","DOI":"10.1109\/SP.1982.10014"},{"key":"8_CR23","volume-title":"A Shorter Model Theory","author":"W Hodges","year":"1997","unstructured":"Hodges, W.: A Shorter Model Theory. Cambridge University Press, Cambridge (1997)"},{"issue":"3\/4","key":"8_CR24","doi-asserted-by":"publisher","first-page":"104","DOI":"10.1145\/2429135.2429155","volume":"46","author":"D Jovanovi\u0107","year":"2013","unstructured":"Jovanovi\u0107, D., De Moura, L.: Solving non-linear arithmetic. ACM Commun. Comput. Algebra 46(3\/4), 104\u2013105 (2013)","journal-title":"ACM Commun. Comput. Algebra"},{"key":"8_CR25","first-page":"471","volume":"74","author":"G Kahn","year":"1974","unstructured":"Kahn, G.: The semantics of a simple language for parallel programming. Inf. Process. 74, 471\u2013475 (1974)","journal-title":"Inf. Process."},{"key":"8_CR26","unstructured":"Kahn, G., MacQueen, D.: Coroutines and networks of parallel processes. Research Report INRIA-00306565 (1976)"},{"issue":"04","key":"8_CR27","doi-asserted-by":"publisher","first-page":"571","DOI":"10.1142\/S012905410200128X","volume":"13","author":"N Klarlund","year":"2002","unstructured":"Klarlund, N., M\u00f8ller, A., Schwartzbach, M.I.: Mona implementation secrets. Int. J. Found. Comput. Sci. 13(04), 571\u2013586 (2002)","journal-title":"Int. J. Found. Comput. Sci."},{"issue":"7","key":"8_CR28","doi-asserted-by":"publisher","first-page":"2235","DOI":"10.1090\/S0002-9939-02-06753-9","volume":"131","author":"M Laczkovich","year":"2003","unstructured":"Laczkovich, M.: The removal of $$\\pi $$ from some undecidable problems involving elementary functions. Proc. Am. Math. Soc. 131(7), 2235\u20132240 (2003)","journal-title":"Proc. Am. Math. Soc."},{"key":"8_CR29","doi-asserted-by":"crossref","unstructured":"McCullough, D.: Noninterference and the composability of security properties. In: Proceedings 1988 IEEE Symposium on Security and Privacy, p. 177. IEEE Computer Society (1988)","DOI":"10.1109\/SECPRI.1988.8110"},{"key":"8_CR30","doi-asserted-by":"crossref","unstructured":"McLean, J.: A general theory of composition for trace sets closed under selective interleaving functions. In: Proceedings of 1994 IEEE Computer Society Symposium on Research in Security and Privacy, pp. 79\u201393. IEEE (1994)","DOI":"10.1109\/RISP.1994.296590"},{"key":"8_CR31","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-03983-0","volume-title":"Algebraic Number Theory","author":"J Neukirch","year":"2013","unstructured":"Neukirch, J.: Algebraic Number Theory, vol. 322. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-662-03983-0"},{"issue":"8","key":"8_CR32","doi-asserted-by":"publisher","first-page":"871","DOI":"10.1080\/00029890.1969.12000359","volume":"76","author":"I Niven","year":"1969","unstructured":"Niven, I.: Formal power series. Am. Math. Mon. 76(8), 871\u2013889 (1969)","journal-title":"Am. Math. Mon."},{"key":"8_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"548","DOI":"10.1007\/10722167_42","volume-title":"Computer Aided Verification","author":"S Owre","year":"2000","unstructured":"Owre, S., Rue\u00df, H.: Integrating WS1S with PVS. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 548\u2013551. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/10722167_42"},{"key":"8_CR34","unstructured":"Pradic, P.: Some proof-theoretical approaches to Monadic Second-Order logic. Ph.D. thesis, Universit\u00e9 de Lyon; Uniwersytet Warszawski. Wydzia\u0142 Matematyki, Informatyki (2020)"},{"issue":"4","key":"8_CR35","doi-asserted-by":"publisher","first-page":"1260","DOI":"10.1017\/jsl.2014.52","volume":"80","author":"A Prestel","year":"2015","unstructured":"Prestel, A.: Definable henselian valuation rings. J. Symb. Log. 80(4), 1260\u20131267 (2015)","journal-title":"J. Symb. Log."},{"key":"8_CR36","doi-asserted-by":"crossref","unstructured":"Richardson, D., Fitch, J.: The identity problem for elementary functions and constants. In: Proceedings of the International Symposium on Symbolic and Algebraic Computation, pp. 285\u2013290 (1994)","DOI":"10.1145\/190347.190429"},{"key":"8_CR37","unstructured":"Rutten, J.: On streams and coinduction. Technical report, CWI (2002)"},{"key":"8_CR38","unstructured":"Rutten, J.: The Method of Coalgebra: exercises in coinduction, vol. ISBN 978-90-6196-568-8. CWI, Amsterdam (2019)"},{"key":"8_CR39","doi-asserted-by":"publisher","first-page":"358","DOI":"10.1016\/S1571-0661(04)80972-1","volume":"45","author":"JJ Rutten","year":"2001","unstructured":"Rutten, J.J.: Elements of stream calculus: an extensive exercise in coinduction. Electron. Notes Theor. Comput. Sci. 45, 358\u2013423 (2001)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"8_CR40","doi-asserted-by":"crossref","unstructured":"Rutten, J.J.: Rational streams coalgebraically. Log. Methods Comput. Sci. 4 (2008)","DOI":"10.2168\/LMCS-4(3:9)2008"},{"key":"8_CR41","doi-asserted-by":"crossref","unstructured":"Schechter, E.: Handbook of Analysis and Its Foundations. Academic Press, Cambridge (1996)","DOI":"10.1016\/B978-012622760-4\/50002-9"},{"key":"8_CR42","doi-asserted-by":"crossref","unstructured":"Shamseddine, K., Comicheo, A.B.: On non-archimedean valued fields: a survey of algebraic, topological and metric structures, analysis and applications. In: Advances in Non-Archimedean Analysis and Applications: The p-adic Methodology in STEAM-H, pp. 209\u2013254 (2021)","DOI":"10.1007\/978-3-030-81976-7_6"},{"key":"8_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"156","DOI":"10.1007\/3-540-63475-4_4","volume-title":"Formal Hardware Verification","author":"M Srivas","year":"1997","unstructured":"Srivas, M., Rue\u00df, H., Cyrluk, D.: Hardware verification using PVS. In: Kropf, T. (ed.) Formal Hardware Verification. LNCS, vol. 1287, pp. 156\u2013205. Springer, Heidelberg (1997). https:\/\/doi.org\/10.1007\/3-540-63475-4_4"},{"key":"8_CR44","doi-asserted-by":"crossref","unstructured":"Tarski, A.: A Decision Method for Elementary Algebra and Geometry. Springer, Heidelberg (1998)","DOI":"10.1007\/978-3-7091-9459-1_3"},{"key":"8_CR45","unstructured":"van\u00a0der Waerden, B.: Algebra (1966)"},{"key":"8_CR46","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/s002000050055","volume":"8","author":"V Weispfenning","year":"1997","unstructured":"Weispfenning, V.: Quantifier elimination for real algebra-the quadratic case and beyond. Appl. Algebra Eng. Commun. Comput. 8, 85\u2013101 (1997)","journal-title":"Appl. Algebra Eng. Commun. Comput."}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-63501-4_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,23]],"date-time":"2024-11-23T04:38:34Z","timestamp":1732336714000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-63501-4_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031635007","9783031635014"],"references-count":46,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-63501-4_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"2 July 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"IJCAR","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Joint Conference on Automated Reasoning","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Nancy","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 July 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 July 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ijcar2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/merz.gitlabpages.inria.fr\/2024-ijcar\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}