Document Open Access Logo

Efficient Analysis of Unambiguous Automata Using Matrix Semigroup Techniques

Authors Stefan Kiefer, Cas Widdershoven

PDF
Thumbnail PDF

File

LIPIcs.MFCS.2019.82.pdf
  • Filesize: 481 kB
  • 13 pages

Document Identifiers

Author Details

Stefan Kiefer
  • University of Oxford, UK
Cas Widdershoven
  • University of Oxford, UK

Funding

  • Kiefer, Stefan: Work supported by a Royal Society University Research Fellowship.

Cite As Get BibTex

Stefan Kiefer and Cas Widdershoven. Efficient Analysis of Unambiguous Automata Using Matrix Semigroup Techniques. In 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 138, pp. 82:1-82:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.MFCS.2019.82

Abstract

We introduce a novel technique to analyse unambiguous Büchi automata quantitatively, and apply this to the model checking problem. It is based on linear-algebra arguments that originate from the analysis of matrix semigroups with constant spectral radius. This method can replace a combinatorial procedure that dominates the computational complexity of the existing procedure by Baier et al. We analyse the complexity in detail, showing that, in terms of the set Q of states of the automaton, the new algorithm runs in time O(|Q|^4), improving on an efficient implementation of the combinatorial algorithm by a factor of |Q|.

Subject Classification

ACM Subject Classification
  • Theory of computation → Automata over infinite objects
  • Theory of computation → Design and analysis of algorithms
Keywords
  • Algorithms
  • Automata
  • Markov Chains
  • Matrix Semigroups

Metrics

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

Related Versions

References

  1. Christel Baier and Joost-Pieter Katoen. Principles of model checking. MIT press, 2008. Google Scholar
  2. Christel Baier, Stefan Kiefer, Joachim Klein, Sascha Klüppelholz, David Müller, and James Worrell. Markov chains and unambiguous Büchi automata. In Proceedings of Computer Aided Verification (CAV), volume 9779 of LNCS, pages 23-42, 2016. Google Scholar
  3. Christel Baier, Stefan Kiefer, Joachim Klein, Sascha Klüppelholz, David Müller, and James Worrell. Markov chains and unambiguous automata. Draft journal submission. Available at https://arxiv.org/abs/1605.00950, 2019. Google Scholar
  4. Abraham Berman and Robert J. Plemmons. Nonnegative matrices in the mathematical sciences. SIAM, 1994. Google Scholar
  5. Manuel Bodirsky, Tobias Gärtner, Timo von Oertzen, and Jan Schwinghammer. Efficiently Computing the Density of Regular Languages. In LATIN 2004: Theoretical Informatics, pages 262-270. Springer, 2004. Google Scholar
  6. James R. Bunch and John E. Hopcroft. Triangular factorization and inversion by fast matrix multiplication. Mathematics of Computation, 28:231-236, 1974. Google Scholar
  7. Doron Bustan, Sasha Rubin, and Moshe Y. Vardi. Verifying ω-Regular Properties of Markov Chains. In 16th International Conference on Computer Aided Verification (CAV), volume 3114 of Lecture Notes in Computer Science, pages 189-201. Springer, 2004. Google Scholar
  8. Costas Courcoubetis and Mihalis Yannakakis. The Complexity of Probabilistic Verification. Journal of the ACM, 42(4):857-907, 1995. Google Scholar
  9. Erich Grädel, Wolfgang Thomas, and Thomas Wilke, editors. Automata, Logics, and Infinite Games: A Guide to Current Research, volume 2500 of Lecture Notes in Computer Science. Springer, 2002. Google Scholar
  10. Nicholas J. Higham. Accuracy and Stability of Numerical Algorithms. SIAM, second edition, 2002. Google Scholar
  11. M. James. The generalised inverse. The Mathematical Gazette, 62:109-114, 1978. Google Scholar
  12. Stefan Kiefer and Cas Widdershoven. Efficient Analysis of Unambiguous Automata Using Matrix Semigroup Techniques (full version). arXiv:1906.10093, 2016. URL: http://arxiv.org/abs/1906.10093.
  13. Vidyadhar G. Kulkarni. Modeling and Analysis of Stochastic Systems. Chapman & Hall, 1995. Google Scholar
  14. François Le Gall. Powers of Tensors and Fast Matrix Multiplication. In Proceedings of the 39th International Symposium on Symbolic and Algebraic Computation, ISSAC'14, pages 296-303. ACM, 2014. Google Scholar
  15. Marko D. Petković and Predrag S. Stanimirović. Generalised matrix inversion is not harder than matrix multiplication. Journal of Computational and Applied Mathematics, 230:270-282, 2009. Google Scholar
  16. V.Yu. Protasov and A.S. Voynov. Matrix semigroups with constant spectral radius. Linear Algebra and its Applications, 513:376-408, 2017. Google Scholar
  17. Robert Tarjan. Depth-first search and linear graph algorithms. SIAM journal on computing, 1(2):146-160, 1972. Google Scholar
  18. Wen-Guey Tzeng. A polynomial-time algorithm for the equivalence of probabilistic automata. SIAM Journal on Computing, 21(2):216-227, 1992. 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