Efficient Coalgebraic Partition Refinement

DOI10.4230/LIPICS.CONCUR.2017.32zbMATH Open1442.68112arXiv1705.08362OpenAlexW2963074164MaRDI QIDQ5111646FDOQ5111646

Ulrich Dorsch, Stefan Milius, Lutz Schröder, Thorsten Wißmann

Publication date: 27 May 2020

Abstract: We present a generic partition refinement algorithm that quotients coalgebraic systems by behavioural equivalence, an important task in reactive verification; coalgebraic generality implies in particular that we cover not only classical relational systems but also various forms of weighted systems. Under assumptions on the type functor that allow representing its finite coalgebras in terms of nodes and edges, our algorithm runs in time $mathcalO(mcdotlogn)$ where $n$ and $m$ are the numbers of nodes and edges, respectively. Instances of our generic algorithm thus match the runtime of the best known algorithms for unlabelled transition systems, Markov chains, and deterministic automata (with fixed alphabets), and improve the best known algorithms for Segala systems.

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

zbMATH Keywords

Markov chainscoalgebratransition systemspartition refinement

Mathematics Subject Classification ID

Computational methods in Markov chains (60J22) Formal languages and automata (68Q45) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87) Analysis of algorithms (68W40) Abstract data types; algebraic specification (68Q65) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Cites Work

• Universal coalgebra: A theory of systems
• Bisimulation for labelled Markov processes
• Structural Operational Semantics for Weighted Transition Systems
• Title not available (Why is that?)
• Title not available (Why is that?)
• On the final sequence of a finitary set functor
• Bisimulation through probabilistic testing
• Three Partition Refinement Algorithms
• A calculus of communicating systems
• Deciding bisimilarity and similarity for probabilistic processes.
• Bisimulation relations for weighted automata
• Modular algorithms for heterogeneous modal logics via multi-sorted coalgebra
• Title not available (Why is that?)
• Bisimulation Minimisation Mostly Speeds Up Probabilistic Model Checking
• CCS expressions, finite state processes, and three problems of equivalence
• Optimal state-space lumping in Markov chains
• Simple O(m logn) Time Markov Chain Lumping
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Re-describing an algorithm by Hopcroft
• A hierarchy of probabilistic system types
• Monoid-labeled transition systems
• An efficient algorithm for computing bisimulation equivalence
• Generalizing the Paige-Tarjan algorithm by abstract interpretation
• Describing an algorithm by Hopcroft
• Bisimilarity Minimization in O(m logn) Time
• Bisimulation minimization and symbolic model checking
• Flow Faster: Efficient Decision Algorithms for Probabilistic Simulations
• A distributed algorithm for strong bisimulation reduction of state spaces
• Formal verification of timed properties of randomized distributed algorithms
• Introduction to coalgebra. Towards mathematics of states and observation
• Generic Partition Refinement Algorithms for Coalgebras and an Instantiation to Weighted Automata

Cited In (11)

• Lumpability for uncertain continuous-time Markov chains
• Probabilistic mediator: a coalgebraic perspective
• A (co)algebraic theory of succinct automata
• From generic partition refinement to weighted tree automata minimization
• Minimality Notions via Factorization Systems and Examples
• Generic Partition Refinement Algorithms for Coalgebras and an Instantiation to Weighted Automata
• Title not available (Why is that?)
• Quasilinear-time Computation of Generic Modal Witnesses for Behavioural Inequivalence
• Explicit Hopcroft's trick in categorical partition refinement
• Distributed coalgebraic partition refinement
• Generic partition refinement and weighted tree automata

   Recommendations

• Title not available (Why is that?) 👍 👎
• Generic Partition Refinement Algorithms for Coalgebras and an Instantiation to Weighted Automata 👍 👎
• Exploiting parallelism in coalgebraic logic programming 👍 👎
• Coalgebraic semantics for parallel derivation strategies in logic programming 👍 👎
• Enhanced coalgebraic bisimulation 👍 👎
• Coalgebras in functional programming and type theory 👍 👎
• An efficient Coq tactic for deciding Kleene algebras 👍 👎
• A partition refinement algorithm for the \(\pi\)-calculus 👍 👎
• Coalgebraic Components in a Many-Sorted Microcosm 👍 👎
• Transposing partial components--an exercise on coalgebraic refinement 👍 👎

This page was built for publication: Efficient Coalgebraic Partition Refinement

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