[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to main content

Crossing the Syntactic Barrier: Hom-Disequalities for \({\mathcal H}_1\)-Clauses

  • Conference paper
Implementation and Application of Automata (CIAA 2012)

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

Included in the following conference series:

  • 579 Accesses

Abstract

We extend \({\mathcal H}_1\)-clauses with disequalities between images of terms under a tree homomorphism (hom-disequalities). This extension allows to test whether two terms are distinct modulo a semantic interpretation, allowing, e.g., to neglect information that is not considered relevant for the intended comparison. We prove that \({\mathcal H}_1\)-clauses with hom-disequalities are more expressive than \({\mathcal H}_1\)-clauses with ordinary term disequalities, and that they are incomparable with \({\mathcal H}_1\)-clauses with disequalities between paths. Our main result is that \({\mathcal H}_1\)-clauses with this new type of constraints can be normalized into an equivalent tree automaton with hom-disequalities. Since emptiness for that class of automata turns out to be decidable, we conclude that satisfiability is decidable for positive Boolean combinations of queries to predicates defined by \({\mathcal H}_1\)-clauses with hom-disequalities.

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

Access this chapter

Subscribe and save

Springer+ Basic
£29.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
GBP 19.95
Price includes VAT (United Kingdom)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
GBP 35.99
Price includes VAT (United Kingdom)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
GBP 44.99
Price includes VAT (United Kingdom)
  • 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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. Blanchet, B.: An efficient cryptographic protocol verifier based on prolog rules. In: CSFW, pp. 82–96 (2001)

    Google Scholar 

  2. Bugliesi, M., Rossi, S.: Non-interference proof techniques for the analysis of cryptographic protocols. Journal of Computer Security 13(1), 87–113 (2005)

    Google Scholar 

  3. Chatzikokolakis, K.: Probabilistic and Information-Theoretic Approaches to Anonymity. Ph.D. thesis, École polytechnique (2007)

    Google Scholar 

  4. Frühwirth, T.W., Shapiro, E.Y., Vardi, M.Y., Yardeni, E.: Logic programs as types for logic programs. In: LICS, pp. 314–328 (1991)

    Google Scholar 

  5. Godoy, G., Giménez, O., Ramos, L., Àlvarez, C.: The hom problem is decidable. In: STOC, pp. 485–494. ACM (2010)

    Google Scholar 

  6. Goguen, J.A., Meseguer, J.: Security policies and security models. In: IEEE Symposium on Security and Privacy, pp. 11–20 (1982)

    Google Scholar 

  7. Goubault-Larrecq, J.: Deciding H1 by resolution. IPL 95(3), 401–408 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  8. Goubault-Larrecq, J., Parrennes, F.: Cryptographic Protocol Analysis on Real C Code. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 363–379. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  9. Nielson, F., Riis Nielson, H., Seidl, H.: Normalizable Horn Clauses, Strongly Recognizable Relations, and Spi. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477, pp. 20–35. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  10. Reuß, A., Seidl, H.: Bottom-Up Tree Automata with Term Constraints. In: Fermüller, C.G., Voronkov, A. (eds.) LPAR-17. LNCS, vol. 6397, pp. 581–593. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  11. Seidl, H., Neumann, A.: On Guarding Nested Fixpoints. In: Flum, J., Rodríguez-Artalejo, M. (eds.) CSL 1999. LNCS, vol. 1683, pp. 484–498. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  12. Seidl, H., Reuß, A.: Extending H1-clauses with disequalities. IPL 111(20), 1007–1013 (2011)

    Article  Google Scholar 

  13. Seidl, H., Reuß, A.: Extending \({\cal H}_1\)-Clauses with Path Disequalities. In: Birkedal, L. (ed.) FOSSACS 2012. LNCS, vol. 7213, pp. 165–179. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  14. Weidenbach, C.: Towards an Automatic Analysis of Security Protocols in First-Order Logic. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol. 1632, pp. 314–328. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2012 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Reuß, A., Seidl, H. (2012). Crossing the Syntactic Barrier: Hom-Disequalities for \({\mathcal H}_1\)-Clauses. In: Moreira, N., Reis, R. (eds) Implementation and Application of Automata. CIAA 2012. Lecture Notes in Computer Science, vol 7381. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-31606-7_26

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-31606-7_26

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-31605-0

  • Online ISBN: 978-3-642-31606-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics