When are two Parametric Semi-linear Sets Equal?

In a recent work, we considered a version of Presburger arithmetic enriched by special variables, called parameters, which can be multiplied as if they were constants, but cannot be quantified in the same way as normal variables. Emulating the notion of semi-linear sets from Presburger arithmetic, we defined parametric semi-linear sets, functions which, given a valuation of the parameters, produce a semi-linear set. Given two parametric semi-linear set, our main problem was to decide whether there exists parameter valuations such that the two produced sets are equal. We showed that, unfortunately, this test is undecidable in general, as the parameters can be used to encode any multivariate polynomial. Moreover this undecidability holds even with strong restrictions on the degree of the polynomials in the parameters involved in the formula. Finally, we showed that under the additional restriction of using a single parameter, one can compute the set of parameter values achieving equality of the two sets. At Highlights, we intend to present this result through an application to the opacity of one-clock timed automata.

Authors

• Engel Lefaucheux

Keywords

No keywords are indexed for this paper.