A generalized partition refinement algorithm, instantiated to language equivalence checking for weighted automata

2016 ◽  
Vol 22 (4) ◽  
pp. 1103-1120 ◽  
Author(s):  
Barbara König ◽  
Sebastian Küpper
Keyword(s):  
Equivalence Checking ◽  
Weighted Automata ◽  
Language Equivalence ◽  
Generalized Partition ◽  
Refinement Algorithm ◽  
Partition Refinement

scholarly journals Aggregation-based minimization of finite state automata

2020 ◽  
Author(s):  
Johanna Björklund ◽  
Loek Cleophas
Keyword(s):  
Finite State Automata ◽  
Transition Graph ◽  
Solution Approach ◽  
Computation Process ◽  
Finite State ◽  
Language Equivalence ◽  
Derivatives Of ◽  
Optimisation Techniques ◽  
Refinement Algorithm ◽  
Partition Refinement

AbstractWe present a minimization algorithm for non-deterministic finite state automata that finds and merges bisimulation-equivalent states. The bisimulation relation is computed through partition aggregation, in contrast to existing algorithms that use partition refinement. The algorithm simultaneously generalises and simplifies an earlier one by Watson and Daciuk for deterministic devices. We show the algorithm to be correct and run in time $$ O \left( n^2 r^2 \left| \varSigma \right| \right) $$On2r2Σ, where n is the number of states of the input automaton $$M$$M, r is the maximal out-degree in the transition graph for any combination of state and input symbol, and $$\left| \varSigma \right| $$Σ is the size of the input alphabet. The algorithm has a higher time complexity than derivatives of Hopcroft’s partition-refinement algorithm, but represents a promising new solution approach that preserves language equivalence throughout the computation process. Furthermore, since the algorithm essentially computes the maximal model of a logical formula derived from $$M$$M, optimisation techniques from the field of model checking become applicable.

Finite Characterization of the Coarsest Balanced Coloring of a Network

2020 ◽  
Vol 30 (14) ◽  
pp. 2050212
Author(s):  
Ian Stewart
Keyword(s):  
Graph Theory ◽  
Adjacency Matrix ◽  
Universal Cover ◽  
Running Time ◽  
Set Up ◽  
Balanced Coloring ◽  
Refinement Algorithm ◽  
Partition Refinement

Balanced colorings of networks correspond to flow-invariant synchrony spaces. It is known that the coarsest balanced coloring is equivalent to nodes having isomorphic infinite input trees, but this condition is not algorithmic. We provide an algorithmic characterization: two nodes have the same color for the coarsest balanced coloring if and only if their [Formula: see text]th input trees are isomorphic, where [Formula: see text] is the number of nodes. Here [Formula: see text] is the best possible. The proof is analogous to that of Leighton’s theorem in graph theory, using the universal cover of the network and the notion of a symbolic adjacency matrix to set up a partition refinement algorithm whose output is the coarsest balanced coloring. The running time of the algorithm is cubic in [Formula: see text].

scholarly journals Checking for Open Bisimilarity in the pi-Calculus

2001 ◽  
Vol 8 (8) ◽  
Author(s):  
Ulrik Frendrup ◽  
Jesper Nyholm Jensen
Keyword(s):  
User Interface ◽  
Iterative Method ◽  
Time Complexity ◽  
Source Code ◽  
Performance Tests ◽  
Running Time ◽  
Pi Calculus ◽  
Definition Of ◽  
Refinement Algorithm ◽  
Partition Refinement

<p>This paper deals with algorithmic checking of open bisimilarity in the pi-calculus. Most bisimulation checking algorithms are based on the partition refinement approach. Unfortunately the definition of open bisimulation does not permit us to use a partition refinement approach for open bisimulation checking directly, but in the paper 'A Partition Refinement Algorithm for the pi-Calculus' Marco Pistore and Davide Sangiorgi present an iterative method that makes it possible to check for open bisimilarity using partition refinement. We have implemented the algorithm presented by Marco Pistore and Davide Sangiorgi. Furthermore,<br />we have optimized this algorithm and implemented this optimized algorithm. The time-complexity of this algorithm is the same as the time-complexity for the first algorithm, but performance tests have shown that in many cases the running time of the optimized algorithm is shorter than the running time of the first algorithm. Our implementation of the optimized open bisimulation checker algorithm and a user interface have been integrated in a system called the OBC Workbench.The source code and a manual for it is available from http://www.cs.auc.dk/research/FS/ny/PR-pi/.</p>

scholarly journals A Partition Refinement Algorithm for the π-Calculus

2001 ◽  
Vol 164 (2) ◽  
pp. 264-321 ◽  
Author(s):  
Marco Pistore ◽  
Davide Sangiorgi
Keyword(s):  
Π Calculus ◽  
Refinement Algorithm ◽  
Partition Refinement

scholarly journals From generic partition refinement to weighted tree automata minimization

2021 ◽  
Author(s):  
Thorsten Wißmann ◽  
Hans-Peter Deifel ◽  
Stefan Milius ◽  
Lutz Schröder
Keyword(s):  
Tree Automata ◽  
Weighted Tree ◽  
Transition Systems ◽  
Run Time Analysis ◽  
Deterministic Automata ◽  
Weighted Tree Automata ◽  
Run Time ◽  
The Given ◽  
Refinement Algorithm ◽  
Partition Refinement

