arXiv subjects

Viorica Sofronie-Stokkermans

Publications and source records attributed to Viorica Sofronie-Stokkermans.

18 recordsLinked to original sources

arXiv2026

On Constructing Most General Solutions for Parametric Constraints (Extended Preprint)

Let ${\cal T}$ be a theory allowing a form of elimination of existential quantifiers (possibly for formulae in a certain class). We analyze possibilities of constructing (most general) solutions w.r.t.\ ${\cal T}$ for formulae of the form $\exists x_1 \dots \exists x_n ϕ(x_1, \dots, x_n, y_1, \dots, y_m)$, where $ϕ$ is a quantifier-free conjunction of literals in the signature of ${\cal T}$, and the free variables $y_1, \dots, y_m$ are regarded as parameters. We show that in the presence of function symbols which describe ``{\sf if}-{\sf then}-{\sf else}'' constructions in certain models of ${\cal T}$, we can describe the most general solution of such formulae, thus generalizing results about the existence of most general unifiers in discriminator varieties. We illustrate the ideas on examples.

cs.LO↗

arXiv2025

On Symbol Elimination and Uniform Interpolation in Theory Extensions

We define a notion of general uniform interpolant, generalizing the notions of cover and of uniform interpolant and identify situations in which symbol elimination can be used for computing general uniform interpolants. We investigate the limitations of the method we propose, and identify theory extensions for which the computation of general uniform interpolants can be reduced to symbol elimination followed by the computation of uniform quantifier-free interpolants in extensions with uninterpreted function symbols of theories allowing uniform quantifier-free interpolation.

cs.LO↗

arXiv2025

On verification and constraint generation for families of similar hybrid automata

In this paper we give an overview of results on the analysis of parametric linear hybrid automata, and of systems of similar linear hybrid automata: We present possibilities of describing systems with a parametric (i.e. not explicitly specified) number of similar components which can be connected to other systems, such that some parts in the description might be underspecified (i.e. parametric). We consider global safety properties for such systems, expressed by universally quantified formulae, using quantification over variables ranging over the component systems. We analyze possibilities of using methods for hierarchical reasoning and symbol elimination for determining relationships on (some of) the parameters used in the description of these systems under which the global safety properties are guaranteed to be inductive invariants. We discuss an implementation and illustrate its use on several examples.

cs.LO↗

arXiv2023

On the Verification of the Correctness of a Subgraph Construction Algorithm

We automatically verify the crucial steps in the original proof of correctness of an algorithm which, given a geometric graph satisfying certain additional properties removes edges in a systematic way for producing a connected graph in which edges do not (geometrically) intersect. The challenge in this case is representing and reasoning about geometric properties of graphs in the Euclidean plane, about their vertices and edges, and about connectivity. For modelling the geometric aspects, we use an axiomatization of plane geometry; for representing the graph structure we use additional predicates; for representing certain classes of paths in geometric graphs we use linked lists.

cs.LO↗

arXiv2023

On the Verification of Parametric Systems

We present an approach to the verification of systems for whose description some elements - constants or functions - are underspecified and can be regarded as parameters, and, in particular, describe a method for automatically generating constraints on such parameters under which certain safety conditions are guaranteed to hold. We present an implementation and illustrate its use on several examples.

cs.LO↗

arXiv2023

On $P$-Interpolation in Local Theory Extensions and Applications to the Study of Interpolation in the Description Logics ${\cal EL}, {\cal EL}^+$

We study the problem of $P$-interpolation, where $P$ is a set of binary predicate symbols, for certain classes of local extensions of a base theory. For computing the $P$-interpolating terms, we use a hierarchic approach: This allows us to compute the interpolating terms using a method for computing interpolating terms in the base theory. We use these results for proving $\leq$-interpolation in classes of semilattices with monotone operators; we show, by giving a counterexample, that $\leq$-interpolation does not hold if by "shared" symbols we mean just the common symbols. We use these results for the study of $\sqsubseteq$-interpolation in the description logics ${\cal EL}$ and ${\cal EL}^+$.

cs.LO↗

arXiv2021

Symbol Elimination for Parametric Second-Order Entailment Problems (with Applications to Problems in Wireless Network Theory)

We analyze possibilities of second-order quantifier elimination for formulae containing parameters -- constants or functions. For this, we use a constraint resolution calculus obtained from specializing the hierarchical superposition calculus. If saturation terminates, we analyze possibilities of obtaining weakest constraints on parameters which guarantee satisfiability. If the saturation does not terminate, we identify situations in which finite representations of infinite saturated sets exist. We identify situations in which entailment between formulae expressed using second-order quantification can be effectively checked. We illustrate the ideas on a series of examples from wireless network research.

cs.LO↗

arXiv2019

On First-Order Model-Based Reasoning

Reasoning semantically in first-order logic is notoriously a challenge. This paper surveys a selection of semantically-guided or model-based methods that aim at meeting aspects of this challenge. For first-order logic we touch upon resolution-based methods, tableaux-based methods, DPLL-inspired methods, and we give a preview of a new method called SGGS, for Semantically-Guided Goal-Sensitive reasoning. For first-order theories we highlight hierarchical and locality-based methods, concluding with the recent Model-Constructing satisfiability calculus.

cs.AI↗

arXiv2019

Parametric Systems: Verification and Synthesis

In this paper we study possibilities of using hierarchical reasoning, symbol elimination and model generation for the verification of parametric systems, where the parameters can be constants or functions. Our goal is to automatically provide guarantees that such systems satisfy certain safety or invariance conditions. We analyze the possibility of automatically generating such guarantees in the form of constraints on parameters. We illustrate our methods on several examples

