Invited Paper -- Computing the price of anarchy in atomic network congestion games -- FORMATS 2023 Main Track -- Causal Reversibility for Timed Process Calculi with Lazy/Eager Durationless Actions and Time Additivity -- Automata with Timers -- Layered controller synthesis for dynamic multi-agent systems -- On the Susceptibility of QDI Circuits to Transient Faults -- Maximum Satis ability in Mission-time Linear Temporal Logic -- A local-time semantics for negotiations -- Timed non-interference under Partial Observability and Bounded Memory -- Special track on Monitoring of cyber-physical systems Usage- and Risk-aware Falsification Testing for Cyber-Physical Systems -- Model Predictive Runtime Verification for Cyber-Physical Systems with Real-Time Deadlines.