PSL Ontology -- Current Theories and Extensions (version 2.8)

The axioms of PSL are organized into PSL-Core and a set of extensions. PSL-Core is the set of axioms written in CLIF (the Common Logic Interchange Format) and using only the nonlogical lexicon of PSL-Core. The extensions form a lattice of extensions to PSL-Core.

The purpose of PSL-Core is to axiomatise a set of intuitive semantic primitives that is adequate for describing the fundamental concepts of manufacturing processes. Consequently, this characterization of basic processes makes few assumptions about their nature beyond what is needed for describing those processes, and the Core is therefore rather weak in terms of logical expressiveness. In particular, PSL-Core is not strong enough to provide definitions of the many auxiliary notions that become necessary to describe all intuitions about manufacturing processes.

To supplement the concepts of PSL-Core, the ontology includes a set of extensions that introduce new terminology. An PSL extension provides the logical expressiveness to express information involving concepts that are not explicitly specified in PSL-Core. For each symbol in the nonlogical lexicon of an extension of PSL, there exist one or more axioms, written in CLIF, that constrain its interpretation. A distinction is drawn between definitional and nondefinitional extensions of PSL-Core. A definitional extension is an extension whose nonlogical lexicon can be completely defined in terms of PSL-Core. Definitional extensions add no new expressive power to PSL-Core. Nondefinitional extensions (also called core theories) are extensions of PSL-Core that involve at least one new primitive not contained in PSL-Core. All extensions within PSL must be consistent extensions of PSL-Core, and may be consistent extensions of other PSL extensions. However, not all extensions within PSL need be mutually consistent.

The organization of the extensions below reflects the Parts within standard ISO 18629. All files are updates to the standard, except for those marked by “x”, which are in progress. Other status indicators are: “c” (consistency proof completed) and “ca” (consistency verified by the automated theorem prover Vampire). The syntax of all files has been checked by automated theorem provers, see download page.

Core Theories

PSL-Core

• PSL-Core (c, ca)

Outer Core

• Subactivity Theory (c, ca)
• Theory of Occurrence Trees (c, ca)
• Theory of Discrete States (c, ca)
• Theory of Atomic Activities (c, ca)
• Theory of Complex Activities (c, ca)
• Activity Occurrence (c, ca)

Duration and Ordering Theories

• Duration Theory
• Subactivity Occurrence Ordering
• Iterated Activities (x)
• Occurrence Tree Automorphisms
• Envelopes and Umbrae

Resource Theories

• Resource Requirements Theory
• Resource Sets

Actor and Agent Theories

• Activity Performance (x)

Definitional Extensions of PSL

Activity Extensions

Branch Structure

• Deterministic Activities: Permuting Branch Structure
• Nondeterministic Activities: Folding Branch Structure
• Nondeterministic Activities: Branch Structure and Ordering
• Nondeterministic Activities: Repetitive Branch Structure

Spectrum

• Spectrum of Activities: Permuting Activity Trees
• Spectrum of Activities: Compacting Branch Structure
• Spectrum of Activities: Activity Trees and Reordering
• Spectrum and Subtree Containment

Embedded Activity Trees

• Embedding Constraints for Activities
• Skeletal Activity Trees

Atomic Activities

• Atomic Activities: Upwards Concurrency
• Atomic Activities: Downwards Concurrency
• Spectrum for Atomic Activities

Temporal and State Extensions

Preconditions

• Preconditions for Activities
• State-based Preconditions for Activities
• Time-based Preconditions for Activities
• Preconditions based on State and Time
• Occurrence-based Preconditions for Activities
• Preventable Preconditions for Activities
• Periodic Preconditions for Activities
• Historical Preconditions for Activities

Effects

• Effects of Activities
• State-based Effects of Activities
• Time-based Effects of Activities
• Occurrence-based Effects of Activities
• Effects of Activities: State and Occurrences
• Effects of Activities: Time and Occurrences
• Fluent Trees

Distribution

• Distribution of Complex Activities
• State-based Distribution of Complex Activities
• Time-based Distribution of Complex Activities
• Distribution based on State and Time

Variation

• Variation of Complex Activities
• State-based Variation of Complex Activities
• Time-based Variation of Complex Activities
• Variation based on State and Time

Embedded Activity Trees

• Embedded Activities: Plans
• Embedded Activities: Temporal Spread

Atomic Activities

• Variation of Atomic Activities: Upward Concurrency
• Variation of Atomic Activities: Downward Concurrency
• Interfering Preconditions
• Clobbering Effects
• Variation of Interfering Preconditions
• Variation of Clobbering Effects

Activity Ordering and Duration Extensions

Duration

• Duration Constraints for Activity Occurrences
• State-based Duration
• Time-based Duration
• Duration based on State and Time
• Duration-based Effects
• Effects of Activities based on Duration and State
• Ordering and Duration Constraints on Activity Occurrences
• Ordering and Duration Constraints on Embedded Activity Occurrences
• Spoilage Preconditions for Activities
• Scheduled Embedding Constraints

Subactivity Occurrence Orderings

• Strong Partially Ordered Activities
• Weak Partially Ordered Activities (x)
• Complex Activity Occurrence Orderings

Resource Roles

• Resource Roles
• Capacity-Based Concurrency
• Reasoning About Resource Divisibility

Resource Sets

• Resource Set-Based Activities
• Substitutable Resources
• Homogenous Resource Sets
• Inventory Resource Sets
• Resource Pools

Processor Activity Extensions

• Processor Activities
• Resource Paths