1.1 Background to Web Services
- Kenneth J. Turner
Composite web services are defined using the industry-standard language BPEL (Business Process Execution Logic). There is a strong need for graphical and automated support for this task. It is explained how CRESS (Chisel Representation Employing Systematic Specification) has been extended to meet this challenge. CRESS supports straightforward graphical descriptions of composite web services. Sample descriptions are presented of these. It is outlined how they are automatically implemented and systematically analysed using the target languages BPEL and LOTOS (Language Of Temporal
REMARC � Recon�gurable Multimedia Array Coprocessor
- Takashi Miyamori; Kunle Olukotun
This paper describes a new recon�gurable processor ar� chitecture called REMARC �Recon�gurable Multime� dia Array Coprocessor�. REMARC is a recon�gurable coprocessor that is tightly coupled to a main RISC pro� cessor and consists of a global control unit and 64 pro� grammable logic blocks called nano processors. RE� MARC is designed to accelerate multimedia applica� tions � such as video compression � decompression � and image processing. These applications typically use 8� bit or 16�bit data therefore � each nano processor has a 16�bit datapath that is much wider than those of other recon�gurable coprocessors. We have developed a pro�...
ABSTRACT When Do Bounds and Domain Propagation Lead to the Same Search Space
- Christian Schulte
This paper explores the question of when two propagationbased constraint systems have the same behaviour, in terms of search space. We categorise the behaviour of domain and bounds propagators for primitive constraints, and provide theorems that allow us to determine propagation behaviours for conjunctions of constraints. We then show how we can use this to analyse CLP(FD) programs to determine when we can safely replace domain propagators by more efficient bounds propagators without increasing search space. Keywords Constraint (logic) programming, finite domain constraints, bounds propagation, domain propagation, abstract interpretation, program analysis 1.
Extreme model checking
- Thomas A. Henzinger; Ranjit Jhala; Rupak Majumdar; Marco A. A. Sanvido
To Zohar, for teaching me about logic and life.-Tom Abstract. One of the central axioms of extreme programming is the disciplined use of regression testing during stepwise software development. Due to recent progress in software model checking, it has become possible to supplement this process with automatic checks for behavioral safety properties of programs, such as conformance with locking idioms and other programming protocols and patterns. For efficiency reasons, all checks must be incremental, i.e., they must reuse partial results from previous checks in order to avoid all unnecessary repetition of expensive verification tasks. We show that the lazy-abstraction algorithm,...
Abstract PDMC 2007 Preliminary Version A Stack-Slicing Algorithm for Multi-Core Model Checking
- Gerard J. Holzmann
The broad availability of multi-core chips on standard desktop PCs provides strong motivation for the development of new algorithms for logic model checkers that can take advantage of the additional processing power. With a steady increase in the number of available processing cores, we would like the performance of a model checker to increase as well – ideally linearly. The new trend implies a change of focus away from cluster computers towards shared memory systems. In this paper we discuss the multi-core algorithms that are in development for the SPIN model checker. Key words: Multi-core systems. Distributed systems. Multi-threaded programming....
- Deepak Garg; Frank Pfenning
Abstract. We introduce a novel way to integrate functional and concurrent programming based on intuitionistic linear logic. The functional core arises from interpreting proof reduction as computation. The concurrent core arises from interpreting proof search as computation. The two are tightly integrated via a monad that permits both sides to share the same logical meaning for the linear connectives while preserving their different computational paradigms. For example, concurrent computation synthesizes proofs which can be evaluated as functional programs. We illustrate our design with some small examples, including an encoding of the pi-calculus. 1
Integration of Coordination Architecture and Behavior Fuzzy Learning in Quadruped Walking Robots
- Dongbing Gu; Senior Member; Huosheng Hu; Senior Member
Abstract—This paper presents the design and implementation of a coordination architecture for quadruped walking robots to learn and execute soccer-playing behaviors. A typical hybrid architecture combing reactive behaviors with deliberative reasoning is developed. The reactive behaviors directly map spatial information extracted from sensors into actions. The deliberative reasoning represents temporal constraints of a robot’s strategy in terms of finite state machines. In order to achieve real-time and robust control performance in reactive behaviors, fuzzy logic controllers (FLCs) are used to encode the behaviors, and a two-stage learning scheme is adopted to make these FLCs adaptive to complex situations. The experimental...
- Feature Article Tao-shen Li; Ting Han; Guo-ning Chen
Abstract—Document Type Definition (DTD) is a fundamental tool that enables users to constrain the structure of XML documents. This tool does not support semantic query. Therefore, it has recently become an active research topic in Web intelligence to endow XML with semantics for query quality. In this paper, we develop an extension of the DTD using for the provision of formal semantics.. It is implemented using an entity declaration in the DTD to describe the ontology and recurring this description to the form of Frame Logic. After validated by our extended DTD, a semantic valid XML document will be produced,...
Elf: A meta-language for deductive systems (system description
- Frank Pfenning
Elf is a uniform meta-language for the formalization of the theory of programming languages and logics. It provides means for 1. specifying the abstract syntax and semantics of an object language in a natural and direct way; 2. implementing related algorithms (e.g., for type inference, evaluation, or proof search); and 3. representing proofs of meta-theorems about an object language, its semantics, and its implementation. Its conceptual basis are deductive systems which are used pervasively in the study of logic and the theory of programming languages. Logics and type systems for programming languages, for example, are often specified via inference rules....
Learning for Semantic Interpretation: Scaling Up Without Dumbing Down
- Raymond J. Mooney
Abstract. Most recent research in learning approaches to natural language have studied fairly \low-level " tasks such as morphology, part-ofspeech tagging, and syntactic parsing. However, I believe that logical approaches mayhave the most relevance and impact at the level of semantic interpretation, where a logical representation of sentence meaning is important and useful. We have explored the use of inductive logic programming for learning parsers that map natural-language database queries into executable logical form. This work goes against the growing trend in computational linguistics of focusing on shallow but broad-coverage natural language tasks (\scaling up by dumbing down") and instead...
Intuitionistic Letcc via Labelled Deduction
Intuitionistic logic can be presented as a calculus of labelled deduction on multiple-conclusion sequents. The corresponding natural deduction system constitutes a type system for programs using letcc, which capture the current program continuation, restricted to enforce constructive validity. This allows us to develop a rich dependent type theory incorporating letcc, which is known to be highly problematic for computational interpretations of classical logic. Moreover, we give a novel constructive proof for the soundness of labelled deduction, whose algorithmic content is a non-deterministic translation of programs that eliminates the restricted uses of letcc and is fully compatible with dependent types and...
We develop a model of normative systems in which agents are assumed to have multiple goals of increasing priority, and investigate the computational complexity and game theoretic properties of this model. In the underlying model of normative systems, we use Kripke structures to represent the possible transitions of a multiagent system. A normative system is then simply a subset of the Kripke structure, which contains the arcs that are forbidden by the normative system. We specify an agent’s goals as a hierarchy of formulae of Computation Tree Logic (CTL), a widely used logic for representing the properties of Kripke structures:...
Analysis of signalling pathways using continuous time Markov chains
- Muffy Calder; Vladislav Vyshemirsky; David Gilbert; Richard Orton
chains; model checking; continuous stochastic logic. We describe a quantitative modelling and analysis approach for signal transduction networks. We illustrate the approach with an example, the RKIP inhibited ERK pathway [CSK + 03]. Our models are high level descriptions of continuous time Markov chains: proteins are modelled by synchronous processes and reactions by transitions. Concentrations are modelled by discrete, abstract quantities. The main advantage of our approach is that using a (continuous time) stochastic logic and the PRISM model checker, we can perform quantitative analysis such as what is the probability that if a concentration reaches a certain level, it...
Games for Modal and Temporal Logics
- Martin Lange
Every logic comes with several decision problems. One of them is the model checking problem: does a given structure satisfy a given formula? Another is the satisfiability problem: for a given formula, is there a structure fulfilling it? For modal and temporal logics; tableaux, automata and games are commonly accepted as helpful techniques that solve these problems. The fact that these logics possess the tree model property makes tableau structures suitable for these tasks. On the other hand, starting with Büchi’s work, intimate connections between these logics and automata have been found. A formula can describe an automaton’s behaviour, and...
Formal analysis of java programs in javafan
- Azadeh Farzan; Feng Chen; José Meseguer
Abstract. JavaFAN is a Java program analysis framework, that can symbolically execute multithreaded programs, detect safety violations searching through an unbounded state space, and verify finite state programs by explicit state model checking. Both Java language and JVM bytecode analyses are possible. JavaFAN’s implementation consists of only 3,000 lines of Maude code, specifying formally the semantics of Java and JVM in rewriting logic and then using the capabilities of Maude for efficient execution, search and LTL model checking of rewriting theories. 1
A Typed Foundation for Directional Logic Programming
Mizar’s Soft Type System
- Freek Wiedijk
Abstract. In Mizar, unlike in most other proof assistants, the types are not part of the foundations of the system. Mizar is based on untyped set theory, which means that in Mizar expressions are typed but the values of those expressions are not. In this paper we present the Mizar type system as a collection of type inference rules. We will interpret Mizar types as soft types, by translating Mizar’s type judgments into sequents of untyped first order predicate logic. We will then prove that the Mizar type system is correct with respect to this translation in the sense that...
Automated Generation of Robust Error Recovery Logic in Assembly Systems Using Genetic Programming
Automated assembly lines are subject to unexpected failures, which can cause costly shutdowns. Generally, the recovery process is done “on-line ” by human experts or automated error recovery logic controllers embedded in the system. However, these controller codes are programmed based on anticipated error scenarios and, due to the geometrical features of the assembly lines, there may be error cases that belong to the same anticipated type but are present in different positions, each requiring a different way to recover. Therefore, robustness must be assured in the sense of having a common recovery algorithm for similar cases during the recovery...
Simple nominal type theory
- James Cheney
Abstract. Nominal logic is an extension of first-order logic with features useful for reasoning about abstract syntax with bound names. For computational applications such as programming and formal reasoning, it is desirable to develop constructive type theories for nominal logic which extend standard type theories for propositional, first- or higher-order logic. This has proven difficult, largely because of complex interactions between nominal logic’s name-abstraction operation and ordinary functional abstraction. This difficulty already arises in the case of propositional logic and simple type theory. In this paper we show how this difficulty can be overcome, and present a simple nominal type...
Reasoning about Judgment and Preference Aggregation ABSTRACT
Agents that must reach agreements with other agents need to reason about how their preferences, judgments, and beliefs might be aggregated with those of others by the social choice mechanisms that govern their interactions. The recently emerging field of judgment aggregation studies aggregation from a logical perspective, and considers how multiple sets of logical formulae can be aggregated to a single consistent set. As a special case, judgment aggregation can be seen to subsume classical preference aggregation. We present a modal logic that is intended to support reasoning about judgment aggregation scenarios (and hence, as a special case, about preference...