Up-To Techniques for Weighted Systems

DOI10.1007/978-3-662-54577-5_31MaRDI QIDQ3303913zbMATH OpenOpenAlexFDO

Authors Filippo Bonchi, Barbara König, Sebastian Küpper

Publication date 5 August 2020

Published in Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

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

zbMATH Keywords

normal formweighted automatoncongruence closuredeterminized automatonweighted system

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Grammars and rewriting systems (68Q42) Algebraic theory of languages and automata (68Q70)

Abstract: We show how up-to techniques for (bi-)similarity can be used in the setting of weighted systems. The problems we consider are language equivalence, language inclusion and the threshold problem (also known as universality problem) for weighted automata. We build a bisimulation relation on the fly and work up-to congruence and up-to similarity. This requires to determine whether a pair of vectors (over a semiring) is in the congruence closure of a given relation of vectors. This problem is considered for rings and l-monoids, for the latter we provide a rewriting algorithm and show its confluence and termination. We then explain how to apply these up-to techniques to weighted automata and provide runtime results.

Recommendations

• Weighted systems of equations
• Systems with weighted components
• scientific article; zbMATH DE number 1150272
• Multivalued dynamic systems with weights
• Weighted models for higher-order computation
• Publication:4946087
• Weight functions method in stability study of systems
• On the linearization of weighted T-systems
• Parametric verification of weighted systems
• Applications of the methods of weighted residuals in system science

Cites work

• scientific article; zbMATH DE number 42752 (Why is no real title available?)
• scientific article; zbMATH DE number 1142316 (Why is no real title available?)
• scientific article; zbMATH DE number 2040327 (Why is no real title available?)
• A coalgebraic perspective on linear weighted automata
• A generalized partition refinement algorithm, instantiated to language equivalence checking for weighted automata
• Antichain algorithms for finite automata
• Antichains: A New Algorithm for Checking Universality of Finite Automata
• Checking NFA equivalence with bisimulations up to congruence
• Coinduction up-to in a fibrational setting
• Conjugacy and Equivalence of Weighted Automata and Functional Transducers
• Enhanced coalgebraic bisimulation
• Enhancements of the bisimulation proof method
• Equational theories of tropical semirings
• Funayama's theorem revisited
• Generic forward and backward simulations. III: Quantitative simulations by matrices
• Methods and applications of (,+) linear algebra
• On Shostak's decision procedure for combinations of theories
• THE EQUALITY PROBLEM FOR RATIONAL SERIES WITH MULTIPLICITIES IN THE TROPICAL SEMIRING IS UNDECIDABLE
• Weighted Bisimulation in Linear Algebraic Form
• What's decidable about weighted automata?
• When simulation meets antichains. (On checking language inclusion of nondeterministic finite (tree) automata)

Cited in

(7)

• Bisimulation and coinduction enhancements: a historical perspective
• Up-to techniques for behavioural metrics via fibrations
• PAWS: a tool for the analysis of weighted systems
• Up-to techniques for behavioural metrics via fibrations
• (In)finite trace equivalence of probabilistic transition systems
• Graded monads and behavioural equivalence games
• Systems with weighted components

This page was built for publication: Up-To Techniques for Weighted Systems

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