Document Open Access Logo

Verifying Quantitative Temporal Properties of Procedural Programs

Authors Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, Prakash Saivasan

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2018.15.pdf
  • Filesize: 0.49 MB
  • 17 pages

Document Identifiers

Author Details

Mohamed Faouzi Atig
  • Uppsala University, Sweden
Ahmed Bouajjani
  • IRIF, Paris Diderot University, France
K. Narayan Kumar
  • Chennai Mathematical Institute and UMI RELAX, India
Prakash Saivasan
  • TU Braunschweig, Germany

Funding

  • Bouajjani, Ahmed: Partially supported by Indo-French project AVeCSo
  • Narayan Kumar, K.: Partially supported by Indo-French project AVeCSo, Infosys Foundation, DST-VR Project P-02/2014

Cite As Get BibTex

Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, and Prakash Saivasan. Verifying Quantitative Temporal Properties of Procedural Programs. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 15:1-15:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018) https://doi.org/10.4230/LIPIcs.CONCUR.2018.15

Abstract

We address the problem of specifying and verifying quantitative properties of procedural programs. These properties typically involve constraints on the relative cumulated costs of executing various tasks (by invoking for instance some particular procedures) within the scope of the execution of some particular procedure. An example of such properties is "within the execution of each invocation of procedure P, the time spent in executing invocations of procedure Q is less than 20 % of the total execution time". We introduce specification formalisms, both automata-based and logic-based, for expressing such properties, and we study the links between these formalisms and their application in model-checking. On one side, we define Constrained Pushdown Systems (CPDS), an extension of pushdown systems with constraints, expressed in Presburger arithmetics, on the numbers of occurrences of each symbol in the alphabet within invocation intervals (subcomputations between matching pushes and pops), and on the other side, we introduce a higher level specification language that is a quantitative extension of CaRet (the Call-Return temporal logic) called QCaRet where nested quantitative constraints over procedure invocation intervals are expressible using Presburger arithmetics. Then, we investigate (1) the decidability of the reachability and repeated reachability problems for CPDS, and (2) the effective reduction of the model-checking problem of procedural programs (modeled as visibly pushdown systems) against QCaRet formulas to these problems on CPDS.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Software and its engineering → Model checking
  • Software and its engineering → Software verification
