Skip to content

Temporal Logic

Temporal properties using Linear Temporal Logic (LTL).

Overview

UPIR uses Linear Temporal Logic to express properties that must hold over time:

  • TemporalOperator: Enum of LTL operators
  • TemporalProperty: Property with operator and predicate

TemporalOperator

upir.core.temporal.TemporalOperator

Bases: Enum

Linear Temporal Logic (LTL) operators for expressing temporal properties.

Based on Pnueli's temporal logic formalism, these operators allow expressing properties about all time points (ALWAYS), some future time point (EVENTUALLY), bounded time constraints (WITHIN), and sequential properties (UNTIL).

References: - Pnueli (1977): Standard LTL operators - TD Commons disclosure: UPIR temporal property specification

Source code in upir/core/temporal.py 
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
class TemporalOperator(Enum):
    """
    Linear Temporal Logic (LTL) operators for expressing temporal properties.

    Based on Pnueli's temporal logic formalism, these operators allow
    expressing properties about all time points (ALWAYS), some future time
    point (EVENTUALLY), bounded time constraints (WITHIN), and sequential
    properties (UNTIL).

    References:
    - Pnueli (1977): Standard LTL operators
    - TD Commons disclosure: UPIR temporal property specification
    """
    ALWAYS = "ALWAYS"  # ◻P or G(P) - Property holds at all time points
    EVENTUALLY = "EVENTUALLY"  # ◇P or F(P) - Property holds at some future point
    WITHIN = "WITHIN"  # Bounded eventually - Property holds within time bound
    UNTIL = "UNTIL"  # P U Q - P holds until Q becomes true

TemporalProperty

upir.core.temporal.TemporalProperty dataclass

A temporal property with formal semantics for distributed system verification.

Temporal properties express constraints that must hold over time, such as "the system ALWAYS responds to requests" or "backups complete WITHIN 1 hour".

Based on Linear Temporal Logic (LTL) as defined in Pnueli (1977), extended with bounded operators for practical system verification per TD Commons.

Attributes:

Name Type Description
operator TemporalOperator

The temporal operator (ALWAYS, EVENTUALLY, WITHIN, UNTIL)
predicate str

String description of the property being asserted (e.g., "data_consistent", "request_processed")
time_bound Optional[float]

Optional time bound in seconds for bounded operators (WITHIN)
parameters Dict[str, Any]

Additional parameters for property evaluation (e.g., thresholds)
Example

System always responds within 100ms

prop = TemporalProperty( ... operator=TemporalOperator.WITHIN, ... predicate="response_received", ... time_bound=0.1, ... parameters={"max_latency_ms": 100} ... )

References: - TD Commons: Temporal property structure - Pnueli (1977): LTL semantics

