Document Open Access Logo

Parity Automata for Quantitative Linear Time Logics

Authors Corina Cirstea, Shunsuke Shimizu, Ichiro Hasuo

PDF

File

Thumbnail PDF
PDF
LIPIcs.CALCO.2017.7.pdf
  • Filesize: 0.63 MB
  • 18 pages

Document Identifiers

Subject Classification

Keywords
  • coalgebra
  • quantitative logic
  • linear time logic
  • parity automaton

Metrics

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

Abstract

We initiate a study of automata-based model checking for previously proposed quantitative linear time logics interpreted over coalgebras. Our results include: (i) an automata-theoretic characterisation of the semantics of these logics, based on a notion of extent of a quantitative parity automaton, (ii) a study of the expressive power of Buchi variants of such automata, with implications on the expressiveness of fragments of the logics considered, and (iii) a naive algorithm for computing extents, under additional assumptions on the domain of truth values.

Cite As Get BibTex

Corina Cirstea, Shunsuke Shimizu, and Ichiro Hasuo. Parity Automata for Quantitative Linear Time Logics. In 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 72, pp. 7:1-7:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017) https://doi.org/10.4230/LIPIcs.CALCO.2017.7

Author Details

Corina Cirstea
Shunsuke Shimizu
Ichiro Hasuo

References

  1. A. Arnold and D. Niwiński. Rudiments of μ-Calculus. Studies in Logic and the Foundations of Mathematics. North-Holland, 2001. Google Scholar
  2. C. Baier, M. Größer, and N. Bertrand. Probabilistic ω-automata. J. ACM, 59(1):1, 2012. Google Scholar
  3. C. Baier and J.-P. Katoen. Principles of model checking. MIT Press, 2008. Google Scholar
  4. C. Cîrstea. A coalgebraic approach to linear-time logics. In A. Muscholl, editor, Foundations of Software Science and Computation Structures, 17th International Conference, pages 426-440. Springer, 2014. Google Scholar
  5. C. Cîrstea. A coalgebraic approach to quantitative linear time logics. CoRR, abs/1612.07844, 2016. URL: http://arxiv.org/abs/1612.07844.
  6. C. Cîrstea. From branching to linear time, coalgebraically. Fundamenta Informaticae, 150:1-28, 2017. Google Scholar
  7. R. Cleaveland, M. Klein, and B. Steffen. Faster model checking for the modal μ-calculus. In Computer Aided Verification, 4th International Workshop, pages 410-422. Springer, 1993. Google Scholar
  8. D. Coumans and B. Jacobs. Scalars, monads, and categories. In Quantum Physics and Linguistics. A Compositional, Diagrammatic Discourse, pages 184-216. Oxford Univ. Press, 2013. Google Scholar
  9. M. Dam. Fixed points of Büchi automata. In R. Shyamasundar, editor, Foundations of Software Technology and Theoretical Computer Science, 12th Conference, pages 39-50. Springer, 1992. Google Scholar
  10. B. A. Davey and H. A. Priestley. Introduction to Lattices and Order (2. ed.). Cambridge University Press, 2002. Google Scholar
  11. B. Farwer. ω-Automata. In E. Grädel, W. Thomas, and T. Wilke, editors, Automata, Logics, and Infinite Games: A Guide to Current Research, pages 3-20. Springer, 2002. Google Scholar
  12. M. J. Fischer and R. E. Ladner. Propositional dynamic logic of regular programs. Journal of Computer and System Sciences, 18(2):194 - 211, 1979. Google Scholar
  13. I. Hasuo, S. Shimizu, and C. Cîrstea. Lattice-theoretic progress measures and coalgebraic model checking. In 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 718-732, 2016. Google Scholar
  14. D. Kirsten. Alternating tree automata and parity games. In E. Grädel, W. Thomas, and T. Wilke, editors, Automata Logics, and Infinite Games: A Guide to Current Research, pages 153-167. Springer, 2002. Google Scholar
  15. I. Meinecke. A weighted μ-calculus on words. In 13th International Conference on Developments in Language Theory, pages 384-395. Springer, 2009. Google Scholar
  16. M. O. Rabin. Decidability of second-order theories and automata on infinite trees. Transactions of the American Mathematical Society, 141:1-35, 1969. Google Scholar
  17. N. Urabe, S. Shimizu, and I. Hasuo. Coalgebraic trace semantics for büchi and parity automata. In J. Desharnais and R. Jagadeesan, editors, 27th International Conference on Concurrency Theory, volume 59 of LIPICS, pages 24:1-24:15, 2016. Google Scholar
  18. Y. Venema. Lectures on the modal μ-calculus. Lecture notes, Institute for Logic, Language and Computation, University of Amsterdam, 2012. Google Scholar
  19. I. Walukiewicz. Automata and logic, 2001. Notes available from http://www.labri.fr/perso/igw/Papers/igw-eefss01.ps. 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