Paper Info
Title
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.
Year
DOI
Venue
2017
10.1016/j.ic.2016.03.007
Information and Computation
Keywords
Field
DocType
Kleisli category,Simulation,Language inclusion,Weighted automaton,Tropical semiring
Discrete mathematics,Kleisli category,Algebra,Categorical variable,Matrix (mathematics),Automaton,Correctness,Theoretical computer science,Soundness,Linear inequality,Rotation formalisms in three dimensions,Mathematics
Journal
Volume
ISSN
Citations 
252
0890-5401
0
PageRank 
References 
Authors
0.34
16
2
Name
Order
Citations
PageRank
Natsuki Urabe1144.69
Ichiro Hasuo226026.13