le prochaine seminaire PPS est
le Jeudi 3 Juin, 11h salle 3E91
Silvia Crafa (Padova)
A Logic for True Concurrency
(joint work with Paolo Baldan)
We propose a logic for true concurrency whose formulae predicate about
events in computations and their causal dependencies. The induced logical
equivalence is hereditary history preserving bisimilarity, and fragments
of the logic can be identified which correspond to other true concurrent
behavioural equivalences in the literature: step, pomset and history
preserving bisimilarity. Standard Hennessy-Milner logic, thus
(interleaving) bisimilarity, is also recovered as a fragment. We believe
that this contributes to a rational presentation of the true concurrent
spectrum and to a deeper understanding of the relations between the
involved behavioural equivalences.
