2018/10/31 by Natsuki Urabe, Ichiro Hasuo
Computer Science · #cs.LO
paper · pdf · doi:10.1016/j.ic.2016.03.007
published as Information and Computation, Volume 252, February 2017, Pages 110-137 · Extended version of [Urabe & Hasuo, CONCUR 2014]
arxiv created 2018/11/16 · arxiv updated 2018/11/19
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.