Measure-theoretic semantics for quantitative parity automata

Cîrstea, Corina and Kupke, Clemens; Klin, Bartek and Pimentel, Elaine, eds. (2023) Measure-theoretic semantics for quantitative parity automata. In: 31st EACSL Annual Conference on Computer Science Logic. Leibniz International Proceedings in Informatics . Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Saarbrücken/Wadern, 14:1-14:20. ISBN 9783959772648 (https://doi.org/10.4230/LIPIcs.CSL.2023.14)

[thumbnail of Cirstea-Kupke-CSL2023-Measure-theoretic-semantics-for-quantitative-parity-automata]
Preview
 Text. Filename: Cirstea_Kupke_CSL2023_Measure_theoretic_semantics_for_quantitative_parity_automata.pdf
Final Published Version
License: Creative Commons Attribution 4.0 logo
Download (695kB)| Preview

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.

CORE (COnnecting REpositories)