The book features a collection of invited talks and regular papers that explore various topics in the field of automata, synthesis, and formal methods. Key discussions include decidability and undecidability results related to probabilistic automata on infinite words, abstraction learning, and the synthesis of words and traces. The complexity of codiagnosability in discrete event and timed systems, as well as methods for knowledge-based control of distributed systems, are examined. The work also delves into reachability analyses of hybrid systems, scenario synchronization, and compositional algorithms for LTL synthesis. Additional topics cover the convergence of steady-state probabilities in closed fork-join networks, lattice-valued binary decision diagrams, and a specification logic for exceptions. Techniques for non-monotonic refinement of control abstraction in concurrent programs, class testing from contracts, and efficient emptiness checks for timed Büchi automata are also presented. The book addresses reachability as derivability, automatic generation of access control from information flow specifications, and auxiliary constructs for proving liveness in discrete systems. Finally, it introduces various tools for model checking, automated analysis, and software synthesis, including GAVS, CRI, MCGP, ECDAR, and Rbminer.