AbstractPartition refinement is a method for minimizing automata and transition systems of various types. Recently, we have developed a partition refinement algorithm that is generic in the transition type of the given system and matches the run time of the best known algorithms for many concrete types of systems, e.g. deterministic automata as well as ordinary, weighted, and probabilistic (labelled) transition systems. Genericity is achieved by modelling transition types as functors on sets, and systems as coalgebras. In the present work, we refine the run time analysis of our algorithm to cover additional instances, notably weighted automata and, more generally, weighted tree automata. For weights in a cancellative monoid we match, and for non-cancellative monoids such as (the additive monoid of) the tropical semiring even substantially improve, the asymptotic run time of the best known algorithms. We have implemented our algorithm in a generic tool that is easily instantiated to concrete system types by implementing a simple refinement interface. Moreover, the algorithm and the tool are modular, and partition refiners for new types of systems are obtained easily by composing pre-implemented basic functors. Experiments show that even for complex system types, the tool is able to handle systems with millions of transitions.

scholarly journals DEL-based Epistemic Planning for Human-Robot Collaboration: Theory and Implementation

2021 ◽  
Author(s):  
Thomas Bolander ◽  
Lasse Dissing ◽  
Nicolai Herrmann
Keyword(s):  
Theory Of Mind ◽  
Epistemic Logic ◽  
Autonomous Robots ◽  
Dynamic Epistemic Logic ◽  
Epistemic States ◽  
Planning Algorithm ◽  
Implicit Coordination ◽  
Human Robot Collaboration ◽  
Refinement Algorithm ◽  
Partition Refinement

Epistemic planning based on Dynamic Epistemic Logic (DEL) allows agents to reason and plan from the perspective of other agents. The framework of DEL-based epistemic planning thereby has the potential to represent significant aspects of Theory of Mind in autonomous robots, and to provide a foundation for human-robot collaboration in which coordination is achieved implicitly through perspective shifts. In this paper, we build on previous work in epistemic planning with implicit coordination. We introduce a new notion of indistinguishability between epistemic states based on bisimulation, and provide a novel partition refinement algorithm for computing unique representatives of sets of indistinguishable states. We provide an algorithm for computing implicitly coordinated plans using these new constructs, embed it in a perceive-plan-act agent loop, and implement it on a robot. The planning algorithm is benchmarked against an existing epistemic planning algorithm, and the robotic implementation is demonstrated on human-robot collaboration scenarios requiring implicit coordination.

scholarly journals Equivalence checking for weak bi-Kleene algebra

2021 ◽  
Vol Volume 17, Issue 3 ◽  
Author(s):  
Tobias Kappé ◽  
Paul Brunet ◽  
Bas Luttik ◽  
Alexandra Silva ◽  
Fabio Zanasi
Keyword(s):  
Decision Procedure ◽  
Equivalence Checking ◽  
Operational Model ◽  
Kleene Algebra ◽  
Single Thread ◽  
Rational Expressions ◽  
Language Equivalence

Pomset automata are an operational model of weak bi-Kleene algebra, which describes programs that can fork an execution into parallel threads, upon completion of which execution can join to resume as a single thread. We characterize a fragment of pomset automata that admits a decision procedure for language equivalence. Furthermore, we prove that this fragment corresponds precisely to series-rational expressions, i.e., rational expressions with an additional operator for bounded parallelism. As a consequence, we obtain a new proof that equivalence of series-rational expressions is decidable.

scholarly journals Improved algorithms for computing the greatest right and left invariant Boolean matrices and their application

Filomat ◽  
2019 ◽  
Vol 33 (9) ◽  
pp. 2809-2831
Author(s):  
Stefan Stanimirovic ◽  
Aleksandar Stamenkovic ◽  
Miroslav Ciric
Keyword(s):  
Computational Linguistics ◽  
Zero Divisor ◽  
Matrix Equations ◽  
Weighted Automata ◽  
Idempotent Semirings ◽  
Quasi Order ◽  
Invariant Matrices ◽  
Partition Refinement

We define right and left invariant matrices as Boolean matrices that are solutions to certain systems of matrix equations and inequalities over additively idempotent semirings. We provide improved algorithms for computing the greatest right and left invariant equivalence and quasi-order matrices. The improvements are based on the usage of the well-known partition refinement technique. Afterwards, we present the application of right invariant matrices in the determinization of weighted automata over additively idempotent, commutative and zero-divisor free semirings. In particular, we provide improvements of the well-known determinization method of weighted automata over tropical semirings given by Mohri [Computational Linguistics 23 (2) (1997) 269-311].

A General Vertex Partition Refinement Algorithm for Graph Isomorphism

2013 ◽  
Vol 760-762 ◽  
pp. 1919-1924 ◽  
Author(s):  
Ai Min Hou ◽  
Chuan Fu Hu ◽  
Zhi Feng Hao
Keyword(s):  
Time Complexity ◽  
Polynomial Algorithm ◽  
Graph Isomorphism ◽  
Vertex Partition ◽  
Refinement Algorithm ◽  
Partition Refinement

A general depth-first backtracking algorithm for graph isomorphism with the vertex partition and refinement technique is presented in this paper. The time complexity of this nondeterministic polynomial algorithm is O(nα+3) where nα is the number of backtracking points and (h-1)/2α (h+1)/2 for h=logn in the worst cases. The tests on many types of graphs validated the efficiency of this algorithm for graph isomorphism.

Sign in / Sign up

Export Citation Format

Share Document