nach oben

2007 | Buch

Kapitel lesen Erstes Kapitel lesen

Frontiers of Combining Systems

6th International Symposium, FroCoS 2007 Liverpool, UK, September 10-12, 2007 Proceedings

herausgegeben von: Boris Konev, Frank Wolter

Verlag: Springer Berlin Heidelberg

Buchreihe : Lecture Notes in Computer Science

Enthalten in: Springer Professional "Wirtschaft+Technik" , Springer Professional "Technik" , Springer Professional "Wirtschaft"

Einloggen, um Zugang zu erhalten

Inhaltsverzeichnis

Frontmatter

Section 1. Invited Contributions

Architecting Solvers for SAT Modulo Theories: Nelson-Oppen with DPLL

Abstract

We offer a transition system representing a high-level but detailed architecture for SMT solvers that combine a propositional SAT engine with solvers for multiple disjoint theories. The system captures succintly and accurately all the major aspects of the solver’s global operation: boolean search with across-the-board backjumping, communication of theory-specific facts and equalities between shared variables, and cooperative conflict analysis. Provably correct and prudently underspecified, our system is a usable ground for high-quality implementations of comprehensive SMT solvers.

Sava Krstić, Amit Goel

From KSAT to Delayed Theory Combination: Exploiting DPLL Outside the SAT Domain

Abstract

In the last two decades we have witnessed an impressive advance in the efficiency of propositional satisfiability techniques (SAT), which has brought large and previously-intractable problems at the reach of state-of-the-art SAT solvers. Most of this success is motivated by the impressive level of efficiency reached by current implementations of the DPLL procedure. Plain propositional logic, however, is not the only application domain for DPLL. In fact, DPLL has also been successfully used as a boolean-reasoning kernel for automated reasoning tools in much more expressive logics.

In this talk I overview a 12-year experience on integrating DPLL with logic-specific decision procedures in various domains. In particular, I present and discuss three main achievements which have been obtained in this context: the DPLL-based procedures for modal and description logics, the lazy approach to Satisfiability Modulo Theories, and Delayed Theory Combination.

Roberto Sebastiani

Hierarchical and Modular Reasoning in Complex Theories: The Case of Local Theory Extensions

Abstract

We present an overview of results on hierarchical and modular reasoning in complex theories. We show that for a special type of extensions of a base theory, which we call local, hierarchic reasoning is possible (i.e. proof tasks in the extension can be hierarchically reduced to proof tasks w.r.t. the base theory). Many theories important for computer science or mathematics fall into this class (typical examples are theories of data structures, theories of free or monotone functions, but also functions occurring in mathematical analysis). In fact, it is often necessary to consider complex extensions, in which various types of functions or data structures need to be taken into account at the same time. We show how such local theory extensions can be identified and under which conditions locality is preserved when combining theories, and we investigate possibilities of efficient modular reasoning in such theory combinations.

We present several examples of application domains where local theories and local theory extensions occur in a natural way. We show, in particular, that various phenomena analyzed in the verification literature can be explained in a unified way using the notion of locality.

Viorica Sofronie-Stokkermans

Temporalising Logics: Fifteen Years After

Abstract

A straightforward way of adding a temporal dimension to a logical system is to combine it with a suitable temporal logic. Typical examples are first-order temporal logic [3], temporal description logics [1] or spatio-temporal logics [4]. In 1992, Finger and Gabbay [2] started an investigation of possible ways of temporalising abstract logical systems.

Michael Zakharyaschev

Section 2. Technical Papers

Termination of Innermost Context-Sensitive Rewriting Using Dependency Pairs

Abstract

Innermost context-sensitive rewriting has been proved useful for modeling computations of programs of algebraic languages like Maude, OBJ, etc. Furthermore, innermost termination of rewriting is often easier to prove than termination. Thus, under appropriate conditions, a useful strategy for proving termination of rewriting is trying to prove termination of innermost rewriting. This phenomenon has also been investigated for context-sensitive rewriting (CSR). Up to now, only few transformations have been proposed and used to prove termination of innermost CSR. In this paper, we investigate direct methods for proving termination of innermost CSR. We adapt the recently introduced context-sensitive dependency pairs approach to innermost CSR and show that they can be advantageously used for proving termination of innermost CSR. We have implemented them as part of the termination tool mu-term.

Beatriz Alarcón, Salvador Lucas

A Compressing Translation from Propositional Resolution to Natural Deduction

Abstract

We describe a translation from SAT solver generated propositional resolution refutation proofs to classical natural deduction proofs. The resulting proof can usually be checked quicker than one that simply simulates the original resolution proof. We use this result in interactive theorem provers, to speed up reconstruction of SAT solver generated proofs. The translation is efficient, running in time linear in the length of the original proof, and effective, easily scaling up to large proofs with millions of inferences.

Hasan Amjad

