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 wrt. 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. © 2014 Springer-Verlag.
Cite
CITATION STYLE
Urabe, N., & Hasuo, I. (2014). Generic forward and backward simulations III: Quantitative simulations by matrices. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8704 LNCS, pp. 451–466). Springer Verlag. https://doi.org/10.1007/978-3-662-44584-6_31
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
