Room 206 (2nd floor, badged access)

Room 206 (2nd floor, badged access)

9 September 2022 - 14h00

On an Invariance Problem for Parameterized Concurrent Systems

by Lucas Bueri from 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.