We present a design framework for small-satellite systems that ensures that (1) each satellite has a consistent theory to infer new information from information it perceives and (2) the theory for the entire system is consistent so that a satellite can infer new information from information communicated to it. This research contributes to our Reliable and Formal Design (RFD) process, which strives for designs that are "correct by construction" by introducing formal methods early. Our framework uses Barwise's channel theory, founded on category theory, and allied work in situation semantics and situation theory. Each satellite has a "classi cation", which consists of tokens (e.g., observed situations) and types (e.g., situation features) and a binary relation classifying tokens with types. The core of a system of classi cations is a category-theoretic construct that amalgamates the several classi cations. We show how to derive the theory associated with a classi cation and the theory of the system core, and we show how to check whether a given requirement is derivable from or consistent with a theory.
This research represents our ongoing e ort to develop a model-based systems engineering methodology for small satellite systems that is reliable, formal and results in a "correct-by-construction" design. We present a knowledge-based design framework for ensuring that (1) each satellite has a consistent theory it can use to infer new information from information it perceives and (2) the theory for the entire system is consistent so that a satellite can infer new information from information communicated to it, and it can assess purported information from fellow satellites. The theories mentioned can be updated as insight is gained about the sensing satellites and the part of the world observed.
This research contributes to our development of a Reliable and Formal Design
(RFD) process [
Consider a particular small satellite S. A type (for S) is a feature of interest that S may observe in a monitored situation. We assume that we can identify a set of types that characterize S's sensory capabilities and, further, that we can form a table indicating the combinations of types that may occur together in an observed situation. In Section IV.A, we present an algorithm to derive a theory (for S) from this classi cation table. The algorithm can detect inconsistency. We may have to update S's classi cation table: we may nd a new combination of types that may occur together (and so add a row to the table), or we may nd that a previously postulated combination is in fact spurious (and so delete a row from the table). We may even nd it necessary to introduce a new type for S. Whenever S's classi cation table is updated, we can run our algorithm and update S's theory (and check for consistency). S's theory allows it to infer additional information about a situation from information about that situation that it has perceived or received via communication with other satellites. S's theory also allows it to detect when purported information about a given situation from another satellite is incoherent from its (that is, S's) point of view or is inconsistent with the information S has about the situation in question.
We are concerned with a system of small satellites, so we consider the amalgamation of the classi cation tables of the several satellites in a given system as well as the theory inherent in this amalgamation. The amalgamation combines the content of the classi cation tables for the individual satellites and adds relations among types from several satellites. We describe this amalgamation in Section IV.C in terms of category theory. We can think of the system (with its classi cation table and theory) as the "whole" and the individual satellites as "parts". Again, in deriving the theory, we can determine whether it is consistent, and we can update the theory of the whole when the classi cation table for a part or a cross-part type dependency changes.
We describe, in an abstract manner, the algorithms and procedures that are used at a system-wide level in order to manipulate information and general knowledge for the satellite system. We do not suggest that the nal implementation of the system of satellites will use these procedures. Rather, they are to be taken in the spirit of executable speci cations. Later stages of the design process will re ne the speci cations into concrete designs that can be directly implemented.
The higher-level view taken here is based in the rst instance on category
theory, which captures abstract algebraic structures and their interactions in a
coherent way (as categories) and also captures the relations between the
categories. We make use of Barwise and Seligman's channel theory [
Barwise and Seligman developed channel theory to explain the notion of a
constraint, which was central in Barwise's account of "X being carries the
information that Y is " in situation semantics. Barwise and Perry [
A situation is an ongoing happening in the world, while an infon is the basic item of information. An infon involves an n-place relation R, n objects appropriate for the corresponding argument places of R, a spatiotemporal location, and a polarity of 1 (indicating that the objects are thus related at the indicated place and time) or 0 (indicating otherwise). Alternatively, one may think of a situation as a partial function from tuples, with all the above components except polarity, to the codomain f0; 1g. A situation, unlike a possible world in the semantics of modal logics, targets only part of the world. A real situation is a part of reality (and considered a single entity) that supports an inde nite number of infons, while an abstract situation is a xed set of infons.
Information ow is made possible by uniformities across relations between situations, that is, (as in channel theory) constraints (including natural laws and linguistic rules) that link various types of situations. Situation semantics addresses speech acts (utterances) and the "situatedness" of language use. It presents a theory of meaning that is relational in that language use relates situations: a linguistic unit (such as a declarative sentence) is uttered in an "utterance situation" whose descriptive content is some "described situation".
We retain the terminology of situation semantics for communication among small satellites since viewing satellite communication at a high level, in terms of utterance situations, allows us to abstract away unnecessary detail that adds nothing to the analysis. It also allows us to exploit notions relating to conversation that are not applicable at a lower level. A satellite broadcasting information delineates a spatiotemporal region in which there occurs an utterance situation (which also includes the satellites that are its physical neighbors given that an appropriate channel exists). We are interested in the information, its ow, conventions for taking turns, assumptions about content, and many other things at the level of speech and conversation. We are not interested in the physical aspects of communication and so eschew terms such as "broadcast".
The information of interest here concerns only the observed situations. The types relate only to observed situations, never to the satellites themselves. We do not address the issue of control actions taking by the satellites nor are we concerned with how information is extracted from signal. Real situations, with real objects and happenings, are observed although di erent satellites observe the same real situation from di erent perspectives and with di erent modalities. We generally prefer "observe" for the verb relating to the source of information unless the emphasis is on the medium, in which case we tend to use "perceive".
We view the critical aspects of a small satellite as an intelligent knowledge based system (IKBS). An IKBS as proposed here has a syntactic aspect and a semantic aspect. The semantic aspect relates to the speci c kind of information that the satellite can process and is represented by a nite number of "classi cations." For generality, we allow for several classi cations associated with the same satellite since it is common for a single satellite to have several sensing modalities or to use several fusion techniques. Each classi cation A (in the sense of channel theory) consists of a set typ(A) of types and a set tok(A) of tokens; a token a 2 tok(A) may be classi ed of type 2 typ(A) in classi cation A, written a A and called a simple proposition. So a classi cation A is a triple, (tok(A); typ(A); A). For a small satellite system, tokens are real situations (as observed by the satellites). All the classi cations with which a given satellite is endowed are amalgamated into a core classi cation (as explained in Section IV) for that satellite, which we shall refer to as the classi cation of the IKBS.
The syntactic aspect of the IKBS of a satellite is a set of implication rules, which are the constraints mentioned above. Each rule is a sequent, of the form ` , where and are sets of types. Suppose the classi cation in question here is A. This sequent is satis ed by a token (real situation) a as long as, if a A for all 2 , then a A for some 2 . A sequent is a constraint (for A) if it is satis ed by all tokens in tok(A). The deductive closure of the set of constraints is the IKBS's (or satellite's) theory (discussed above). The deductive closure of the set of rules is the IKBS's (or satellite's) theory (discussed above). Such a rule, if appropriately enabled, allows the satellite to infer new infons from its IKBS given other infons in the observed situation or the described situation associated with an utterance situation (where the utterance is by a neighboring satellite).
The next section describes our Reliable and Formal Design (RFD) process and how the techniques reported in this paper t into this framework. Section III presents enough category theory and channel theory so that the reader may understand the rest of this paper. Section IV is the technical heart of this paper and presents techniques for amalgamating classi cations, deriving a theory from a classi cation, and checking whether a requirement (encoded as a sequent) is derivable from a theory or may be consistently added to it. Section V considers how the satellites in a system maintain and communicate information on real situations. We assume that an IKBS may use its theory or the theory for the entire system to infer new information. Special attention is given to communication since an IKBS may fail to interpret an utterance or the content of what is uttered may be inconsistent with the information the IKBS has. Section VI concludes.
The RFD (Reliable and Formal Design) process [
This RFD systems engineering process takes into account the fact that the design team is small and multi-disciplinary as well as the fact that system is complex and heterogeneous and is a ected by its operational environment. Additionally, design of a complex system involves multiple disciplines that must interact symbiotically. This also implies that at the rst step in the process each of the disciplines must have a global view of the system. As they proceed towards re nement, the design process becomes a local or discipline-speci c activity, though always with a global perspective. The integration of formal methods into the design process of a complex system can reduce the need for a signi cant amount of revision during the system integration phase because of the "correct by construction" nature of the process. This leads to testing virtually at each level of re nement. Therefor, the theme of this design process from a systems engineering point of view is: Think globally, design locally, and test virtually.
At each level of abstraction, Ai, the state of the RFD process can be represented by requirements, models, and simulations: Ai = (Lin; Lli; Mi; Spi ; Sbi),where the information ow between these components is indicated with arrows as follows:
i i Ln () Ll ()
Mi =) Sp i (1) + i
Sb Here { Lin is the set of requirements written in natural language form { Lli is the set of requirements written as a set of logical functions { Mi is the system of interconnected models i { Spi is the set of simulations based on the parameters of M . { Sbi is the set of simulations based on the logical description in Ll. i
The central result of this paper is the technique presented in Section IV.A for developing a theory for a satellite/IKBS from the classi cation table for it. As this addresses individual satellites, it is in the realm of local design, albeit at a very abstract level. The classi cation system used by an IKBS may be an amalgamation of several classi cations. We form the classi cation for the entire satellite system by a similar amalgamation (see Section IV.C) given the classi cations of the component IKBS; the theory for the system is derived from this classi cation table. This is a return to a global perspective since the individual satellites with their sensing and communication capabilities were originally selected or built as required by the global mission. Theories for individual satellites and for the entire system are tested for consistency, which is virtual testing from the point of view of the system being developed.
The aspect in this knowledge-level design process emphasized in this paper is endowing each IKBS present within the distributed system with a theory in the form of a set of constraints. One determines for each IKBS the core classication with which it should be endowed and the classi cations into which this core should be decomposed as "parts". Henceforth, we call the core classi cation for the IKBS simply the "IKBS classi cation". One then determines the types for each of the "part" classi cations and the IKBS classi cation. These are the features of the IKBS's environment that it can sense or be informed about. One then produces a classi cation table for each "part" and for the core. The columns in the classi cation table are labeled with the classi cation's types, and we have a row for each abstract situation that (to our knowledge) may arise for that classi cation. A row has an '1' under a type if the abstract situation represented by that row supports that type; otherwise, it has a '0' under the type. Once the classi cation table for the IKBS classi cation is xed, one can determine the IKBS's initial theory (a set of constraints) as described in Section IV.A. Determining the classi cations for an IKBS can be done in a top-down fashion by rst determining its core (or IKBS) classi cation and then determining the relative parts in a way that is sensitive to its physical attributes. Alternatively, this can be done in a bottom-up fashion, by mixing and matching basic classi cations in an engineering repertoire and forming the IKBS classi cation once the parts are given.
Given a system of small satellites, we consider the amalgamation (the core) of the IKBS classi cations. As with forming an IKBS classi cation, forming the core for the entire system is (in category-theory terms) a sum operation. Section IV.C shows how the classi cation table for the system core is constructed from the classi cation tables for the individual IKBSs. Again, we can form the initial theory of the system using the techniques described in Section IV.A. Combining theories raises the threat of inconsistency, and we check for inconsistency syntactically by determining whether, from the combined theory, we can derive some formula and its negation or, equivalently, we can derive the empty sequent h;; ;i. Consistency can also be de ned semantically: see Section IV.B.
Designing a small satellite system is not just a matter of selecting the right kinds of satellites, developing their theories, and combining their reports at the knowledge level. One must also determine the overall situation, extended in both space and time, that the system will perceive. And one must formulate policies for how this overall situation will be divided into overlapping component situations allocated as regions of responsibility to the di erent satellites; these are policies for allocating sequences of overlapping situations to the various satellites. How regions of responsibility should overlap depends both on what is monitored and the capabilities and theories with which the satellites are endowed. Signi cant overlap is expected when two satellites have complementary sensing modes or perspectives on a target.
How a satellite is actually deployed may give rise to additional constraints to be incorporated into its theory. And how several satellites are designed to collaborate may a ect how the system core is formed and thus the theory for the system whole.
Once the satellite system is deployed, constraints will be added to the IKBSs, and their theories as well as the theory of the system as a whole will evolve. That is, new abstract situations will become apparent and could be added to the appropriate classi cation tables. One can check that the resulting theory remains consistent. One of the strengths of our approach is that, at any point in the lifetime of the systems, new requirements can be checked for consistency against current theories and, when consistent, used to augment those theories. At any time, the various theories must meet their requirements that have been collected over time. One way a theory can violate a requirement is by failing to include it. The solution in that case is to add the requirement to the theory and test for consistency. Another way a theory can violate a requirement is to be inconsistent with it, in which case the theory must be adjusted. 3
This section provides background for formal addressing the aggregation and ow of information in a small satellite system. The topics discussed here include category theory, channel theory, and the application of these theories to computational systems. 3.1
Category Theory
A category C consists of a class of objects and a class of morphisms (or arrows or maps) between the objects. Each morphism f has a unique source object a and target object b; we writef : a ! b. The composition of f : a ! b and g : b ! c is written as g f and is required to be associative: if in addition h : c ! d, then h (g f ) = (h g) f . It is also required that, for every object x, there exists a morphism 1x : x ! x (the identity morphism for x) such that, for every morphism f : a ! b, we have 1b f = f = f 1a. It follows from these properties that there is exactly one identity morphism for every object.
A functor from one category to another is a structure-preserving mapping, preserving the identity and composition of morphisms. More exactly, if C and D are categories, then a functor F from C to D is a mapping that associates with each object x 2 C an object F (x) 2 D and, with each morphism f : x ! y 2 C, a morphism F (f ) : F (x) ! F (y) 2 D. In addition, it requires that F (idx) = idF x for every object x 2 C, and F (g f ) = F (g) F (f ) for all morphisms f : x ! y and g : y ! z. In category theory, a commutative diagram is a diagram of objects (as vertices) and morphisms (arrows between objects) such that all directed paths in the diagram with the same start and end points lead to the same result by composition.
The classic presentation of category theory is in [
Channel Theory and the Flow of Information
Barwise and Seligman [
Components of the system may be distant from one another in time and space, and the system can be made up of heterogeneous components. The system is "distributed" in this sense and not necessarily in the classical sense used in computer science. For example, the students, classrooms, scheduling system, and attendance records together form a distributed system related to students' attendance at a certain university.
An information channel is a family of infomorphisms with a common codomain, called the core. Essentially, a channel consists of a set A1; :::; An of classi cations that represent the parts of the distributed system, a classi cation C (the core) that represents the system as a whole, and a set of infomorphisms f1; :::; fn from each of the parts onto C. Tokens in C are the connections of the system: a given token c in C connects the tokens it is related to by means of f1; :::; fn. Parts A1; :::; An carry information about each other as long as they all are parts of C. Intuitively, an information channel is a part to whole Ai-to-C informational relationship. Categorically, the core is a cocone in the category of classi cations (objects are classi cations and morphisms are informorphisms).
A distributed system D is a collection of elements that carry information about each other. Formally, D consists of an indexed class cla(D) of classi cations together with a class of infomorphisms, inf (D), whose domains and codomains are all in cla(D). An information channel C covers distributed system D if and only if cla(D) are the classi cations of the channel and, for every infomorphism f 2 inf (D), there are infomorphisms from both the domain and codomain of f to the core of C such that these three infomorphisms are commutative in there interrelation. Basically, all classi cations in D are \informational parts" of the core whose channel covers D.
Turning to regularities in a classi cation's types, let A be a classi cation and
and be subsets of types in A. Recall (from Section I) that a token a of A
satis es the sequent ` provided that, if a is a token of every type in , then
it is of some type in . If every token of A satis es ` , then is said to entail
and ` is called a constraint supported by A. The set of all constraints
supported by A is called the complete theory of A, denoted by T h(A). These
constraints are systematic regularities, and it is by virtue of regularities among
connections that information about certain component of a distributed system
can be carried by other components into diverse parts of the system. Barwise and
Seligman's summary statement of their analysis of information ow, restricted
to the simple case of a system with two components, is as follows. \Suppose that
the token a is of type . Then a's being of type carries the information that
b is of type , relative to channel C, if a and b are connected in C and if the
translation 0 of entails the translation 0 of in the theory T h(C), where C
is the core of C" ( [
Category Theory and Channel Theory for Computational Systems
Channel theory and category theory in general have had a signi cant
impact in computer science, especially those aspects related to complex systems.
Schorlemmer and Kalfoglou and their colleagues have applied channel theory in
addressing semantic interoperability of federated databases [
Goguen and Burstall's theory of institutions [
The Duquenne{Guigues [
Algorithm 1 computes a basis of the theory of a given classi cation. The theory is the deductive closure of its basis. We use the Duquenne{Guigues theorem to compute part of the set of the constraints, namely, those that are implications. Note that in Algorithm 1 a sequent Gama ` where = ; is handled separately.
Algorithm 1 Constraint extraction procedure 1: Input: Classi cation A 2: T h(A) = ? 3: For typ(A) 4: Compute [ 5: If [ = tok(A) then ` ? 2 T h(A) 6: If ` is in a Duquenne{Guigues basis of A then 7: End for 8: Output T h(A) ` 2 T h(A)
The proof is not always as short and easy as this. Generally, one would use an automatic or semi-automatic theorem prover such as PVS [24]. The derivability can also be shown semantically. Semantically, a sequent is valid in a classi cation A if each token of A satis es the sequent. For a sequent ` , this is equivalent to the inclusion \ [. For example, for the sequent f ; g ` f ; g, we have f ; g\ = fa1g fa1; a2; a3g = f ; g[. In classical deductive logic, a consistent theory is one that does not contain a contradiction. The lack of contradiction can be de ned in either semantic or syntactic terms. Here a model is taken to be a classi cation. The semantic de nition states that a theory is consistent if and only if it has a model, i.e., there exists an interpretation under which all formulas in the theory are true. This is the same sense used in traditional Aristotelian logic, although, in contemporary mathematical logic, the term \satis able" is used instead of \true". The syntactic de nition states that a theory is consistent if and only if there is no formula p such that both p and its negation are provable from the axioms of the theory under the associated deductive system.
We introduced the notion of the core of an information channel in Section II.B, and we have viewed it as the whole that provides the amalgamation of the classi cations of the parts. The core is formed as the category-theoretic sum of the classi cations of the parts. Here we illustrate the sum of three classi cations A1, A2, and A3, which is the core of the information channel containing the classi cations. The sum A1 + A2 + A3 is the classi cation de ned as follows: 1. The set tok(A1 + A2 + A3) of tokens is the Cartesian product of tok(A1), tok(A2) and tok(A3). Thus, the tokens of A1 + A2 + A3 are triples (a1; a2; a3) of tokens, a1 2 tok(A1), a2 2 tok(A2) and a3 2 tok(A3). 2. The set typ(A1 + A2 + A3) of types is the disjoint union of typ(A1), typ(A2) and typ(A3). For concreteness, the types of A1 + A2 + A3 are pairs hi; i, where i = 1 and 2 typ(A1) or i = 2 and 2 typ(A2) or i = 3 and 2 typ(A3). 3. The classi cation relation A1+A2+A3 of A1 + A2 + A3 is de ned by (a1; a2; a3) A1+A2+A3 hi; i if and only if ai Ai ; 8i 2 f1; 2; 3g.
To make this example concrete, suppose that classi cations A1, A2 and A3 are given by the classi cation tables in following Table . Note that each abstract situation (row) is labeled. Then the rst six rows classi cation table for A1 +
A1 A2 + A3 are shown below. a1 1 0 1 0 a2 0 1 1 0 a3 0 1 0 0
A2 a4 1 0 0 a5 1 1 1 a6 0 1 0
A3 a7 0 1 0 1 a8 0 1 1 0
As an example, consider a system of three small satellites, S1, S2, and S3, whose goal is to image the auroral ovals that exist around both magnetic poles of Earth and thereby study the impact of the solar wind on the magnetosphere. S1 measures the intensity of the auroral brightness; if this is over a given threshold, then S1 measures the magnetic disturbance density and sends a message to S2 and S3 to begin imaging. S2 and S3 do the same thing from di erent perspectives, viz., take an image of the auroral oval to determine its extent.
For types for S1, we distinguish auroral brightness below the threshold (LAB, "Low Auroral Brightness") and at or above the threshold (HAB, "High Auroral Brightness"). We arbitrarily partition the magnetic density measurement, a continuous magnitude, into a small number (viz., three) of ranges for simplicity, giving types LM D ("Low Magnetic Density"), M M D ("Medium"), and HM D ("high"). For S2, we arbitrarily partition the auroral extent, a continuous magnitude, into three ranges: LAE2 ("Low Auroral Extent"), M AE2 ("Medium"), and HAE2 ("High"). We recognize the same types for S3 but use subscript "3" in place of "2": LAE3, M AE3, and HAE3.
The classi cation table for S1 is shown below. Some of the constraints derived from this table are the following, where (1) indicates that, if the auroral brightness is high, then there is a magnetic density measurement of high, medium, or low, and (2) indicates that the auroral brightness is (unconditionally) high or low. 1. HAB ` LM D; M M D; HM D 2. ; ` fHAB; LABg The classi cation table for S2 is shown below. The obvious constraints here are that there must be a measured auroral extent, low, medium, or high (; ` fLAE2; M AE2; HAE2g), and it cannot be, for example, low and medium at the same time (fLAE2; M AE2g ` ;). The classi cation table for S3 is identical to that for S2 but for the subscripts.
SAT 1 HAB LAB LM D M M D HM D 1a 0 1 0 0 0 1b 1 0 1 0 0 1c 1 0 0 1 0 1d 1 0 0 0 1 SAT 2 LAE2 M AE2 HAE2 2a 1 0 0 2b 0 1 0 2c 0 0 1
The classi cation table for the core will be analogous to the core classi cation produced in the previous example but will induce some constraints that cross system parts. At this point, it is convenient to enlarge our system to include a classi cation for the "part" that is observed by the satellites, namely, the magnetosphere and solar wind as well as the auroral oval produced by their interaction. The real situations classi ed with the types we have picked out so far certainly include these aspects of the environment and various types that characterize them. We consider here only four types that relate to this environmental part. Let AL indicate that the magnetosphere and solar wind are aligned (within some level of tolerance), and let N AL indicate that they are not aligned. Let CON D indicate that this part is in a state where ionospheric conductivity could be exceptional, and let N CON D indicate the denial of this. If we were to construct a classi cation table relating these types to types for the other three "parts" of the system (i.e., the satellite classi cations), we could use our techniques to derive the following (and many more) constraints. 1. CON D ` AL 2. fM M D; HAE2; HAE3g ` AL 3. fHM D; HAE2; M AE3g ` CON D Constraint (1) indicates that, if the situation is such that ionospheric conductivity could be exceptional, then the magnetosphere and solar wind are aligned. Constraint (2) indicates that, if the magnetic density is medium and the auroral extent is high from the perspective of both S2 and S3, then the magnetosphere and solar wind are aligned. And (3) indicates that, if the magnetic density is high and the auroral extent is high from the perspective of S2 but medium from the perspective of S3, then ionospheric conductivity could be exceptional. 5
Consider now the situation table with the information an IKBS has on various real situations. We contrast the situation table with the classi cation table of a satellite, which is where design starts. The classi cation table has a column for each type relevant to the satellites sensing capability and the behavior of the monitored region. The rows indicate the combinations of types (columns) that may occur together in an observed situation. That is, the rows specify all the realizable abstract situations by indicating the types realized in them.
In contrast, the situation table has a row for each real situation observed. Like a classi cation table, a situation table has a column for each observable type, but the situation table needs information on more types. An IKBS has information on a situation not only by observation but also by virtue of utterance situations and by inferring information from information it already has. The descriptive content of an utterance may involve types observable by any satellite in the system, so the situation table must have columns for all these types. The IKBS has its own theory for inferring new information, but, since the IKBS is part of a distributed system, the theory of the whole, or core, is relevant as well for lling out entries in the situation table. Since the "whole" or core does not correspond to a physical entity over and above the "parts" (satellites), inferencing done with the theory of the core must be delegated to these parts. The easiest approach is to assume that all IKBSs have, besides their own theories, the theory of the core.
The general picture, then, has an IKBS, on observing a real situation, make an entry for it in its situation table, indicating what types were observed. When the descriptive content of an utterance relates to this situation, its table entry may be lled by checking further types. It is also possible that observation may ll in an entry over an extended period. As information on the situation becomes available, various sequents of the local or core theory may allow further information to be inferred and recorded in the entry for the situation. A variation of this picture has the IKBS rst nding out about the real situation in question via another's utterance. Note that issues we avoid in this paper include how real situations are denoted, how they are related as parts and wholes, and to what extent something true in a part is also true of the whole. These issues are addressed in the standard literature cited, and the part-whole relation has been extensively studied in terms of lattice structures [25].
The conditions for lling in an entry of the situation table because of a relevant utterance needs to be addressed in more detail since the IKBS may fail to interpret an utterance or the content of what is uttered may be inconsistent with the information the IKBS has. The descriptive content of what may be considered a normal utterance is what we call an utterance proposition, of the form a : , where a is a token and is a set of types and type placeholders. For each type, we assume there is a corresponding placeholder ? . If 2 , then part of what the utterance asserts is a A , while if neither 2 nor ? 2 , part of what it asserts is a a 2A ; we cannot have both 2 and ? 2 . If ? 2 , then the utterance says nothing about a being of type . If the content of an utterance is consistent with an IKBS's theory (as discussed in Section IV.B), then it is included in the IKBS's situation table unless it is inconsistent with an entry already in that table. The situation table also includes results of observations, and it contains at most one entry for a given real situation (i.e., token). (As an IKBS's classi cation table constitutes in large part its semantic memory, its situation table constitutes its episodic memory.) We say that an utterance proposition a : is in the situation table if the situation table has an entry for situation a and that entry records types and type placeholders as per . If the situation table includes the utterance proposition a : 1 and the IKBS perceives an utterance whose descriptive content is a : 2 with the same token a, then the utterance proposition for a in the situation table can be updated with the information a : 2 as long as, for all types of the IKBS classi cation, is not in one of 1 or 2 but not the other. Violation of this condition indicates that the two utterance propositions are inconsistent. It may be the case, though, that is in one but ? is in the other, or is not in one but ? is in the other. Then the situation table entry for a, a : 1, is updated by replacing any ? 2 1 with if 2 2 and by removing any ? 2 1 if 2= 2. If an IKBS succeeds in incorporating an utterance proposition into its situation table, we say that it has interpreted that utterance proposition.
In addition to the utterances just addressed, whose descriptive contents are utterance propositions, we allow utterances whose contents are partial utterance propositions; we call such utterances p-utterances and their descriptive content p-propositions. A p-proposition is again of the form a : , but now, for any type , if 2= , then a 2A is not being asserted; rather, the p-proposition has nothing to say about a being of type . A p-utterance presents an occasion for an IKBS to infer (using its theory) additional types for tokens, as illustrated by the paradigmatic case of inferring re from smoke. A p-utterance could be used as a query, when one IKBS utters a p-utterance, and another utters a (normal) utterance in reply, providing missing types if they in fact are uniquely determined by the theory. A p-proposition a : 1 is inconsistent with an utterance proposition a : 2 in the situation table if there is at least one type such that 2 1 but 2= 2. If the p-proposition is not inconsistent with any utterance proposition in the IKBS's situation table, then we say that the IKBS interprets that p-proposition; this is the case whether or not it is able to uniquely determine additional types for the token.
There are several ways an IKBS may fail to interpret the descriptive content of an utterance proposition or a p-proposition and hence fail to interpret the utterance or p-utterance itself. We say that an IKBS is acquainted with a token a if there is an utterance proposition a : in its situation table, and we say that it is acquainted with a type if is among the types labeling the columns of its situation table. If an IKBS is unacquainted with a type, it is normally because that type is new and not yet incorporated into the IKBS's computational structures. An IKBS cannot interpret an utterance proposition or p-proposition a : if there is a type 2 with which it is not acquainted, and it cannot interpret a p-proposition a : if it is not acquainted with token a. Failure of interpretation due to lack of acquaintance amounts to a failure to understand. The other way interpretation can fail arises from inconsistency with content of the situation table, as described above. 6
As part of our engineering methodology for small satellite systems that is reliable, formal and results in a "correct-by-construction" design, we presented in this paper a knowledge-based design framework for ensuring that (1) each satellite has a consistent theory it can use to infer new information from information it perceives and (2) the theory for the entire system is consistent so that a satellite can infer new information from information communicated to it, and it can assess purported information from fellow satellites. The point of departure for our framework, from the previous RFD process, is Barwise's channel theory, founded on category theory, and allied work on situation semantics and situation theory. Each small satellite is viewed as an intelligent knowledge base system (IKBS) consisting of classi cations in the sense of channel theory. A classi cation consists of tokens (e.g., observed situations) and types (e.g., features of a situation, such as a certain kind of event) as well as a binary relation that classi es tokens with types. Each IKBS has a semantic part, namely, the classi cations with which it is endowed, and a syntactic part, which is a logic or theory of classi cation that allows each satellite to infer new information from observed and communicated situations. Communication (as per situation semantics) is viewed in terms of utterances; the descriptive content of an utterance is an assertion that a given token is of a given set of types. The core of a system of classi cations, as explained in this paper, is a category-theoretic construct that amalgamates the several classi cations; the core and the individual classi cations essentially form the "whole" and the "parts" of what is termed a channel. We show how to derive the theory for an IKBS and for the system core, and we show how to check whether a given requirement is derivable from or consistent with a theory. 23. Beeri, C., Dowd, M., Fagin, R., Statman, R.: On the structure of armstrong relations for functional dependencies. Journal of the ACM (1984) 24. Sam Owre, J.M.R., Shankar, N.: pvs: A prototype veri cation system. In: 11th
International Conference on Automated Deduction (CADE). (1992) 25. Link, G.: Algebraic Semantics in Language and Philosophy. CSLI Lecture Notes No. 74 (1998)