Quantitative simulations by matrices

DOI10.1016/J.IC.2016.03.007MaRDI QIDQ729815zbMATH OpenOpenAlexFDO

Authors Natsuki Urabe, Ichiro Hasuo

Publication date 22 December 2016

Published in Information and Computation (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1810.09146

zbMATH Keywords

simulationtropical semiringKleisli categoryweighted automatonlanguage inclusion

Mathematics Subject Classification ID

Algebraic theory of languages and automata (68Q70) Eilenberg-Moore and Kleisli constructions for monads (18C20) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

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.

Recommendations

• Generic forward and backward simulations. III: Quantitative simulations by matrices
• The complexity of simulation and matrix multiplication
• scientific article; zbMATH DE number 194194
• Computational matrix analysis
• scientific article; zbMATH DE number 3892457
• Numerical methods in matrix computations
• Matrix‐analytic Models and their Analysis

Cites work

• scientific article; zbMATH DE number 5839262 (Why is no real title available?)
• scientific article; zbMATH DE number 3716792 (Why is no real title available?)
• scientific article; zbMATH DE number 3466805 (Why is no real title available?)
• scientific article; zbMATH DE number 1163636 (Why is no real title available?)
• scientific article; zbMATH DE number 2040327 (Why is no real title available?)
• scientific article; zbMATH DE number 1497803 (Why is no real title available?)
• scientific article; zbMATH DE number 783754 (Why is no real title available?)
• scientific article; zbMATH DE number 3189697 (Why is no real title available?)
• A Coalgebraic Perspective on Minimization and Determinization
• A Polynomial-Time Algorithm for the Equivalence of Probabilistic Automata
• A final coalgebra theorem
• A new polynomial-time algorithm for linear programming
• A strongly polynomial algorithm for solving two-sided linear systems in max-algebra
• Algebra and Coalgebra in Computer Science
• Algebra-coalgebra duality in Brzozowski's minimization algorithm
• Algorithmic probabilistic game semantics. Playing games with automata
• Automata, Languages and Programming
• Beyond Bisimulation: The “up-to” Techniques
• Bisimulations for fuzzy automata
• Bisimulations for weighted automata over an additively idempotent semiring
• Coalgebraic Infinite Traces and Kleisli Simulations
• Coalgebraic Trace Semantics via Forgetful Logics
• Coalgebraic trace semantics for continuous probabilistic transition systems
• Coinduction up-to in a fibrational setting
• Computation of the greatest simulations and bisimulations between fuzzy automata
• EQUIVALENCE OF LABELED MARKOV CHAINS
• Exponential behaviour of the Butkovič-Zimmermann algorithm for solving two-sided linear systems in max-algebra
• Fair Simulation Relations, Parity Games, and State Space Reduction for Büchi Automata
• Forward and backward simulations. I. Untimed Systems
• Generic Forward and Backward Simulations
• Generic Trace Semantics via Coinduction
• Generic forward and backward simulations. II: Probabilistic simulation
• Generic forward and backward simulations. III: Quantitative simulations by matrices
• Handbook of weighted automata
• Maximal traces and path-based coalgebraic temporal logics
• Nominal Kleene coalgebra
• On the average number of steps of the simplex method of linear programming
• Positional strategies for mean payoff games
• Probabilistic anonymity via coalgebraic simulations
• Probabilistic weak simulation is decidable in polynomial time
• Probable innocence revisited
• Quantitative languages
• Simulations in coalgebra
• Sound and complete axiomatizations of coalgebraic language equivalence
• THE CATEGORY OF SIMULATIONS FOR WEIGHTED TREE AUTOMATA
• The complexity of mean payoff games on graphs
• The equality problem for rational series with multiplicities in the tropical semiring is undecidable
• Trace semantics via determinization
• Tropical polyhedra are equivalent to mean payoff games
• Undecidable problems for probabilistic automata of fixed dimension
• Weighted Bisimulation in Linear Algebraic Form
• Weighted automata and weighted logics

Cited in

(7)

• A Backward and a Forward Simulation for Weighted Tree Automata
• Simulations for quantitative alternating transition systems
• Simulations and bisimulations for max-plus automata
• THE CATEGORY OF SIMULATIONS FOR WEIGHTED TREE AUTOMATA
• From qualitative matrices to quantitative restrictions
• Generic forward and backward simulations. III: Quantitative simulations by matrices
• Quantitative fair simulation games

This page was built for publication: Quantitative simulations by matrices

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q729815)