Détails sur le séminaire

Room 206 (2nd floor, badged access)

9 septembre 2022 - 14h00
On an Invariance Problem for Parameterized Concurrent Systems
par Lucas Bueri de Verimag

Abstract: We consider concurrent systems consisting of replicated finite-state
processes that synchronize via joint interactions in a network with
user-defined topology. The system is specified using a resource
logic with a multiplicative connective and inductively defined
predicates, reminiscent of Separation Logic \cite{Reynolds02}. The
problem we consider is if a given formula in this logic defines an
invariant, namely whether any model of the formula, following an
arbitrary firing sequence of interactions, is transformed into
another model of the same formula. This property, called \emph{havoc
invariance}, is quintessential in proving the correctness of
reconfiguration programs that change the structure of the network at
runtime. We show that the havoc invariance problem is many-one
reducible to the entailment problem $\phi \models \psi$, asking if
any model of $\phi$ is also a model of $\psi$. Although, in general,
havoc invariance is found to be undecidable, this reduction allows
to prove that havoc invariance is in \twoexptime, for a general
fragment of the logic, with a \twoexptime\ entailment problem.

This is a MOHYTOS seminar and a rehearsal for the CONCUR 2022 talk.

Contact | Plan du site | Site réalisé avec SPIP 3.2.19 + AHUNTSIC [CC License]

info visites 2140742