Ambient calculus-based modal logics for mobile ambients

Abstract

Ambient calculus-based modal logics for mobile ambients are disclosed. Formal analysis mechanisms or frameworks with which mobile ambients can be described, and within which policies such as security policies can be tested against those ambients, are disclosed. In one embodiment, a computer-implemented method receives at least one container, where each container has at least one process. The method applies the containers, including their processes, against a predetermined modal logic. The modal logic is based on ambient calculus, and provides for spatial relationships among the processes of the containers. The containers and their processes are output, as applied against the logic.

Claims

We claim:

1. A computer-implemented method, comprising:

receiving at least one container, each container having at least one process;

applying the at least one container, including the at least one process of each container, against a predetermined modal logic based on ambient calculus and providing for spatial relationships among the at least one process of each container, and outputting a result that indicates whether the at least one container, including the at least one process of each container, satisfies the predetermined modal logic, wherein the result is utilized to allow the at least one container to move or replicate when the at least one container satisfies the predetermined modal logic.

2. The method of claim 1, wherein each container comprises one of a hardware container and a software container.

3. The method of claim 1, wherein the predetermined modal logic comprises a predetermined processes syntax.

4. The method of claim 1, wherein the predetermined modal logic comprises a predetermined structural congruence relation between processes.

5. The method of claim 1, wherein the predetermined modal logic comprises a predetermined reduction semantics.

6. The method of claim 1, wherein the predetermined modal logic comprises at least one logic formula selected from the group essentially consisting of: true, negation, disjunction, inaction, location, composition, universal quantification over names, sometime modality, somewhere modality, location adjunct, and composition adjunct.

7. The method of claim 1, wherein the predetermined modal logic comprises at least one derived connective selected from the group essentially consisting of false, conjunction, implication, logical equivalence, decomposition, every component satisfaction, some component satisfaction, existential quantification over names, everytime modality, everywhere modality, in every location context, and in every composition context.

8. The method of claim 1, wherein the predetermined modal logic comprises at least one of: one or more valid formulas, one or more valid sequents, and one or more valid logical inference rules.

9. The method of claim 1, wherein the predetermined modal logic comprises a quantale.

10. The method of claim 1, wherein the predetermined modal logic has embedded therein intuitionistic linear logic.

11. A computer-implemented method, comprising:

receiving a configuration of a plurality of ambients, each ambient having at least one thread;

representing the plurality of ambients, including that at least one thread of each ambient, using a predetermined modal logic based on ambient calculus and providing for spatial relationships among the at least one thread of each ambient, and outputting a result that indicates whether the plurality of ambients, including the at least one thread of each ambient, as represented using the predetermined modal logic, satisfies a policy represented in ambient calculus, wherein the result is utilized to allow the plurality of ambients to move or replicate when the plurality of ambients satisfies the policy.

12. The method of claim 11, wherein the predetermined modal logic policy comprises a security policy.

13. A computer-implemented method, comprising:

receiving a first representation of a plurality of ambients defining one of a formula and a policy, each ambient having at least one thread, receiving a second representation of at least one ambient, each ambient having at least one thread;

applying the second representation against the first representation within a predetermined modal logic based on ambient calculus and providing for spatial relationships among the at least one thread of each ambient of the first and the second representation, to determine if the second representation satisfies the first representation; and

outputting information that indicates whether the second representation satisfies the first representation for further analysis by a program that draws a conclusion based on the output information, wherein the conclusion is utilized to allow the second representation to move or replicate when the second representation satisfies the first representation.

14. The method of claim 13, wherein the policy comprises a security policy.

15. A machine-readable medium having instructions stored thereon for execution by a processor to perform a method, comprising:

receiving at least one container, each container having at least one process;

applying the at least one container, including the at least one process of each container, against a predetermined modal logic based on ambient calculus and providing for spatial relationships among the at least one process of each container; and

outputting a result that indicates whether the at least one container, including the at least one process of each container, satisfies the predetermined modal logic, to at least one of a monitor, a printer, and a storage device, wherein the result is utilized to allow the at least one container to move or replicate when the at least one container satisfies the predetermined modal logic.

16. The medium of claim 15, wherein the predetermined modal logic comprises a predetermined processes syntax.

17. The medium of claim 15, wherein the predetermined modal logic comprises a predetermined structural congruence relation between processes.

18. The medium of claim 15, wherein the predetermined modal logic comprises a predetermined reduction semantics.

19. The medium of claim 15, wherein the predetermined modal logic comprises at least on logic formula selected from the group essentially consisting of: true, negation, disjunction, inaction, location, composition, universal quantification over names, sometime modality, somewhere modality, location adjunct, and composition adjunct.

20. The medium of claim 15, wherein the predetermined modal logic comprises at least on derived connective selected from the group essentially consisting of: false, conjunction, implication, logical equivalence, decomposition, every component satisfaction, some component satisfaction, existential quantification over names, everytime modality, everywhere modality, in every location context, and in every composition context.

21. The medium of claim 15, wherein the predetermined modal logic comprises at least one of: one or more valid formulas, one or more valid sequents, and one or more valid logical inference rules.