Source code in upir/core/temporal.py 
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
@dataclass
class TemporalProperty:
    """
    A temporal property with formal semantics for distributed system verification.

    Temporal properties express constraints that must hold over time, such as
    "the system ALWAYS responds to requests" or "backups complete WITHIN 1 hour".

    Based on Linear Temporal Logic (LTL) as defined in Pnueli (1977), extended
    with bounded operators for practical system verification per TD Commons.

    Attributes:
        operator: The temporal operator (ALWAYS, EVENTUALLY, WITHIN, UNTIL)
        predicate: String description of the property being asserted
                  (e.g., "data_consistent", "request_processed")
        time_bound: Optional time bound in seconds for bounded operators (WITHIN)
        parameters: Additional parameters for property evaluation (e.g., thresholds)

    Example:
        >>> # System always responds within 100ms
        >>> prop = TemporalProperty(
        ...     operator=TemporalOperator.WITHIN,
        ...     predicate="response_received",
        ...     time_bound=0.1,
        ...     parameters={"max_latency_ms": 100}
        ... )

    References:
    - TD Commons: Temporal property structure
    - Pnueli (1977): LTL semantics
    """
    operator: TemporalOperator
    predicate: str
    time_bound: Optional[float] = None
    parameters: Dict[str, Any] = field(default_factory=dict)

    def __post_init__(self):
        """Validate temporal property constraints."""
        if self.operator == TemporalOperator.WITHIN and self.time_bound is None:
            raise ValueError("WITHIN operator requires a time_bound")

        if self.time_bound is not None and self.time_bound <= 0:
            raise ValueError("time_bound must be positive")

        if not self.predicate:
            raise ValueError("predicate cannot be empty")

    def to_smt(self) -> str:
        """
        Convert temporal property to SMT-LIB format for Z3 solver.

        Encoding follows standard temporal logic to first-order logic translation:
        - ALWAYS P: ∀t. P(t) - Universal quantification over time
        - EVENTUALLY P: ∃t. P(t) - Existential quantification over time
        - WITHIN P (bound b): ∃t. (t ≤ b) ∧ P(t) - Bounded existential
        - P UNTIL Q: ∃t. Q(t) ∧ ∀s. (s < t) → P(s) - Q eventually holds, P until then

        Returns:
            SMT-LIB formatted string suitable for Z3

        References:
        - Z3 tutorial: https://microsoft.github.io/z3guide/
        - Temporal logic encoding: Standard translation to FOL

        Example:
            >>> prop = TemporalProperty(
            ...     operator=TemporalOperator.ALWAYS,
            ...     predicate="data_consistent"
            ... )
            >>> smt = prop.to_smt()
            >>> "forall" in smt
            True
        """
        pred_name = self.predicate

        if self.operator == TemporalOperator.ALWAYS:
            # ∀t. P(t) - Property holds at all time points
            return f"(forall ((t Real)) ({pred_name} t))"

        elif self.operator == TemporalOperator.EVENTUALLY:
            # ∃t. P(t) - Property holds at some future time point
            return f"(exists ((t Real)) ({pred_name} t))"

        elif self.operator == TemporalOperator.WITHIN:
            # ∃t. (t ≤ bound) ∧ P(t) - Property holds within time bound
            bound = self.time_bound
            return f"(exists ((t Real)) (and (<= t {bound}) ({pred_name} t)))"

        elif self.operator == TemporalOperator.UNTIL:
            # P UNTIL Q encoding: ∃t. Q(t) ∧ ∀s. (s < t) → P(s)
            # Note: For UNTIL, predicate should contain both P and Q predicates
            # This is a simplified encoding; full UNTIL may need parameters
            return (
                f"(exists ((t Real)) "
                f"(and ({pred_name}_q t) "
                f"(forall ((s Real)) (=> (< s t) ({pred_name}_p s)))))"
            )

        else:
            raise ValueError(f"Unknown temporal operator: {self.operator}")

    def to_dict(self) -> Dict[str, Any]:
        """
        Serialize temporal property to JSON-compatible dictionary.

        Returns:
            Dictionary with all property fields in serializable format

        Example:
            >>> prop = TemporalProperty(
            ...     operator=TemporalOperator.WITHIN,
            ...     predicate="backup_complete",
            ...     time_bound=3600.0,
            ...     parameters={"backup_type": "full"}
            ... )
            >>> d = prop.to_dict()
            >>> d["operator"]
            'WITHIN'
        """
        return {
            "operator": self.operator.value,
            "predicate": self.predicate,
            "time_bound": self.time_bound,
            "parameters": self.parameters.copy()
        }

    def hash(self) -> str:
        """
        Generate SHA-256 hash of this temporal property.

        Uses deterministic JSON serialization to ensure same property
        always produces the same hash, enabling caching and integrity checks.

        Returns:
            Hexadecimal SHA-256 hash string

        Example:
            >>> prop = TemporalProperty(
            ...     operator=TemporalOperator.ALWAYS,
            ...     predicate="test"
            ... )
            >>> hash1 = prop.hash()
            >>> hash2 = prop.hash()
            >>> hash1 == hash2  # Deterministic
            True

        References:
        - SHA-256: Industry standard cryptographic hash
        - Python hashlib: https://docs.python.org/3/library/hashlib.html
        """
        prop_dict = self.to_dict()
        json_str = json.dumps(prop_dict, sort_keys=True)
        hash_obj = hashlib.sha256(json_str.encode('utf-8'))
        return hash_obj.hexdigest()

    @classmethod
    def from_dict(cls, data: Dict[str, Any]) -> "TemporalProperty":
        """
        Deserialize temporal property from dictionary.

        Args:
            data: Dictionary containing property fields

        Returns:
            TemporalProperty instance

        Raises:
            ValueError: If operator is invalid or required fields missing

        Example:
            >>> data = {
            ...     "operator": "ALWAYS",
            ...     "predicate": "data_consistent",
            ...     "time_bound": None,
            ...     "parameters": {}
            ... }
            >>> prop = TemporalProperty.from_dict(data)
            >>> prop.operator == TemporalOperator.ALWAYS
            True
        """
        return cls(
            operator=TemporalOperator(data["operator"]),
            predicate=data["predicate"],
            time_bound=data.get("time_bound"),
            parameters=data.get("parameters", {})
        )

    def __str__(self) -> str:
        """Human-readable string representation."""
        if self.time_bound is not None:
            return f"{self.operator.value}[{self.time_bound}s]({self.predicate})"
        return f"{self.operator.value}({self.predicate})"

    def __repr__(self) -> str:
        """Developer-friendly representation."""
        return (
            f"TemporalProperty(operator={self.operator}, "
            f"predicate='{self.predicate}', "
            f"time_bound={self.time_bound}, "
            f"parameters={self.parameters})"
        )

Functions

__post_init__()

Validate temporal property constraints.

Source code in upir/core/temporal.py 
80
81
82
83
84
85
86
87
88
89
def __post_init__(self):
    """Validate temporal property constraints."""
    if self.operator == TemporalOperator.WITHIN and self.time_bound is None:
        raise ValueError("WITHIN operator requires a time_bound")

    if self.time_bound is not None and self.time_bound <= 0:
        raise ValueError("time_bound must be positive")

    if not self.predicate:
        raise ValueError("predicate cannot be empty")

to_smt()

Convert temporal property to SMT-LIB format for Z3 solver.

Encoding follows standard temporal logic to first-order logic translation: - ALWAYS P: ∀t. P(t) - Universal quantification over time - EVENTUALLY P: ∃t. P(t) - Existential quantification over time - WITHIN P (bound b): ∃t. (t ≤ b) ∧ P(t) - Bounded existential - P UNTIL Q: ∃t. Q(t) ∧ ∀s. (s < t) → P(s) - Q eventually holds, P until then

Returns:

Type Description
str

SMT-LIB formatted string suitable for Z3

References: - Z3 tutorial: https://microsoft.github.io/z3guide/ - Temporal logic encoding: Standard translation to FOL

Example

prop = TemporalProperty( ... operator=TemporalOperator.ALWAYS, ... predicate="data_consistent" ... ) smt = prop.to_smt() "forall" in smt True

