Abstract
Temporal stream logic (TSL) extends LTL with updates and predicates over arbitrary function terms. This allows for specifying data-intensive systems for which LTL is not expressive enough. In the semantics of TSL, functions and predicates are left uninterpreted. In this paper, we extend TSL with first-order theories, enabling us to specify systems using interpreted functions and predicates such as incrementation or equality. We investigate the satisfiability problem of TSL modulo the standard underlying theory of uninterpreted functions as well as with respect to Presburger arithmetic and the theory of equality: For all three theories, TSL satisfiability is neither semi-decidable nor co-semi-decidable. Nevertheless, we identify three fragments of TSL for which the satisfiability problem is (semi-)decidable in the theory of uninterpreted functions. Despite the undecidability, we present an algorithm – which is not guaranteed to terminate – for checking the satisfiability of a TSL formula in the theory of uninterpreted functions and evaluate it: It scales well and is able to validate assumptions in a real-world system design.
This work was partially supported by the German Research Foundation (DFG) as part of the Collaborative Research Center “Foundations of Perspicuous Software Systems” (TRR 248, 389792660), and by the European Research Council (ERC) Grant OSARES (No. 683300). Philippe Heim and Noemi Passing carried out this work as PhD candidates at Saarland University, Germany.
Chapter PDF
Similar content being viewed by others
References
D’Antoni, L., Ferreira, T., Sammartino, M., Silva, A.: Symbolic Register Automata. In: Dillig, I., Tasiran, S. (eds.) Computer Aided Verification - 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part I. Lecture Notes in Computer Science, vol. 11561, pp. 3–21. Springer (2019), https://doi.org/10.1007/978-3-030-25540-4_1
D’Antoni, L., Veanes, M.: The Power of Symbolic Automata and Transducers. In: Majumdar, R., Kuncak, V. (eds.) Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I. Lecture Notes in Computer Science, vol. 10426, pp. 47–67. Springer (2017), https://doi.org/10.1007/978-3-319-63387-9_3
D’Antoni, L., Veanes, M.: Automata modulo Theories. Commun. ACM 64(5), 86–95 (2021), https://doi.org/10.1145/3419404
Demri, S.: Linear-time Temporal Logics with Presburger Constraints: An Overview. J. Appl. Non Class. Logics 16(3-4), 311–348 (2006), https://doi.org/10.3166/jancl.16.311-347
Demri, S.: LTL Over Integer Periodicity Constraints. Theor. Comput. Sci. 360(1-3), 96–123 (2006), https://doi.org/10.1016/j.tcs.2006.02.019
Demri, S., D’Souza, D.: An Automata-Theoretic Approach to Constraint LTL. Inf. Comput. 205(3), 380–415 (2007), https://doi.org/10.1016/j.ic.2006.09.006
Demri, S., D’Souza, D., Gascon, R.: A Decidable Temporal Logic of Repeating Values. In: Artëmov, S.N., Nerode, A. (eds.) Logical Foundations of Computer Science, International Symposium, LFCS 2007, New York, NY, USA, June 4-7, 2007, Proceedings. Lecture Notes in Computer Science, vol. 4514, pp. 180–194. Springer (2007), https://doi.org/10.1007/978-3-540-72734-7_13
Demri, S., Lazic, R.: LTL with the Freeze Quantifier and Register Automata. In: 21th IEEE Symposium on Logic in Computer Science (LICS 2006), 12-15 August 2006, Seattle, WA, USA, Proceedings. pp. 17–26. IEEE Computer Society (2006), https://doi.org/10.1109/LICS.2006.31
Demri, S., Lazic, R., Nowak, D.: On the Freeze Quantifier in Constraint LTL: Decidability and Complexity. In: 12th International Symposium on Temporal Representation and Reasoning (TIME 2005), 23-25 June 2005, Burlington, Vermont, USA. pp. 113–121. IEEE Computer Society (2005), https://doi.org/10.1109/TIME.2005.28
Demri, S., Lazic, R., Nowak, D.: On the Freeze Quantifier in Constraint LTL: Decidability and Complexity. In: 12th International Symposium on Temporal Representation and Reasoning (TIME 2005), 23-25 June 2005, Burlington, Vermont, USA. pp. 113–121. IEEE Computer Society (2005), https://doi.org/10.1109/TIME.2005.28
Duret-Lutz, A., Lewkowicz, A., Fauchille, A., Michaud, T., Renault, E., Xu, L.: Spot 2.0 - A Framework for LTL and \(\omega \)-Automata Manipulation. In: Artho, C., Legay, A., Peled, D. (eds.) Automated Technology for Verification and Analysis - 14th International Symposium, ATVA 2016, Chiba, Japan, October 17-20, 2016, Proceedings. Lecture Notes in Computer Science, vol. 9938, pp. 122–129 (2016), https://doi.org/10.1007/978-3-319-46520-3_8
Exibard, L., Filiot, E., Reynier, P.: Synthesis of Data Word Transducers. Log. Methods Comput. Sci. 17(1) (2021), https://lmcs.episciences.org/7279
Finkbeiner, B., Heim, P., Passing, N.: Temporal Stream Logic modulo Theories. CoRR abs/2104.14988v1 (2021), https://arxiv.org/abs/2104.14988v1
Finkbeiner, B., Heim, P., Passing, N.: Temporal Stream Logic modulo Theories (Full Version). CoRR abs/2104.14988v2 (2021), https://arxiv.org/abs/2104.14988v2
Finkbeiner, B., Klein, F., Piskac, R., Santolucito, M.: Temporal Stream Logic: Synthesis Beyond the Bools. In: Dillig, I., Tasiran, S. (eds.) Computer Aided Verification - 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part I. Lecture Notes in Computer Science, vol. 11561, pp. 609–629. Springer (2019), https://doi.org/10.1007/978-3-030-25540-4_35
Fischer, M.J., Ladner, R.E.: Propositional Dynamic Logic of Regular Programs. J. Comput. Syst. Sci. 18(2), 194–211 (1979), https://doi.org/10.1016/0022-0000(79)90046-1
Geier, G., Heim, P., Klein, F., Finkbeiner, B.: Syntroids: Synthesizing a Game for FPGAs using Temporal Logic Specifications. In: 2019 Formal Methods in Computer Aided Design, FMCAD 2019, San Jose, CA, USA, October 22-25, 2019. pp. 138–146. IEEE (2019), https://doi.org/10.23919/FMCAD.2019.8894261
Harel, D.: First-Order Dynamic Logic, Lecture Notes in Computer Science, vol. 68. Springer (1979), https://doi.org/10.1007/3-540-09237-4
Harel, D., Meyer, A.R., Pratt, V.R.: Computability and Completeness in Logics of Programs (Preliminary Report). In: Hopcroft, J.E., Friedman, E.P., Harrison, M.A. (eds.) Proceedings of the 9th Annual ACM Symposium on Theory of Computing, May 4-6, 1977, Boulder, Colorado, USA. pp. 261–268. ACM (1977), https://doi.org/10.1145/800105.803416
Jacobs, S., Klein, F., Schirmer, S.: A High-level LTL Synthesis Format: TLSF v1.1. In: Piskac, R., Dimitrova, R. (eds.) Proceedings Fifth Workshop on Synthesis, SYNT@CAV 2016, Toronto, Canada, July 17-18, 2016. EPTCS, vol. 229, pp. 112–132 (2016), https://doi.org/10.4204/EPTCS.229.10
Kaminski, M., Francez, N.: Finite-Memory Automata. Theor. Comput. Sci. 134(2), 329–363 (1994), https://doi.org/10.1016/0304-3975(94)90242-9
Khalimov, A., Maderbacher, B., Bloem, R.: Bounded Synthesis of Register Transducers. In: Lahiri, S.K., Wang, C. (eds.) Automated Technology for Verification and Analysis - 16th International Symposium, ATVA 2018, Los Angeles, CA, USA, October 7-10, 2018, Proceedings. Lecture Notes in Computer Science, vol. 11138, pp. 494–510. Springer (2018), https://doi.org/10.1007/978-3-030-01090-4_29
Krogmeier, P., Mathur, U., Murali, A., Madhusudan, P., Viswanathan, M.: Decidable Synthesis of Programs with Uninterpreted Functions. In: Lahiri, S.K., Wang, C. (eds.) Computer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part II. Lecture Notes in Computer Science, vol. 12225, pp. 634–657. Springer (2020), https://doi.org/10.1007/978-3-030-53291-8_32
Lamport, L.: The Temporal Logic of Actions. ACM Trans. Program. Lang. Syst. 16(3), 872–923 (1994), https://doi.org/10.1145/177492.177726
Li, J., Zhang, L., Pu, G., Vardi, M.Y., He, J.: LTL Satisfiability Checking Revisited. In: Sánchez, C., Venable, K.B., Zimányi, E. (eds.) 2013 20th International Symposium on Temporal Representation and Reasoning, Pensacola, FL, USA, September 26-28, 2013. pp. 91–98. IEEE Computer Society (2013), https://doi.org/10.1109/TIME.2013.19
Lisitsa, A., Potapov, I.: Temporal Logic with Predicate \(\lambda \)-Abstraction. In: 12th International Symposium on Temporal Representation and Reasoning (TIME 2005), 23-25 June 2005, Burlington, Vermont, USA. pp. 147–155. IEEE Computer Society (2005), https://doi.org/10.1109/TIME.2005.34
Maderbacher, B., Bloem, R.: Reactive Synthesis Modulo Theories Using Abstraction Refinement. CoRR abs/2108.00090 (2021), https://arxiv.org/abs/2108.00090
Manna, Z., Pnueli, A.: Verification of Concurrent Programs: The Temporal Framework. In: Boyer, R.S., Moore, J.S. (eds.) The Correctness Problem in Computer Science. Academic Press, London (1981)
Mathur, U., Madhusudan, P., Viswanathan, M.: Decidable Verification of Uninterpreted Programs. Proc. ACM Program. Lang. 3(POPL), 46:1–46:29 (2019), https://doi.org/10.1145/3290359
Mathur, U., Madhusudan, P., Viswanathan, M.: What’s Decidable About Program Verification Modulo Axioms? In: Biere, A., Parker, D. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 26th International Conference, TACAS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings, Part II. Lecture Notes in Computer Science, vol. 12079, pp. 158–177. Springer (2020), https://doi.org/10.1007/978-3-030-45237-7_10
de Moura, L.M., Bjørner, N.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings. Lecture Notes in Computer Science, vol. 4963, pp. 337–340. Springer (2008), https://doi.org/10.1007/978-3-540-78800-3_24
Pnueli, A.: The Temporal Logic of Programs. In: Annual Symposium on Foundations of Computer Science, 1977. pp. 46–57. IEEE Computer Society (1977)
Pratt, V.R.: Semantical Considerations on Floyd-Hoare Logic. In: 17th Annual Symposium on Foundations of Computer Science, Houston, Texas, USA, 25-27 October 1976. pp. 109–121. IEEE Computer Society (1976), https://doi.org/10.1109/SFCS.1976.27
Pratt, V.R.: A Practical Decision Method for Propositional Dynamic Logic: Preliminary Report. In: Lipton, R.J., Burkhard, W.A., Savitch, W.J., Friedman, E.P., Aho, A.V. (eds.) Proceedings of the 10th Annual ACM Symposium on Theory of Computing, May 1-3, 1978, San Diego, California, USA. pp. 326–337. ACM (1978), https://doi.org/10.1145/800133.804362
Ramakrishna, Y.S.: On the Satisfiability Problem for Lamport’s Propositional Temporal Logic of Actions and Some of Its Extensions. Fundam. Informaticae 24(4), 387–405 (1995), https://doi.org/10.3233/FI-1995-2444
Rozier, K.Y., Vardi, M.Y.: LTL Satisfiability Checking. In: Bosnacki, D., Edelkamp, S. (eds.) Model Checking Software, 14th International SPIN Workshop, Berlin, Germany, July 1-3, 2007, Proceedings. Lecture Notes in Computer Science, vol. 4595, pp. 149–167. Springer (2007), https://doi.org/10.1007/978-3-540-73370-6_11
Sistla, A.P., Clarke, E.M.: The Complexity of Propositional Linear Temporal Logics. J. ACM 32(3), 733–749 (1985), https://doi.org/10.1145/3828.3837
Vardi, M.Y., Wolper, P.: Reasoning About Infinite Computations. Inf. Comput. 115(1), 1–37 (1994), https://doi.org/10.1006/inco.1994.1092
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Copyright information
© 2022 The Author(s)
About this paper
Cite this paper
Finkbeiner, B., Heim, P., Passing, N. (2022). Temporal Stream Logic modulo Theories. In: Bouyer, P., Schröder, L. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2022. Lecture Notes in Computer Science, vol 13242. Springer, Cham. https://doi.org/10.1007/978-3-030-99253-8_17
Download citation
DOI: https://doi.org/10.1007/978-3-030-99253-8_17
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-99252-1
Online ISBN: 978-3-030-99253-8
eBook Packages: Computer ScienceComputer Science (R0)