Does this computation satisfy LTL formulas?

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

The discussion centers on the satisfaction of two Linear Temporal Logic (LTL) formulas: (p U q) U r and p U (q U r). The computation {r}ᵂ satisfies both formulas, while {p}{q}{p}{q}{r}ᵂ satisfies only the first, and {p}{r}ᵂ satisfies only the second. The computation {p}{q}{r}ᵂ is debated, with the user asserting it satisfies only the first formula due to the failure of p to hold at all times before r. The community emphasizes the importance of adhering to forum rules against using AI tools for verification.

PREREQUISITES
  • Understanding of Linear Temporal Logic (LTL)
  • Familiarity with temporal operators such as "U" (until)
  • Knowledge of computation sequences and their interpretations
  • Basic principles of formal verification
NEXT STEPS
  • Study the semantics of LTL formulas in detail
  • Explore formal verification techniques for LTL
  • Learn about computation sequences and their satisfaction conditions
  • Investigate the differences between various LTL tools and their outputs
USEFUL FOR

This discussion is beneficial for students and professionals in formal methods, particularly those focusing on temporal logic, verification engineers, and anyone interested in understanding the nuances of LTL formula satisfaction.

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
Undergrad Ways to put n balls in m boxes such that exactly k boxes are empty?
  • · Replies 29 ·
Replies
29
Views
4K
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
MHB Please help with bool algebra and logic things
  • · Replies 2 ·
Replies
2
Views
2K
Computing conditional extinction probabilities for pollen cells
  • · Replies 1 ·
Replies
1
Views
1K