Modular verification of a non-blocking stack
- Matthew Parkinson; Richard Bornat; Peter O’Hearn
This paper contributes to the development of techniques for the modular proof of programs that include concurrent algorithms. We present a proof of a non-blocking concurrent algorithm, which provides a shared stack. The inter-thread interference, which is essential to the algorithm, is confined in the proof and the specification to the modular operations, which perform push and pop on the stack. This is achieved by the mechanisms of separation logic. The effect is that inter-thread interference does not pollute specification or verification of clients of the stack.
Doctoral Dissertation Temporal Linear Logic and Its Applications
- Takaharu Hirai
Linear logic, introduced by Girard in 1987, has been called a resource conscious logic. In order to express a dynamic change in process environment, it is useful to consider a concept of resource such as data consumption. The expressive power of linear logic is evidenced by some very natural encodings of computational models such as Petri nets, counter machines, Turing machines, and others. For example, in Petri nets, tokens are considered as resources that are consumed and transitions are considered as reusable resources. It is well known that the reachability problem for ordinary Petri nets is equivalent to the provability...
This paper presents a new method for modeling and solving high-level synthesis problem. In our approach, finite domain constraints and related constraints solving techniques offered by constrained logic programming are used. They make it possible to define basic constraints on operations and registers and provide a way to find optimal or suboptimal solutions to the data-path synthesis problem. Different design styles, such as multicycling, chaining, pipelined components and algorithmic pipelining can be modeled in this framework. The proposed formulation combines different constraints in one representation and thus the optimization can find a better solution. The prototype system has been implemented...
Interoperable transactions in business models -- a structured approach
- H. Weigand; E. Verharen; F. Dignum
Recent database research has given much attention to the specification of "flexible" transactions that can be used in interoperable systems. Starting from a quite different angle, Business Process Modelling has approached the area of communication modelling as well (the Language/Action perspective). The main goal of this paper is to provide some useful structuring mechanisms for interoperable transactions based on the Language/Action perspective. The paper thus tries to build a bridge between two rather separated worlds: the research on interoperable transactions on the one hand, and the research on business process models on the other. Extended deontic logic provides the material...
Kernels on Prolog Proof Trees: Statistical Learning in the ILP Setting
- A. Passerini Passerini A○dsi·unifi·it; P. Frasconi P-f A○dsi·unifi·it; L. De Raedt Deraedt A○informatik·uni-freiburg·de
We develop kernels for measuring the similarity between relational instances using background knowledge expressed in first-order logic. The method allows us to bridge the gap between traditional inductive logic programming representations and statistical approaches to supervised learning. Logic programs will be used to generate proofs of given visitor programs which exploit the available background knowledge, while kernel machines will be employed to learn from such proofs. We report positive empirical results on Bongard-like and M-of-N problems that are difficult or impossible to solve with traditional ILP techniques, as well as on a real data set. 1.
Complexity-Effective Superscalar Embedded Processors Using Instruction-Level Distributed Processing
- Ian Caulfield
Modern trends in mobile and embedded devices require ever increasing levels of performance, while maintaining low power consumption and silicon area usage. This thesis presents a new architecture for a high-performance embedded processor, based upon the instruction-level distributed processing (ILDP) methodology. A qualitative analysis of the complexity of an ILDP implementation as compared to both a typical scalar RISC CPU and a superscalar design is provided, which shows that the ILDP architecture eliminates or greatly reduces the size of a number of structures present in a superscalar architecture, allowing its complexity and power consumption to compare favourably with a simple...
Executable Temporal Logic for Distributed A.I
- Michael Fisher; Michael Wooldridge
DAI’93 Themes: societies and organisations of agents; modeling through communication in adversarial and cooperative systems This paper describes Concurrent METATEM, a programming language based on temporal logic, and applies it to the study of Distributed Artificial Intelligence (DAI). A Concurrent METATEM system consists of a number of asynchronously executing objects, which are able to communicate through broadcast message-passing. Each individual object directly executes a specification of its desired behaviour. Such specifications are given using a set of temporal logic ‘rules’, determining how the object may generate ‘commitments’, which it subsequently attempts to satisfy. This language provides a novel and powerful...
SOS 2005 Preliminary Version Divide and Congruence Applied to η-Bisimulation
- Wan Fokkink; Rob Van Glabbeek
We present congruence formats for η- and rooted η-bisimulation equivalence. These formats are derived using a method for decomposing modal formulas in process algebra. To decide whether a process algebra term satisfies a modal formula, one can check whether its subterms satisfy formulas that are obtained by decomposing the original formula. The decomposition uses the structural operational semantics that underlies the process algebra. Key words: Structural operational semantics; modal logic; decomposition; congruence; η-bisimulation 1
Coordination of Many Agents
- Joxan Jaffar; H. C. Yap; Kenny Q. Zhu
Abstract. This paper presents a reactive programming and triggering framework for the coordination of a large number of distributed agents with shared knowledge. At the heart of this framework is a highly structured shared store in the form of a constraint logic program (CLP), which is used as a knowledge base and being reacted to by agents through the use of “reactors”. The biggest challenge arising from such a reactive programming framework using CLP is to develop a trigger mechanism that allows efficient “wakeup ” of blocked reactors. This paper addresses the architecture of this open framework, and discusses a...
Visual and Textual Knowledge Representation in DESIRE
- Catholijn M. Jonker; Rob Kremer; Pim Van Leeuwen; Dong Pan
Abstract. In this paper, graphical, conceptual graph-based representations for knowledge structures in the compositional development method DESIRE for knowledge-based and multi-agent systems are presented, together with a graphical editor based on the Constraint Graph environment. Moreover, a translator is described which translates these graphical representations to textual representations in DESIRE. The strength of the combined environment is a powerful-- yet easy-to-use-- framework to support the development of knowledge based and multi-agent systems. Finally, a mapping is presented from DESIRE, that is based on order sorted predicate logic, to Conceptual Graphs. 1
1 Workshop Coordinators
- Ricardo Lopes; Michel Ferreira (eds; Michel Ferreira; Ricardo Lopes (portugal; Bart Demoen (belgium; David S. Warren (usa; Enrico Pontelli (usa; Haifeng Guo (usa; Inês De Castro Dutra (brazil; Kostis Sagonas (sweden; Manuel Carro (spain; Michel Ferreira (portugal; Ricardo Lopes (portugal; Luís Lopes; Manuel Carro; Manuel Eduardo Correia; Michel Ferreira; Nikolay Pelov; Ricardo Lopes; Ricardo Rocha
CICLOPS’03 means to bring together, in an informal setting, people involved in research on sequential and parallel implementation technologies for logic and constraint programming languages and systems, in order to promote a much needed exchange of ideas and feedback on recent developments. We hope that the workshop will provide meeting ground for people working on implementation technology for different aspects of execution of logic-based and constraint-based languages and systems. This workshop continues a tradition of successful workshops on Implementations of Logic
Linear logic programming languages offer the implementor new challenges not present in more traditional logic languages such as Prolog or *Prolog. Among these, the efficient management of the linear formulas contained in the context is of crucial importance for the use of these languages in non-trivial applications.
Extending SWRL to express fully-quantified constraints
- Craig Mckenzie; Peter Gray; Alun Preece
Abstract. Drawing on experience gained over a series of distributed knowledge base and database projects, we argue for the utility of an expressive quantified constraint language for the Semantic Web logic layer. Our Constraint Interchange Format (CIF) is based on classical range-restricted FOL. CIF allows the expression of invariant conditions in Semantic Web data models, but the choice of how to implement the constraints is left to local reasoners. We develop the quantified constraint representation as an extension of the current proposal for a Semantic Web Rule Language (SWRL). An RDF syntax for our extended CIF/SWRL is given in this...
Non-Heuristic Optimization and Synthesisof Parallel-Prefix Adders
Abstract The class of parallel-prefix adders comprises the most area-delay efficient adder architectures- such as the ripple-carry, the carry-increment, and the carry-lookahead adders- for the entire range of possible area-delay trade-offs. The generic description of these adders as prefixstructures allows their simple and consistent area optimization and synthesis under given timing constraints, including non-uniform input and output signal arrival times. This paperpresents an efficient non-heuristic algorithm for the generation of size-optimal parallel-prefix structures under arbitrary depth constraints. Keywords Parallel-prefix adders, non-heuristic synthesis algorithm, circuit timing and area optimization,computer arithmetic, cell-based VLSI. 1 Introduction Cell-based design techniques, such as standard-cells and...
IOS Press Controllable Delay-Insensitive Processes
- Mark B. Josephs; Hemangee K. Kapoor
Abstract. Josephs and Udding’s DI-Algebra offers a convenient way of specifying and verifying designs that must rely upon delay-insensitive signalling between modules (asynchronous logic blocks). It is based on Hoare’s theory of CSP, including the notion of refinement between processes, and is similarly underpinned by a denotational semantics. Verhoeff developed an alternative theory of delay-insensitive design based on a testing paradigm and the concept of reflection. The first contribution of this paper is to define a relation between processes in DI-Algebra that captures Verhoeff’s notion of a closed system passing a test (by being free of interference and deadlock). The...
An observationally complete program logic for imperative higher-order functions
- Kohei Honda; Nobuko Yoshida; Martin Berger
We propose a simple compositional program logic for an imperative extension of call-by-value PCF, built on Hoare logic and our preceding work on program logics for pure higher-order functions. A systematic use of names and operations on them allows precise and general description of complex higher-order imperative behaviour. The logic offers a foundation for general treatment of aliasing and local state on its basis, with minimal extensions. After establishing soundness, we prove that valid assertions for programs completely characterise their behaviour up to observational congruence, which is proved using a variant of finite canonical forms. The use of the logic...
ARTIFICIAL INTELLIGENCE 227 Linear Resolution with Selection Function Recommended by B. Meltzer
- Robert Kowalski; Donald Kuehnm
Linear resolution with selection function (SL.resolution) is a restricted form of linear resolution. The main restriction is e~ected by a selection function which chooses fro: ~ each clause a sit, gle literal to be resolved upon in that clause. This and other restrictions are adapted to linear resolution from Loveland's model elimination. We show that SL-resolution achieves a substantial reduction in the generation of redundant and irrelevant derivations and does so without significantly increasing the complexity of simplest proofs. We base our argument for the increased efficiency of SL-resolution upon precise calculation of these quantities. A more far reaching advantage...
Exogenous Probabilistic Computation Tree Logic
- Pedro Baltazar; Paulo Mateus; Rajagopal Nagarajan; Nikolaos Papanikolaou
Replace this file with prentcsmacro.sty for your meeting, or with entcsmacro.sty for your meeting. Both can be
A modal extension of logic programming
- Matteo Baldoni; Laura Giordano; Alberto Martelli
In this paper we present a modal extension of logic programming, which provides reasoning capabilities in a multiagent situation. The language contains embedded implications, modal operators [ai] to represent agent beliefs, together with a kind of "common knowledge " operator. In this language we can also de ne modules, compose them in several ways, and, also, we can perform hypothetical reasoning. 1
Abstract Local reasoning, separation and aliasing
- Richard Bornat
Structures built by pointer aliasing, such as DAGs and graphs, are notoriously tricky to deal with. The mechanisms of separation logic can deal with these structures, but so far this has been done by the maintenance of a global invariant. Specifications and proofs which use local reasoning, and which may point the way to a structured programming for pointers, are discussed. An idiom for inclusion sharing, where one structure is included in another, is presented. A notion of ‘partial graphs ’ – graphs with dangling pointers – is used to facilitate proof. 1