We present an executable rewriting logic semantics for the Lingua Franca (LF) coordination language for cyber-physical systems developed at UC Berkeley. Our semantics enables automatic formal analysis of LF programs using Maude and Real-Time Maude. We capture the intended “logical-time” semantics of LF, which gives us correct analysis that is also magnitudes faster than other verification approaches for LF, which are based on an interleaving semantics. We capture larger subsets of LF than those other approaches, and support all analysis methods provided by them. Benchmarking on the LF Verifier benchmark suite shows that our analyses drastically outperform those of LF Verifier. We have also extended the LF compiler to automatically generate a Maude model from an LF program and to perform the desired analysis.