Source code in upir/core/temporal.py 
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
def to_smt(self) -> str:
    """
    Convert temporal property to SMT-LIB format for Z3 solver.

    Encoding follows standard temporal logic to first-order logic translation:
    - ALWAYS P: ∀t. P(t) - Universal quantification over time
    - EVENTUALLY P: ∃t. P(t) - Existential quantification over time
    - WITHIN P (bound b): ∃t. (t ≤ b) ∧ P(t) - Bounded existential
    - P UNTIL Q: ∃t. Q(t) ∧ ∀s. (s < t) → P(s) - Q eventually holds, P until then

    Returns:
        SMT-LIB formatted string suitable for Z3

    References:
    - Z3 tutorial: https://microsoft.github.io/z3guide/
    - Temporal logic encoding: Standard translation to FOL

    Example:
        >>> prop = TemporalProperty(
        ...     operator=TemporalOperator.ALWAYS,
        ...     predicate="data_consistent"
        ... )
        >>> smt = prop.to_smt()
        >>> "forall" in smt
        True
    """
    pred_name = self.predicate

    if self.operator == TemporalOperator.ALWAYS:
        # ∀t. P(t) - Property holds at all time points
        return f"(forall ((t Real)) ({pred_name} t))"

    elif self.operator == TemporalOperator.EVENTUALLY:
        # ∃t. P(t) - Property holds at some future time point
        return f"(exists ((t Real)) ({pred_name} t))"

    elif self.operator == TemporalOperator.WITHIN:
        # ∃t. (t ≤ bound) ∧ P(t) - Property holds within time bound
        bound = self.time_bound
        return f"(exists ((t Real)) (and (<= t {bound}) ({pred_name} t)))"

    elif self.operator == TemporalOperator.UNTIL:
        # P UNTIL Q encoding: ∃t. Q(t) ∧ ∀s. (s < t) → P(s)
        # Note: For UNTIL, predicate should contain both P and Q predicates
        # This is a simplified encoding; full UNTIL may need parameters
        return (
            f"(exists ((t Real)) "
            f"(and ({pred_name}_q t) "
            f"(forall ((s Real)) (=> (< s t) ({pred_name}_p s)))))"
        )

    else:
        raise ValueError(f"Unknown temporal operator: {self.operator}")

to_dict()

Serialize temporal property to JSON-compatible dictionary.

Returns:

Type Description
Dict[str, Any]

Dictionary with all property fields in serializable format
Example

prop = TemporalProperty( ... operator=TemporalOperator.WITHIN, ... predicate="backup_complete", ... time_bound=3600.0, ... parameters={"backup_type": "full"} ... ) d = prop.to_dict() d["operator"] 'WITHIN'

Source code in upir/core/temporal.py 
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
def to_dict(self) -> Dict[str, Any]:
    """
    Serialize temporal property to JSON-compatible dictionary.

    Returns:
        Dictionary with all property fields in serializable format

    Example:
        >>> prop = TemporalProperty(
        ...     operator=TemporalOperator.WITHIN,
        ...     predicate="backup_complete",
        ...     time_bound=3600.0,
        ...     parameters={"backup_type": "full"}
        ... )
        >>> d = prop.to_dict()
        >>> d["operator"]
        'WITHIN'
    """
    return {
        "operator": self.operator.value,
        "predicate": self.predicate,
        "time_bound": self.time_bound,
        "parameters": self.parameters.copy()
    }

hash()

Generate SHA-256 hash of this temporal property.

Uses deterministic JSON serialization to ensure same property always produces the same hash, enabling caching and integrity checks.

Returns:

Type Description
str

Hexadecimal SHA-256 hash string
Example

prop = TemporalProperty( ... operator=TemporalOperator.ALWAYS, ... predicate="test" ... ) hash1 = prop.hash() hash2 = prop.hash() hash1 == hash2 # Deterministic True

References: - SHA-256: Industry standard cryptographic hash - Python hashlib: https://docs.python.org/3/library/hashlib.html

Source code in upir/core/temporal.py 
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
def hash(self) -> str:
    """
    Generate SHA-256 hash of this temporal property.

    Uses deterministic JSON serialization to ensure same property
    always produces the same hash, enabling caching and integrity checks.

    Returns:
        Hexadecimal SHA-256 hash string

    Example:
        >>> prop = TemporalProperty(
        ...     operator=TemporalOperator.ALWAYS,
        ...     predicate="test"
        ... )
        >>> hash1 = prop.hash()
        >>> hash2 = prop.hash()
        >>> hash1 == hash2  # Deterministic
        True

    References:
    - SHA-256: Industry standard cryptographic hash
    - Python hashlib: https://docs.python.org/3/library/hashlib.html
    """
    prop_dict = self.to_dict()
    json_str = json.dumps(prop_dict, sort_keys=True)
    hash_obj = hashlib.sha256(json_str.encode('utf-8'))
    return hash_obj.hexdigest()