Combining Algorithms for Deciding Knowledge in Security Protocols

Abstract

In formal approaches, messages sent over a network are usually modeled by terms together with an equational theory, axiomatizing the properties of the cryptographic functions (encryption, exclusive or, ...). The analysis of cryptographic protocols requires a precise understanding of the attacker knowledge. Two standard notions are usually considered: deducibility and indistinguishability. Those notions are well-studied and several decidability results already exist to deal with a variety of equational theories. However most of the results are dedicated to specific equational theories.

We show that decidability results can be easily combined for any disjoint equational theories: if the deducibility and indistinguishability relations are decidable for two disjoint theories, they are also decidable for their union. As an application, new decidability results can be obtained using this combination theorem.

Mathilde Arnaud, Véronique Cortier, Stéphanie Delaune

Combining Classical and Intuitionistic Implications

Abstract

We present a simple logic that combines, in a conservative way, the implicative fragments of both classical and intuitionistic logics, thus settling a problem posed by Dov Gabbay in [5]. We also show that the logic can be given a nice complete axiomatization by adding four simple mixed axioms to the usual axiomatizations of classical and intuitionistic implications.

Carlos Caleiro, Jaime Ramos

Towards an Automatic Analysis of Web Service Security

Abstract

Web services send and receive messages in XML syntax with some parts hashed, encrypted or signed, according to the WS-Security standard. In this paper we introduce a model to formally describe the protocols that underly these services, their security properties and the rewriting attacks they might be subject to. Unlike other protocol models (in symbolic analysis) ours can handle non-deterministic receive/send actions and unordered sequence of XML nodes. Then to detect the attacks we have to consider the services as combining multiset operators and cryptographic ones and we have to solve specific satisfiability problems in the combined theory. By non-trivial extension of the combination techniques of [3] we obtain a decision procedure for insecurity of Web services with messages built using encryption, signature, and other cryptographic primitives. This combination technique allows one to decide insecurity in a modular way by reducing the associated constraint solving problems to problems in simpler theories.

Yannick Chevalier, Denis Lugiez, Michaël Rusinowitch

Certification of Automated Termination Proofs

Abstract

Nowadays, formal methods rely on tools of different kinds: proof assistants with which the user interacts to discover a proof step by step; and fully automated tools which make use of (intricate) decision procedures. But while some proof assistants can check the soundness of a proof, they lack automation. Regarding automated tools, one still has to be satisfied with their answers Yes/No/Do not know, the validity of which can be subject to question, in particular because of the increasing size and complexity of these tools.

In the context of rewriting techniques, we aim at bridging the gap between proof assistants that yield formal guarantees of reliability and highly automated tools one has to trust. We present an approach making use of both shallow and deep embeddings. We illustrate this approach with a prototype based on the CiME rewriting toolbox, which can discover involved termination proofs that can be certified by the Coq proof assistant, using the Coccinelle library for rewriting.

Evelyne Contejean, Pierre Courtieu, Julien Forest, Olivier Pons, Xavier Urbain

Temporal Logic with Capacity Constraints

Abstract

Often when modelling systems, physical constraints on the resources available are needed. For example, we might say that at most N processes can access a particular resource at any moment or exactly M participants are needed for an agreement. Such situations are concisely modelled where propositions are constrained such that at most N, or exactly M, can hold at any moment in time. This paper describes both the logical basis and a verification method for propositional linear time temporal logics which allow such constraints as input. The method incorporates ideas developed earlier for a resolution method for the temporal logic TLX and a tableaux-like procedure for PTL. The complexity of this procedure is discussed and case studies are examined. The logic itself represents a combination of standard temporal logic with classical constraints restricting the numbers of propositions that can be satisfied at any moment in time.

Clare Dixon, Michael Fisher, Boris Konev

Idempotent Transductions for Modal Logics

Abstract

We investigate the extension of modal logics by bisimulation quantifiers and present a class of modal logics which is decidable when augmented with bisimulation quantifiers. These logics are refered to as the idempotent transduction logics and are defined using the programs of propositional dynamic logic including converse and tests. This is a nontrivial extension of the decidability of the positive idempotent transduction logics which do not use converse operators in the programs (French, 2006). This extension allows us to apply bisimulation quantifiers to, for example, logics of knowledge, logics of belief and tense logics. We show the idempotent transduction logics preserve the axioms of propositional quantification and are decidable. The definition of idempotent transduction logics allows us to apply these results to a number of combined modal logics with a variety of interactions between modalities.

Tim French

A Temporal Logic of Robustness

Abstract

