Quantitative Simulations by Matrices

TL;DR

This paper introduces matrix-based simulation notions for semiring-weighted automata, enabling quantitative system verification through linear inequalities and existing algorithms, with implementations for specific semirings and automata types.

Contribution

It presents a concrete matrix-based framework for simulations in weighted automata, extending to tree automata and leveraging categorical concepts for verification.

Findings

Verification of quantitative correctness via language inclusion

Implementation for plus-times and max-plus semirings

Extension to weighted tree automata

Abstract

We introduce notions of simulation between semiring-weighted automata as models of quantitative systems. Our simulations are instances of the categorical/coalgebraic notions previously studied by Hasuo---hence soundness against language inclusion comes for free---but are concretely presented as matrices that are subject to linear inequality constraints. Pervasiveness of these formalisms allows us to exploit existing algorithms in: searching for a simulation, and hence verifying quantitative correctness that is formulated as language inclusion. Transformations of automata that aid search for simulations are introduced, too. This verification workflow is implemented for the plus-times and max-plus semirings. Furthermore, an extension to weighted tree automata is presented and implemented.