Does this computation satisfy LTL formulas?

  • Context: Graduate 
  • Thread starter Thread starter alma359
  • Start date Start date
Click For Summary

Discussion Overview

The discussion revolves around the satisfaction of two Linear Temporal Logic (LTL) formulas: (p U q) U r and p U (q U r). Participants explore various computations and their compliance with these formulas, focusing on the nuances of temporal logic and the implications of different sequences of truth values.

Discussion Character

  • Exploratory, Technical explanation, Debate/contested

Main Points Raised

  • One participant presents two LTL formulas and several computations, asserting that {r}ᵂ satisfies both formulas, while {p}{q}{p}{q}{r}ᵂ satisfies only the first, and {p}{r}ᵂ satisfies only the second.
  • The same participant claims that computations {p}ᵂ or ∅ᵂ do not satisfy either formula.
  • Another participant seeks clarification on the definition of LTL, suggesting it relates to Sentence Logic.
  • A third participant confirms that LTL stands for Linear Temporal Logic.
  • The original poster expresses confusion over AI tool results regarding the computation {p}{q}{r}ᵂ, stating that it satisfies both formulas according to the tools, but they believe it only satisfies the first formula due to the timing of p's satisfaction.
  • A later reply emphasizes that AI references are not permitted in the technical forums, aligning with the community's rules.

Areas of Agreement / Disagreement

Participants express differing views on the satisfaction of the computation {p}{q}{r}ᵂ with respect to the second formula, indicating a lack of consensus on this point.

Contextual Notes

The discussion highlights potential confusion regarding the interpretation of LTL formulas and the implications of different sequences of truth values, as well as the limitations of AI tools in providing accurate assessments in this context.

Who May Find This Useful

Individuals interested in Linear Temporal Logic, computational logic, or those learning about the nuances of temporal formulas may find this discussion relevant.

alma359
Messages
2
Reaction score
1
I have two LTL formulas.

The first one is (p U q) U r
The second one is p U (q U r)

I know the computation {r}ᵂ satisfies both formulas, computation {p}{q}{p}{q}{r}ᵂ satisfies only the first formula, computation {p}{r}ᵂ satisfies only the second one and computations {p}ᵂ or ∅ᵂ don't satisfy any of them.

Currently I'm learning LTL and I tried using AI tools to find more computations that satisfy the formulas, but I got confused because of mixed results. For example the computation {p}{q}{r}ᵂ. According to AI tools it satisfies both formulas but I believe it only satisfies the first formula, and does not satisfy the second formula, because p is not satisfied at all times before r (p is satisfied at t = 0 but not at t = 1).

If someone could confirm if I am right or wrong it would be very helpful.
 
Last edited:
Physics news on Phys.org
Welcome to PF!. What is LTL? This seems to deal with Sentence Logic.
 
Linear temporal logic
 
Reply
  • Like
Likes   Reactions: WWGD
alma359 said:
Currently I'm learning LTL and I tried using AI tools to find more computations that satisfy the formulas, but I got confused because of mixed results. For example the computation {p}{q}{r}ᵂ. According to AI tools it satisfies both formulas but I believe it only satisfies the first formula, and does not satisfy the second formula, because p is not satisfied at all times before r (p is satisfied at t = 0 but not at t = 1).
Please keep in mind that we do not allow AI as a reference in the technical forums here. That is expressly against the PF rules at this time.
 

Similar threads

Undergrad Understanding extinction probability in simple GWP
  • · Replies 1 ·
Replies
1
Views
2K
Undergrad An Elementary Observation Regarding Definability
  • · Replies 13 ·
Replies
13
Views
2K
Cubic equation solutions form
  • · Replies 2 ·
Replies
2
Views
2K
High School How does r∪(-p∩q∩-r) simplify to r∪(-p∩q) ?
  • · Replies 3 ·
Replies
3
Views
2K
Graduate Defining the membership relation in set theory?
  • · Replies 14 ·
Replies
14
Views
5K
Graduate Runners in a race, probability paradox
  • · Replies 3 ·
Replies
3
Views
2K
Undergrad Ways to put n balls in m boxes such that exactly k boxes are empty?
  • · Replies 29 ·
Replies
29
Views
5K
Graduate Quadrupole radiation formula for gravity
  • · Replies 3 ·
Replies
3
Views
1K
Undergrad Counterexample Required (Standard Notations)
  • · Replies 16 ·
Replies
16
Views
3K
Undergrad How Does Probability Affect the Total Number of Coupons a Customer Can Expect?
  • · Replies 2 ·
Replies
2
Views
2K