cs.LO↗

arXiv2019

On Invariant Synthesis for Parametric Systems

We study possibilities for automated invariant generation in parametric systems. We use (a refinement of) an algorithm for symbol elimination in theory extensions to devise a method for iteratively strengthening certain classes of safety properties to obtain invariants of the system. We identify conditions under which the method is correct and complete, and situations in which the method is guaranteed to terminate. We illustrate the ideas on various examples.

cs.LO↗

arXiv2018

On Interpolation and Symbol Elimination in Theory Extensions

In this paper we study possibilities of interpolation and symbol elimination in extensions of a theory $\mathcal{T}_0$ with additional function symbols whose properties are axiomatised using a set of clauses. We analyze situations in which we can perform such tasks in a hierarchical way, relying on existing mechanisms for symbol elimination in $\mathcal{T}_0$. This is for instance possible if the base theory allows quantifier elimination. We analyze possibilities of extending such methods to situations in which the base theory does not allow quantifier elimination but has a model completion which does. We illustrate the method on various examples.

cs.LO↗

arXiv2016

Decidability of Verification of Safety Properties of Spatial Families of Linear Hybrid Automata

We consider systems composed of an unbounded number of uniformly designed linear hybrid automata, whose dynamic behavior is determined by their relation to neighboring systems. We present a class of such systems and a class of safety properties whose verification can be reduced to the verification of (small) families of neighbouring systems of bounded size, and identify situations in which such verification problems are decidable, resp. fixed parameter tractable. We illustrate the approach with an example from coordinated vehicle guidance, and describe an implementation which allows us to perform such verification tasks automatically.

cs.LO↗

arXiv2013

Locality and applications to subsumption testing and interpolation in $\mathcal{EL}$ and some of its extensions

In this paper we show that subsumption problems in lightweight description logics (such as $\mathcal{EL}$ and $\mathcal{EL}^+$) can be expressed as uniform word problems in classes of semilattices with monotone operators. We use possibilities of efficient local reasoning in such classes of algebras, to obtain uniform PTIME decision procedures for CBox subsumption in $\mathcal{EL}$, $\mathcal{EL}^+$ and extensions thereof. These locality considerations allow us to present a new family of (possibly many-sorted) logics which extend $\mathcal{EL}$ and $\mathcal{EL}^+$ with $n$-ary roles and/or numerical domains. As a by-product, this allows us to show that the algebraic models of ${\cal EL}$ and ${\cal EL}^+$ have ground interpolation and thus that ${\cal EL}$, ${\cal EL}^+$, and their extensions studied in this paper have interpolation. We also show how these ideas can be used for the description logic $\mathcal{EL}^{++}$.

cs.LO↗

arXiv2010

Automatic Verification of Parametric Specifications with Complex Topologies

The focus of this paper is on reducing the complexity in verification by exploiting modularity at various levels: in specification, in verification, and structurally. For specifications, we use the modular language CSP-OZ-DC, which allows us to decouple verification tasks concerning data from those concerning durations. At the verification level, we exploit modularity in theorem proving for rich data structures and use this for invariant checking. At the structural level, we analyze possibilities for modular verification of systems consisting of various components which interact.We illustrate these ideas by automatically verifying safety properties of a case study from the European Train Control System standard, which extends previous examples by comprising a complex track topology with lists of track segments and trains with different routes.

cs.SE↗

arXiv2010

System Description: H-PILoT (Version 1.9)

This system description provides an overview of H-PILoT (Hierarchical Proving by Instantiation in Local Theory extensions), a program for hierarchical reasoning in extensions of logical theories. H-PILoT reduces deduction problems in the theory extension to deduction problems in the base theory. Specialized provers and standard SMT solvers can be used for testing the satisfiability of the formulae obtained after the reduction. For a certain type of theory extension (namely for local theory extensions) this hierarchical reduction is sound and complete and -- if the formulae obtained this way belong to a fragment decidable in the base theory -- H-PILoT provides a decision procedure for testing satisfiability of ground formulae, and can also be used for model generation.

cs.LO↗

arXiv2008

Sheaves and geometric logic and applications to the modular verification of complex systems

In this paper we show that states, transitions and behavior of concurrent systems can often be modeled as sheaves over a suitable topological space. In this context, geometric logic can be used to describe which local properties (i.e. properties of individual systems) are preserved, at a global level, when interconnecting the systems. The main area of application is to modular verification of complex systems. We illustrate the ideas by means of an example involving a family of interacting controllers for trains on a rail track.

cs.LO↗

arXiv2008

Interpolation in local theory extensions

In this paper we study interpolation in local extensions of a base theory. We identify situations in which it is possible to obtain interpolants in a hierarchical manner, by using a prover and a procedure for generating interpolants in the base theory as black-boxes. We present several examples of theory extensions in which interpolants can be computed this way, and discuss applications in verification, knowledge representation, and modular reasoning in combinations of local theories.

cs.LO↗

arXiv2008

On combinations of local theory extensions

In this paper we study possibilities of efficient reasoning in combinations of theories over possibly non-disjoint signatures. We first present a class of theory extensions (called local extensions) in which hierarchical reasoning is possible, and give several examples from computer science and mathematics in which such extensions occur in a natural way. We then identify situations in which combinations of local extensions of a theory are again local extensions of that theory. We thus obtain criteria both for recognizing wider classes of local theory extensions, and for modular reasoning in combinations of theories over non-disjoint signatures.

cs.LO↗