Quantitative Simulations by Matrices
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.
Cite
@article{arxiv.1810.09146,
title = {Quantitative Simulations by Matrices},
author = {Natsuki Urabe and Ichiro Hasuo},
journal= {arXiv preprint arXiv:1810.09146},
year = {2018}
}
Comments
Extended version of [Urabe & Hasuo, CONCUR 2014]