22. The medium of claim 15, wherein the predetermined modal logic comprises a quantale.

23. The medium of claim 15, wherein the predetermined modal logic has embedded therein intuitionistic linear logic.

24. A computerized system, comprising:

a component that receives at least one container, each container having at least one process;

a component that receives a policy represented as a predetermined modal logic based on ambient calculus and providing spatial relationships among the at least one process of each container; and

a processor that compares an ambient calculus based representation of the at least one container with the predetermined modal logic based on ambient calculus to determine whether the at least one container satisfies the policy, wherein the container is allowed to move or replicate when the at least one container satisfies the policy.

Description

FIELD OF THE INVENTION

This invention relates generally to mobile ambients and processes, and more specifically to ambient calculus-based modal logics for such ambients and processes.

BACKGROUND OF THE INVENTION

Computing has become increasingly interconnected. Whereas before computers were discrete, unconnected units, because of the Internet as well as other networks, they are increasingly fluid, interconnected units. A computer program, which may be made up of one or more executable processes, or threads, may be mobile. For example, a thread of the program may move from computer to computer over the Internet. It may be executed in a distributed fashion over many computers, or a different instance of the thread may be run on each of many computers.

The movement of threads from computer to computer, or even to different parts within the same computer, poses new security and other risks for which there is no formal analysis mechanism. For example, a thread may be unstable, such that having it be run on a particular computer may cause the computer to crash. More so, the thread may be malicious, such as part of a virus program, such that its purpose is to compromise the computers it moves to.

More specifically, there are two distinct areas of work in mobility: mobile computing, concerning computation that is carried out in mobile devices (laptops, personal digital assistants, etc.), and mobile computation, concerning mobile code that moves between devices (agents, etc.). Mobility requires more than the traditional notion of authorization to run or to access information in certain domains: it involves the authorization to enter or exit certain domains. In particular, as far as mobile computation is concerned, it is not realistic to imagine that an agent can migrate from any point A to any point B on the Internet. Rather an agent must first exit its administrative domain (obtaining permission to do so), enter someone else's administrative domain (again, obtaining permission to do so) and then enter a protected area of some machine where it is allowed to run (after obtaining permission to do so).

Access to information is controlled at many levels, thus multiple levels of authorization may be involved. Among these levels we have: local computer, local area network, regional area network, wide-area intranet and internet. Mobile programs should be equipped to navigate this hierarchy of administrative domain, at every step obtaining authorization to move further. Laptops should be authorized to access resources depending on their location in the administrative hierarchy.

In general, a process or thread resides within a container referred to as an ambient. The ambient includes one or more processes or threads, as well as any data, etc., that move with the processes or threads. An ambient that can move is referred to as a mobile ambient. The ambient can be any type of container: a software container such as a particular part of an operating system, for example, as well as a hardware container, such as a particular computer or peripheral device.

More specifically, an ambient has the following main characteristics. First, an ambient is a bounded placed where computation happens. The interesting property here is the existence of a boundary around an ambient. Examples of ambients include: a web page (bounded by a file), a virtual address space (bounded by an addressing range), a Unix file system (bounded within a physical volume), a single data object (bounded by `Itself`) and a laptop (bounded by its case and data ports). Non-examples are: threads (the boundary of what is "reachable" is difficult to determine) and logically related collections of objects.

Second, an ambient is something that can be nested within other ambients. For example, to move a running application from work to home, the application must be removed from an enclosing (work) ambient and inserted in a different enclosing (home) ambient. A laptop may need a removal pass to leave a workplace, and a government pass to leave or enter a country.

Third, an ambient is something that can be moved as a whole. If a laptop is connected to a different network, all the address spaces and file systems within it move accordingly and automatically. If an agent is moved from one computer to another, its local data should move accordingly and automatically. As mentioned, there is no formal analysis mechanism within the prior art for such mobile ambients. This means that there is no manner by which to describe formally, for example, a security policy for a given computer system, which could be applied against a mobile ambient within a formal analysis mechanism to determine if the ambient poses a security or other risk to the system. In particular, most formal analysis mechanisms, or frameworks, only provide for temporal distinction among processes and ambients, but assume that the processes and ambients are stationary--or otherwise do not provide for spatial distinction among them.

For these and other reasons, there is a need for the present invention.

SUMMARY OF THE INVENTION

The invention relates to ambient calculus-based modal logics for mobile ambients. That is, the invention provides for formal analysis mechanisms or frameworks with which mobile ambients can be described, and within which policies such as security policies can be tested against those ambients. In one embodiment, a computer-implemented method receives at least one container, where each container has at least one process. The containers can in one embodiment be referred to as ambients, and the processes as threads. The method applies the containers, including their resident processes, against a predetermined modal logic. The modal logic is based on ambient calculus, and provides for spatial relationships among the processes of the containers. The containers and their processes are then output, as they have been applied against the logic. As used herein, the phrase "applied against the logic" refers to testing for conformance against a policy or formula of the logic.

