Skip to main content
SpringerLink
Log in

TAGED Approximations for Temporal Properties Model-Checking

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

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

Included in the following conference series:

Abstract

This paper investigates the use of tree automata with global equalities and disequalities (TAGED for short) in reachability analysis over term rewriting systems (TRSs). The reachability problem being in general undecidable on non terminating TRSs, we provide TAGED-based construction, and then design approximation-based semi-decision procedures to model-check useful temporal patterns on infinite state rewriting graphs. To show that the above TAGED-based construction can be effectively carried out, complexity analysis for rewriting TAGED-definable languages is given.

This work has been funded by the French ANR-06-SETI-014 RAVAJ project.

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 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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Armando, A., Carbone, R., Compagna, L.: Ltl model checking for security protocols. In: CSF, pp. 385–396 (2007)

    Google Scholar 

  2. Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)

    Book  MATH  Google Scholar 

  3. Balland, E., Boichut, Y., Genet, T., Moreau, P.-E.: Towards an efficient implementation of tree automata completion. In: Meseguer, J., Roşu, G. (eds.) AMAST 2008. LNCS, vol. 5140, pp. 67–82. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  4. Bogaert, B., Tison, S.: Equality and disequality constraints on direct subterms in tree automata. In: Finkel, A., Jantzen, M. (eds.) STACS 1992, vol. 577, pp. 161–171. Springer, Heidelberg (1992)

    Chapter  Google Scholar 

  5. Boichut, Y., Courbis, R., Héam, P.-C., Kouchnarenko, O.: Finer is better: Abstraction refinement for rewriting approximations. In: Voronkov, A. (ed.) RTA 2008. LNCS, vol. 5117, pp. 48–62. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  6. Boichut, Y., Genet, T., Jensen, T., Le Roux, L.: Rewriting approximations for fast prototyping of static analyzers. In: Baader, F. (ed.) RTA 2007. LNCS, vol. 4533, pp. 48–62. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  7. Boichut, Y., Héam, P.-C., Kouchnarenko, O.: Approximation-based tree regular model-checking. Nordic Journal of Computing (to appear, 2009)

    Google Scholar 

  8. Clarke, E.M.: Counterexample-guided abstraction refinement. In: TIME-ICTL, p. 7. IEEE Computer Society, Los Alamitos (2003)

    Google Scholar 

  9. Comon, H., Cortier, V.: Tree automata with one memory set constraints and cryptographic protocols. Theoretical Computer Science (TCS 2005) 331 (2005)

    Google Scholar 

  10. Comon, H., Dauchet, M., Gilleron, R., Jacquemard, F., Lugiez, D., Tison, S., Tommasi, M.: Tree Automata Techniques and Applications (2002), http://www.grappa.univ-lille3.fr/tata/

  11. Dauchet, M., Caron, A.-C., Coquidé, J.-L.: Automata for reduction properties solving. J. Symb. Comput. 20(2), 215–233 (1995)

    Article  MathSciNet  MATH  Google Scholar 

  12. Dershowitz, N., Jouannaud, J.-P.: ch. 6: Rewrite Systems. In: Handbook of Theoretical Computer Science, vol. B, pp. 244–320. Elsevier Science Publishers B. V., Amsterdam (1990)

    Google Scholar 

  13. Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Property specification patterns for finite-state verification. In: Proceedings of the Second Workshop on Formal Methods in Software Practice, pp. 7–15. ACM Press, New York (1998)

    Chapter  Google Scholar 

  14. Escobar, S., Meseguer, J.: Symbolic model checking of infinite-state systems using narrowing. In: Baader, F. (ed.) RTA 2007. LNCS, vol. 4533, pp. 153–168. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  15. Feuillade, G., Genet, T., VietTriemTong, V.: Reachability analysis over term rewriting systems. Journal on Automated Reasoning 33(3-4) (2004)

    Google Scholar 

  16. Filiot, E., Talbot, J.-M., Tison, S.: Tree automata with global constraints. In: Ito, M., Toyama, M. (eds.) DLT 2008. LNCS, vol. 5257, pp. 314–326. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  17. Genet, T., Klay, F.: Rewriting for Cryptographic Protocol Verification. In: McAllester, D. (ed.) CADE 2000, vol. 1831, pp. 271–290. Springer, Heidelberg (2000)

    Google Scholar 

  18. Gilleron, R., Tison, S.: Regular tree languages and rewrite systems. Fundamenta Informatica 24(1/2), 157–174 (1995)

    MathSciNet  MATH  Google Scholar 

  19. Gyenizse, P., Vágvölgyi, S.: Linear Generalized Semi-Monadic Rewrite Systems Effectively Preserve Recognizability. Theoretical Computer Science 194(1-2), 87–122 (1998)

    Article  MathSciNet  MATH  Google Scholar 

  20. Jacquemard, F.: Decidable approximations of term rewriting systems. In: Ganzinger, H. (ed.) RTA 1996, vol. 1103, pp. 362–376. Springer, Heidelberg (1996)

    Chapter  Google Scholar 

  21. Jacquemard, F., Rusinowitch, M., Vigneron, L.: Tree automata with equality constraints modulo equational theories. IJCAR, 557–571 (2006)

    Google Scholar 

  22. Karianto, W., Löding, C.: Unranked tree automata with sibling equalities and disequalities. In: Arge, L., Cachin, C., Jurdziński, T., Tarlecki, A. (eds.) ICALP 2007. LNCS, vol. 4596, pp. 875–887. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  23. Lamport, L.: A temporal logic of actions. ACM Transactions On Programming Languages And Systems, TOPLAS 16(3), 872–923 (1994)

    Article  Google Scholar 

  24. Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification. SV (1992)

    Google Scholar 

  25. Meseguer, J.: Conditioned rewriting logic as a united model of concurrency. Theoretical Computer Science 96(1), 73–155 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  26. Meseguer, J.: The temporal logic of rewriting. Technical Report UIDCS-R-2007-2815, Dept. of Computer Science, University of Illinois at Urbana-Champaign (September 2007)

    Google Scholar 

  27. Meseguer, J.: The temporal logic of rewriting: A gentle introduction. In: Concurrency, Graphs and Models: Essays Dedicated to Ugo Montanari on the Occasion of His 65th Birthday, pp. 354–382 (2008)

    Google Scholar 

  28. Ohsaki, H., Takai, T.: ACTAS: A system design for associative and commutative tree automata theory. Electronic Notes in Theoretical Computer Science 124(1), 97–111 (2005)

    Article  Google Scholar 

  29. Pnueli, A.: The temporal logic of programs. In: FOCS 1977, pp. 46–57 (1977)

    Google Scholar 

  30. Seidl, H., Schwentick, T., Muscholl, A., Habermehl, P.: Counting in trees for free. In: Díaz, J., Karhumäki, J., Lepistö, A., Sannella, D. (eds.) ICALP 2004. LNCS, vol. 3142, pp. 1136–1149. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  31. Takai, T., Kaji, Y., Seki, H.: Right-linear finite-path overlapping term rewriting systems effectively preserve recognizability. In: Bachmair, L. (ed.) RTA 2000. LNCS, vol. 1833. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. INRIA/CASSIS, LIFC/University of Franche-Comté, 16 route de Gray, F-25030, Besançon Cedex, France

    Roméo Courbis, Pierre-Cyrille Héam & Olga Kouchnarenko

  2. LSV CNRS/INRIA/ENS Cachan, 61 av. du Président Wilson, F-94235, Cachan Cedex, France

    Pierre-Cyrille Héam

Authors
  1. Roméo Courbis
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Pierre-Cyrille Héam
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Olga Kouchnarenko
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. NICTA and University of New South Wales, Sydney, Australia

    Sebastian Maneth

Rights and permissions

Reprints and permissions

Copyright information

© 2009 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Courbis, R., Héam, PC., Kouchnarenko, O. (2009). TAGED Approximations for Temporal Properties Model-Checking. In: Maneth, S. (eds) Implementation and Application of Automata. CIAA 2009. Lecture Notes in Computer Science, vol 5642. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-02979-0_17

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-02979-0_17

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-02978-3

  • Online ISBN: 978-3-642-02979-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation