L2 Glossary

Back to Main Page

Agenda
A set of items ordered by a weight property; that is, a priority queue. Code: opsat/cbfs_agenda.h
apigen
An executable utility that takes a model and generates a *.h C header file for Enumerations.
Assign
Assignable Variable
An Assignable Variable is an independent Variable, one whose value can be assigned by the client. The set of Assignable Variables is partitioned into three subsets: It has the following properties: The opposite of an Assignable Variable is a Dependent Variable">. Code: conflict_db/assignable.*
Assignment
A binding of a Variable to a value in its domain. It has the following properties: Each Assignable maintains a list of all legal Assignments, as well as the current one, if any. Code: conflict_db/assignment.h
Assumption Variable
An Assignable Variable the value of which the Search Procedure can re-assign. Either a Mode Transition Variable or the State Variable. Code: conflict_db/assumption.*
Attribute
In the JMPL-to-XMPL Compiler, any element of a Component node.
Autonomous Transition
A Transition that can occur at any time without a guard condition being satisfied. The most important type is a Failure Transition.
Background
A property of a Clause that specifies a system invariant rather than properties of a Mode Transition. For example, every Variable must have exactly one value. If the domain is v1, v2, ... , , then the Constraints are
          variable[timeStep]=v1 | variable[timeStep]=v2 | ... | variable[timeStep]=vn
          !variable[timeStep]=v1 | !variable[timeStep]=v2
          !variable[timeStep]=v1 | !variable[timeStep]=v3
          ...
          !variable[timeStep]=v(n-1) | !variable[timeStep]=vn
          