In differing embodiments of the invention, the modal logic has one or more of the following aspects, characteristics and qualities: a structural congruence relation between processes; reduction semantics; logical formulae such as true, negation, disjunction, inaction, location, composition, universal quantification over names, sometime modality, somewhere modality, location adjunct, and composition adjunct; derived connectives such as false, conjunction, implication, logical equivalence, decomposition, every component satisfaction, some component satisfaction, existential quantification over names, everytime modality, everywhere modality, and unsatisfiability; valid formulas, sequents and/or logical inference rules; quantales; and, intuitionistic linear logic.

Embodiments of the invention provide for advantages over the prior art. The modal logic can be used to formally describe a given mobile ambient, as well as a policy, such as a security policy, of a given computer. The mobile ambient can then be analyzed against the policy within the framework provided by the modal logic. Since the modal logic provides for spatial relationships among different processes of ambients, embodiments of the invention are particularly well suited for analysis of such mobile computing problems.

Embodiments of the invention include computer-implemented methods, computer-readable media, and computerized systems of varying scope. Still other embodiments, advantages and aspects of the invention will become apparent by reading the following detailed description, and by reference to the drawings.

BRIEF DESCRIPTION OF THE DRAWINGS

FIG. 1 is a diagram of an operating environment in conjunction with which embodiments of the invention may be practiced;

FIG. 2 is a diagram of an example environment of ambients and processes in conjunction with which embodiments of the invention may be practiced;

FIGS. 3-5 are flowcharts of methods according to different embodiments of the invention; and,

FIGS. 6-7 are diagrams of example situations of mobile ambients utilized in conjunction with the modal logic of varying embodiments of the invention.

DETAILED DESCRIPTION OF THE INVENTION

In the following detailed description of exemplary embodiments of the invention, reference is made to the accompanying drawings which form a part hereof, and in which is shown by way of illustration specific exemplary embodiments in which the invention may be practiced. These embodiments are described in sufficient detail to enable those skilled in the art to practice the invention, and it is to be understood that other embodiments may be utilized and that logical, mechanical, electrical and other changes may be made without departing from the spirit or scope of the present invention. The following detailed description is, therefore, not to be taken in a limiting sense, and the scope of the present invention is defined only by the appended claims.

Some portions of the detailed descriptions which follow are presented in terms of algorithms and symbolic representations of operations on data bits within a computer memory. These algorithmic descriptions and representations are the means used by those skilled in the data processing arts to most effectively convey the substance of their work to others skilled in the art. An algorithm is here, and generally, conceived to be a self-consistent sequence of steps leading to a desired result. The steps are those requiring physical manipulations of physical quantities. Usually, though not necessarily, these quantities take the form of electrical or magnetic signals capable of being stored, transferred, combined, compared, and otherwise manipulated. (It is noted that the terms document and text are used interchangeably herein and should be construed as interchangeable as well.)

It has proven convenient at times, principally for reasons of common usage, to refer to these signals as bits, values, elements, symbols, characters, terms, numbers, or the like. It should be borne in mind, however, that all of these and similar terms are to be associated with the appropriate physical quantities and are merely convenient labels applied to these quantities. Unless specifically stated otherwise as apparent from the following discussions, it is appreciated that throughout the present invention, discussions utilizing terms such as processing or computing or calculating or determining or displaying or the like, refer to the action and processes of a computer system, or similar electronic computing device, that manipulates and transforms data represented as physical (electronic) quantities within the computer system's registers and memories into other data similarly represented as physical quantities within the computer system memories or registers or other such information storage, transmission or display devices.

Operating Environment

Referring to FIG. 1, a diagram of the hardware and operating environment in conjunction with which embodiments of the invention may be practiced is shown. The description of FIG. 1 is intended to provide a brief, general description of suitable computer hardware and a suitable computing environment in conjunction with which the invention may be implemented. Although not required, the invention is described in the general context of computer-executable instructions, such as program modules, being executed by a computer, such as a personal computer. Generally, program modules include routines, programs, objects, components, data structures, etc., that perform particular tasks or implement particular abstract data types.

Moreover, those skilled in the art will appreciate that the invention may be practiced with other computer system configurations, including hand-held devices, multiprocessor systems, microprocessor-based or programmable consumer electronics, network PC's, minicomputers, mainframe computers, and the like. The invention may also be practiced in distributed computing environments where tasks are performed by remote processing devices that are linked through a communications network. In a distributed computing environment, program modules may be located in both local and remote memory storage devices.

The exemplary hardware and operating environment of FIG. 1 for implementing the invention includes a general purpose computing device in the form of a computer 20, including a processing unit 21, a system memory 22, and a system bus 23 that operatively couples various system components include the system memory to the processing unit 21. There may be only one or there may be more than one processing unit 21, such that the processor of computer 20 comprises a single central-processing unit (CPU), or a plurality of processing units, commonly referred to as a parallel processing environment. The computer 20 may be a conventional computer, a distributed computer, or any other type of computer; the invention is not so limited.