It can be desirable to specify polices that require a system to achieve some outcome even if a certain number of failures occur. This paper proposes a logic, RoCTL*, which extends CTL* with operators from Deontic logic, and a novel operator referred to as “Robustly”. This novel operator acts as variety of path quantifier allowing us to consider paths which deviate from the desired behaviour of the system. Unlike most path quantifiers, the Robustly operator must be evaluated over a path rather than just a state; the Robustly operator quantifies over paths produced from the current path by altering a single step. The Robustly operator roughly represents the phrase “even if an additional failure occurs now or in the future”. This paper examines the expressivity of this new logic, motivates its use and shows that it is decidable.

Tim French, John C. Mc Cabe-Dansted, Mark Reynolds

Noetherianity and Combination Problems

Abstract

In abstract algebra, a structure is said to be Noetherian if it does not admit infinite strictly ascending chains of congruences. In this paper, we adapt this notion to first-order logic by defining the class of Noetherian theories. Examples of theories in this class are Linear Arithmetics without ordering and the empty theory containing only a unary function symbol. Interestingly, it is possible to design a non-disjoint combination method for extensions of Noetherian theories. We investigate sufficient conditions for adding a temporal dimension to such theories in such a way that the decidability of the satisfiability problem for the quantifier-free fragment of the resulting temporal logic is guaranteed. This problem is firstly investigated for the case of Linear time Temporal Logic and then generalized to arbitrary modal/temporal logics whose propositional relativized satisfiability problem is decidable.

Silvio Ghilardi, Enrica Nicolini, Silvio Ranise, Daniele Zucchelli

Languages Modulo Normalization

Abstract

We propose a new class of tree automata, called tree automata with normalization (TAN). This framework is obtained by extending equational tree automata, and improves the results of the previous work, such as: recognized tree languages modulo the idempotency f(x,x) = x are closed under complement, which are not closed in equational tree automata, besides we do not lose important decidability. In the paper, first we investigate the closure properties of this class for Boolean operations and the decidability relative to the equational tree automata. Next we consider the relationship to other automata frameworks, in particular, hedge automata, which is a class of unranked tree automata. Hedge automata have been recognized in the XML database community as a theoretical basis for modeling the manipulation of semi-structured data. Through the observation about transformations from hedge automata to tree automata, we discuss advantages in the expressiveness and complexity of TAN. As an application of our framework, we show an example that XML schema with constraints that can not be dealt with by other tree automata frameworks is manipulated by TAN.

Hitoshi Ohsaki, Hiroyuki Seki

Combining Proof-Producing Decision Procedures

Abstract

Constraint solvers are key modules in many systems with reasoning capabilities (e.g., automated theorem provers). To incorporate constraint solvers in such systems, the capability of producing conflict sets or explanations of their results is crucial. For expressiveness, constraints are usually built out in unions of theories and constraint solvers in such unions are obtained by modularly combining solvers for the component theories. In this paper, we consider the problem of modularly constructing conflict sets for a combined theory by re-using available proof-producing procedures for the component theories. The key idea of our solution to this problem is the concept of explanation graph, which is a labelled, acyclic and undirected graph capable of recording the entailment of some equalities. Explanation graphs allow us to record explanations computed by a proof-producing procedure and to refine the Nelson-Oppen combination method to modularly build conflict sets for disjoint unions of theories. We also study how the computed conflict sets relate to an appropriate notion of minimality.

Silvio Ranise, Christophe Ringeissen, Duc-Khanh Tran

Visibly Pushdown Languages and Term Rewriting

Abstract

To combine tree languages with term rewriting, we introduce a new class of tree languages, that both extends regular languages and restricts context-free languages, and that is closed under intersection (unlike context-free languages). To do it, we combine the concept of visibly pushdown language, with top-down pushdown tree automata, and we get the visibly pushdown tree automata. Then, we use them to express the sets of descendants for a sub-class of growing term rewrite systems, and thanks to closure under intersection, we get that joinability and (restricted) unifiability are decidable.

Jacques Chabin, Pierre Réty

Proving Termination Using Recursive Path Orders and SAT Solving

Abstract

We introduce a propositional encoding of the recursive path order with status (RPO). RPO is a combination of a multiset path order and a lexicographic path order which considers permutations of the arguments in the lexicographic comparison. Our encoding allows us to apply SAT solvers in order to determine whether a given term rewrite system is RPO-terminating. Furthermore, to apply RPO within the dependency pair framework, we combined our novel encoding for RPO with an existing encoding for argument filters. We implemented our contributions in the termination prover AProVE. Our experiments show that due to our encoding, combining termination provers with SAT solvers improves the performance of RPO-implementations by orders of magnitude.

Peter Schneider-Kamp, René Thiemann, Elena Annov, Michael Codish, Jürgen Giesl

Backmatter

Titel: Frontiers of Combining Systems
herausgegeben von: Boris Konev
Frank Wolter
Verlag: Springer Berlin Heidelberg
Electronic ISBN: 978-3-540-74621-8
Print ISBN: 978-3-540-74620-1
DOI: https://doi.org/10.1007/978-3-540-74621-8