bin
See l2bin.
Boolean Constraint Propagation
The same as Unit Propagation.
Candidate
A set of Assignments constituting an element of a Diagnosis. The Find Candidates operation returns a set of Candidate objects.
cb
Circuit Breaker, a very simple Model used for regression testing
CBFS
See Conflict-Directed Best-First Search.
CBFS Max Candidates
Configuration Parameter: maximum number of Candidates returned by the CBFS Tracker.
CBFS Max Rank
Configuration Parameter: maximum value of Ranks used by the CBFS Tracker.
CBFS Search Space
Configuration Parameter: maximum number of search space nodes to visit by the CBFS Tracker.
Checkpoint
Stores a checkpoint, which allows later restoring the state of Livingstone to this point.
Checksum
Two bytes are reserved for a cyclic redundancy check in l2bin Model Files, but the checksum is currently set to the constant 0.
Clause
A Clause is a conjunct Formula for a Propositional Theory. It is a disjunction of one or more Literals. It is represented by a list of Positive Propositions, a list of Negative Propositions and a Volatile flag.
cmdIn
By convention, this is the name for the Command input to a Component.
cmdOut
When a Component issues a Command to another Component, this is the name of the Command.
CNF
Conjunctive Normal Form (expressing a proposition as a conjunction of disjunctions).
Command
A control signal to a Device directing it to do something. Commands are represented in Livingstone as Command Variables. The arrival of a Command causes Livingstone to Progress
Command Variable
A Variable the value of which is a Command to a Device.
Commanded Transition
A Mode Transition that asserts how the Mode of a Component depends on the command. There are two types of Commanded Transition: Component and Unindexed Transition for the uncommanded Components. See also Idle Transition.
Component
Conflict
A set of Assignments to Assumption Variables that, if made, would imply inconsistent values for the same Variable.
Conflict Data Base
An in-memory store for the Variables, their values, and the Constraints on them. It has the following properties: It expresses Variable-value pairs as propositions for use by the LTMS. Code: conflict_db/conflict_db.*
Conflict-Directed Best-First Search
A Search Style that uses the Conflict-Directed Best-First Search search algorithm for diagnosis. The alternative is Cover./dd>
Consistency Checker
Code that checks whether an Assignment is consistent with a set of Constraints.
Constraint
A Clause representing permissible Assignments to Variables.
Cookie
An l2bin Model File begins with a 4-character code that identifies the file as a binary Model file for Livingstone. If this set of 4 characters is not found, the Model File Reader will not attempt to read in the Model from the file.
Cover
Search Style that uses the rho conflict coverage search algorithm for diagnosis. The alternative is CBFS. Code: cover/cover.*
Cover Max Rank
Configuration Parameter: maximum value of Ranks used by the Cover .
Datum
An application-specific data structure associated with a Clause that is the thing that the Clause describes.
Dependent Variable
A Dependent Variable is one whose value is inferred by the Conflict Data Base
from the Assignable Variables and the Constraints. The user can not set its value. The opposite of a Dependent Variable is an Assignable Variable. Code: conflict_db/dependent.*
Device
A structural and functional unit of a system being modeled. Devices are represented indirectly in Livingstone, by means of the Mode Transition Variables that characterize them. Also called a
Diagnosis
The set of Candidates at a given time.
Different Proposition
A predicate that the value of a Variable is unequal to that of a second Variable.
Discrepancy
The Observed Variables and Command Variables that conflict with the current Mode Assignment. After diagnosis, the Discrepancy will be null.
Discrete State Estimation
Diagnosis using Variables with finite domains, that is, Enumerations.
Domain
The set of values a Variable can be assigned.
Enumeration
Not only do all Variables in L2 have a discrete domain, these domains are finite, and have small cardinalities as well. An Enumeration is the domain of some Variable.
Evolution
The change in the state of the system (Assignments to Variables) as a function of time.
Explain
Prints the entire decision tree back to the Observations, initial Modes, and Mode Transitions.
Extend
A Find Candidates Style. It is available only with the CBFS Search Style. Takes all Candidates and uses them as the prefix for new ones. Consistent Candidates are returned unchanged; inconsistent ones may have new failures added.
Failure
Code: api/livingstone.*
Failure Mode
The device being modeled behaves not in the way it was intended to, but in one of a set of enumerated faulty ways. A Mode that is not a Failure Mode is a Nominal Mode.
Failure Transition
An Autonomous Transition from any Mode to a Failure Mode.
FC
Abbreviation for Find Candidates.
Find Candidates
Find Candidates Style
Configuration Parameter. One of the following:
Find Fresh Candidates
A Find Candidates Style. It is available only with the Cover Search Style. Discards all existing Candidates and then initiates diagonosis. It is slower because it has to re-discover discarded Candidates, but the set of Candidates will be most likely./dd>
Fringe
The fringe is the set of Unit Clauses. It is cached because they are often processed first.
Full Progress
A mode of operation of the Transition System in which all Variables are copied to the next Time Step upon receipt of a Command. See also Min Progress.
Gamma
The likelihood limit of Cover search.
GPU
Ground Processing Unit
Ground Processing Unit
A computer at a ground base running processes that receive, interpret and display Telemetry" data from a vehicle.
Harness
A Model File, with extension .hrn, that specifies which Assignable Variables are Observable Variables and which are Command Variables. See also Ini and Params.
History
Horizon
The earliest Time Step for which a full History is retained. It is expressed as a non-negative integer. A Transitioned Variable maintains pointers to the Mode Transition Variable at both the Horizon and the Zenith.
Horizon Transition
An Assumption Variable progressed backward in time from a Mode Transition Variable, representing the transition from the State Variable to the earliest stored Transitioned Variable.
Idle Transition
The Mode Transition taken by the Transition System when the Command is null (absent). For each component, one Constraint is added, to assert that the mode does not change if the Mode Transition was nominal:
          modeVariable[timeStep]=m & modeTransition[timeStep]=nominal =>
          modeVariable[timeStep+1]=m
          
See also Commanded Transition.
Indexed Transition
A Commanded Transition that asserts how the Mode of a commanded Component depends on the Command. One Constraint is added, asserting the change to the mode of the Component that is commanded if the Mode Transition is nominal:
         modeVariable[timeStep]=m1 & modeTransition[timeStep]=nominal & cmdIn=c =>
         modeVariable[timeStep+1]=m2
         