from_dict(data) classmethod

Deserialize temporal property from dictionary.

Parameters:

Name Type Description Default
data Dict[str, Any]

Dictionary containing property fields

 required

Returns:

Type Description
TemporalProperty

TemporalProperty instance

Raises:

Type Description
ValueError

If operator is invalid or required fields missing
Example

data = { ... "operator": "ALWAYS", ... "predicate": "data_consistent", ... "time_bound": None, ... "parameters": {} ... } prop = TemporalProperty.from_dict(data) prop.operator == TemporalOperator.ALWAYS True

Source code in upir/core/temporal.py 
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
@classmethod
def from_dict(cls, data: Dict[str, Any]) -> "TemporalProperty":
    """
    Deserialize temporal property from dictionary.

    Args:
        data: Dictionary containing property fields

    Returns:
        TemporalProperty instance

    Raises:
        ValueError: If operator is invalid or required fields missing

    Example:
        >>> data = {
        ...     "operator": "ALWAYS",
        ...     "predicate": "data_consistent",
        ...     "time_bound": None,
        ...     "parameters": {}
        ... }
        >>> prop = TemporalProperty.from_dict(data)
        >>> prop.operator == TemporalOperator.ALWAYS
        True
    """
    return cls(
        operator=TemporalOperator(data["operator"]),
        predicate=data["predicate"],
        time_bound=data.get("time_bound"),
        parameters=data.get("parameters", {})
    )

__str__()

Human-readable string representation.

Source code in upir/core/temporal.py 
231
232
233
234
235
def __str__(self) -> str:
    """Human-readable string representation."""
    if self.time_bound is not None:
        return f"{self.operator.value}[{self.time_bound}s]({self.predicate})"
    return f"{self.operator.value}({self.predicate})"

__repr__()

Developer-friendly representation.

Source code in upir/core/temporal.py 
237
238
239
240
241
242
243
244
def __repr__(self) -> str:
    """Developer-friendly representation."""
    return (
        f"TemporalProperty(operator={self.operator}, "
        f"predicate='{self.predicate}', "
        f"time_bound={self.time_bound}, "
        f"parameters={self.parameters})"
    )

Usage Examples

ALWAYS Operator

Property must hold at all times:

from upir.core.temporal import TemporalOperator, TemporalProperty

always_consistent = TemporalProperty(
    operator=TemporalOperator.ALWAYS,
    predicate="data_consistent"
)

# SMT encoding: ∀t. data_consistent(t)

EVENTUALLY Operator

Property must eventually hold:

eventually_complete = TemporalProperty(
    operator=TemporalOperator.EVENTUALLY,
    predicate="all_tasks_complete",
    time_bound=60000  # within 60 seconds
)

# SMT encoding: ∃t. (t ≤ 60000) ∧ all_tasks_complete(t)

WITHIN Operator

Property must occur within time bound:

within_100ms = TemporalProperty(
    operator=TemporalOperator.WITHIN,
    predicate="respond",
    time_bound=100
)

# SMT encoding: ∃t. (t ≤ 100) ∧ respond(t)

UNTIL Operator

Property P holds until Q becomes true:

until_complete = TemporalProperty(
    operator=TemporalOperator.UNTIL,
    predicate="processing",
    time_bound=30000  # max 30 seconds
)

# SMT encoding: ∃t. (t ≤ 30000) ∧ (∀s < t. processing(s)) ∧ complete(t)

SMT Encoding

Convert temporal properties to SMT formulas for verification:

property = TemporalProperty(
    operator=TemporalOperator.ALWAYS,
    predicate="data_consistent"
)

# Get SMT encoding
smt_formula = property.to_smt()
print(smt_formula)
# Output: "(forall ((t Int)) (>= t 0) (data_consistent t))"

See Also