We study prefix-dependent congruences for random deterministic transition systems with state outputs. In this setting, the admissible continuations used to compare two states may depend on the observed prefix, and two states are identified only if no common admissible continuation distinguishes their future outputs. The framework includes probabilistic deterministic finite automata as a motivating special case. We analyze the random transition model in which all transition values are independent and uniform. Each state is also assigned an independent label that specifies both its output and its set of admissible symbols. If two independent labels agree with probability strictly less than one, and every label has at least three admissible symbols, then the induced congruence is trivial with high probability. The proof combines a pruning process on pairs, a collision-free exploration controlling its early evolution, and a first-moment argument showing that the remaining pairs cannot organize into nontrivial equivalence classes.

We present the AL*RTA algorithm for learning alternating real-time automata (ARTAs) using membership and equivalence queries. AL*RTA combines ideas from AL*for learning alternating finite automata and NL*RTA for learning nondeterministic real-time automata. We first define ARTAs and show that alternation improves succinctness, although it does not increase expressive power. We then present AL*RTA and show its termination. Our empirical evaluation suggests that AL*RTA generally learns smaller automata than NL*RTA at the cost of more queries.

Hypergraphic automata are automata whose state sets and output symbol sets are hypergraphs invariant under the actions of the transition and output functions. Universally attracting objects in the category of such automata are called universal hypergraphic automata; their semigroups of input symbols are algebras of mappings whose properties are tightly linked to the algebraic structure of the automata themselves. This paper establishes a complete characterisation of epimorphisms of universal hypergraphic automata and of their semigroups of input symbols. A central contribution is the introduction of two distinct notions of epimorphism for hypergraphs including weak, strong and the proof that these notions diverge in general but necessarily coincide for the important subclass of $p^*$-hypergraphs, which includes automata whose state hypergraphs and output hypergraphs are projective or affine planes. The main results give necessary and sufficient conditions for a triple $(f, \mathbb{P}_s, g)$ to be an epimorphism of universal hypergraphic automata, expressed in terms of the component maps on the state and output hypergraphs.

In this paper, we systematically investigate the connection between linearizable objects and forward simulation. We prove that the sets of linearizable objects satisfying wait-freedom (resp., lock-freedom or obstruction-freedom) form a bounded join-semilattice under the forward simulation relation, and that the sets of linearizable objects without liveness constraints form a bounded lattice under the same relation. Thus, forward simulation is not only a proof technique for linearizability but also induces an algebraic hierarchy of linearizable objects. As part of our lattice result, we propose an equivalent characterization of linearizability by reducing checking linearizability w.r.t. sequential specification $Spec$ into checking forward simulation w.r.t. a wait-free universal construction $\mathcal{U}_{Spec}^{WF}$. We also propose an object $\mathcal{U}_{Spec}^s$, which simplifies $\mathcal{U}_{Spec}^{WF}$ and is more suitable for verification. We prove that the Herlihy-Wing queue is simulated by $\mathcal{U}_{Queue}^s$ with $Queue$ the sequential specification of the queue. Thus, our object $\mathcal{U}_{Spec}^s$ can be used in the verification of linearizability. To demonstrate the forward simulation relation between concrete linearizable objects, we prove that the time-stamped queue simulates the Herlihy-Wing queue, while the Herlihy-Wing queue cannot simulate the time-stamped queue. All these three proofs have been machine-verified by Isabelle/HOL.