See also Unindexed Transition.
Initial Value
The value of a Variable when Livingstone is started.
Ini
A Model File, with extension .ini, that specifies initial values for Variables. See also Harness and Params.
Install
Insert a Candidate into the set to allow looking up its effects. Has no effect on the future evolution of the system.
Integrated Vehicle Health Management
A system for monitoring, diagnosing and correcting the state of a spacecraft.
IVHM
See Integrated Vehicle Health Management.
Java-Based Model Programming Language
A Model File Format. The syntax is more similar to that of Java than it is to that of Lisp. The JMPL compiler translates from JMPL to XMPL. See also L2 Format, l2bin, MPL and XMPL.
JMPL
See Java-based Model Programming Language.
JMPL Compiler
A Java program that translates a Model from JMPL to XMPL.
Kind
A partition of the set of Variables into Command Variables, Mode Transition Variables and Observed Variables.
L1
Livingstone 1, written in Common Lisp.
L2
l2bin
Binary Model File Format, a highly compressed representation. The structure is all present, but there are no print names for the model elements. Use utility xmpl2l2 to translate an XMPL format Model File into an l2bin format Model File. See also JMPL, L2 Format, MPL, and XMPL.
l2flight
An executable that runs L2 models with a minimal user interface and only flight code other than the UI. This allows for size and timing measurements. See also l2test.
L2 Format
An ASCII Model File Format. See also JMPL, l2bin, MPL and XMPL.
l2test
An executable that runs L2 models with a text interface (in contrast to the Stanley/Skunkworks GUI). See also l2flight
Likelihood Level
Listener
A Propositional Theory can have any number of Listeners. A Transition System can have any number of Listeners.
Literal
In a Clause, a Proposition, whether a Positive Proposition or a Negative Proposition.
Livingstone
A program that takes a model of a real-world system and a description of its state and, if there is any discrepancy between the intended and actual states of the system, delivers a diagnosis of the most likely cause(s) of that discrepancy.
Logic-Based Truth Maintenance System
LTMS
Logic-based Truth Maintenance System, and the name of a C++ class that implements it. It is the propositional inference system of the Conflict Data Base.
Magic Cookie
See "Cookie".
Max Truncated Candidates
Configuration Parameter: the maximum number of Candidates tracked before.
MBA Utilities
Because the C++ Standard Template Library is not standard enough, the support classes that are needed have been implemented for the use of L2.
Transition System in which the minimal number of Variables (only those that could possibly change) is tranistioned upon receipt of a Command. Min Progres requires that a Model be Optimized. See also Full Progress.
Mode
Mode Assignment
At a given Time Step, the Mode of a Device.
Mode Identification
Determination of the state of each device that is represented in the Model. This is active in Shadow Mode.
Mode Reconfiguration/Mode Recovery
Selecting (and executing) a Command that is intended to correct a faulty condition in the device being modeled.
Mode Transition Variable
Synonym for Transition Variable. An Assumption that a Component changed its Mode.
Mode Variable
A Dependent Variable, representing the state of a Device, the value of which is inferred. The domain is the union of the set of Nominal Modes and the set of Failure Modes, to which may be added a unique element representing an unknown mode. The initial value will typically be a Nominal Mode.
Model
A data structure that represents the real-world Device the faults of which Livingstone diagnoses. Models can be stored in Model Files of several different Model File Formats.
Model File
A file containing a specification of the Livingstone Model in some Model File Format or one of three kinds of files that is read in at the same time:
Model File Format
An encoding scheme for Model Files. The alternatives are:
Module
In Stanley, a non-leaf node of a Module. See Component.
Monitor
Code that maps a sensor reading value onto an Observed Variable.
Monitored Variable
Synonym for Observed Variable.
MPL
Model Programming Language, a representation of models for Livingstone using Lisp syntax. Many model builders are not comfortable with Lisp syntax, and so resist its use. See also JMPL and XMPL.
name2ids
An executable that translates a human-readable script (using names rather than numbers) into one that can be read by l2flight.
Negative Proposition
A Proposition" that a Variable does not have a specific value from an Enumeration.
Nominal Mode
A Device in the system being modeled behaves as it was intended to behave. There may be more than one Nominal Mode for a Device. The opposite is Failure Mode.
Nominal Transition
A Transition that is as intended; that is, it is not a Failure.
Observable Variable
Synonym for Observed Variable.
Observed Variable
An Assignable Variable is an Observed Variable if its value comes from a sensor.
Observation
A sensor reading from a Device, such as current, pressure, temperature, valve state or voltage. Observations are represented in Livingstone as Observation Variables.
Observe
Assign a value to an Observed Variable. An Observation does not causes Livingstone to Progress. The value will not be propagated immediately.
Observation Variable
Synonym for Observed Variable.
Opsat
Another name for the CBFS Tracker.
Optimize
Re-write a Model so that it is logically equivalent but Transitions can be computed more rapidly. Min Progress requires that a Model be optimized.
Parameter
A value that configures L2. Parameters can be read in from a file when the Model File is read in, or they can be set programmatically. The parameters are
Params
A Model File, with extension .params, that specifies configuration Parameters. See also Harness and Ini.
Positive Proposition
A Proposition that a Variable has a specific value from an Enumeration.
Present Variable
In T_system.h, a Variable at the NOW Time Step with the exception of the Mode Transition Variables. A Present Variable must be an instance of the following four classes: Note that when the Transition System copies a Present Variable into the history, the object's type may change to that of a supertype.
Prime Implicate
Progress
When a arrives, advance the Time Step one unit. There are two Progress Styles:
Progress Style
Configuration Parameter. One of two ways of performing a Progress:
Propagation
The LTMS performs propositional inference, determining whether its Propositional Theory is consistent. Propagate the values in the TMS to compute the logical inferences of the current set of Clauses.
Proposition
In Livingstone, a Proposition is an element of a Clause. It is an equality predicate that is partitioned into Positive Propositions and Negative Propositions. Same Propositions can be expressed as Positive Propositions and Different Propositions can be expressed as Negative Propositions. A Clause may Support a Proposition.
Propositional Theory
A Theory of a physical system consisting solely of statements in propositional logic, as opposed to first-order predicate calculus, a modal logic, etc. It consists of two parts: An LTMS has a Propositional Theory.
Prune and Search
A Find Candidates Style. Prunes the current set of Candidates.
PTheory
A short name for a
Rank
The relative plausibility of a Transition. If the Transition is Nominal Mode, the Rank is 0. Otherwise, for Failure Mode, the Rank is a positive number, essentially the negative of the logarithm of its prior probability.
Read
To incorporate a Model into Livingstone from a Model File in one of the Model File Formats.
Reader
The part of Livingstone that Reads a Model from a Model Filein one of the Model File Formats.
. The Readers also Optimize the Model.
Reconfiguration
Recovery from failure in the device. Livingstone can be compiled to do either diagnosis or planning, but not both with the same executable.
Recovery Mode
IVHM autonomously effects physical changes in the device being modeled. The opposite is Shadow Mode.
Restore
Restores the state of livingstone to what it was when the Checkpoint was stored.
RTAPI
Real-Time Application Programming Interface, an API for handling asynchronous input and output to Livingstone.
Same Proposition
A predicate that the value of one Variable is equal to that of a second Variable.
Satisfaction Search
A search which returns solutions based on whether they are consistent with some criterion. Code: opsat/opsat.h
Satisfiable
A Theory is Satisfiable if there is a way to Assign Truth Values that Satisfy all of its Clauses.
Satisfy
A Clause is said to be Satisified if at least one of its Propositions has a Truth Value of TRUE.
Search Method
Synonym for Search Style
Search Procudure
The code that makes Assignments to the Assumption Variable after a change to an Assignable Variable.
Search Style
One of the following:
Shadow Mode
IHVM diagnoses and communicates its inferences, but does not autonomously effect physical changes in the device being modeled. The opposite is Recovery Mode.
Skunkworks
The suite of programs including Livingstone and Stanley.
Solver
From the point of view of the Conflict Data Base, the LTMS is the "Solver."
Stanley
The model-building GUI tool, written in Tcl. The Models it produces are represented as JMPL files.
State Constraint
A Clause that constrains the values of Variables within the same Transitions.
State Variable
When the History is Truncated, the information for the removed Time Steps is stored in a special data structure called a State Variable. The State Variable is an Assumption Variable.
State Vector
A set of Variable-Value pairs that specifies the state of a device being modeled.
Summarize
When perfoming a Truncate operation, this is the mechanism for inserting "stub" Clauses that justify the Variable Assignments at the Horizon.
Support
A Clause supports a Proposition if the latter can be inferred from the former. Code: tms/clause.*; tms/proposition.*
Telemetry
The means of communication between the vehicle and the GPU.
Theory
A logical Model of a system, comprising the set of Variables and the set of Constraints. Currently, L2 can have only Propositional Theories.
Time Point
Synonym for Time Step.
Time Step
All Clauses having the same Time Step are re-evaluated together. The Transition System increments the Time Step.
TMS
Truth-Maintenance System.
Tracker
Controls the growth of the Transition System. A Tracker can be one of two types, depending on the Find Candidates Style: Code: transition/tracker.*
Trajectory
A sequence of state transitions from the initial state to a Candidate.
Transition
A Clause that constrains the values of Variables between one Time Step and the next Time Step.