Keywords
  • Verification
  • Formal Methods
  • Pushdown systems
  • Visibly pushdown
  • Quantitative Temporal Properties

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. P. A. Abdulla, M. F. Atig, and J. Stenman. The minimal cost reachability problem in priced timed pushdown systems. In LATA, volume 7183 of LNCS, 2012. Google Scholar
  2. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Giorgio Delzanno, and Andreas Podelski. Push-down automata with gap-order constraints. In Fundamentals of Software Engineering - 5th International Conference, FSEN 2013, Tehran, Iran, April 24-26, 2013, Revised Selected Papers, volume 8161 of Lecture Notes in Computer Science. Springer, 2013. Google Scholar
  3. Parosh Aziz Abdulla, Mohamed Faouzi Atig, and Jari Stenman. Dense-timed pushdown automata. In Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, LICS 2012, Dubrovnik, Croatia, June 25-28, 2012, pages 35-44. IEEE Computer Society, 2012. Google Scholar
  4. S. Akshay, Paul Gastin, and Shankara Narayanan Krishna. Analyzing Timed Systems Using Tree Automata. In Josée Desharnais and Radha Jagadeesan, editors, 27th International Conference on Concurrency Theory (CONCUR 2016), volume 59 of Leibniz International Proceedings in Informatics (LIPIcs). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2016. Google Scholar
  5. Rajeev Alur, Marcelo Arenas, Pablo Barceló, Kousha Etessami, Neil Immerman, and Leonid Libkin. First-order and temporal logics for nested words. Logical Methods in Computer Science, 4(4), 2008. URL: http://dx.doi.org/10.2168/LMCS-4(4:11)2008.
  6. Rajeev Alur, Kousha Etessami, and P. Madhusudan. A temporal logic of nested calls and returns. In Tools and Algorithms for the Construction and Analysis of Systems, 10th International Conference, TACAS 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004, Barcelona, Spain, March 29 - April 2, 2004, Proceedings, 2004. URL: http://dx.doi.org/10.1007/978-3-540-24730-2_35.
  7. Rajeev Alur and P. Madhusudan. Visibly pushdown languages. In Proceedings of the 36th Annual ACM Symposium on Theory of Computing, Chicago, IL, USA, June 13-16, 2004, 2004. URL: http://dx.doi.org/10.1145/1007352.1007390.
  8. Mohamed Faouzi Atig, Dmitry Chistikov, Piotr Hofman, K. Narayan Kumar, Prakash Saivasan, and Georg Zetzsche. The complexity of regular abstractions of one-counter languages. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, New York, NY, USA, July 5-8, 2016. URL: http://dx.doi.org/10.1145/2933575.2934561.
  9. Benedikt Bollig, Aiswarya Cyriac, Paul Gastin, and K. Narayan Kumar. Model checking languages of data words. In Foundations of Software Science and Computational Structures - 15th International Conference, FOSSACS 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012. Proceedings, volume 7213 of Lecture Notes in Computer Science. Springer, 2012. Google Scholar
  10. A. Bouajjani, R. Echahed, and R. Robbana. On the automatic verification of systems with continuous variables and unbounded discrete data structures. In Hybrid Systems II, volume 999 of LNCS. Springer, 1994. Google Scholar
  11. Ahmed Bouajjani and Peter Habermehl. Symbolic reachability analysis of fifo-channel systems with nonregular sets of configurations. Theor. Comput. Sci., 221(1-2):211-250, 1999. Google Scholar
  12. Michaël Cadilhac, Alain Finkel, and Pierre McKenzie. On the expressiveness of parikh automata and related models. In Third Workshop on Non-Classical Models for Automata and Applications - NCMA 2011, Milan, Italy, July 18 - July 19, 2011. Proceedings, 2011. Google Scholar
  13. Michaël Cadilhac, Alain Finkel, and Pierre McKenzie. Bounded parikh automata. Int. J. Found. Comput. Sci., 23(8):1691-1710, 2012. Google Scholar
  14. X. Cai and M. Ogawa. Well-structured pushdown systems. In CONCUR 2013, volume 8052 of LNCS. Springer, 2013. Google Scholar
  15. Krishnendu Chatterjee, Andreas Pavlogiannis, and Yaron Velner. Quantitative interprocedural analysis. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015. Google Scholar
  16. Lorenzo Clemente and Slawomir Lasota. Timed pushdown automata revisited. In 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015, Kyoto, Japan, July 6-10, 2015. IEEE Computer Society, 2015. Google Scholar
  17. F. S. de Boer, M. M. Bonsangue, and J. Rot. It is pointless to point in bounded heaps. Sci. Comput. Program., 112, 2015. Google Scholar
  18. Javier Esparza, Pierre Ganty, Stefan Kiefer, and Michael Luttenberger. Parikh’s theorem: A simple and direct automaton construction. Inf. Process. Lett., 111(12), 2011. URL: http://dx.doi.org/10.1016/j.ipl.2011.03.019.
  19. Oscar H. Ibarra. Visibly pushdown automata and transducers with counters. Fundam. Inform., 148(3-4):291-308, 2016. Google Scholar
  20. Felix Klaedtke and Harald Rueß. Monadic second-order logics with cardinalities. In JosC.M. Baeten, JanKarel Lenstra, Joachim Parrow, and GerhardJ. Woeginger, editors, Automata, Languages and Programming, volume 2719 of Lecture Notes in Computer Science. Springer Berlin Heidelberg, 2003. Google Scholar
  21. Christof Löding and Karianto Wong. On nondeterministic unranked tree automata with sibling constraints. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2009, December 15-17, 2009, IIT Kanpur, India, 2009. URL: http://dx.doi.org/10.4230/LIPIcs.FSTTCS.2009.2328.
  22. Helmut Seidl, Thomas Schwentick, and Anca Muscholl. Counting in trees. In Logic and Automata: History and Perspectives [in Honor of Wolfgang Thomas]., 2008. Google Scholar
  23. Helmut Seidl, Thomas Schwentick, Anca Muscholl, and Peter Habermehl. Counting in trees for free. In Automata, Languages and Programming: 31st International Colloquium, ICALP 2004, Turku, Finland, July 12-16, 2004. Proceedings, volume 3142 of Lecture Notes in Computer Science. Springer, 2004. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact