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

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.

From generic partition refinement to weighted tree automata minimization

Partition 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.

Finite Characterization of the Coarsest Balanced Coloring of a Network

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].

Aggregation-based minimization of finite state automata

We 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.

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

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].