## 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.

Original language | English |
---|---|

Title of host publication | 31st EACSL Annual Conference on Computer Science Logic |

Editors | Bartek Klin, Elaine Pimentel |

Place of Publication | Saarbrücken/Wadern |

Pages | 14:1-14:20 |

Number of pages | 20 |

ISBN (Electronic) | 9783959772648 |

DOIs | |

Publication status | Published - 1 Feb 2023 |

Event | Computer Science Logic 2023 - Duration: 13 Feb 2023 → 16 Feb 2023 https://csl2023.mimuw.edu.pl/ |

### Publication series

Name | Leibniz International Proceedings in Informatics |
---|---|

Volume | 252 |

ISSN (Electronic) | 1868-8969 |

### Conference

Conference | Computer Science Logic 2023 |
---|---|

Period | 13/02/23 → 16/02/23 |

Internet address |

## Keywords

- coalgebra
- measure theory
- parity automaton