Document Open Access Logo

Measure-Theoretic Semantics for Quantitative Parity Automata

Authors Corina Cîrstea , Clemens Kupke

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2023.14.pdf
  • Filesize: 0.79 MB
  • 20 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Program verification
Keywords
  • parity automaton
  • coalgebra
  • measure theory

Metrics

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

Abstract

Quantitative parity automata (QPAs) generalise non-deterministic parity automata (NPAs) by adding weights from a certain semiring to transitions. QPAs run on infinite word/tree-like structures, modelled as coalgebras of a polynomial functor F. They can also arise as certain products between a quantitative model (with branching modelled via the same semiring of quantities, and linear behaviour described by the functor F) and an NPA (modelling a qualitative property of F-coalgebras). We build on recent work on semiring-valued measures to define a way to measure the set of paths through a quantitative branching model which satisfy a qualitative property (captured by an unambiguous NPA running on F-coalgebras). Our main result shows that the notion of extent of a QPA (which generalises non-emptiness of an NPA, and is defined as the solution of a nested system of equations) provides an equivalent characterisation of the measure of the accepting paths through the QPA. This result makes recently-developed methods for computing nested fixpoints available for model checking qualitative, linear-time properties against quantitative branching models.

Cite As Get BibTex

Corina Cîrstea and Clemens Kupke. Measure-Theoretic Semantics for Quantitative Parity Automata. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 14:1-14:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023) https://doi.org/10.4230/LIPIcs.CSL.2023.14

Author Details

Corina Cîrstea
  • University of Southampton, UK
Clemens Kupke
  • University of Strathclyde, UK

Funding

Research carried out as part of the Leverhulme Trust Research Project Grant RPG-2020-232.

References

  1. Christel Baier, Luca de Alfaro, Vojtech Forejt, and Marta Kwiatkowska. Model checking probabilistic systems. In Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem, editors, Handbook of Model Checking, pages 963-999. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-10575-8_28.
  2. Christel Baier and Joost-Pieter Katoen. Principles of model checking. MIT Press, 2008. Google Scholar
  3. Paolo Baldan, Barbara König, Christina Mika-Michalski, and Tommaso Padoan. Fixpoint games on continuous lattices. Proceedings of the ACM on Programming Languages, 3(POPL):1-29, 2019. URL: https://doi.org/10.1145/3302515.
  4. Corina Cîrstea. Linear time logics - a coalgebraic perspective. arXiv:1612.07844. Google Scholar
  5. Corina Cîrstea. From branching to linear time, coalgebraically. Fundamenta Informaticae, 150:1-28, 2017. URL: https://doi.org/10.3233/FI-2017-1474.
  6. Corina Cîrstea, Shunsuke Shimizu, and Ichiro Hasuo. Parity Automata for Quantitative Linear Time Logics. In F. Bonchi and B. König, editors, 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017), volume 72 of Leibniz International Proceedings in Informatics (LIPIcs), pages 7:1-7:18, 2017. URL: https://doi.org/10.4230/LIPIcs.CALCO.2017.7.
  7. Thomas Colcombet. Forms of determinism for automata (invited talk). In Christoph Dürr and Thomas Wilke, editors, 29th International Symposium on Theoretical Aspects of Computer Science, STACS 2012, February 29th - March 3rd, 2012, Paris, France, volume 14 of Leibniz International Proceedings in Informatics (LIPIcs), pages 1-23, 2012. URL: https://doi.org/10.4230/LIPIcs.STACS.2012.1.
  8. Luca de Alfaro, Marco Faella, and Mariëlle Stoelinga. Linear and branching metrics for quantitative transition systems. In Josep Díaz, Juhani Karhumäki, Arto Lepistö, and Donald Sannella, editors, Automata, Languages and Programming, pages 97-109. Springer, 2004. Google Scholar
  9. Marco Faella, Axel Legay, and Mariëlle Stoelinga. Model checking quantitative linear time logic. Electr. Notes Theor. Comput. Sci., 220:61-77, 2008. URL: https://doi.org/10.1016/j.entcs.2008.11.019.
  10. 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, 2002. URL: https://doi.org/10.1007/3-540-36387-4.
  11. Ichiro Hasuo, Shunsuke Shimizu, and Corina Cîrstea. Lattice-theoretic progress measures and coalgebraic model checking. In Rastislav Bodík and Rupak Majumdar, editors, Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, pages 718-732. ACM, 2016. URL: https://doi.org/10.1145/2837614.2837673.
  12. Daniel Hausmann and Lutz Schröder. Quasipolynomial computation of nested fixpoints. In Jan Friso Groote and Kim Guldstrand Larsen, editors, Tools and Algorithms for the Construction and Analysis of Systems - 27th International Conference, TACAS 2021, Proceedings, volume 12651 of Lecture Notes in Computer Science, pages 38-56. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-72016-2_3.
  13. Bart Jacobs. Introduction to coalgebra, volume 59 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2016. Google Scholar
  14. Claus Thrane, Uli Fahrenberg, and Kim Larsen. Quantitative analysis of weighted transition systems. Journal of Logic and Algebraic Programming, 79:689-703, 2010. URL: https://doi.org/10.1016/j.jlap.2010.07.010.
  15. Natsuki Urabe, Shunsuke Shimizu, and Ichiro Hasuo. Coalgebraic trace semantics for Büchi and parity automata. arXiv:1606.09399. 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