Skip to main content
SpringerLink
Log in

Model-Checking HyperLTL for Pushdown Systems

  • Conference paper
  • First Online:
Model Checking Software (SPIN 2018)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 10869))

Included in the following conference series:

Abstract

Temporal logics such as LTL are often used to express safety or correctness properties of programs. However, they cannot model complex formulas known as hyperproperties introducing relations between different execution paths of a same system. In order to do so, the logic HyperLTL adds existential and universal quantifications of path variables to LTL. The model-checking problem, that is, determining if a given representation of a program verifies a HyperLTL property, has been shown to be decidable for finite state systems. In this paper, we prove that this result does not hold for Pushdown Systems nor for the subclass of Visibly Pushdown Systems. We therefore introduce an algorithm that over-approximates the model-checking problem with an automata-theoretic approach. We also detail an under-approximation method based on a phase-bounded analysis of Multi-Stack Pushdown Systems. We then show how these approximations can be used to check security policies.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. Alur, R., Madhusudan, P.: Visibly pushdown languages. In: Proceedings of the Thirty-sixth Annual ACM Symposium on Theory of Computing, STOC 2004, pp. 202–211. ACM, New York (2004)

    Google Scholar 

  2. Bermudez, M.E., Schimpf, K.M.: Practical arbitrary lookahead LR parsing. J. Comput. Syst. Sci. 41(2), 230–250 (1990)

    Article  MathSciNet  Google Scholar 

  3. Bouajjani, A., Esparza, J., Maler, O.: Reachability analysis of pushdown automata: application to model-checking. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol. 1243, pp. 135–150. Springer, Heidelberg (1997). https://doi.org/10.1007/3-540-63141-0_10

    Chapter  Google Scholar 

  4. Carotenuto, D., Murano, A., Peron, A.: 2-visibly pushdown automata. In: Harju, T., Karhumäki, J., Lepistö, A. (eds.) DLT 2007. LNCS, vol. 4588, pp. 132–144. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-73208-2_15

    Chapter  Google Scholar 

  5. Clarke, E., Kroening, D., Sharygina, N., Yorav, K.: SATABS: SAT-based predicate abstraction for ANSI-C. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 570–574. Springer, Heidelberg (2005). https://doi.org/10.1007/978-3-540-31980-1_40

    Chapter  MATH  Google Scholar 

  6. Clarkson, M.R., Finkbeiner, B., Koleini, M., Micinski, K.K., Rabe, M.N., Sánchez, C.: Temporal logics for hyperproperties. In: Abadi, M., Kremer, S. (eds.) POST 2014. LNCS, vol. 8414, pp. 265–284. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-642-54792-8_15

    Chapter  Google Scholar 

  7. Clarkson, M.R., Schneider, F.B.: Hyperproperties. J. Comput. Secur. 18(6), 1157–1210 (2010)

    Article  Google Scholar 

  8. Esparza, J., Hansel, D., Rossmanith, P., Schwoon, S.: Efficient algorithms for model checking pushdown systems. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 232–247. Springer, Heidelberg (2000). https://doi.org/10.1007/10722167_20

    Chapter  Google Scholar 

  9. Finkbeiner, B., Rabe, M.N., Sánchez, C.: Algorithms for model checking HyperLTL and HyperCTL\(^*\). In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 30–48. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21690-4_3

    Chapter  Google Scholar 

  10. Hague, M., Ong, C.-H.L.: Analysing mu-calculus properties of pushdown systems. In: van de Pol, J., Weber, M. (eds.) SPIN 2010. LNCS, vol. 6349, pp. 187–192. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-16164-3_14

    Chapter  Google Scholar 

  11. Kinder, J., Veith, H.: Jakstab: a static analysis platform for binaries. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 423–427. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-70545-1_40

    Chapter  Google Scholar 

  12. Pereira, F.C.N., Wright, R.N.: Finite-state approximation of phrase structure grammars. In: Proceedings of the 29th Annual Meeting on Association for Computational Linguistics, ACL 1991, pp. 246–255. Association for Computational Linguistics, Stroudsburg (1991)

    Google Scholar 

  13. Qadeer, S., Rehof, J.: Context-bounded model checking of concurrent software. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 93–107. Springer, Heidelberg (2005). https://doi.org/10.1007/978-3-540-31980-1_7

    Chapter  MATH  Google Scholar 

  14. Seth, A.: Global reachability in bounded phase multi-stack pushdown systems. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 615–628. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-14295-6_53

    Chapter  Google Scholar 

  15. Prasad Sistla, A., Vardi, M.Y., Wolper, P.: The complementation problem for Büchi automata with applications to temporal logic. Theoret. Comput. Sci. 49(2), 217–237 (1987)

    Article  MathSciNet  Google Scholar 

  16. Torre, S.L., Madhusudan, P., Parlato, G.: A robust class of context-sensitive languages. In: 22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007), pp. 161–170, July 2007

    Google Scholar 

  17. Vardi, M.Y.: An automata-theoretic approach to linear temporal logic. In: Moller, F., Birtwistle, G. (eds.) Logics for Concurrency. LNCS, vol. 1043, pp. 238–266. Springer, Heidelberg (1996). https://doi.org/10.1007/3-540-60915-6_6

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. LIPN and Université Paris-Diderot, Paris, France

    Adrien Pommellet

  2. LIPN, CNRS, and Université Paris 13, Villetaneuse, France

    Tayssir Touili

Authors
  1. Adrien Pommellet
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Tayssir Touili
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding authors

Correspondence to Adrien Pommellet or Tayssir Touili .

Editor information

Editors and Affiliations

  1. University of Málaga, Málaga, Spain

    María del Mar Gallardo

  2. University of Málaga, Málaga, Spain

    Pedro Merino

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG, part of Springer Nature

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Pommellet, A., Touili, T. (2018). Model-Checking HyperLTL for Pushdown Systems. In: Gallardo, M., Merino, P. (eds) Model Checking Software. SPIN 2018. Lecture Notes in Computer Science(), vol 10869. Springer, Cham. https://doi.org/10.1007/978-3-319-94111-0_8

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-94111-0_8

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-94110-3

  • Online ISBN: 978-3-319-94111-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation