Lower bounds provide essential insights into the minimal computational resources required for algorithm execution. This paper focuses on logical theories, a domain where estimating resources is particularly difficult, and provides a novel, fully-automated method for computing lower bounds on memory usage, serving as a proxy for the computational resources required to perform logical reasoning. Specifically, the paper focuses on computing lower bounds on the size of the minimal deterministic finite automaton that encodes the solution set of a given Presburger arithmetic (also known as linear integer arithmetic) formula. The lower bounds are accompanied by independently verifiable certificates which also support a union-like operation that can be used to increase the computed bounds.We conducted an extensive empirical evaluation of our method using over 5 000 formulae from the quantifier-free fragment of Presburger arithmetic, sourced from the SMT-LIB repository. The results show that our method often produces lower bounds that are close to the actual size of the minimal deterministic finite automaton. Moreover, it succeeds in computing non-trivial bounds even for instances that are out of reach (by several orders of magnitude) for the existing state-of-the-art automata-based tools for solving Presburger arithmetic.

We propose an automated procedure to prove polyhedral abstractions (also known as polyhedral reductions) for Petri nets. Polyhedral abstraction is a new type of state space equivalence, between Petri nets, based on the use of linear integer constraints between the marking of places. In addition to defining an automated proof method, this paper aims to better characterize polyhedral reductions, and to give an overview of their application to reachability problems. Our approach relies on encoding the equivalence problem into a set of SMT formulas whose satisfaction implies that the equivalence holds. The difficulty, in this context, arises from the fact that we need to handle infinite-state systems. For completeness, we exploit a connection with a class of Petri nets, called flat nets, that have Presburger-definable reachability sets. We have implemented our procedure, and we illustrate its use on several examples.

Abstract We propose a semi-decision procedure for checking generalized reachability properties, on generalized Petri nets, that is based on the Property Directed Reachability (PDR) method. We actually define three different versions, that vary depending on the method used for abstracting possible witnesses, and that are able to handle problems of increasing difficulty. We have implemented our methods in a model-checker called SMPT and give empirical evidences that our approach can handle problems that are difficult or impossible to check with current state of the art tools.

We define a new method for taking advantage of net reductions in combination with a SMT-based model checker. Our approach consists in transforming a reachability problem about some Petri net, into the verification of an updated reachability property on a reduced version of this net. This method relies on a new state space abstraction based on systems of constraints, called polyhedral abstraction. We prove the correctness of this method using a new notion of equivalence between nets. We provide a complete framework to define and check the correctness of equivalence judgements; prove that this relation is a congruence; and give examples of basic equivalence relations that derive from structural reductions. Our approach has been implemented in a tool, named SMPT, that provides two main procedures: Bounded Model Checking (BMC) and Property Directed Reachability (PDR). Each procedure has been adapted in order to use reductions and to work with arbitrary Petri nets. We tested SMPT on a large collection of queries used in the Model Checking Contest. Our experimental results show that our approach works well, even when we only have a moderate amount of reductions.