| Policy-Based Design and Verification for Mission Assurance |
Aug 2011 |
15 pages |
| Authors:
Shiu-Kai Chin; Sarah Muccio; Susan Older; Thomas N Vestal; SYRACUSE UNIV NY DEPT OF ELECTRICAL ENGINEERING AND COMPUTER SCIENCE
|
 | Intelligent systems often operate in a blend of cyberspace and physical space. Cyberspace operations planning, actions, and effects in realms where signals affect intelligent systems - often occur in milliseconds without human intervention. Decisions and actions in cyberspace can affect physical space, particularly in SCADA - supervisory control and data acquisition systems. For critical military missions, intelligent and autonomous systems must adhere to commander intent and operate in ways that ... |
|
| Function Extraction (FX) Research for Computation of Software Behavior: 2010 Development and Application of Semantic Reduction Theorems for Behavior Analysis |
Feb 2011 |
35 pages |
| Authors:
Richard Linger; Tim Daly; Mark Pleszkoch; CARNEGIE-MELLON UNIV PITTSBURGH PA SOFTWARE ENGINEERING INST
|
| For several years, the Software Engineering Institute (SEI) at Carnegie Mellon University has been engaged in a project to compute the behavior of software with mathematical precision to the maximum extent possible. Air Force Office of Scientific Research (AFOSR) sponsorship has played a key role in this effort. The general thrust of the research for AFOSR has been in technology for the following: (1) overcoming difficult aspects of behavior computation, ... |
|
| Optimization-Based Routing and Scheduling of IED-Detection Assets in Contemporary Military Operations |
JUN 2009 |
228 pages |
| Authors:
Christopher E. Marks; ALFRED P SLOAN SCHOOL OF MANAGEMENT CAMBRIDGE MA
|
| Improvised Explosive Devices, or IEDs, have become a familiar and lethal part of contemporary military operations in Iraq and Afghanistan, producing more casualties than any other weapons system. One reason for their success is their practicality in an environment characterized by imbalances in the capabilities of opposing forces. The military forces conducting stability operations in Iraq and Afghanistan rely on the existing road networks to support logistical and operational movements. ... |
|
| A Metadata Calculus for Securing Information Flows |
Dec-2008 |
8 pages |
| Authors:
Mudhakar Srivatsa; Dakshi Agrawal; Shane Balfe; IBM THOMAS J WATSON RESEARCH CENTER YORKTOWN HEIGHTS NY
|
| Traditional approaches to information sharing use a highly conservative approach to deduce the metadata for an output object x derived from input objects y(sub 1), y(sub 2), ... , y(sub n) [e.g.: maximum over the security labels of all input objects]. Such approaches does not account for functions that explicitly down- grade the value of an object. Consequently, the security labels in traditional approaches tend to monotonically increase as newer ... |
|
| Approved Methods and Algorithms for DoD Risk-Based Explosives Siting |
02 FEB 2007 |
321 pages |
| Authors:
Meredith J. Harwick; John Hall; John W. Tatom; Robert G. Baker; APT RESEARCH INC HUNTSVILLE AL
|
| The Safety Assessment for Explosives Risk (SAFER) model was developed to provide a more comprehensive assessment of the overall risk associated with explosives operations and storage. The SAFER model calculates risk in terms of the statistical expectation for loss of life from an explosives event. Three components are multiplied to estimate annual maximum probability of fatality, P(f), and the expected fatalities, E(f): (1) the probability of an explosives event, P(e), ... |
|
| Equational Abstractions |
01-Jan-2007 |
37 pages |
| Authors:
Jose Meseguer; Miguel Palomino; Narciso Marti-Oliet; ILLINOIS UNIV AT URBANA-CHAMPAIGN DEPT OF COMPUTER SCIENCE
|
| Abstraction reduces the problem of whether an infinite state system satisfies a temporal logic property to model checking that property on a finite state abstract version. The most common abstractions are quotients of the original system. We present a simple method of defining quotient abstractions by means of equations collapsing the set of states. Our method yields the minimal quotient system together with a set of proof obligations that guarantee ... |
|
| Information Sharing Policies for Coalition Systems |
01 OCT 2006 |
33 pages |
| Authors:
Laurence Cholvy; Christophe Garion; Claire Saurel; OFFICE NATIONAL D'ETUDES ET DE RECHERCHES AEROSPATIALES TOULOUSE (FRANCE)
|
| The aim of this paper is to define a logical language to express information sharing policies for coalitions, which have to cope with dynamical environments. We propose to use a first-order logic base language to express policies via concepts like time, action, context, roles in organizations and deontic notions. We define then consistency for a sharing policy and propose two definitions for policy completeness. |
|
| On Applying Point-Interval Logic to Criminal Forensics (Student Paper) |
JUN 2006 |
33 pages |
| Authors:
Mashhood Ishaque; Abbas K. Zaidi; Alexander H. Levis; GEORGE MASON UNIV FAIRFAX VA SYSTEMS ARCHITECTURE LAB
|
| Application of a temporal logic to forensic analysis, especially in answering certain investigative questions related to time-sensitive information, is presented. A set of temporal facts is taken from the London bombing incident that took place on July 7, 2005, to illustrate the approach. The information used in the illustration is gathered through the online news sites. A hypothetical investigation on the information is carried out to identify certain time intervals ... |
|
| Information-Based Security Protocols for Ideal Agents |
10 FEB 2006 |
101 pages |
| Authors:
Hans-Pieter van Ditmarsch; OTAGO UNIV DUNEDIN (NEW ZEALAND)
|
| The objective to model check properties of protocols for card playing agents has been met. Beyond the objectives we are pleased to report that we have made a state-of-the-art comparison of epistemic model checkers. We have paid some attention to other protocols, namely different generalizations of card playing protocols. We applied model checking tools to a rather different protocol (that has the form of a riddle about natural numbers). We ... |
|
| Automated Tools for Mapping Among Ontologies |
FEB 2006 |
23 pages |
| Authors:
Drew McDermott; YALE UNIV NEW HAVEN CT DEPT OF COMPUTER SCIENCE
|
| The Yale/BBN effort was focused on developing techniques for implementing and managing ontology translations. The simplest case is translation of datasets or queries expressed using one ontology into datasets or queries expressed in another. They devised and implemented the merging-deduction- projection model: Bridging axioms are stored in merged ontologies; a set of facts to translate are used to start forward chaining using the bridging axioms; conclusions in the target ontology ... |
|
| Numerical Solution of the Problem of the Computational Time Reversal in the Quadrant |
21 SEP 2005 |
17 pages |
| Authors:
Michael V. Klibanov; Sergey I. Kabanikhin; Dmitrii V. Nechaev; NORTH CAROLINA UNIV AT CHARLOTTE DEPT OF MATHEMATICS
|
| The problem of the computational time reversal is posed as the inverse problem of the determination of an unknown initial condition with a finite support in a hyperbolic equation, given the Cauchy data at the lateral surface. A stability estimate for this ill-posed problem implies refocusing of the time reversed wave field. Two such two-dimensional inverse problems are solved numerically in the case when the domain is quadrant and the ... |
|
| Composite Combat Identification (CCID) Common Reasoning Algorithm Development Program |
20 JAN 2005 |
21 pages |
| Authors:
RAYTHEON CO TEWKSBURY MA INTEGRATED DEFENSE SYSTEMS
|
| This report presents the CRA (the CCID Common Reasoning Algorithm) Evaluation activity and its findings for the ONR CRA Development program, for which Raytheon is the prime contractor and HRL is a subcontractor responsible for the evaluation task. The CRA is a new implementation of the CCID algorithm CIDER, which was developed by Raytheon/HRL under the ONR CCID Phase-I program. Like CIDER, CRA also contains an ingest module and a ... |
|
| Probability Distribution Classification Processor |
05 JAN 2005 |
32 pages |
| Authors:
Christopher M. DeAngelis; DEPARTMENT OF THE NAVY WASHINGTON DC
|
| This patent application discloses a system and method that preferably comprises several groups of artificial neural networks (ANNs) for classifying the probability distribution of random data. Each group of artificial neural networks is preferably trained to produce a selected output in response to data having a particular probability distribution, and each group preferably analyzes a different sample size of data. A parameter estimator module calculates statistical parameters for the different ... |
|
| An Approximation Technique for Belief Revision in Timed Influence Nets |
JUN 2004 |
28 pages |
| Authors:
Sajjad Haider; Alexander Levis; GEORGE MASON UNIV FAIRFAX VA SYSTEMS ARCHITECTURE LAB
|
| The paper presents an approach for belief updating in Timed Influence Nets. Influence Nets provide graphical representation of causal or influencing relationships in complex situations. They are used to model and evaluate courses of actions in certain domains and to compare the performance of actions based on the desired outcome. In Timed Influence Nets, the impact or effect of these actions on target variables is not instantaneous. This is modeled ... |
|
| Forward-Chaining Planning in Nondeterministic Domains |
2004 |
7 pages |
| Authors:
Ugur Kuter; Dana Nau; MARYLAND UNIV COLLEGE PARK DEPT OF COMPUTER SCIENCE
|
| This paper presents a general technique for taking forward-chaining planners for deterministic domains (e.g., HSP, TLPlan, TALplanner, and SHOP2) and adapting them to work in nondeterministic domains. Our results suggest that our technique preserves many of the desirable properties of these planners, such as the ability to use heuristic techniques to achieve highly e cient planning. In our experimental studies on two problem domains, the well-known MBP algorithm took exponential ... |
|
| Time Sensitive Control of Aerospace Operations |
NOV 2003 |
9 pages |
| Authors:
Alexander H. Levis; Lee W. Wagenhals; GEORGE MASON UNIV FAIRFAX VA CENTER OFEXCELLENCE IN COMMAND CONTROL COMMUNICATIONS/INTELLIGENCE
|
| Task 1 The theoretical objectives of the task have been achieved; the approach can now handle MTMF-type I systems with the help of hierarchical Point graphs, developed as part of the research initiative. The software implementation of the methodology, called TEMPER, incorporates some of the new features; however, a comprehensive revision of the tool is required to satisfy the objective stated. The provision for point-interval representation of time, an expressive ... |
|
| Formal Compiler Implementation in a Logical Framework |
29 APR 2003 |
54 pages |
| Authors:
Jason Hickey; Aleksey Nogin; Adam Granicz; Brian Aydemir; CALIFORNIA INST OF TECH PASADENA
|
| The task of designing and implementing a compiler can be a difficult and error-prone process. In this paper, we present a new approach based on the use of higher-order abstract syntax and term rewriting in a logical framework. All program transformations, from parsing to code generation, are cleanly isolated and specified as term rewrites. This has several advantages. The correctness of the compiler depends solely on a small set of ... |
|
| Adaptability - A New Principle of War |
07 APR 2003 |
52 pages |
| Authors:
Brian D. Dickerson; ARMY WAR COLL CARLISLE BARRACKS PA
|
| The Principles of War are an accepted tool to assist warfighters. They attempt to model those aspects of war the U.S. military feels are important to consider when planning for war or executing a campaign. The Principles also consciously and unconsciously influence the U.S. military establishment across a wide spectrum outside of war. These include, but are by no means limited to visioning the future military, weapons development and acquisition, ... |
|
| A Syntactic Approach to Foundational Proof-Carrying Code |
2002 |
45 pages |
| Authors:
Nadeem A. Hamid; Zhong Shao; Valery Trifonov; Stefan Monnier; Zhaozhong Ni; YALE UNIV NEW HAVEN CT DEPT OF COMPUTER SCIENCE
|
| Proof-Carrying Code (PCC) is a general framework for verifying the safety properties of machine-language programs. PCC proofs are usually written in a logic extended with language-specific typing rules; they certify safety but only if there is no bug in the typing rules. In Foundational Proof-Carrying Code (FPCC), on the other hand, proofs are constructed and veri ed using strictly the foundations of mathematical logic, with no type-specific axioms. FPCC is ... |
|
| HOL2GDT a Formal Verification-Based Design Methodology |
APR 2001 |
122 pages |
| Authors:
Anand Chavan; Byoung Woo Min; Shiu-Kai Chin; SYRACUSE UNIV NY
|
| HOL2GDT is a VLSI design methodology. It starts with a design implementation description that is formally verified using the Higher Order Logic (HOL) theorem prover. This implementation description is translated into a hardware description language model by using a HOL2GDT compiler, and with this model a physical design layout is generated by using IC design placement and routing tools in Mentor Graphic's Generator Design Technology (GDT) package. Thus, the final ... |
|
| Prediction and Inference with Incomplete Probabilistic Knowledge |
28 FEB 2001 |
8 pages |
| Authors:
Gordon M. Kaufman; ALFRED P SLOAN SCHOOL OF MANAGEMENT CAMBRIDGE MA
|
| A principal goal of modern reliability analysis is to design methods for appraising the reliability of large, logically complex systems that must operate at exceptionally high levels of reliability, but are subject to failure at uncertain times in uncertain ways. Nuclear power plants, the space shuttle, DARPA net and fly-by-wire aircraft are examples of such systems. Current practice is to design a probabilistic model of the stochastic behavior of a ... |
|
| Elimination of Negation in a Logical Framework |
15 DEC 2000 |
164 pages |
| Authors:
Alberto Momigliano; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| We address the issue of endowing a logical framework with a logically justified notion of negation. Logical frameworks with a logic programming interpretation such as hereditary Harrop formulae cannot directly express negative information, although negation is a useful specification tool. Since negation-as-failure does not fit well in a logical framework, especially one endowed with hypothetical and parametric judgments, we adapt the idea of elimination of negation from Horn logic to ... |
|
| Optimal Allocation of Distributed Resources Using Fuzzy Logic and a Genetic Algorithm |
29 SEP 2000 |
22 pages |
| Authors:
James F. Smith III; Robert D. Rhyne Ii; NAVAL RESEARCH LAB WASHINGTON DC TACTICAL ELECTRONIC WARFARE DIV
|
| A fuzzy logic-based resource manager (RM) that will allocate electronic attack (EA) resources distributed across many platforms is under development. The platforms will consist of ships, helicopters, airplanes, land- based facilities, robotic devices, and, potentially, satellites. The RM will allow codification of military expertise in a simple mathematical formalism known as the fuzzy decision tree. The fuzzy decision tree will form what is known ... |
|
| Validation and Verification of Formal Specifications in Object-Oriented Software Engineering |
SEP 2000 |
|
| Authors:
Steven A. Thomson; AIR FORCE INST OF TECH WRIGHT-PATTERSONAFB OH
|
 | The use of formal specifications allows for a software system to be defined with stringent mathematical semantics and syntax via such tools as propositional calculus and set theory. There are many perceived benefits garnered from formal specifications, such as a thorough and in-depth understanding of the domain and system being specified and a reduction in user requirement ambiguity. Probably the greatest benefit of formal specifications, and that which is least ... |
