This talk is based on our work in LiCS 2024: https://dl.acm.org/doi/abs/10.1145/3661814.3662110. In the talk I will first introduce the setting of concurrent computation via asynchronous automata on Mazurkiewikz traces, I will then get into the syntax and semantics of our logic “LocPastPDL”. I will talk about its applications for formal verification of concurrent systems and for proving a Krohn-Rhodes style decomposition theorem for regular languages over Mazurkiewicz traces. Finally if time permits I will go into the proof sketch of our main result which is ‘LocPastPDL is expressively complete with respect to regular trace languages.’