The system bus 23 may be any of several types of bus structures including a memory bus or memory controller, a peripheral bus, and a local bus using any of a variety of bus architectures. The system memory may also be referred to as simply the memory, and includes read only memory (ROM) 24 and random access memory (RAM) 25. A basic input/output system (BIOS) 26, containing the basic routines that help to transfer information between elements within the computer 20, such as during start-up, is stored in ROM 24. The computer 20 further includes a hard disk drive 27 for reading from and writing to a hard disk, not shown, a magnetic disk drive 28 for reading from or writing to a removable magnetic disk 29, and an optical disk drive 30 for reading from or writing to a removable optical disk 31 such as a CD ROM or other optical media.

The hard disk drive 27, magnetic disk drive 28, and optical disk drive 30 are connected to the system bus 23 by a hard disk drive interface 32, a magnetic disk drive interface 33, and an optical disk drive interface 34, respectively. The drives and their associated computer-readable media provide nonvolatile storage of computer-readable instructions, data structures, program modules and other data for the computer 20. It should be appreciated by those skilled in the art that any type of computer-readable media which can store data that is accessible by a computer, such as magnetic cassettes, flash memory cards, digital video disks, Bernoulli cartridges, random access memories (RAMs), read only memories (ROMs), and the like, may be used in the exemplary operating environment.

A number of program modules may be stored on the hard disk, magnetic disk 29, optical disk 31, ROM 24, or RAM 25, including an operating system 35, one or more application programs 36, other program modules 37, and program data 38. A user may enter commands and information into the personal computer 20 through input devices such as a keyboard 40 and pointing device 42. Other input devices (not shown) may include a microphone, joystick, game pad, satellite dish, scanner, or the like. These and other input devices are often connected to the processing unit 21 through a serial port interface 46 that is coupled to the system bus, but may be connected by other interfaces, such as a parallel port, game port, or a universal serial bus (USB). A monitor 47 or other type of display device is also connected to the system bus 23 via an interface, such as a video adapter 48. In addition to the monitor, computers typically include other peripheral output devices (not shown), such as speakers and printers.

The computer 20 may operate in a networked environment using logical connections to one or more remote computers, such as remote computer 49. These logical connections are achieved by a communication device coupled to or a part of the computer 20; the invention is not limited to a particular type of communications device. The remote computer 49 may be another computer, a server, a router, a network PC, a client, a peer device or other common network node, and typically includes many or all of the elements described above relative to the computer 20, although only a memory storage device 50 has been illustrated in FIG. 1. The logical connections depicted in FIG. 1 include a local-area network (LAN) 51 and a wide-area network (WAN) 52. Such networking environments are commonplace in office networks, enterprise-wide computer networks, intranets and the Internet, which are all types of networks.

When used in a LAN-networking environment, the computer 20 is connected to the local network 51 through a network interface or adapter 53, which is one type of communications device. When used in a WAN-networking environment, the computer 20 typically includes a modem 54, a type of communications device, or any other type of communications device for establishing communications over the wide area network 52, such as the Internet. The modem 54, which may be internal or external, is connected to the system bus 23 via the serial port interface 46. In a networked environment, program modules depicted relative to the personal computer 20, or portions thereof, may be stored in the remote memory storage device. It is appreciated that the network connections shown are exemplary and other means of and communications devices for establishing a communications link between the computers may be used.

Mobile Computing Environment

In this section of the detailed description, an example mobile computing environment in conjunction with which embodiments of the invention can be practiced. That is, an example mobile computing environment, made up of ambients (containers) and processes (threads), is presented. Modal logics according to the invention can then be used to represent these ambients and processes, as well as describe configurations of multiple such ambients and processes, and policies and formulas against which specific ambients and processes can be applied to determine if they satisfy the policies and formulas.

Referring to FIG. 2, an example mobile computing environment 200 is shown. The environment 200 specifically includes ambients, or containers, 202, 204 and 206. As shown in FIG. 2, the ambient 202 resides within the ambient 204. The ambient 202 is named a; the ambient 204 is named b; and, the ambient 206 is named c. A process P resides within the ambient 204, while a process Q resides within the ambient 202, and processes R and S reside within the ambient 206.

As has been described, each ambient, or container, can be a software or a hardware container. A software container may be a particular area defined by an operating system. Examples include stacks, heaps, sand boxes, as the latter term is referred to in the context of the Java programming language, etc. A hardware container may be a particular computer, such as a client or a server computer, as well as a particular computer peripheral. An example of a computer has been described in the preceding section of the detailed description.

More specifically, an ambient as used herein has the following properties:

Each ambient has a name. The name of an ambient is used to control access (entry, exit, communication, etc.). In a realistic situation the true name of an ambient would be guarded very closely, and only specific capabilities would be handed out about how to use the name. In our examples we are usually more liberal in the handling of names, for sake of simplicity.

Each ambient has a collection of local agents (referred interchangeably herein as threads or processes). These are the computations that run directly within the ambient and, in a sense, control the ambient. For example, they can instruct the ambient to move.

Each ambient may have a collection of subambients. Each subambient has its own name, agents, subambients, etc.

Names refer to:

something that can be created, passed around and used to name new ambients.

something from which capabilities can be extracted.