|
| Approximate Symbolic Model Checking Using Overlapping Projections |
AUG 2000 |
155 pages |
| Authors:
Gaurishankar Govindaraju; STANFORD UNIV CA DEPT OF ELECTRICAL ENGINEERING
|
| Bugs in hardware cost money. Whenever an error creeps into a design, time and money must be spent to locate the problem and correct it. With the growing complexity of digital systems, and the tremendous pressure for early- time-to-market schedules, the need for verification tools that can help designers catch bugs at an early stage in the design process cannot be overemphasized. Traditional methods of verification are empirical in nature ... |
|
| Proof-Term Synthesis on Dependent-Type Systems via Explicit Substitutions |
NOV 1999 |
33 pages |
| Authors:
Cesar Munoz; INSTITUTE FOR COMPUTER APPLICATIONS IN SCIENCE AND ENGINEERING HAMPTON VA
|
| Typed lambda-terms are used as a compact and linear representation of proofs in intuitionistic logic. This is possible since the Curry-Howard isomorphism relates proof trees with typed lambda-terms. The proofs-as-terms principle can be used to check a proof by type checking the lambda-term extracted from the complete proof tree. However, proof trees and typed lambda- terms are built differently. Usually, an auxiliary representation of unfinished ... |
|
| Combination and Interoperation of Logical Systems Research in Formal Interoperability |
30 APR 1999 |
10 pages |
| Authors:
John McCarthy; Carolyn Talcott; STANFORD UNIV CA DEPT OF COMPUTER SCIENCE
|
| This project involved investigation of both interpretations of the phrase formal interoperability: (1) formal semantics of the interoperation of components and their combination into complex systems; and (2) the interoperation of formal systems and their combined use to specify the many aspects of complex systems. (1) scientific foundations for sensible, correct and secure interaction between components; (2) formalizing different aspects of complex systems and ... |
|
| Site and Workspaces Layout Process Employing MDS and a PDI Formula in Which Density is Calculated Using a Unit Lattice Superposed over Circumscribing-Convex-Hulls |
02 MAR 1999 |
|
| Authors:
Francis J. O'Brien Jr; DEPARTMENT OF THE NAVY WASHINGTON DC
|
| A process is provided for producing layouts of building units. on a quadrilateral facility site and layouts of personnel workstations and items of equipment (collectively "workplace elements") in quadrilateral subarea in the building units. There are inter-building-unit, and inter-workplace- element, operational criteria associated with the activity being performed in the facility. The well known multidimensional scaling (MDS) methodology is employed in optimizing building unit and workplace element configurations to suit ... |
|
| Ordered Linear Logic Programming |
22 DEC 1998 |
35 pages |
| Authors:
Jeff Polakow; Frank Pfenning; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| We begin with a review of intuitionistic non-commutative linear logic (INCLL), a refinement of linear logic with an inherent notion of order proposed by the authors in prior work. We then develop a logic programming interpretation for INCLL in two steps: (1) we give a system of ordered uniform derivations which is sound and complete with respect to INCLL, and (2) we present a model of resource consumption ... |
|
| On Hybrid Systems and the Modal Mu-Calculus |
NOV 1998 |
35 pages |
| Authors:
J. M. Davoren; CORNELL UNIV ITHACA NY CENTER FOR FOUNDATIONS OF INTELLIGENT SYSTEMS
|
| Much of the contemporary work in logics for the formal verification of hybrid systems (notably the work of Henzinger at UC Berkeley and Manna at Stanford) builds directly on the framework of temporal logic verification of discrete systems. The core computational model is that of a hybrid automaton, which is represented formally as a transition system over a hybrid state space Xsubset contained in Q x IR(n), where Q is ... |
|
| Compiling with Proofs |
18 SEP 1998 |
272 pages |
| Authors:
George C. Necula; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| One of the major challenges of building software systems is to ensure that the various components fit together in a well-defined manner. This problem is exacerbated by the recent advent of software components whose origin is unknown or inherently untrusted, such as mobile code or user extensions for operating-system kernels or database servers. Such extensions are useful for implementing an efficient interaction model between a client and a server because ... |
|
| Classical Combinatorial Sequential Machine Components Implemented with Quantum Devices |
MAY 1998 |
36 pages |
| Authors:
Daniel J. Pease; SYRACUSE UNIV NY OFFICE OF SPONSORED PROGRAMS
|
| The majority of work today relating to quantum computing has provided results that are almost incomprehensible to even the most advanced computer architect. This paper uses the recent research results of quantum mechanical logic as building blocks to derive a computer architecture based on quantum devices that is consistent with existing system architectures. The new and admittedly exotic nature of quantum computing notwithstanding, this work presents a quantum mechanical analog ... |
|
| HOOTS II Second Workshop on Higher-Order Operational Techniques in Semantics. Volume 10 |
12 DEC 1997 |
311 pages |
| Authors:
Andrew Gordon; Andrew Pitts; Carolyn Talcott; STANFORD UNIV PALO ALTO CA
|
| This issue of ENTCS is an unrefereed conference record of talks presented at the Second Workshop on Higher Order Operational Techniques in Semantics held at Stanford University, December 8-11, 1997. The meeting was organized by A. Gordon, A. Pitts and C. Talcott with generous sponsorship from Harlequin Ltd, NSF and ONR. The study of operational techniques for higher-order languages has much research activity going on in distinct communities, including the ... |
|
| On the Properties of Multiple-Valued Functions that are Symmetric in Both Variable Values and Labels |
02 DEC 1997 |
22 pages |
| Authors:
John T. Butler; Tsutomu Sasao; NAVAL POSTGRADUATE SCHOOL MONTEREY CA DEPT OF ELECTRICAL AND COMPUTER ENGINEERING
|
| Functions that are symmetric in both variable labels and variable values are important for use as benchmarks. We present the properties of such functions, showing that they are isomorphic to partitions on r (the number of variables) with no part greater than r (the number of logic values). From this, we do an enumeration. Further, we derive lower bounds, upper bounds, and exact values for the number of prime implicants ... |
|
| Review Guidelines for Software Languages for use in Nuclear Power Plant Safety Systems |
01-Oct-1997 |
563 pages |
| Authors:
M Hecht; D Decker; S Graff; W Green; D Lin; G Dinsmore; S Koch; SOHAR INC BEVERLY HILLS CA
|
| Guidelines for the programming and auditing of software written in high level languages for safety systems are presented. The guidelines are derived from a framework of issues significant to software safety which was gathered from relevant standards and research literature. Language-specific adaptations of these guidelines are provided for the following high level languages: Ada83 and Ada95; C and C++; International Electrotechnical Commission (IEC) Standard 1131-3 Ladder Logic, Sequential Function Charts, ... |
|
| Second Calculus of Binary Relations as a Concurrent Programming Language |
26 AUG 97 |
5 pages |
| Authors:
Vaughan R. Pratt; STANFORD UNIV CA DEPT OF COMPUTER SCIENCE
|
| This grant supported Anna Patterson from June 1994 to October 1996, Russ Allbery from October 1995 to March 1997, and Larry Yogman from January 1997 to June 1997. Patterson wrote (1) A new semantics for constructible falsity, presented at ASL Summer Meeting 96, appearing in the Bulletin of Symbolic Logic and submitted to JSL; (2) Bisimulation and Propositional Intuitionistic Logic, presented at ESSLLI'96 and in more detail at Concur 1997 ... |
|
| Using Diagonally Implicit Multistage Integration Methods for Solving Ordinary Differential Equations. Part 2: Implicit Methods |
AUG 97 |
122 pages |
| Authors:
Jack Van Wieren; NAVAL AIR WARFARE CENTER WEAPONS DIV CHINA LAKE CA
|
| New theoretical results for implicit methods of the recently invented and highly promising class of diagonally implicit multistage integration methods (DIMSIMs) are described. Some new A-stable and L-stable methods are derived, and conditions for a method to have an A-stable or L-stable FASAL (First Approximately Same As Last) implementation are derived. New alternative error estimates are proposed and successfully tested. The stability regions for alternative predictor-corrector DIMSIM implementations are derived. ... |
|
| Relative Size of Certain Polynomial Time Solvable Subclasses of Satisfiability |
97 |
13 pages |
| Authors:
J. Franco; CINCINNATI UNIV OH DEPT OF ELECTRICAL AND COMPUTER ENGINEERING
|
| We determine, according to a certain measure, the relative sizes of several well known polynomially solvable subclasses of SAT. The measure we adopt is the probability that randomly selected k-SAT formulas belong to the subclass of formulas in question. This probability is a function of the ratio r of clauses to variables and we determine those ranges of this ratio that result in membership with high probability. We show, for ... |
|
| Model for Trauma Patient Simulation and Fluid Resuscitation |
NOV 96 |
275 pages |
| Authors:
Brian L. Robey; SOUTHWEST RESEARCH INST SAN ANTONIO TX
|
| SwRI performed mathematical modeling and simulation research aimed at developing a trauma patient simulator (TPSIM) for the Life Support Trauma and Transport (LSTAT) Army evacuation platform. The purpose of this research was to develop methods for predicting changes in hemodynamic parameters during and after blood loss. Prediction of hemodynamic parameters based on blood volume changes was the first step in the development of an automated fluid resuscitation system. The research ... |
|
| Automatic Construction of Accurate Models of Physical Systems |
29 AUG 96 |
6 pages |
| Authors:
Elizabeth Bradley; COLORADO UNIV AT BOULDER DEPT OF COMPUTER SCIENCE
|
|
| Maximum Entropy and Bayesian Methods |
JUL 96 |
414 pages |
| Authors:
glenn r. heidbreder; Hua Lee; CALIFORNIA UNIV SANTA BARBARA
|
| This volume contains selections from among the presentations at the Thirteenth International Workshop on Maximum Entropy and Bayesian Methods- MAXENT93 for short- held at the University of California, Santa Barbara (UCSB), August 1-5, 1993. This annual workshop is devoted to the theory and practice of Bayesian probability and the use of the maximum entropy principle in assigning prior probabilities. Like its predecessors, MAXENT93 attracted researchers and scholars representing a wide ... |
|
| Fuzzy Logic |
MAY 96 |
15 pages |
| Authors:
Sanjay Tailor; ARMY ARMAMENT RESEARCH DEVELOPMENT AND ENGINEERING CENTER PICATINNY ARSENAL N J FIRE SUPPORT ARMAMENT CENTER
|
| This report deals with the concepts of fuzzy logic and its use in modern commercial systems. The fundamental differences between conventional and fuzzy logic are explained. The discussion also includes procedures used to design systems with fuzzy logic and the capability of modern design tools. Some examples are provided to further clarify the concepts of fuzzy logic and to show how to develop fuzzy models using mathematical sets. The overall ... |
|
| Robust Transfiguring Network Protocols |
APR 96 |
35 pages |
| Authors:
Richard G. Ogler; Julie S. Wong; Irfan H. Khan; SRI INTERNATIONAL MENLO PARK CA
|
| In RTNP, we have developed a protocol that uses two artificial intelligence methods, neural networks and evidential reasoning, to recognize and predict adverse network conditions, and that uses fuzzy logic to dynamically control the parameters of a tunable routing protocol in response to the perceived environment. Examples of the tunable protocol parameters are: (1) a parameter that controls the degree to which traffic is spread over multiple paths; (2) a ... |
|
| A Case Study in Model Checking Software Systems |
APR 96 |
|
| Authors:
Jeanette M. Wing; Mandana Vaziri-Farahani; CARNEGIE-MELLON UNIV PITTSBURGH PA DEPT OF COMPUTER SCIENCE
|
| Model checking is a proven successful technology for verifying hardware. It works, however, on only finite state machines, and most software systems have infinitely many states. Our approach to applying model checking to software hinges on identifying appropriate abstractions that exploit the nature of both the system, S, and the property, phi, to be verified. We check phi on an abstracted, but finite, model of S. Following this approach we ... |
|
| Algebraic Representations of Linguistic and Numerical Modifications of Probability Statements and Inferences Based on a Product Space Construction |
MAR 96 |
6 pages |
| Authors:
I. R. Goodman; NAVAL COMMAND CONTROL AND OCEAN SURVEILLANCE CENTER RDT AND E DIV SAN DIEGO CA
|
| This paper addresses the problem of obtaining for any given probability space (A, B, P) an extension to a probability space (Ao, Bo, Po) such that for any given function f:(O,1)n to (0,1), suitably analytic, and any given finite collection of ordinary events a, b, c,...,m in sample space B, with possible relations among them, there is an event alpha sub f = alpha sub f (a,b, c,...,m) in Bo ... |
|
| Hierarchical Learning of Complex Systems |
29 FEB 96 |
25 pages |
| Authors:
Donald A. Glaser; CALIFORNIA UNIV BERKELEY DEPT OF PHYSICS
|
| A central problem in forecasting and controlling nonlinear processes is quantifying the trade-off between available computational resources, model complexity, and prediction error. A more subtle, but important issue that strongly affects success is the choice of representation, or model class. Should one use Fourier or wavelet transforms, neural networks, hidden Markov models, or fuzzy logic, as modeling frameworks? As a tool for answering the questions of representation dependence, brittleness, and ... |
|
| Workshop on Partial Order Methods in Verification |
1996 |
367 pages |
| Authors:
Doron Peled; Vaughan Pratt; Gerard Holzmann; RUTGERS - THE STATE UNIV PISCATAWAY NJ
|
| This report consists of the written papers presented at POMIV, the Workshop on Partial Order Methods in Verification held at Princeton July 24-26. POMIV is one of the workshops participating in the DIMACS Special Year in Logic, 1995-1996, and also immediately preceded the Federated Logic Conference (FLoC) held at Rutgers July 27-August 3. The theme of the workshop was the transition from the traditional interleaving model of concurrent computation to ... |
|
| Transforming Algebraically-Based Object Models into a Canonical Form for Design Refinement |
06 DEC 95 |
183 pages |
| Authors:
Charles G. Beem; AIR FORCE INST OF TECH WRIGHT-PATTERSON AFB OH SCHOOL OF ENGINEERING
|
| The understandability of object-oriented design techniques and the rigor of formal methods have improved the state of software development; however, both ideas have limitations. Object-oriented techniques, which are semi-formal, can still result in incorrect designs, while formal methods are complex and require an extensive mathematical background. The two approaches can be coupled, however, to produce designs that are both understandable and verifiable, and to produce executable code. This research proposes ... |
|
| Application of Artificial Intelligence in Decision Making in Mine Countermeasures |
DEC 95 |
|
| Authors:
T. M. Mansell; D. R. Skinner; K. K. Benke; DEFENCE SCIENCE AND TECHNOLOGY ORGANIZATION CANBERRA (AUSTRALIA)
|
| A number of analytic techniques used in Artificial Intelligence are examined in the context of decision making in mine countermeasures. Attention is directed at five major techniques, involving statistical inference, probabilistic inference, evidential reasoning, fuzzy logic and artificial neural networks. In the cases of statistical inference and evidential reasoning, solutions to appropriate problems are described. Eleven other techniques are dealt with more briefly, in most cases with worked examples of ... |
|
| Semantic Interpretation of An Artificial Neural Network |
DEC 95 |
95 pages |
| Authors:
Stanley D. Kinderknecht; AIR FORCE INST OF TECH WRIGHT-PATTERSON AFB OH
|
| Recent advances in machine learning theory have opened the door for applications to many difficult problem domains. One area that has achieved great success for stock market analysis/prediction is artificial neural networks. However, knowledge embedded in the neural network is not easily translated into symbolic form. Recent research, exploring the viability of merging artificial neural networks with traditional rule-based expert systems, has achieved limited success. In particular, extracting production (IF.. ... |
|
Reports by Keyword(s)
MATHEMATICAL LOGIC
