Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top

2011 | Book

Tailoring Temporal Description Logics for Reasoning over Temporal Conceptual Models Read chapter Read first chapter

Frontiers of Combining Systems

8th International Symposium, FroCoS 2011, Saarbrücken, Germany, October 5-7, 2011. Proceedings

Editors: Cesare Tinelli, Viorica Sofronie-Stokkermans

Publisher: Springer Berlin Heidelberg

Book Series : Lecture Notes in Computer Science

Part of: Springer Professional "Wirtschaft+Technik" , Springer Professional "Technik" , Springer Professional "Wirtschaft"

Login to get access
insite
SEARCH

About this book

This book constitutes the refereed proceedings of the 8th International Symposium on Frontiers of Combining Systems, FroCoS 2011, held in Saarbrücken, Germany, in October 2011. The 15 revised full papers presented together with three invited papers were carefully reviewed and selected from 22 submissions. The event builds a common forum for research activities in the general area of combination, modularization and integration of systems, with emphasis on logic-based ones, and of their practical use.

Table of Contents

Frontmatter

Invited Papers

Tailoring Temporal Description Logics for Reasoning over Temporal Conceptual Models
Abstract
Temporal data models have been used to describe how data can evolve in the context of temporal databases. Both the Extended Entity-Relationship (EER) model and the Unified Modelling Language (UML) have been temporally extended to design temporal databases. To automatically check quality properties of conceptual schemas various encoding to Description Logics (DLs) have been proposed in the literature. On the other hand, reasoning on temporally extended DLs turn out to be too complex for effective reasoning ranging from 2ExpTime up to undecidable languages. We propose here to temporalize the ‘light-weight’ DL-Lite logics obtaining nice computational results while still being able to represent various constraints of temporal conceptual models. In particular, we consider temporal extensions of \(\ensuremath{\textsl{DL-Lite}_\textit{bool}}^\mathcal{N}\), which was shown to be adequate for capturing non-temporal conceptual models without relationship inclusion, and its fragment \(\smash{\ensuremath{\textsl{DL-Lite}_\textit{core}}^\mathcal{N}}\) with most primitive concept inclusions, which are nevertheless enough to represent almost all types of atemporal constraints (apart from covering).
Alessandro Artale, Roman Kontchakov, Vladislav Ryzhikov, Michael Zakharyaschev
Automatic Proof and Disproof in Isabelle/HOL
Abstract
Isabelle/HOL is a popular interactive theorem prover based on higher-order logic. It owes its success to its ease of use and powerful automation. Much of the automation is performed by external tools: The metaprover Sledgehammer relies on resolution provers and SMT solvers for its proof search, the counterexample generator Quickcheck uses the ML compiler as a fast evaluator for ground formulas, and its rival Nitpick is based on the model finder Kodkod, which performs a reduction to SAT. Together with the Isar structured proof format and a new asynchronous user interface, these tools have radically transformed the Isabelle user experience. This paper provides an overview of the main automatic proof and disproof tools.
Jasmin Christian Blanchette, Lukas Bulwahn, Tobias Nipkow
Size-Change Termination and Satisfiability for Linear-Time Temporal Logics
Abstract
In the automata-theoretic framework, finite-state automata are used as a machine model to capture the operational content of temporal logics. Decision problems like satisfiability, subsumption, equivalence, etc. then translate into questions on automata like emptiness, inclusion, language equivalence, etc. Linear-time temporal logics like LTL, PSL and the linear-time μ-calculus have relatively simple translations into alternating parity automata, and this automaton model is closed under all Boolean operations with very simple constructions. Thus, the typical decision problems for such linear-time temporal logics reduce relatively simply to the emptiness problem for alternating parity automata. In this paper we present a method for decision this emptiness problem without going through intermediate automaton models like nondeterministic ones. The method is a direct adaptation of the size-change termination principle which was orgininally used to decide termination of abstract functional programs.
Martin Lange

Contributed Papers

