ICE-TCS Lecture Series - Luca Aceto - Decompositional Reasoning about the History of Parallel Processes
The second ICE-TCS talk for this semester will be delivered on Friday, 22 January by Luca Aceto (Reykjavík University). The talk, which is entitled Decompositional Reasoning about the History of Parallel Processes, will be held at 14:00 in room M1.05 at the new premises of Reykjavik University in Nauthólsvík.
Further information about forthcoming ICE- TCS events may be found on the ICE-TCS news page
Abstract
Decompositional reasoning aims at automatically decomposing a global property of a composite system into local properties of (possibly unknown) components.
In concurrency theory, decompositional reasoning techniques date back to the seminal work of Larsen and Liu in the late 1980s and early 1990s. However, we are not aware of any such decomposition technique that applies to reasoning about the ``past history of a computation''. In this talk, I will address this problem and present a decomposition technique for Hennessy-Milner logic with past. In order to highlight the main ideas, as a language for processes, I will use a subset of Milner's CCS with parallel composition, non-deterministic choice, action prefixing and the inaction constant. I will focus on developing decompositional reasoning techniques for parallel contexts in that language.
The talk is based on joint work with Arnar Birgisson (Chalmers), Anna Ingolfsdottir (RU) and Mohammadreza Mousavi (TU Eindhoven)
