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 woexptime, for a general
fragment of the logic, with a woexptime entailment problem.
This is a MOHYTOS seminar and a rehearsal for the CONCUR 2022 talk.
