eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2022-09-06
24:1
24:16
10.4230/LIPIcs.CONCUR.2022.24
article
On an Invariance Problem for Parameterized Concurrent Systems
Bozga, Marius
1
Bueri, Lucas
1
Iosif, Radu
1
Univ. Grenoble Alpes, CNRS, Grenoble INP, VERIMAG, 38000, France
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 [John C. Reynolds, 2002]. 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 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 ϕ ⊧ ψ, asking if any model of ϕ is also a model of ψ. Although, in general, havoc invariance is found to be undecidable, this reduction allows to prove that havoc invariance is in 2EXP, for a general fragment of the logic, with a 2EXP entailment problem.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol243-concur2022/LIPIcs.CONCUR.2022.24/LIPIcs.CONCUR.2022.24.pdf
parameterized verification
invariant checking
resource logics
reconfigurable systems
tree automata