Verifying Privacy Enhanced Mail Functions with Higher Order Logic
- Dan Zhou,Shiu-kai Chin
. Security properties such as privacy, authentication, and integrity
are of increasing importance to networked systems([KAU]). Systems with
security requirements typically must operate with a high degree of confidence.
We show how the message structures of Privacy Enhanced Mail (PEM,
[LIN, BAL]) and the functions on PEM structures have the desired implementation
-independent security properties. Higher-order logic ([AND]) and the
HOL theorem-prover([GOR]) are used to precisely relate security properties
to system specifications. The structures of MIC-CLEAR and ENCRYPTED
messages are modeled as tuples of fields. Each of these fields is modeled as a
type which takes only a limited set of values as valid ([MEL]). Security functions
for checking privacy,...
Automatic Verification of Real-time Systems with Discrete Probability Distributions
- Marta Kwiatkowska,Roberto Segala
We consider the timed automata model of , which allows the analysis of realtime
systems expressed in terms of quantitative timing constraints. Traditional approaches
to real-time system description express the model purely in terms of nondeterminism;
however, it is often desirable to express the likelihood of the system
making certain transitions. In this paper, we present a model for real-time systems
augmented with discrete probability distributions. Furthermore, two approaches to
model checking are introduced for this model. The first uses the algorithm of 
to provide a verification technique for our model against temporal logic properties
which can refer both to timing properties and probabilities. The second, generally
Using Abduction to Evolve Inconsistent Requirements Specifications
- Bashar Nuseibeh,Alessandra Russo
Requirements specifications are often inconsistent. Inconsistencies may arise because multiple conflicting
requirements are embodied in these specifications, or because the specifications themselves are in a
transient stage of evolutionary development. In this paper we argue that such inconsistencies, rather than
being undesirable, are actually useful drivers for changing the requirements specifications in which they
arise. We present a formal technique to reason about inconsistency handling changes. Our technique is an
adaptation of logical abduction -- adapted to generate changes that address some specification
inconsistencies, while leaving others. We represent our specifications in quasi-classical (QC) logic -- an
adaptation of classical logic that allows continued reasoning in the...
Extending Fuzzy Logics to Support Decisions
- Wojciech Jamroga
. In this paper a concept of evaluation schema for uncertain statements is proposed. The aim is to represent
and process knowledge and to support decision making under uncertainty, involving the information with unmeasurable
uncertainty in the reasoning process. This 'uncertainty logic' is based on fuzzy logics and L/ukasiewicz
three-valued logic, but it's underlied by a richer structure that makes more subtle analysis of statements possible.
The logic is a kind of L-fuzzy logic formally. However, its ontological motivations are different.
Keywords: knowledge representation, reasoning under uncertainty,
decision making, fuzzy logics, three-valued logic.
1.1 Philosophical Motivations
According to (Klir & Folger 1988), situations of uncertainty arise either...
Logic Programming with Linear Logic
- Michael David Winikoff
Programming languages are the basic tools of computer science. The design of a good
programming language is a trade-off between many factors. Perhaps the most important
and difficult trade-off is between execution efficiency and programmer efficiency.
Higher level languages reduce the amount of work the programmer has to do; however
they have, to date, been less efficient than lower level languages. That lower level languages
are necessarily more efficient is a piece of folklore which is under attack -- higher
level languages are constantly coming closer to the performance of the lower level languages.
A consequence of this constantly closing performance gap is that the abstraction
Transition Density, A New Measure of Activity in Digital Circuits
- Farid N. Najm
Reliability assessment is an important part of the design process of digital integrated circuits.
We observe that a common thread that runs through most causes of run-time failure is the
extent of circuit activity, i.e., the rate at which its nodes are switching. We propose a new
measure of activity, called the transition density, which may be defined as the "average
switching rate" at a circuit node. Based on a stochastic model of logic signals, we also
present an algorithm to propagate density values from the primary inputs to internal and
output nodes. To illustrate the practical significance of this work, we demonstrate how the
Holcf = Hol + Lcf
- Olaf Muller,Tobias Nipkow,David Von Oheimb,Oscar Slotosch
HOLCF is the definitional extension of Church's Higher-Order Logic with Scott's Logic
for Computable Functions that has been implemented in the theorem prover Isabelle. This
results in a flexible setup for reasoning about functional programs. HOLCF supports standard
domain theory (in particular fixpoint reasoning and recursive domain equations) but
also coinductive arguments about lazy datatypes. This paper describes in detail how domain
theory is embedded in HOL and presents applications from functional programming,
concurrency and denotational semantics.
HOLCF is a logic for reasoning about functional programs. It provides arbitrary
forms of recursion (via a fixpoint operator) and a package for defining datatypes.
The latter caters for infinite objects,...
Goal-Directed Proof Search in Multiple-Conclusioned Intuitionistic Logic
- James Harland,Tatjana Lutovac,Michael Winikoff
. A key property in the definition of logic programming languages is
the completeness of goal-directed proofs. This concept originated in the study of
logic programming languages for intuitionistic logic in the (single-conclusioned)
sequent calculus LJ, but has subsequently been adapted to multiple-conclusioned
systems such as those for linear logic. Given these developments, it seems interesting
to investigate the notion of goal-directed proofs for a multiple-conclusioned
sequent calculus for intuitionistic logic, in that this is a logic for which there are
both single-conclusioned and multiple-conclusioned systems (although the latter
are less well known). In this paper we show that the language obtained for
the multiple-conclusioned system differs from that...
Fuzzy Selection and Blending of Behaviors for Situated Autonomous Agent
- Franois Michaud,Grard Lachiver,Chon Tam,Le Dinh
Intelligent control is a field of research attempting to
attain demanding control goals in complex systems. To
do so, many methods and theories must be combined and
used efficiently. We propose a new control architecture
that tries to unify the principles and characteristics
associated with intelligence. This architecture uses
behaviors as its basic control components. These
behaviors are selected dynamically and their actions are
combined according to the intentions of the agent.
Introspection of its reactions is one major new ability
given to the agent by this architecture. A simulated world
for mobile robots is used to validate the characteristics and
the principles associated with our proposed architecture.
This article focuses on the...
Testing Attribute Grammars
- Universitt Rostock Fachbereich Informatik
Fundamental notions for testing attribute grammars are developed. Two dimensions are explored. The structural dimension focuses on the context-free grammar part of an attribute grammar, whereas the semantic dimension is concerned with attributes, attribute types, conditions, and computations. In both dimensions, and also for the combination of them, we are interested in coverage notions, test set criteria (e.g., minimum test sets), and test set generation. The described framework builds upon abstract interpretation technology, and search algorithms. The approach is also applicable to some other representatives of the declarative paradigm, such as logic programming and term rewriting. Examples illustrate that the...
Formal Development of Secure Email
- Dan Zhou,Joncheng C. Kuo,Susan Older,Shiu-kai Chin
Developing systems that are assured to be secure requires
precise and accurate descriptions of specifications, designs,
implementations, and security properties. Formal specification
and verification have long been recognized as giving
the highest degree of assurance. In this paper, we describe
a software development process that integrates formal
verification and synthesis. We demonstrate this process
by developing assured sender and receiver C++ code for
a secure electronic mail system, Privacy Enhanced Mail.
We use higher-order logic for system-requirements specification,
design specifications and design verification. We
use a combination of higher-order logic and category theory
and tools supporting these formalisms to refine specifications
and synthesize code. Much of our work is applicable
to other secure email...
Pipelined DSP Design with a True Single-Phase Energy-Recovering Logic Style
- Suhwan Kim,Marios C. Papaefthymiou
We recently invented a true single-phase energy-recovering circuit family, called TSEL, that relies
on a cross-coupled latch structure and two DC reference voltages to achieve low energy consumption
for a broad range of operating frequencies. In this paper, we explore the application of TSEL to
the design of low-energy DSP circuits. Specically, we describe and evaluate a 6,768-transistor,
pipelined TSEL module that performs the 8-point Hadamard Transform. In layout simulations with
a standard 0.5m CMOS technology, our TSEL module functions correctly for operating frequencies
in excess of 280MHz. Above 40MHz, our TSEL design is more energy-ecient than any other
energy-recovering alternative with a similar cross-coupled latch structure....
Linear Relaxations and Reduced-Cost Based Propagation of Continuous Variable Subscripts
- Greger Ottosson,Erlendur S. Thorsteinsson
In hybrid solvers for combinatorial optimization, combining Constraint (Logic) Programming (CLP) and Mixed Integer Programming (MIP), it is important to have tight connections between the two domains. We extend and generalize previous work on automatic linearizations and propagation of symbolic CLP constraints that cross the boundary between CLP and MIP. We also present how reduced costs from the linear programming relaxation can be used for domain reduction on the CLP side. Computational results comparing our hybrid approach with pure CLP and MIP on a configuration problem show significant speed-ups.
SimNet, A Tool for Simulation with Application to Project Network Analysis
- Fredrick Von Schoultz,Aimo Torn
Simulation Nets (SN) are Petri
Nets extended for convenient modelling of
discrete event simulation problems. The extensions
included are zero testing, firing time
for transitions, or-logic and net hierarchies.
The tool SimNet accepts a text equivalence
of SNs and performs the simulation implied
by the SN model. Validation is facilitated
by providing trace, animation, and statistics
collection. An application to project network
analysis is described.
Key words: Petri Nets, discrete event simulation,
Simula, Simulation Nets, project networks
Simulation Nets or as they then were called, Simulation
Graphs, were introduced in 1981 as a simulation
modelling tool based on extended Petri Nets
[Torn 1981]. The first computer tool, Simnex, capable
of reading a single Simulation Net and...
Single-Phase Source-Coupled Adiabatic Logic
- Suhwan Kim,Marios C. Papaefthymiou
Adiabatic circuits offer a promising alternative to conventional circuitry
for low energy design. Their operation is nevertheless subject
to fundamental energy-speed trade-offs, just like any other physical
realization of boolean logic. Thus, adiabatic circuits with very
low energy consumption at low frequencies fail to function at high
operating frequencies. Conversely, high-speed adiabatic circuits
tend to be dissipative at low clock rates.
This paper describes SCAL, a single-phase source-coupled adiabatic
logic family that operates efficiently across a wide range
of operating frequencies. In layout-based simulations with 0.5m
CMOS process parameters, pipelined carry-lookahead adders developed
in our logic function correctly from 10MHz up to 280MHz.
Our SCAL adders are less dissipative than corresponding designs...
A Kleene Analysis of Mobile Ambients
- Flemming Nielson,Hanne Riis Nielson,Mooly Sagiv
We show how a program analysis technique originally developed for C-like pointer structures can be adapted to analyse the hierarchical structure of processes in the ambient calculus. The technique is based on modeling the semantics of the language in a two-valued logic; by reinterpreting the logical formulae in Kleene's three-valued logic we obtain an analysis allowing us to reason about may as well as must properties. The correctness of the approach follows from a general Embedding Theorem for Kleene's logic; furthermore embeddings allow us to reduce the size of structures so as to control the time and space complexity of...
BI as an Assertion Language for Mutable Data Structures
- Peter W. O'hearn,Samin Ishtiaq
Reynolds has recently developed a logic for reasoning about mutable data structures,
where pre- and post-conditions are written in an intuitionistic logic enriched with a spatial
form of conjunction. We investigate the approach from the point of view of the logic BI
of O'Hearn and Pym. We begin by giving a model in which the law of the excluded
middle holds, thus showing that the approach is compatible with classical logic. The
relationship between the intuitionistic and classical versions of the system is established by
a translation, analogous to Kripke's translation of intuitionistic logic into the modal logic
S4. We also consider the question of completeness of...
Constructing Conditional Plans by a Theorem-Prover
- Jussi Rintanen
The research on conditional planning rejects the assumptions that there is no uncertainty
or incompleteness of knowledge with respect to the state and changes of the system the
plans operate on. Without these assumptions the sequences of operations that achieve
the goals depend on the initial state and the outcomes of nondeterministic changes in the
system. This setting raises the questions of how to represent the plans and how to perform
plan search. The answers are quite different from those in the simpler classical framework.
In this paper, we approach conditional planning from a new viewpoint that is motivated by
the use of satisfiability algorithms in classical...
Computationally Grounded Theories of Agency
- Michael Wooldridge
In this paper, I motivate, define, and illustrate the notion
of computationally grounded theories of agency. A theory
of agency is said to be computationally grounded if we can
give the theory an interpretation in terms of some concrete
computational model. This requirement is essential if we
are to claim that the theories we develop can be understood
as expressing properties of real multiagent systems. After
introducing and formally defining the concept of a computationally
grounded theory of agency, I illustrate the idea with
reference to VSK logic, a formalism for reasoning about
agent systems that has a semantics defined with respect to
an automata-like model of agents. VSK logic is...
Model Checking in CLP
- Giorgio Delzanno,Andreas Podelski
. We show that Constraint Logic Programming (CLP) can
serve as a conceptual basis and as a practical implementation platform
for the model checking of infinite-state systems. Our contributions are:
(1) a semantics-preserving translation of concurrent systems into CLP
programs, (2) a method for verifying safety and liveness properties on
the CLP programs produced by the translation. We have implemented
the method in a CLP system and verified well-known examples of infinitestate
programs over integers, using here linear constraints as opposed to
Presburger arithmetic as in previous solutions.
Automated verification methods can today be applied to practical systems
[McM93]. One reason for this success is that implicit representations of