The field of formal methods and automata theory is currently witnessing significant developments, with a focus on advancing the understanding of behavioral equivalences, synchronisation, and measure-theoretic aspects of languages. Researchers are exploring new notions of equivalences, such as reversible behavioral equivalences, and investigating their decidability. Additionally, there is a growing interest in generalizing traditional automata models, including the introduction of discharging deterministic finite automata and fresh labelled transition systems. These advancements have important implications for the study of formal languages, semantics, and verification. Noteworthy papers in this area include: A paper that improves lower bounds on the length of carefully synchronising words for partial DFAs, simplifying previous constructions and providing new insights into the diameter of transformation semigroups. A paper that introduces a non-wellfounded and labelled sequent calculus for bimodal provability logic, providing a sound and complete system with respect to the semantics. A paper that proposes a logic for fresh labelled transition systems, enabling the expression of properties such as the existence of infinite paths of distinct data values and the violation of taint properties.