Combining Theories: The Ackerman and Guarded Fragments
Abstract
Combination of decision procedures is at the heart of Satisfiability Modulo Theories (SMT) solvers. It provides ways to compose decision procedures for expressive languages which mix symbols from various decidable theories. Typical combinations include (linear) arithmetic, uninterpreted symbols, arrays operators, etc. In [7] we showed that any first-order theory from the Bernays-Schönfinkel-Ramsey fragment, the two variable fragment, or the monadic fragment can be combined with virtually any other decidable theory. Here, we complete the picture by considering the Ackermann fragment, and several guarded fragments. All theories in these fragments can be combined with other decidable (combinations of) theories, with only minor restrictions. In particular, it is not required for these other theories to be stably-infinite.
Carlos Areces, Pascal Fontaine
On the Undecidability of Fuzzy Description Logics with GCIs and Product T-norm
Abstract
The combination of Fuzzy Logics and Description Logics (DLs) has been investigated for at least two decades because such fuzzy DLs can be used to formalize imprecise concepts. In particular, tableau algorithms for crisp Description Logics have been extended to reason also with their fuzzy counterparts. Recently, it has been shown that, in the presence of general concept inclusion axioms (GCIs), some of these fuzzy DLs actually do not have the finite model property, thus throwing doubt on the correctness of tableau algorithm for which it was claimed that they can handle fuzzy DLs with GCIs.
In a previous paper, we have shown that these doubts are indeed justified, by proving that a certain fuzzy DL with product t-norm and involutive negation is undecidable. In the present paper, we show that undecidability also holds if we consider a t-norm-based fuzzy DL where disjunction and involutive negation are replaced by the constructor implication, which is interpreted as the residuum. The only condition on the t-norm is that it is a continuous t-norm “starting” with the product t-norm, which covers an uncountable family of t-norms.
Franz Baader, Rafael Peñaloza
The Complexity of Reversal-Bounded Model-Checking
Abstract
We study model-checking problems on counter systems when guards are quantifier-free Presburger formulae, the specification languages are LTL-like dialects with arithmetical constraints and the runs are restricted to reversal-bounded ones. We introduce a generalization of reversal-boundedness and we show the NExpTime-completeness of the reversal-bounded model-checking problem as well as for related reversalbounded reachability problems. As a by-product, we show the effective Presburger definability for sets of configurations for which there is a reversal-bounded run verifying a given temporal formula. Our results generalize existing results about reversal-bounded counter automata and provides a uniform and more general framework.
Marcello M. Bersani, Stéphane Demri
Expressing Polymorphic Types in a Many-Sorted Language
Abstract
In this paper, we study translation from a first-order logic with polymorphic types la ML (of which we give a formal description) to a many-sorted or one-sorted logic as accepted by mainstream automated theorem provers. We consider a three-stage scheme where the last stage eliminates polymorphic types while adding the necessary “annotations” to preserve soundness, and the first two stages serve to protect certain terms so that they can keep their original unannotated form. This protection allows us to make use of provers’ built-in theories and operations. We present two existing translation procedures as sound and complete instances of this generic scheme. Our formulation generalizes over the previous ones by allowing us to protect terms of arbitrary monomorphic types. In particular, we can benefit from the built-in theory of arrays in SMT solvers such as Z3, CVC3, and Yices. The proposed methods are implemented in the Why3 tool and we compare their performance in combination with several automated provers.
François Bobot, Andrei Paskevich
A Combination of Rewriting and Constraint Solving for the Quantifier-Free Interpolation of Arrays with Integer Difference Constraints
Abstract
The use of interpolants in model checking is progressively gaining importance. The application of encodings based on the theory of arrays, however, is limited by the impossibility of deriving quantifier-free interpolants in general. To overcome this problem, we have recently proposed a quantifier-free interpolation solver for a natural variant of the theory of arrays. However, arrays are usually combined with fragments of arithmetic over indexes in applications, especially those related to software verification. In this paper, we propose a quantifier-free interpolation solver for the variant of arrays considered in previous work when combined with integer difference logic over indexes.
Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise
Superposition Modulo Non-linear Arithmetic
Abstract
The first-order theory over non-linear arithmetic including transcendental functions (NLA) is undecidable. Nevertheless, in this paper we show that a particular combination with superposition leads to a sound and complete calculus that is useful in practice. We follow basically the ideas of the SUP(LA) combination, but have to take care of undecidability, resulting in “unknown” answers by the NLA reasoning procedure. A pipeline of NLA constraint simplification techniques related to the SUP(NLA) framework significantly decreases the number of “unknown” answers. The resulting approach is implemented as SUP(NLA) by a system combination of Spass and iSAT. Applied to various scenarios of traffic collision avoidance protocols, we show by experiments that Spass(iSAT) can fully automatically proof and disproof safety properties of such protocols using the very same formalization.
Andreas Eggers, Evgeny Kruglov, Stefan Kupferschmid, Karsten Scheibler, Tino Teige, Christoph Weidenbach
The Modal Logic of Equilibrium Models
Abstract
Here-and-there models and equilibrium models were investigated as a semantical framework for answer set programming by Pearce, Cabalar, Lifschitz, Ferraris and others. The semantics of equilibrium logic is indirect in that the notion of satisfiability is defined in terms of satisfiability in the logic of here-and-there. We here give a direct semantics of equilibrium logic, stated in terms of a modal language into which the language of equilibrium logic can be embedded.
Luis Fariñas del Cerro, Andreas Herzig
Harnessing First Order Termination Provers Using Higher Order Dependency Pairs
Abstract
Many functional programs and higher order term rewrite systems contain, besides higher order rules, also a significant first order part. We discuss how an automatic termination prover can split a rewrite system into a first order and a higher order part. The results are applicable to all common styles of higher order rewriting with simple types, although some dependency pair approach is needed to use them.
Carsten Fuhs, Cynthia Kop
Stochastic Local Search for SMT: Combining Theory Solvers with WalkSAT
Abstract
A dominant approach to Satisfiability Modulo Theories (SMT) relies on the integration of a Conflict-Driven-Clause-Learning (CDCL) SAT solver and of a decision procedure able to handle sets of atomic constraints in the underlying theory \(\mathcal{T}\) (\({\ensuremath{\mathcal{T}} }\textit{-solver}\) ). In pure SAT, however, Stochastic Local-Search (SLS) procedures sometimes are competitive with CDCL SAT solvers on satisfiable instances. Thus, it is a natural research question to wonder whether SLS can be exploited successfully also inside SMT tools.
In this paper we investigate this issue. We first introduce a general procedure for integrating a SLS solver of the WalkSAT family with a \({\ensuremath{\mathcal{T}} }\textit{-solver}\). Then we present a group of techniques aimed at improving the synergy between these two components. Finally we implement all these techniques into a novel SLS-based SMT solver for the theory of linear arithmetic over the rationals, combining UBCSAT/UBCSAT++ and MathSAT, and perform an empirical evaluation on satisfiable instances. The results confirm the potential of the approach.
Alberto Griggio, Quoc-Sang Phan, Roberto Sebastiani, Silvia Tomasi
Controlled Term Rewriting
Abstract
Motivated by the problem of verification of imperative tree transformation programs, we study the combination, called controlled term rewriting systems (CntTRS), of term rewriting rules with constraints selecting the possible rewrite positions. These constraints are specified, for each rewrite rule, by a selection automaton which defines a set of positions in a term based on tree automata computations.
We show that reachability is PSPACE-complete for so-called monotonic CntTRS, such that the size of every left-hand-side of every rewrite rule is larger or equal to the size of the corresponding right-hand-side, and also for the class of context-free non-collapsing CntTRS, which transform Context-Free (CF) tree language into CF tree languages.
When allowing size-reducing rules, reachability becomes undecidable, even for flat CntTRS (both sides of rewrite rules are of depth at most one) when restricting to words (i.e. function symbols have arity at most one), and for ground CntTRS (rewrite rules have no variables).
We also consider a restricted version of the control such that a position is selected if the sequence of symbols on the path from that position to the root of the tree belongs to a given regular language. This restriction enables decision results in the above cases.
Florent Jacquemard, Yoshiharu Kojima, Masahiko Sakai
Sharing Is Caring: Combination of Theories
Abstract
One of the main shortcomings of the traditional methods for combining theories is the complexity of guessing the arrangement of the variables shared by the individual theories. This paper presents a reformulation of the Nelson-Oppen method that takes into account explicit equality propagation and can ignore pairs of shared variables that the theories do not care about. We show the correctness of the new approach and present care functions for the theory of uninterpreted functions and the theory of arrays. The effectiveness of the new method is illustrated by experimental results demonstrating a dramatic performance improvement on benchmarks combining arrays and bit-vectors.
Dejan Jovanović, Clark Barrett
Modular Termination and Combinability for Superposition Modulo Counter Arithmetic
Abstract
Modularity is a highly desirable property in the development of satisfiability procedures. In this paper we are interested in using a dedicated superposition calculus to develop satisfiability procedures for (unions of) theories sharing counter arithmetic. In the first place, we are concerned with the termination of this calculus for theories representing data structures and their extensions. To this purpose, we prove a modularity result for termination which allows us to use our superposition calculus as a satisfiability procedure for combinations of data structures. In addition, we present a general combinability result that permits us to use our satisfiability procedures into a non-disjoint combination method à la Nelson-Oppen without loss of completeness. This latter result is useful whenever data structures are combined with theories for which superposition is not applicable, like theories of arithmetic.
Christophe Ringeissen, Valerio Senni
Congruence Closure of Compressed Terms in Polynomial Time
Abstract
The word-problem for a finite set of equational axioms between ground terms is the question whether for terms s,t the equation s = t is a consequence. We consider this problem under grammar based compression of terms, in particular compression with singleton tree grammars (STGs) and with directed acyclic graphs (DAGs) as a special case. We show that given a DAG-compressed ground and reduced term rewriting system T, the T-normal form of an STG-compressed term s can be computed in polynomial time, and hence the T-word problem can be solved in polynomial time. This implies that the word problem of STG-compressed terms w.r.t. a set of DAG-compressed ground equations can be decided in polynomial time. If the ground term rewriting system (gTRS) T is STG-compressed, we show NP-hardness of T-normal-form computation. For compressed, reduced gTRSs we show a PSPACE upper bound on the complexity of the normal form computation of STG-compressed terms. Also special cases are considered and a prototypical implementation is presented.
Manfred Schmidt-Schauss, David Sabel, Altug Anis
Generalized and Formalized Uncurrying
Abstract
Uncurrying is a termination technique for applicative term rewrite systems. During our formalization of uncurrying in the theorem prover Isabelle, we detected a gap in the original pen-and-paper proof which cannot directly be filled without further preconditions. Our final formalization does not demand additional preconditions, and generalizes the existing techniques since it allows to uncurry non-applicative term rewrite systems. Furthermore, we provide new results on uncurrying for relative termination and for dependency pairs.
Christian Sternagel, René Thiemann
A Semantic Account for Modularity in Multi-language Modelling of Search Problems
Abstract
Motivated by the need to combine systems and logics, we develop a modular approach to the model expansion (MX) problem, a task which is common in applications such as planning, scheduling, computational biology, formal verification. We develop a modular framework where parts of a modular system can be written in different languages. We start our development from a previous work, ?, but modify and extend that framework significantly. In particular, we use a model-theoretic setting and introduce a feedback (loop) operator on modules. We study the expressive power of our framework and demonstrate that adding the feedback operator increases the expressive power considerably. We prove that, even with individual modules being polytime solvable, the framework is expressive enough to capture all of NP, a property which does not hold without loop. Moreover, we demonstrate that, using monotonicity and anti-monotonicity of modules, one can significantly reduce the search space of a solution to a modular system.
Shahab Tasharrofi, Eugenia Ternovska
Backmatter
Metadata
Title
Frontiers of Combining Systems
Editors
Cesare Tinelli
Viorica Sofronie-Stokkermans
Copyright Year
2011
Publisher
Springer Berlin Heidelberg
Electronic ISBN
978-3-642-24364-6
Print ISBN
978-3-642-24363-9
DOI
https://doi.org/10.1007/978-3-642-24364-6

Premium Partner

    Image Credits