A Does this computation satisfy LTL formulas?

  • A
  • Thread starter Thread starter alma359
  • Start date Start date
AI Thread Summary
The discussion revolves around two LTL formulas: (p U q) U r and p U (q U r). It is established that the computation {r}ᵂ satisfies both formulas, while {p}{q}{p}{q}{r}ᵂ satisfies only the first, and {p}{r}ᵂ satisfies only the second. The user expresses confusion over AI tool results, particularly regarding the computation {p}{q}{r}ᵂ, which they believe only satisfies the first formula due to the timing of p's satisfaction. The forum emphasizes that AI references are not permitted in technical discussions.
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
 
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.
 

Thread 'Value of intuitionistic logic'

I'm taking a look at intuitionistic propositional logic (IPL). Basically it exclude Double Negation Elimination (DNE) from the set of axiom schemas replacing it with Ex falso quodlibet: ⊥ → p for any proposition p (including both atomic and composite propositions). In IPL, for instance, the Law of Excluded Middle (LEM) p ∨ ¬p is no longer a theorem. My question: aside from the logic formal perspective, is IPL supposed to model/address some specific "kind of world" ? Thanks.
View full post »

Thread 'Formal derivation of statement from Peano Arithmetic system'

I was reading a Bachelor thesis on Peano Arithmetic (PA). PA has the following axioms (not including the induction schema): $$\begin{align} & (A1) ~~~~ \forall x \neg (x + 1 = 0) \nonumber \\ & (A2) ~~~~ \forall xy (x + 1 =y + 1 \to x = y) \nonumber \\ & (A3) ~~~~ \forall x (x + 0 = x) \nonumber \\ & (A4) ~~~~ \forall xy (x + (y +1) = (x + y ) + 1) \nonumber \\ & (A5) ~~~~ \forall x (x \cdot 0 = 0) \nonumber \\ & (A6) ~~~~ \forall xy (x \cdot (y + 1) = (x \cdot y) + x) \nonumber...
View full post »

Similar threads

I Understanding extinction probability in simple GWP
Replies
1
Views
2K
I An Elementary Observation Regarding Definability
Replies
13
Views
2K
Cubic equation solutions form
Replies
2
Views
2K
B How does r∪(-p∩q∩-r) simplify to r∪(-p∩q) ?
Replies
3
Views
2K
I Ways to put n balls in m boxes such that exactly k boxes are empty?
Replies
29
Views
3K
A Quadrupole radiation formula for gravity
Replies
3
Views
1K
I Counterexample Required (Standard Notations)
Replies
16
Views
3K
I How Does Probability Affect the Total Number of Coupons a Customer Can Expect?
Replies
2
Views
2K
MHB Please help with bool algebra and logic things
Replies
2
Views
2K
Computing conditional extinction probabilities for pollen cells
Replies
1
Views
1K

Hot Threads

Recent Insights

Back
Top