Case Studies in Symbolic Model Checking
- Ganesh Gopalakrishnan; Dilip Khandekar; Ganesh Gopalakrishnan; Dilip Kh; Dilip Kh; Ravi Kuramkote; Ravi Kuramkote; Ratan Nalumasu; Ratan Nalumasu
Formal verification of hardware and software systems has long been recognized as an essential step in the development process of a system. It is of importance especially in concurrent systems that are more difficult to debug than sequential systems. Tools that are powerful enough to verify real-life systems have become available recently. Model checking tools have become quite popular because of their ability to carry out proofs with minimal human intervention. In this paper we report our experience with SMV, a symbolic model verifier on practical problems of significant sizes. We present verification of a software system, a distributed shared...
A NExpTime-Complete Description Logic Strictly Contained in C²
- Stephan Tobies
We examine the complexity and expressivity of the combination of the Description Logic ALCQI with a terminological formalism based on cardinality restrictions on concepts. This combination can naturally be embedded into C², the two variable fragment of predicate logic with counting quantifiers. We prove that ALCQI has the same complexity as C² but does not reach its expressive power.
Applying the Mu-Calculus in Planning and Reasoning about Action
- Munindar P. Singh
Planning algorithms have traditionally been geared toward achievement goals in single-agent environments. Such algorithms essentially produce plans to reach one of a specified set of states. More general approaches for planning based on temporal logic (TL) are emerging. Current approaches tend to use linear TL, and can handle sets of sequences of states. However, they assume deterministic actions with all changes effected solely by one agent. By contrast, we use a branching model of time that can express concurrent actions by multiple agents and the environment, leading to nondeterministic effects of an agent's actions. For this reason, we view plans...
Loading a Cache with Query Results
- Laura M. Haas; Donald Kossmann; Ioana Ursu
Data intensive applications today usually run in either a clientserver or a middleware environment. In either case, they must efficiently handle both database queries, which process large numbers of data objects, and application logic, which involves fine-grained object accesses (e.g., method calls). We propose a wholistic approach to speeding up such applications: we load the cache of a system with relevant objects as a by-product of query processing. This can potentially improve the performance of the application, by eliminating the need to fault in objects. However, it can also increase the cost of queries by forcing them to handle more...
Resource Interpretations, Bunched Implications and the alphalambda-calculus
- Peter W. O'Hearn
. We introduce the ff-calculus, a typed calculus that includes a multiplicative function type \Gamma alongside an additive function type !. It arises proof-theoretically as a calculus of proof terms for the logic of bunched implications of O'Hearn and Pym, and semantically from doubly closed categories, where a single category possesses two closed structures. Typing contexts in ff are bunches, i.e., trees built from two combining operations, one that admits the structural rules of Weakening and Contraction and another that does not. To illuminate the consequences of ff's approach to the structural rules we define two resource interpretations, extracted from...
Objects, Types and Modal Logics
- Dan S. Andersen; Lars H. Pedersen; Hans Hüttel; Josva Kleist; Ac Abadi; Cardelli Present
In this paper we present a modal logic for describing properties of terms in the object calculus of Abadi and Cardelli [AC96]. The logic is essentially the modal mu-calculus of [Koz83]. The fragment allows us to express the temporal modalities of the logic CTL [BAMP83]. We investigate the connection between the type system Ob 1!:¯ and the mu-calculus, providing a translation of types into modal formulae and an ordering on formulae that is sound w.r.t. to the subtype ordering of Ob 1!:¯ . 1 Introduction In [AC94b, AC94c, AC94a, AC96] Abadi and Cardelli present and investigate several versions of the...
PSpace Reasoning for DLs with Qualifying Number Restrictions
- Stephan Tobies
The description logic ALCQI extends the "standard" description logic ALC by qualifying number restrictions and converse roles. We show that concept satisfiability for this DL is still decidable in polynomial space. The presented algorithm combines techniques from [Tob99a] to deal with qualifying number restrictions and from [HST99] to deal with converse roles. Additionally, we extend the result to ALCQIR, which extends ALCQI by role intersections. This solves an open problem from [DLNN97]. The result for ALCQI has already been presented in the seperate technical report [Tob99b]. In this report we use the same techniques to obtain the stronger result for...
Intervals (Pairs of Fuzzy Values), Triples, etc.: Can We Thus Get an Arbitrary Ordering?
- Vladik Kreinovich; Masao Mukaidono
Traditional fuzzy logic uses real numbers as truth values. This description is not always adequate, so in interval-valued fuzzy logic, we use pairs (t \Gamma ; t + ) of real numbers, t \Gamma t + , to describe a truth value. To make this description even more adequate, instead of using real numbers to described each value t \Gamma and t + , we can use intervals, and thus get fuzzy values which can be described by 4 real numbers each. We can iterate this procedure again and again. The question is: can we get an arbitrary partially ordered...
Cumulative Higher-Order Logic as a Foundation for Set Theory
- Wolfgang Degen; Jan Johannsen
The systems K of transnite cumulative types up to are extended to systems K 1 that include a natural innitary inference rule, the so-called limit rule. For countable a semantic completeness theorem for K 1 is proved by the method of reduction trees, and it is shown that every model of K 1 is equivalent to a cumulative hierarchy of sets. This is used to show that several axiomatic rst-order set theories can be interpreted in K 1 , for suitable . Keywords: cumulative types, innitary inference rule, logical foundations of set theory. MSC: 03B15 03B30 03E30 03F25 1 Introduction...
A Logic of Situated Know-how
- Munindar P. Singh
Know-how is an important concept in Artificial Intelligence. It has been argued previously that it cannot be successfully reduced to the knowledge of facts. In this paper, I present sound and complete axiomatizations for two non-reductive and intuitively natural formal definitions of the know-how of an agent situated in a complex environment. I also present some theorems giving useful properties of know-how, and discuss and resolve an interesting paradox (which is described within). This is done using a new operator in the spirit of Dynamic Logic that is introduced herein and whose semantics and proof-theory are given. 1 Introduction Knowledge...
Extraction of Meta-Knowledge to Restrict the Hypothesis Space for ILP Systems
- Eric Mccreath; Arun Sharma
Many ILP systems, such as GOLEM, FOIL, and MIS, take advantage of user supplied meta-knowledge to restrict the hypothesis space. This meta-knowledge can be in the form of type information about arguments in the predicate being learned, or it can be information about whether a certain argument in the predicate is functionally dependent on the other arguments (supplied as mode information). This meta-knowledge is explicitly supplied to an ILP system in addition to the data. The present paper argues that in many cases the meta- knowledge can be extracted directly from the raw data. Three algorithms are presented that learn...
ILFA - A Project in Experimental Logic Computation
- Ulf Dunker; Andreas Flögel; Hans Kleine Büning; Jürgen Lehmann; Theodor Lettmann
ILFA provides programs and libraries of reusable software components for logic processing. "ILFA" stands for Inte- grated Logic Functions for Advanced Applications and has its roots in a research project between the german IBM in Heidelberg and the Universities of Duisburg and Paderborn. The implementation by the C programming language supports an efficient work with logic methods in different computer environments. ILFA contains a great number of logic algorithms divided in implementations for important subclasses of logic. Special attention has been considered to visual user interfaces for the ILFA library components, i.e. for using them, programming with them and providing...
A Formalization of the B-Method in Coq and PVS
- Jean Paul Bodeveix; Mamoun Filali; César A. Muñoz
. We formalize the generalized substitution mechanism of the B-method in the higher-order logic of Coq and PVS. Thanks to the dependent type feature of Coq and PVS, our encoding is compact and highly integrated with the logic supported by the theorem provers. In addition, we describe a tool that mechanizes, at the user level, most of the effort of the encoding. 1 Introduction In recent years, important work has been done in the design and implementation of general specification languages and theorem provers. The concretization of these efforts is illustrated in systems like HOL [Gor93], Coq [BBC + 97],...
A semantic view of classical proofs -- type-theoretic, categorical, and denotational characterizations (Extended Abstract)
- C.-H. L. Ong
Classical logic is one of the best examples of a mathematical theory that is truly useful to computer science. Hardware and software engineers apply the theory routinely. Yet from a foundational standpoint, there are aspects of classical logic that are problematic. Unlike intuitionistic logic, classical logic is often held to be non-constructive, and so, is said to admit no proof semantics. To draw an analogy in the proofsas -programs paradigm, it is as if we understand well the theory of manipulation between equivalent specifications (which we do), but have comparatively little foundational insight of the process of transforming one program...
Machine Learning Techniques for Adaptive Logic-Based Multi-Agent Systems: A Preliminary Report
- Eduardo Alonso; Daniel Kudenko
: It is widely recognised in the agent community that one of the more important features of high level agents is their capability to adapt and learn in dynamic, uncertain domains [12, 30]. A lot of work has been recently produced on this topic, particularly in the field of learning in multi-agent systems [1, 32, 33, 34, 42, 43]. It is, however, worth noticing that whereas some kind of logic is used to specify the (multi-)agents' architecture, mainly non-relational learning techniques such as reinforcement learning are applied. We think that these approaches are not well-suited to deal with the large...
That SnS Can Be Modally Characterized
- Hans Hüttel
We show that a modal mu-calculus with label set f1; : : : ; ng can define the Rabin recognizable tree languages up to an equivalence similar to the observational equivalence of Milner. 1 Introduction In  it was shown that the temporal logic ETL  can define exactly the class of !-regular languages. In  it was shown that a fixed-point calculus whose signature apart from maximal and minimal fixed points and disjunction includes the usual operators on trees can define exactly the sets of infinite trees recognized by Rabin tree automata ; this class of sets corresponds to...
- Norman Foo; Abhaya Nayak; Maurice Pagnucco
. Certain constraints that should be interpreted as definitions or quasi-definitions can cause prediction problems for logics of action. Standard ways to avoid them rely on notions of priority in the minimization of fluent change. We offer an alternative approach based on belief revision. Revision is performed on the reduct of the system theory after isolating definitions, and the revised theory is then expanded by restoring the definitions. The basis for this is a weak monotonicity result for AGM contraction. Examples from the literature are used to illustrate the approach. 1 Introduction A substantial part of knowledge representation research is...
Non-repudiation Evidence Generation for CORBA using XML
- Michael Wichert; David Ingham; Steve Caughey
This paper focuses on the provision of a nonrepudiation service for CORBA. The current OMG specification of a CORBA non-repudiation service forces the programmer to augment the application with calls to functions for generating or validating evidence. Furthermore, the application itself has to manage the exchange of this evidence between parties and its storage. The paper describes our design for a generic CORBA non-repudiation service implementation. Our approach provides a separation between the application business logic and the generation of evidence allowing nonrepudiation support to be incorporated into applications with the minimum of programmer effort. Our design is described in...
Frame-buffer on Demand: Applications of Stateless Client Systems in Web-based Learning
- Sheng Feng Li; Quentin Stafford-Fraser; Andy Hopper
The growth of the Internet and the World Wide Web has changed the way people are educated, and distance learning is amongst the most promising fields of new Web applications built from existing services with supporting infrastructures. In this paper, we introduce a number of new applications built from Stateless Client Systems to assist the learning of computer-based activities. Stateless Client Systems separate the display interface from the application logic in windowing systems. They embed a client/server architecture, where the server executes all the applications and the client simply presents the frame buffers or screen images to the user and...
Deliverables: A Categorical Approach to Program Development in Type Theory
- James Hugh McKinna
This thesis considers the problem of program correctness within a rich theory of dependent types, the Extended Calculus of Constructions (ECC). This system contains a powerful programming language of higher-order primitive recursion and higher-order intuitionistic logic. It is supported by Pollack's versatile LEGO implementation, which I use extensively to develop the mathematical constructions studied here. I systematically investigate Burstall's notion of deliverable, that is, a program paired with a proof of correctness. This approach separates the concerns of programming and logic, since I want a simple program extraction mechanism. The \Sigma-types of the calculus enable us to achieve this. There...