Tata Institute of Fundamental Research
LocPastPDL: An expressively complete logic over Mazurkiewicz traces and its applications to concurrency theory
STCS Student Seminar
Speaker:
Shantanu Kulkarni (IIT Bombay)
Organiser:
Pranshu Gaba, Shibashis Guha
Date:
Friday, 8 Nov 2024, 16:00 to 17:00
Venue:
A-201 (STCS Seminar Room)
(Scan to add to calendar)
Abstract:
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.’
| Speaker: | Shantanu Kulkarni (IIT Bombay) |
| Organiser: | Pranshu Gaba, Shibashis Guha |
| Date: | Friday, 8 Nov 2024, 16:00 to 17:00 |
| Venue: | A-201 (STCS Seminar Room) |
(Scan to add to calendar)
Abstract:
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.’