The logic of embodiments of the invention pertains to a mobile computing environment. Thus, the ambients of FIG. 2 are mobile. As shown in FIG. 2, for example, the ambient 202 is moving out of the ambient 204. There may be, for example, a particular policy or formula, expressed in the logic, that defines whether such a move can occur, such that it can be applied against the ambient 202 and the policy therein to determine whether such a move should be allowed to occur. Each of the ambients and their resident processes are also representable in the logic of embodiments of the invention, which is described in the next section of the detailed description.

Modal Logic

In this section of the detailed description, modal logics based on ambient calculus, and providing for spatial relationships among processes of containers, according to varying embodiments of the invention, are presented. The logic makes assertions about the containment and contiguity of containers. Part of the logic is concerned with matching the syntactic structure of expressions in the calculus. The matching of the structure of formulas to the structure of processes is done in a flexible manner, up to a process equivalence, such that it is not entirely syntactical. A number of logical inference rules, including rules for propositional logic, rules for modal operators such as time, space and validity, and rules for locations and process composition is also derived.

Basic Ambient Calculus

The following table summarizes a basic ambient calculus upon which a modal logic according to an embodiment of the invention is based. There is no name restriction in the basic ambient calculus. The subsequent tables summarize the syntax of processes, the structural congruence relation between processes, and the reduction semantics.

                P,Q,R::=           processes
                0                  inactivity
                P.vertline.Q       composition
                !P                 replication
                M[P]               ambient
                M.P                capability action
                (n).P              input action
                <M>          async output action
                M::=               messages
                n                  name
                in M               can enter into M
                out M              can exit out of M
                open M             can open M
                .epsilon.          null
                M.M'               path

                     (1) fn(0) {character pullout} .phi.
                     (2) fn(P.vertline.Q) {character pullout} fn(P) .orgate.
     fn(Q)
                     (3) fn(!P)  {character pullout} fn(P)
                     (4) fn(M[P]) {character pullout} fn(M) .orgate. fn(P)
                     (5) fn(M.P) {character pullout} fn(M) .orgate. fn(P)
                     (6) fn((n).P) {character pullout} fn(P) - {n}
                     (7) fn(<M>) {character pullout} fn(M)
                     (8) fn(n) {character pullout} {n}
                     (9) fn(in M) {character pullout} fn(M)
                    (10) fn(out M) {character pullout} fn(M)
                    (11) fn(open M) {character pullout} fn(M)
                    (12) fn(.epsilon.) {character pullout} .phi.
                    (13) fn(M .M') {character pullout} fn(M) .orgate. fn(M')

           (1) P .ident. P               (Struct Refl)
           (2) P .ident. Q {character pullout} Q .ident. P (Struct Symm)
           (3) P .ident. Q, Q .ident. R {character pullout} P .ident. R (Struct
     Trans)
           (4) P .ident. Q {character pullout} P.vertline.R .ident.
     Q.vertline.R (Struct Par)
           (5) P .ident. Q {character pullout} !P .ident. !Q (Struct Repl)
           (6) P .ident. Q {character pullout} M[P] .ident. M[Q] (Struct Amb)
           (7) P .ident. Q {character pullout} M.P .ident. M.Q (Struct Action)
           (8) P .ident. Q {character pullout} (x).P .ident. (x).Q (Struct
     Input)
           (9) .epsilon..P .ident. P     (Struct .epsilon.)
          (10) (M.M').P .ident. M.M'.P   (Struct .)
          (11) P.vertline.Q .ident. Q.vertline.P (Struct Par Comm)
          (12) (P.vertline.Q).vertline.R .ident. P.vertline.(Q.vertline.R)
     (Struct Par Assoc)
          (13) !P .ident. P.vertline.!P  (Struct Repl Par)
          (14) P.vertline.0 .ident. P    (Struct Zero Par)
          (15) !0 .ident. 0              (Struct Zero Repl)

    (1) n[in m.P.vertline.Q].vertline.m[R] .fwdarw.
     m[n[P.vertline.Q].vertline.R] (Red In)
    (2) m[n[out m.P.vertline.Q].vertline.R] .fwdarw.
     n[P.vertline.Q].vertline.m[R] (Red Out)
    (3) open n.P.vertline.n[Q] .fwdarw. P.vertline.Q (Red Open)
    (4) (n).P.vertline.(M) .fwdarw. P{n .rarw. M} (Red Comm)
    (5) P .fwdarw. Q {character pullout} n[P] .fwdarw. n[Q] (Red Amb)
    (6) P .fwdarw. Q {character pullout} P.vertline.R .fwdarw. Q.vertline.R
     (Red Par)
    (7) P' .ident. P,P .fwdarw. Q,Q .ident. Q' {character pullout} P' .fwdarw.
     Q' (Red .ident.)
    (8) .fwdarw.*                    reflexive and transitive closure
                                     of .fwdarw.

                !P.vertline.Q is read            (!P).vertline.Q
                M.P.vertline.Q is read            (M.P).vertline.Q
                (n).P.vertline.Q is read            ((n).P).vertline.Q

              n[ ]  {character pullout} n[0]
              M     {character pullout} M.0 (where appropriate)

          A,B,C::=
           1 T              true
           2 {character pullout}A negation
           3 A{character pullout}B disjunction
           4 n[A]           location
           5 A'.vertline.A" composition
           6 .E-backward.n.A existential quantification over names
           7 {character pullout}A somewhere modality (spatial)
           8 .diamond.A     sometime modality (temporal)
           9 A@n            location adjunct
          10 A{character pullout}B composition adjunct

     1 F      {character pullout} {character pullout}T false
     2 A {character pullout} B {character pullout} {character
     pullout}({character pullout}A {character pullout} {character pullout}B)
     conjunction
     3 A {character pullout} B {character pullout} {character pullout}A
     {character pullout} B implication
     4 A {character pullout} B {character pullout} (A {character pullout} B)
     {character pullout} (B {character pullout} A) logical equivalence
     5 A {character pullout} B {character pullout} {character
     pullout}({character pullout}A.vertline.{character pullout}B) decomposition
     6 !A     {character pullout} A {character pullout} F every component
     satisfies A
     7 ?A     {character pullout} A.vertline.T ({character pullout} {character
     pullout}!{character pullout}A) some component satisfies A
     8 .A-inverted.n.A {character pullout} {character
     pullout}.E-backward.n.{character pullout}A universal quantification over
     names
     9 {character pullout}A {character pullout} {character pullout}{character
     pullout}{character pullout}A everywhere modality (spatial)
    10 .quadrature.A {character pullout} {character pullout}.diamond.{character
     pullout}A everytime modality (temporal)
    11 A@     {character pullout} .A-inverted.n.A@n in every location context
    12 {character pullout}A {character pullout} T{character pullout}A in every
     composition context

    .A-inverted.P:.PI.. P {character pullout} T {character pullout}
    .A-inverted.P:.PI., A:.PHI. P {character pullout} {character pullout}A
     {character pullout} {character pullout}P {character pullout} A
    .A-inverted.P:.PI., A,B:.PHI.. P {character pullout} A{character pullout}B
     {character pullout} P {character pullout} A {character pullout} P
     {character pullout} B
    .A-inverted.P:.PI., n:.LAMBDA., A:.PHI.. P {character pullout} n[A]
     {character pullout} .E-backward.P':.PI..P .ident. n[P'] {character
     pullout} P' {character pullout} A
    .A-inverted.P:.PI., A,B:.PHI.. P {character pullout} A.vertline.B
     {character pullout} .E-backward.P',P":.PI..P .ident. P'.vertline.P"
     {character pullout} P' {character pullout} A {character pullout} P"
     {character pullout} B
    .A-inverted.P:.PI., n:.LAMBDA., A:.PHI.. P {character pullout}
     .E-backward.n.A {character pullout} .E-backward.m:.LAMBDA..P {character
     pullout} A{n.rarw.m}
    .A-inverted.P:.PI., A:.PHI. P {character pullout} {character pullout}A
     {character pullout} .E-backward.P':.PI..P.dwnarw.*P' {character pullout}
     P' {character pullout} A
    .A-inverted.P:.PI., A:.PHI. P {character pullout} .diamond.A {character
     pullout} .E-backward.P':.PI..P.fwdarw.*P' {character pullout} P'
     {character pullout} A
    .A-inverted.P:.PI., A:.PHI. P {character pullout} A@n {character pullout}
     n[P] {character pullout} A
    .A-inverted.P:.PI., A,B:.PHI.. P {character pullout} A{character pullout}B
     {character pullout} .A-inverted.P':.PI..P' {character pullout} A
     {character pullout} P.vertline.P' {character pullout} B

    .A-inverted.P:.PI.. {character pullout} P {character pullout} F
    .A-inverted.P:.PI.,A,B: .PHI.. P {character pullout} A{character pullout}B
     iff P {character pullout} A {character pullout} P {character pullout} B
    .A-inverted.P:.PI.,A,B: .PHI.. P {character pullout} A{character pullout}B
     iff P {character pullout} A {character pullout} P {character pullout} B
    .A-inverted.P:.PI.,A,B: .PHI.. P {character pullout} A{character pullout}B
     iff P {character pullout} A {character pullout} P {character pullout} B
    .A-inverted.P:.PI.,A,B: .PHI.. P {character pullout} A{character pullout}B
     iff .A-inverted.P',P":.PI.. P .ident. P'.vertline.P" {character pullout}
     P' {character pullout} A {character pullout} P"{character pullout} B
    .A-inverted.P:.PI.,A: .PHI.. P {character pullout} !A iff
     .A-inverted.P',P":.PI.. P .ident. P'.vertline.P" {character pullout} P'
     {character pullout} A
    .A-inverted.P:.PI.,A: .PHI.. P {character pullout} ?A iff
     .E-backward.P',P":.PI.. P .ident. P'.vertline.P" {character pullout} P'
     {character pullout} A
    .A-inverted.P:.PI., P {character pullout} .A-inverted.n.A iff
     .A-inverted.m: .LAMBDA.. P {character pullout} A{n.rarw.m}
    n: .LAMBDA.,A: .PHI..
    .A-inverted.P:.PI.,A: .PHI.. P {character pullout} {character pullout}A iff
     .A-inverted.P':.PI.. P.dwnarw.*P' {character pullout} P' {character
     pullout} A
    .A-inverted.P:.PI.,A: .PHI.. P {character pullout} .quadrature.A iff
     .A-inverted.P':.PI.. P.fwdarw.*P' {character pullout} P' {character
     pullout} A
    .A-inverted.P:.PI.,A: .PHI.. P {character pullout} A@ iff .A-inverted.n:
     .LAMBDA.. P {character pullout} A@n
    .A-inverted.P:.PI.,A: .PHI.. P {character pullout} {character pullout}A iff
     .A-inverted.P':.PI.. P.vertline.P' {character pullout} A
    .A-inverted.P:.PI.,A,B: .PHI.. P {character pullout} {character
     pullout}(A{character pullout}B) iff .A-inverted.P':.PI.. P'.vertline.P
     {character pullout} A {character pullout} P'.vertline.P {character
     pullout} B (cf. P A{character pullout}B)

    an n {character pullout} n[T].vertline. T (there is now an n here)
    no n {character pullout} {character pullout}an n (there is now no n here)
    one n {character pullout} n[T] .vertline. no n (there is now exactly one n
     here)
    unique n {character pullout} n[{character pullout}no n] .vertline.
     {character pullout}no n (there is now exactly one n, and it is here)
    !(n[T] {character pullout} n[A]) (every n here satisfies A)

            vld A {character pullout} .A-inverted.P:.PI.. P {character pullout}
     A A is valid
            sat A {character pullout} .E-backward.P:.PI.. P {character pullout}
     A A is satisfiable

          (A-L)         A{character pullout}(C{character pullout}D)
     .perp-right. B // (A{character pullout}C) {character pullout}D
     .perp-right. B
          (A-R)         A .perp-right. (C{character pullout}D) {character
     pullout}B // A .perp-right. C{character pullout}(D{character pullout}B)
          (X-L)         A{character pullout}C .perp-right. B / C{character
     pullout}A .perp-right. B
          (X-R)         A .perp-right. C{character pullout}B / A .perp-right.
     B{character pullout}C
          (C-L)         A{character pullout}A .perp-right. B / A .perp-right. B
          (C-R)         A .perp-right. B{character pullout}B / A .perp-right. B
          (W-L)         A .perp-right. B / A{character pullout}C .perp-right. B
          (W-R)         A .perp-right. B / A .perp-right. C{character pullout}B
          (Id)          / A .perp-right. A
          (Cut)         A .perp-right. C{character pullout}B; A'{character
     pullout}C .perp-right. B' / A{character pullout}A' .perp-right. B
     {character pullout} B'
          (T)           A{character pullout}T .perp-right. B / A .perp-right. B
          (F)           A .perp-right. F{character pullout}B / A .perp-right. B
          ({character pullout}-L) A .perp-right. C{character pullout}B /
     A{character pullout}{character pullout}C .perp-right. B
          ({character pullout}-R) A{character pullout}C .perp-right. B /
     A.perp-right.{character pullout}C{character pullout}B
          ({character pullout}) A .perp-right. B; A' .perp-right. B' /
     A{character pullout}A' .perp-right. B{character pullout}B'
          ({character pullout}) A .perp-right. B; A' .perp-right. B' /
     A{character pullout}A' .perp-right. B{character pullout}B'

        (.A-inverted.-L) A {x.rarw.m} .perp-right. B / .A-inverted.x.A
     .perp-right. B
        (.A-inverted.-R) A .perp-right. B / A .perp-right. .A-inverted.x.B
     Where x .epsilon slash. fv(A)
        (.E-backward.-L) A .perp-right. B / .E-backward.x.A .perp-right. B
     Where x .epsilon slash. fv(B)
        (.E-backward.-R) A .perp-right. B {x.rarw.m} / A .perp-right.
     .E-backward.x.B

    (.diamond.) / T .perp-right. .diamond.A {character pullout} {character
     pullout}.quadrature.{character pullout}A ({character pullout}) / T
     .perp-right. {character pullout}A {character pullout} {character
     pullout}{character pullout}{character pullout}A
    (.quadrature.K) / T .perp-right. .quadrature.(A {character pullout} B)
     {character pullout} (.quadrature.A .quadrature.B) ({character pullout}K) /
     T .perp-right. {character pullout}(A {character pullout} B) {character
     pullout} ({character pullout}A {character pullout} {character pullout}B)
    (.quadrature.T) / T .perp-right. .quadrature.A {character pullout} A
     ({character pullout}T) / T .perp-right. {character pullout}A {character
     pullout} A
    (.quadrature.4) / T .perp-right. .quadrature.A {character pullout}
     .quadrature..quadrature.A ({character pullout}4) / T .perp-right.
     {character pullout}A {character pullout} {character pullout}{character
     pullout}A
    (.quadrature.M) A .perp-right. B / .quadrature.A .perp-right. .quadrature.B
     ({character pullout}M) A .perp-right. B / {character pullout}A
     .perp-right. {character pullout}B
    (.quadrature.{character pullout}) .quadrature.(A{character pullout}C)
     .perp-right. B // .quadrature.A{character pullout}.quadrature.C
     .perp-right. B ({character pullout}{character pullout}) {character
     pullout}(A{character pullout}C) .perp-right. B // {character
     pullout}A{character pullout}{character pullout}C .perp-right. B
    (.quadrature.{character pullout}) A .perp-right. .quadrature.(C{character
     pullout}B) // A .perp-right. .quadrature.C{character pullout}.quadrature.B
     ({character pullout}{character pullout}) A .perp-right. {character
     pullout}(C{character pullout}B) // A .perp-right. {character
     pullout}C{character pullout}{character pullout}B

            (n[ ])            A .perp-right. B // n[A] .perp-right. n[B]
            (n[ ]{character pullout}) n[A{character pullout}C] .perp-right. B
     // n[A]{character pullout}n[C] .perp-right. B
            (n[ ]{character pullout}) A .perp-right. n[C{character pullout}B]
     // A .perp-right. n[C]{character pullout}n[B]

    (.vertline.) A' .perp-right. B'; A" .perp-right. B" / A' .vertline. A"
     .perp-right. B' .vertline. B"
    (.vertline.{character pullout}) (A{character pullout}B) .vertline. C
     .perp-right. D / A .vertline. C {character pullout} B .vertline. C
     .perp-right. D
    (.vertline.{character pullout}) A .perp-right. (B{character pullout}C)
     .vertline. D / A .perp-right. B .vertline. D {character pullout} C
     .vertline. D
    (.vertline.[?]{character pullout}) / A' .vertline. A" {character pullout}
     B' .parallel. B" .perp-right. A' .vertline. B" {character pullout} B'
     .vertline. A"
    (.vertline.{character pullout}) / {character pullout}(A' .vertline. A")
     {character pullout} {character pullout}(B' .vertline. B")  .perp-right.
     {character pullout}(B' .vertline. A") {character pullout} ({character
     pullout}A' .vertline. {character pullout}B")
    (.vertline.-E) A .perp-right. B' .vertline. B"; A'{character pullout}(B'
     .vertline. C") .perp-right. D; A"{character pullout}(C' .vertline. B")
     .perp-right. D
              / (A{character pullout}(A'{character pullout}A")){character
     pullout}(C' .parallel. C") .perp-right. D

        (.vertline.) A' B'; A" B"/A'.vertline.A" B'.vertline.B"
        (.vertline.{character pullout}) (A{character pullout}B).vertline.C
     D/A.vertline.C{character pullout}B.vertline.C D
        (.vertline.{character pullout}) A (B{character pullout}C).vertline.D/A
     B.vertline.D {character pullout} C.vertline.D
        (.vertline..PI.) /A'.vertline.A" {character pullout} B'.PI.B"
     A'.vertline.B" {character pullout} B'.vertline.A"
        (.vertline.{character pullout}) /{character pullout}(A'.vertline.A")
     {character pullout} {character pullout}(B'.vertline.B") {character
     pullout}(B'.vertline.A") {character pullout} ({character
     pullout}A'.vertline.{character pullout}B")
        (.vertline.-E) A B'.vertline.B"; A'{character pullout}(B'.vertline.C")
     D; A"{character pullout}(C'.vertline.B") D
                    /(A{character pullout}(A'{character pullout}A")){character
     pullout}(C' .PI. C") D

                       Vld A   {character pullout} ({character pullout}A)
     {character pullout} F
                       Sat A   {character pullout} {character pullout}(A
     {character pullout} F)

          (Sat)         / T .perp-right. SatA {character pullout} {character
     pullout}Vld{character pullout}A
          (Vld K)       / T .perp-right. Vld(A {character pullout} B)
     {character pullout} ((VldA) {character pullout} (VldB))
          (Vld T)       / T .perp-right. (VldA) {character pullout} A
          (Vld 5)       / T .perp-right. (SatA) {character pullout} (Vld Sat A)
          (Vld M)       A .perp-right. B / VldA .perp-right. VldB
          (Vld {character pullout}) Vld(A{character pullout}C) .perp-right. B
     // VldA {character pullout} VldC .perp-right. B
          (Vld {character pullout}) A .perp-right. Vld(C{character pullout}B)
     // A .perp-right. VldC {character pullout} VldB

• Inventors
  Cardelli, Luca; Gordon, Andrew; Ghelli, Giorgio;
• Assignee
  Microsoft Corporation (Redmond, WA)
• Published
  Nov-30-2004
• Current US Classes:
  703/2
  713/200
  718/100
  718/104
• Application #
  430769
• International Classes
  G06F 009/46; G06F 017/10; H04L 009/00
• Field of Search
  709/100 709/102 709/101 709/104 709/200 709/217-219 713/200 703/2
• Examiner
  An; Meng-Al T.
• Agent
  Amin & Turocy, LLP
• US Patent References:
  5754782
  5781732
  6421667