LFCS Seminar: Wednesday, 30 October - Safa Zouari Title: Bisimulations and Logics for Higher-Dimensional Automata Abstract: Higher-dimensional automata (HDAs) are models of non-interleaving concurrency for analyzing concurrent systems. There is a rich literature that deals with bisimulations for concurrent systems, and some of them have been extended to HDAs. However, no logical characterizations of these relations are currently available for HDAs. In this work, we address this gap by introducing Ipomset modal logic, a Hennessy-Milner type logic over HDAs, and show that it characterizes Path-bisimulation, a variant of the standard ST-bisimulation. We also define a notion of Cell-bisimulation, using the open-maps framework of Joyal, Nielsen, and Winskel, and establish the relationship between these bisimulations (and also their "strong" variants, which take restrictions into account). In our work, we rely on the new categorical definition of HDAs as presheaves over concurrency lists and on track objects. Oct 30 2024 16.10 - 17.10 LFCS Seminar: Wednesday, 30 October - Safa Zouari Safa Zouari, Norwegian University of Science and Technology https://www.ntnu.edu/employees/safaz IF G.03 Note: unusual day!
LFCS Seminar: Wednesday, 30 October - Safa Zouari Title: Bisimulations and Logics for Higher-Dimensional Automata Abstract: Higher-dimensional automata (HDAs) are models of non-interleaving concurrency for analyzing concurrent systems. There is a rich literature that deals with bisimulations for concurrent systems, and some of them have been extended to HDAs. However, no logical characterizations of these relations are currently available for HDAs. In this work, we address this gap by introducing Ipomset modal logic, a Hennessy-Milner type logic over HDAs, and show that it characterizes Path-bisimulation, a variant of the standard ST-bisimulation. We also define a notion of Cell-bisimulation, using the open-maps framework of Joyal, Nielsen, and Winskel, and establish the relationship between these bisimulations (and also their "strong" variants, which take restrictions into account). In our work, we rely on the new categorical definition of HDAs as presheaves over concurrency lists and on track objects. Oct 30 2024 16.10 - 17.10 LFCS Seminar: Wednesday, 30 October - Safa Zouari Safa Zouari, Norwegian University of Science and Technology https://www.ntnu.edu/employees/safaz IF G.03 Note: unusual day!
Oct 30 2024 16.10 - 17.10 LFCS Seminar: Wednesday, 30 October - Safa Zouari Safa Zouari, Norwegian University of Science and Technology https://www.ntnu.edu/employees/safaz