A rule for changing a Mode TransitionVariable from one value (the "from" state) to another value (the "to" state). The event is conjunction of Clauses. The Rank of the Transition specifies the relative plausibility that the value is the "to" state.

There are several ways of partitioning Transitions. A ternary partition, based on implementation, is:

And a binary partition, based on semantics, is:
Transitioned Variable
Synonym for Mode Transition Variable.
Transition System
A specialization of the Conflict Data Base that handles time.
Truncate
Removing the oldest data (that is, Time Stepss before the Horizon) from the History.
Truth Value
Livingstone uses a three-valued logic, so a Proposition can have Truth Value of TRUE, FALSE or UNKNOWN.
Unassign
To bind the value UNKNOWN to an Observed Variable. This can not cause any conflicts. At start up, all Observed Variables are Unassigned.
Unindexed Transition
A Commanded Transition that asserts how the Mode remains unchanged when another Component is commanded. One Constraint is added for each uncommanded Component, asserting no change to the mode of the uncommanded Component if the Mode Transition is nominal:
          modeVariable[timeStep]=m & modeTransition[timeStep]=nominal=>
          modeVariable[timeStep+1]=m
          
See also Indexed Transition.
Unit Clause
A Clause with exactly one Literal that is not Assigned and all other Literals having the Truth Value FALSE. The set of Unit Clauses is the Fringe.
Unit Propagation
The same as Boolean Constraint Propagation. The LTMS class performs Unit Propagation.
Variable
The set of Variables used to describe the system is partitioned into two subsets: These sets are further partitioned. Code: conflict_db/variable.*
Volatile
A Clause is Volatile if its constituent Propositions change frequently. As with register variables in C, the Truth Maintenance System may, if given a hint about a Clause's volatility, be able to represent it more efficiently.
Weight
A non-negative floating-point number indicating the degree of confidence in an Assignment.
Width
In l2bin files, the number of elements of each type (Clause, Enumeration, Proposition, Transition, Variable) requires one byte if < 2**8, two bytes if < 2**16, etc. A width is the number of bytes needed to represent the number of Model elements.
XML-Based Model Programming Language
An XML Model File Format. The JMPL Compiler translates from JMPL to XMPL. XMPL is verbose but can be parsed in a relatively standard and robust way. See also JMPL, L2 Format, l2bin and MPL.
XMPL
XML-Based Model Programming Language.
xmpl2l2
An executable utility that translates a Model file from the XMPL Model File Format to either the L2 or l2bin format.
Zenith
As far from a Horizon as can be -- that is, the most recent Time Step. A Transitioned Variable maintains pointers to the Mode Transition Variable at both the Horizon and the Zenith.
Zenith Transition
An Assumption Variable progressed backward in time from a Mode Transition Variable, representing the transition from the latest stored Transitioned Variable to the NOW Transistioned Variable.

Lee S. Brownston
Last modified: Tue Feb 12 14:22:46 PST 2002

Back to Main Page