Document Open Access Logo

Tyrolean Complexity Tool: Features and Usage

Authors Martin Avanzini, Georg Moser

PDF

File

Thumbnail PDF
PDF
LIPIcs.RTA.2013.71.pdf
  • Filesize: 2.5 MB
  • 10 pages

Document Identifiers

Subject Classification

Keywords
  • program analysis
  • term rewriting
  • complexity analysis
  • automation

Metrics

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

Abstract

The Tyrolean Complexity Tool, TCT for short, is an open source complexity analyser for term rewrite systems. Our tool TCT features a majority of the known techniques for the automated characterisation of polynomial complexity of rewrite systems and can investigate derivational and runtime complexity, for full and innermost rewriting. This system description outlines features and provides a short introduction to the usage of TCT.

Cite As Get BibTex

Martin Avanzini and Georg Moser. Tyrolean Complexity Tool: Features and Usage. In 24th International Conference on Rewriting Techniques and Applications (RTA 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 21, pp. 71-80, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013) https://doi.org/10.4230/LIPIcs.RTA.2013.71

Author Details

Martin Avanzini
Georg Moser

References

  1. M. Avanzini, N. Eguchi, and G. Moser. New Order-theoretic Characterisation of the Polytime Computable Functions. In Proceedings of the \nth10 Asian Symposium Programming Languages and Systems, number 7705 in LNCS, pages 280-295. Springer, 2012. Google Scholar
  2. M. Avanzini and G. Moser. Complexity Analysis by Rewriting. In Proc. of \nth8 FLOPS, volume 4989 of LNCS, pages 130-146. Springer, 2008. Google Scholar
  3. M. Avanzini and G. Moser. Closing the Gap Between Runtime Complexity and Polytime Computability. In Proc. of \nst21 RTA, volume 6 of LIPIcs, pages 33-48, 2010. Google Scholar
  4. M. Avanzini and G. Moser. Polynomial Path Orders: A Maximal Model. 2012. Submitted to LMCS. Technical Report available at URL: http://arxiv.org/abs/1209.3793.
  5. M. Avanzini and G. Moser. A Combination Framework for Complexity. In Proc. of \nth24 RTA. LIPIcs, 2013. Technical Report available at URL: http://arxiv.org/abs/1302.0973.
  6. G. Bonfante, A. Cichon, J.-Y. Marion, and H. Touzet. Algorithms with Polynomial Interpretation Termination Proof. JFP, 11(1):33-53, 2001. Google Scholar
  7. U. Dal Lago and S. Martini. Derivational Complexity is an Invariant Cost Model. In Proc. of 1st FOPARA, 2009. Google Scholar
  8. J. Endrullis, J. Waldmann, and H. Zantema. Matrix Interpretations for Proving Termination of Term Rewriting. JAR, 40(2-3):195-220, 2008. Google Scholar
  9. A. Geser, D. Hofbauer, J. Waldmann, and H. Zantema. On Tree Automata that Certify Termination of Left-Linear Term Rewriting Systems. In Proc. of \nth16 RTA, number 3467 in LNCS, pages 353-367. Springer, 2005. Google Scholar
  10. J. Giesl, R. Thiemann, P. Schneider-Kamp, and S. Falke. Mechanizing and Improving Dependency Pairs. JAR, 37(3):155-203, 2006. Google Scholar
  11. N. Hirokawa and G. Moser. Automated Complexity Analysis Based on the Dependency Pair Method. In Proc. of \nth4 IJCAR, volume 5195 of LNAI, pages 364-380, 2008. Google Scholar
  12. N. Hirokawa and G. Moser. Automated Complexity Analysis Based on the Dependency Pair Method. 2012. Submitted to IC, available at URL: http://arxiv.org/abs/1102.3129.
  13. D. Hofbauer and C. Lautemann. Termination Proofs and the Length of Derivations. In Proc. of \nrd3 RTA, volume 355 of LNCS, pages 167-177. Springer, 1989. Google Scholar
  14. A. Koprowski and J. Waldmann. Max/Plus Tree Automata for Termination of Term Rewriting. AC, 19(2):357-392, 2009. Google Scholar
  15. A. Middeldorp, G. Moser, F. Neurauter, J. Waldmann, and H. Zankl. Joint Spectral Radius Theory for Automated Complexity Analysis of Rewrite Systems. In Proc. of \nth4 CAI, volume 6742 of LNCS, pages 1-20. Springer, 2011. Google Scholar
  16. G. Moser. Proof Theory at Work: Complexity Analysis of Term Rewrite Systems. CoRR, abs/0907.5527, 2009. Habilitation Thesis. Google Scholar
  17. G. Moser and A. Schnabl. Proving Quadratic Derivational Complexities using Context Dependent Interpretations. In Proc. of \nth19 RTA, volume 5117 of LNCS, pages 276-290. Springer, 2008. Google Scholar
  18. G. Moser, A. Schnabl, and J. Waldmann. Complexity Analysis of Term Rewriting Based on Matrix and Context Dependent Interpretations. In Proc. of \nth28 FSTTCS, LIPIcs, pages 304-315, 2008. Google Scholar
  19. L. Noschinski, F. Emmes, and J. Giesl. A Dependency Pair Framework for Innermost Complexity Analysis of Term Rewrite Systems. In Proc. of \nrd23 CADE, LNAI, pages 422-438. Springer, 2011. Google Scholar
  20. J. Waldmann. Polynomially Bounded Matrix Interpretations. In Proc. of \nst21 RTA, volume 6 of LIPIcs, pages 357-372, 2010. Google Scholar
  21. H. Zankl and M. Korp. Modular Complexity Analysis via Relative Complexity. In Proc. of \nst21 RTA, volume 6 of LIPIcs, pages 385-400, 2010. 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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact